Wondering what is the minimum syntax needed for everything?

[Gustavo Gonçalves]

(As I wrote this, I realized how long it took to get my point across, so I included a TL;DR at the end.)

Now that I have more time to get back into learning about Metamath and its principles, I saw that the whole theory of classes can be expressed using the wff and setvars we use. It's just much more efficient and easier to read/understand to create that abstraction.

I also took a peek into Whitehead and Russell's Principia Mathematica, and how everything within propositional logic could be defined in terms of the stroke (example: ¬P = (P|P) and P -> Q = (P|(Q|Q)), and so on)

So I started to wonder, how far can we go to reach the bare minimum of syntax needed.

In terms of propositional logic, I get it that all binary connectives can be written in terms of the stroke, so one. But I understand Metamath's approach to use two (negation and implication) since it's much easier to grasp.

We do need quantifiers for predicate logic, so we need to add "for all" into the syntax. Existence can be derived from it using negation, so that's all needed. And since classes can be algorithmically derived from those, is that all we need?

When it comes to atomic formulas, set theory only requires (x ∈ y). Equality, truth, sets, arithmetic and so on all can be derived from those.

I know we can get deeper phylosophically by asking "do we include setvars and wffs as syntax? or do we consider them some sort of metasyntax?" that I don't really plan to get into (unless it looks like it's needed).

TL;DR Informally speaking, is the only syntax we necessarily need (for any x,y variables and any φ,ψ wff) :

{ (φ | ψ), ∀x,  (x ∈ y) } ?

Cause if so, that's really beautiful! If not, I'd love to know what's missing! Thank you for reading.

[Jim Kingdon]

One (sort of nit picky) point: what you say below (which looks correct) is for set.mm

For iset.mm, there are four propositional logic primitives, both "for all" and "there exists" as primitives, and the same as set.mm for x ∈ y (the axioms of set theory are somewhat different, but "Equality, truth, sets, arithmetic and so on all can be derived from those" still holds).

As for what a minimal syntax for iset.mm would be, according to Alexander V. Kuznetsov (as cited at https://en.wikipedia.org/wiki/Intuitionistic_logic#Non-interdefinability_of_operators ) there is a single-operator analogue to the stroke (for propositional logic). I'm not aware of anything more minimal than what we have now for predicate logic or set theory.

--
You received this message because you are subscribed to the Google Groups "Metamath" group.
To unsubscribe from this group and stop receiving emails from it, send an email to metamath+u...@googlegroups.com.
To view this discussion on the web visit https://groups.google.com/d/msgid/metamath/e7a9d008-c63a-46dc-aa28-f6162ea1ab56n%40googlegroups.com.

[Mario Carneiro]

Yes, it suffices to have nand, forall and elementhood to get a complete set of term constructors for ZFC. However, you can ask the same question about the axiom systems and I think here the answer is less clear. For example, although the sheffer stroke is complete for propositional logic using a truth table semantics, that doesn't say anything about how many axioms are needed to axiomatize the behavior of the stroke and ensure that all classical theorems interpreting the stroke as nand are derivable. The ~meredith axiom shows that you can condense lucasiewicz's three axioms + MP into just one (+ MP), and IIRC Wolfram did a computer search (https://www.wolfram.com/language/12/algebraic-computation/the-shortest-possible-axiom-for-boolean-logic.html) to find the shortest axiom for the sheffer stroke (+ equational logic, which I think entails at least two extra axioms). Once you throw in predicate logic, you need quite a few more axioms, and to get ZFC I don't think there is a significantly shorter method than just writing the ZFC axioms.

In terms of metalogical entities, we need at least wffs (since nand, forall, elementhood are all wffs) and set variables (used in forall and elementhood). For predicate logic to work we also need some kind of not-free mechanism, and metamath has done some work on seeing how much you can eliminate this. Metamath itself shows that you can get by with "not present" Instead of "not free", although you need enough axioms to be able to prove the proper not-free notion when it holds. It is sort-of possible to eliminate "not present" as well, but the problem that arises is that you can no longer discharge dummy variables, so you end up accumulating undischargeable hypotheses that say essentially that at least n distinct variable names exist.

Mario

To view this discussion on the web visit https://groups.google.com/d/msgid/metamath/f763b31c-8d5c-3288-d226-d4aefab0a418%40panix.com.