This is not correct. The system called PA is a FOL axiomatization, not SOL. Second order PA is categorical (has at most one model, and exactly one if you think the natural numbers exist), while first order PA is not.
The fifth axiom of PA is not an axiom, it is an axiom scheme, an infinite family of axioms. Indeed, it is well known that PA is not finitely axiomatizable (with the important caveat "... in first order" there). FOL + PEANO is not impossible, it's a perfectly well defined and recursively axiomatizable theory. You can implement a computer program to check whether proofs in PA are valid, you just have a function that will recognize instances of the induction axiom rather than simply listing all valid axioms. Remember that FOL itself has schemes all over the place anyway. Rules like ph -> ps -> ph are axiom schemes. The only thing that makes the induction axiom special is that it is a "non-logical" axiom scheme. (In fact FOL axiom schemes are even more complex than this since they are not merely parametric over formulas, they also have side conditions on free variables and such.) Mario On Sat, Mar 14, 2020 at 7:19 AM 'fl' via Metamath <[email protected]> wrote: > (I'm throwing a new thread because this is different from Ken Kubota's > thoughts.) > > "Hence (1 > <https://plato.stanford.edu/entries/logic-higher-order/#mjx-eqn-ind>1) > [Induction axiom] cannot be expressed in first order logic. " (1) > > So there are 5 axioms in the axiomatic system of natural numbers. Four of > them can be expressed in FOL. > The fifth one [Induction axiom] can only be expressed in second-order > logic. I don't know if there is an official > acronym for second-order logic but let's call it SOL. And let's call PEANO > the system of 5 axioms designed by Peano > > (1) https://plato.stanford.edu/entries/logic-higher-order/ > > A Peano system is necessarily equal to SOL + PEANO. FOL + PEANO is > impossible. > > -- > FL > > -- > 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/68a5f815-8dbd-47d7-99fc-e9678388b33d%40googlegroups.com > <https://groups.google.com/d/msgid/metamath/68a5f815-8dbd-47d7-99fc-e9678388b33d%40googlegroups.com?utm_medium=email&utm_source=footer> > . > -- 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/CAFXXJSuAx%3DsS5jHn95m7fOora0ZPLohuazdzLoGHQoguT2yHcw%40mail.gmail.com.
