Second-order theory

[fl]

(I'm throwing a new thread because this is different from Ken Kubota's thoughts.)

"Hence (11) [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/

A Peano system is necessarily equal to SOL + PEANO. FOL + PEANO is impossible.

-- 

FL

[Ken Kubota]

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/

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

--
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 metamath+u...@googlegroups.com.
To view this discussion on the web visit https://groups.google.com/d/msgid/metamath/68a5f815-8dbd-47d7-99fc-e9678388b33d%40googlegroups.com.

[Mario Carneiro]

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

--

[Ken Kubota]

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

To view this discussion on the web visit https://groups.google.com/d/msgid/metamath/CAFXXJSuAx%3DsS5jHn95m7fOora0ZPLohuazdzLoGHQoguT2yHcw%40mail.gmail.com.

[Norman Megill]

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.

Norm

[Ken Kubota]

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

(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

Kind regards,

Ken Kubota

____________________________________________________

Ken Kubota

doi.org/10.4444/100

[Mario Carneiro]

On Mon, Mar 16, 2020 at 4:55 PM Ken Kubota <ma...@kenkubota.de> wrote:

Am 16.03.2020 um 23:42 schrieb Norman Megill <n...@alum.mit.edu>:

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

[Ken Kubota]

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.

____________________________________________________

Ken Kubota

doi.org/10.4444/100

[Mario Carneiro]

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