You can't really do raw first order logic in metamath, you would need an infinite number of axioms (even for things like propositional logic). Metamath needs to be able to use schemes to define axiom systems, and to write those schemes you need some concession to higher order variables, although you can limit their scope such that you get exactly the correct "first order image" out if no second order variables appear in the statement.
The use of class variables in peano.mm1, as in set.mm, is a convenience only. The real power is already encapsulated in the wff variables, which are schematic variables that do not appear in raw FOL. This is done for a variety of practical reasons, including the exponential speedup it brings relative to direct from axioms proofs, but it is this very speedup that indicates that a real strengthening of the system is at work (conservative though it is). A similar phenomenon happens in FOL vs SOL as traditionally studied. For example, ACA_0 is a conservative extension of PA, but there are O(n) proofs in ACA_0 whose shortest proof in PA has length O(2^^n) (that is, 2^....^2 n times), if I recall correctly. The peano.mm0 system lies somewhere in between these systems, because ACA_0 can have formulas containing any number of second order quantifiers, as long as they don't appear in instances of the induction axiom, while peano.mm0 can only do one level of second order universal quantification (i.e. Pi^1_n, one second order universal quantifier and any number of first order quantifier alternations), which is why it gets only an exponential speedup (or possibly double exponential, not sure) rather than an iterated exponential speedup. Again, set.mm is in the same position between ZFC and second order ZFC (also known as NBG). NBG is a conservative extension of ZFC with second order quantifiers, but not in the schemes (otherwise the proof system becomes stronger and you get MK set theory instead). All the same kinds of theorems from above still apply. ZFC (resp. PA) is not finitely axiomatizable, but proves all its finite fragments. NBG (resp. ACA_0) is finitely axiomatizable, and set.mm (resp. peano.mm0) is also finitely axiomatizable (axiomatized, even - they are clearly text files of finite length). The proofs of the finite fragments of ZFC (resp. PA) get longer and longer, irreducibly, because you necessarily have to bring in the power of the higher levels. The speedup comes from the fact that the higher order axiomatizations have compact ways of referring to these higher levels. (See Solovay's method of "shortening of cuts".) On Wed, Mar 11, 2020 at 12:43 PM 'fl' via Metamath < [email protected]> wrote: > Moreover, it is rather the class variables of the first-order logic than > the propositional > variables that are quantified by the additional quantifier in the > second-order logic. > To clarify: the reason why class variables and wff variables are equivalent in strength here is because of binding notations like "A." that can take a set variable and a wff variable and bind the set variable in the wff. This means that a wff variable can have some number of free variables that can later be bound, and so the denotation of a wff variable is really a relation on all its free variables, which is a proper class, a second order variable in SOL. If a wff was really just a truth value, then every wff would be equivalent to T. or F., but this implies that "A." is useless, since "A. x T." is equivalent to "T." and "A. x F." is equivalent to "F." - but this is clearly not the case, "A. x ph" is not equivalent to "ph" in general. A class variable is also a relation on its free variables, plus one designated extra variable that is baked into the class itself. That is, it's just an n+1-ary relation for some n. This is why you can easily go back and forth between class variables and wff variables using the syntax constructors "{ x | ph }" and "x e. A". Mario -- 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 [email protected]. To view this discussion on the web visit https://groups.google.com/d/msgid/metamath/CAFXXJStA4M92s%2BNNhAH8xm0uAowFG62H-qAymODhfqhebjGJ8A%40mail.gmail.com.
