On Mon, Mar 16, 2020 at 4:55 PM Ken Kubota <[email protected]> wrote:
> > Am 16.03.2020 um 23:42 schrieb Norman Megill <[email protected]>: > > On Monday, March 16, 2020 at 1:06:17 PM UTC-4, Ken Kubota wrote: >> >> 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). >> >> > Schemes are used in FOL to describe the axioms. They aren't the axioms > themselves. > > Propositional calculus also uses schemes to describe its axioms. Note > that the axioms themselves - an infinite number of them - are not schemes. > > If the use of schemes in the description of axioms automatically makes a > logic second order, then there can be no such thing as first-order logic > per your definition, since you can't even specify the underlying > propositional calculus without them. Your definition is not the one used > in the literature to define first-order logic. > > > Let me refine my argument by pointing out that the schematic variable > required for induction in PA in FOL ranges over _predicates_ (unlike the > schemes in propositional calculus or first-order logic), which renders the > formal system de facto second-order, since the schema could also be > replaced by quantification over a predicate variable. > The schematic variable for PA induction does *not* range over predicates, it ranges over formulas with one distinguished variable. That is in fact exactly what makes the difference between first order and second order formulations: in second order PA the induction axiom ranges over all predicates on the natural numbers using a second order quantifier. The reason second order PA is categorical is because when we interpret the second order quantification as a quantification over all subsets, the logic gains access to all uncountably many subsets of the natural numbers via this quantifier, while first order PA is stuck with talking about only the countably many predicates that can be described by a formula. 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/CAFXXJSuzmrkT-T34_hUDQ2hCrbKHR3zA_KOPmeT2wW0KNr-TZg%40mail.gmail.com.
