In terms of expressiveness, schemes are another way of expressing what usually requires a higher order. If you want to determine the order of a logic, it doesn't make sense to allow schemes. What can be expressed in first-order logic (FOL) with schemes requires at least second-order logic (without schemes). So it is adequate to state that PA requires second-order logic (i.e., first-order logic without extensions like schemes is not sufficient).
____________________________________________________ Ken Kubota doi.org/10.4444/100 <https://doi.org/10.4444/100> > Am 15.03.2020 um 01:54 schrieb Mario Carneiro <[email protected]>: > > 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] > <mailto:[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/ > <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] > <mailto:[email protected]>. > To view this discussion on the web visit > https://groups.google.com/d/msgid/metamath/CAFXXJSuAx%3DsS5jHn95m7fOora0ZPLohuazdzLoGHQoguT2yHcw%40mail.gmail.com > > <https://groups.google.com/d/msgid/metamath/CAFXXJSuAx%3DsS5jHn95m7fOora0ZPLohuazdzLoGHQoguT2yHcw%40mail.gmail.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/2C2DABA6-0CF3-4A60-BAF7-898B95EC1F98%40kenkubota.de.
