> 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. In the language of Q0, a variable – ranging over individuals (allowed in first-order logic) has type: i – ranging over predicates (allowed in second-order logic) has type: oi (other notation: i -> o) – ranging over predicates of predicates (allowed in third-order logic) has type: o(oi) (other notation: i -> o -> o) etc. For example, the type of the variable "p" ranging over predicates has type "ot" in the Principle of Mathematical Induction at https://www.owlofminerva.net/files/formulae.pdf#page=369 <https://www.owlofminerva.net/files/formulae.pdf#page=369> (In R0, I use the type variable "t" instead of the type of individuals "i".) For the Induction Theorem in Q0, see [Andrews 2002 (ISBN 1-4020-0763-9), p. 262 (Theorem 6102)]. I usually refrain from quoting non-scientific sources, but this formulation seems to be another way of putting it: "Schematic variables in first-order logic are usually trivially eliminable in second-order logic, because a schematic variable is often a placeholder for any property or relation over the individuals of the theory. This is the case with the schemata of Induction and Replacement mentioned above." – https://en.wikipedia.org/w/index.php?title=Axiom_schema&oldid=855367189#In_higher-order_logic <https://en.wikipedia.org/w/index.php?title=Axiom_schema&oldid=855367189#In_higher-order_logic> Kind regards, Ken Kubota ____________________________________________________ Ken Kubota doi.org/10.4444/100 <https://doi.org/10.4444/100> -- 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/A990156B-0D4A-444F-A05C-74AACAA1127D%40kenkubota.de.
