This is correct. The Induction Axiom (or Induction Theorem) quantifies about predicates, so at least second-order logic is required.
For a formalization of The Principle of Mathematical Induction, see: https://owlofminerva.net/kubota/r0-faq/ <https://owlofminerva.net/kubota/r0-faq/> There is no established acronym for second-order logic since the main formulations of higher-order logic (e.g., Church's type theory, Andrews' Q0, Gordon's HOL) are not limited to a certain order. A restriction to a certain order would be, from a language point of view, rather artificial. ____________________________________________________ Ken Kubota doi.org/10.4444/100 <https://doi.org/10.4444/100> > Am 14.03.2020 um 15:18 schrieb 'fl' via Metamath <[email protected]>: > > (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>) > [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/ > <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] > <mailto:[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/A90E49D1-4AC9-41F4-A55C-5F32CFD36521%40kenkubota.de.
