On Mon, Mar 16, 2020 at 6:07 PM Ken Kubota <[email protected]> wrote:
> > Am 17.03.2020 um 01:17 schrieb Mario Carneiro <[email protected]>: > > > > 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. > > > The formulation that the schematic variable ranges over "formulas with one > distinguished variable" is vague. > The point is that the type of this schematic variable is "oi" (i.e., a > predicate), and not, for example, "o" (proposition). (Clearly, the variable > P in the induction axiom denotes a predicate/property/set.) > Therefore PA cannot be expressed in first-order logic, hence it is at > least second-order. > > You seem to follow the semantic approach ("when we interpret"). > But from a purely syntactic point of view, the interpretation is not > relevant, but only the fact that all theorems of Peano arithmetic can be > obtained syntactically – given a formal language more expressive than > first-order logic. > First order PA, and second order PA, are both purely syntactic constructions. The difference between them is however tied up in the semantics, because it is the interpretation of the second order quantifier as a "full powerset" quantifier that gives it its categorical status. You can also choose to interpret the second order quantifier as the set of (first order) definable subsets of nat, but this will have visible effects from within the theory, because second order PA can define what a first order definable subset of nat is, and so the second order statement |- A. X E. n X = {i | nth-definable-subset(n, i)} is true in this model but not true in the full powerset model. There is nothing vague about "formulas with one distinguished variable". The variable can be fixed to something, like v_0, and FOL has a notion of what a formula is; schemes such as this abound in the definition of FOL itself. Formulas are built up from -> , -. , A. and variables, and for each formula you get a corresponding instance of the induction axiom scheme. You can say that this is a variable of type "oi", but I disagree. There is no type "oi" in peano arithmetic. If such a type existed (and had the obvious properties), then it would be able to prove the consistency of (first order) PA, and indeed second order PA proves the consistency of first order PA. HOL is stronger still, capable of proving the consistency of third order PA and so on. First order PA is not finitely axiomatizable, second order PA and HOL are. There are ways to go second order without increasing the consistency strength - the natural choice being ACA_0 - but this requires a syntactic restriction on the formulas going into the induction axiom that is not at all naturally expressible in HOL: the formula must not use any higher order quantifiers. In short: First order PA can be naturally embedded in second order PA, and HOL, but these theories are not the same as first order PA, they are stronger. 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/CAFXXJSsAbKQ2Csu6AOwrWwRgk_WvueiLDpgoE%3DwnwRYsR52A_w%40mail.gmail.com.
