Hilbert's omega rule, induction, omega-consistency

[nomadreid]

As I understand Hilbert's omega rule for a first-order proposition P over the natural numbers,
P(0) &P(1) &P(2) &... ⇒ ∀n∈ℕ P(n)
which seems to be the same as ω-consistency. Is there a difference?

Further, the axiom schema of induction has each axiom for a proposition P over the natural numbers,
[P(0) & ∀n∈ℕ (P(n)⇒P(n+1))]⇒∀n∈ℕ P(n)

I am not sure if the following argument is correct:

Induction is a weaker principle, because
(a) in order to convert to , you would need a rule of inference allowing you to apply Modus Ponens an infinite number of times.
(b) to convert to , you can take every pair {P(n),P(n+1)}, deduce for each one Q(n):≡ (P(n)⇒P(n+1)), and then apply for Q to get
∀n∈ℕ (P(n)⇒P(n+1)), etc.

 

[Erland]

I have not been able to find on the net exactly what the omega rule says, but I think it is the same as ω-completeness:

A formal theory T in the language of First Order Arithmetic is ω-complete if the following condition holds for each formula P(x) in T:

If the sentence P(n) is provable in T for each numeral n, then ∀xP(x) is provable in T.

Your formulation is some kind of infinite sentence within the theory, which doesn't really make sense. It is important to understand that it is about provability.

ω-consistency is a weaker condition: T (as above) is ω-consistent if the following condition holds for each formula P(x) in T:

If the sentence P(n) is provable in T for each numeral n, then not-∀xP(x) is not provable in T.

 

[nomadreid]

Thanks, Erland.

I have not been able to find on the net exactly what the omega rule says

For a secondary (or tertiary...) reference, download the pdf from
https://www.researchgate.net/publication/38383482_Hilbert%27s_Program_and_the_Omega-Rule
Or, if your German is OK, then the original is on this page:
https://gdz.sub.uni-goettingen.de/id/PPN235181684_0104?tify={%22pages%22:[495],%22panX%22:0.429,%22panY%22:0.797,%22view%22:%22info%22,%22zoom%22:0.346}
(alternatively, go to https://eudml.org/doc/159480
then downloading the full text, and then flipping to p. 491 )

Your formulation is some kind of infinite sentence within the theory, which doesn't really make sense.

You are completely correct here, and I should have been more careful. Even the way Hilbert formulated it, it was (as the secondary reference above states) an informal statement.

If the sentence P(n) is provable in T for each numeral n,

"for each numeral" has always seemed to me to be a bit awkward. I understand that the meaning is "if P(n) is in a form such that, treating n as an arbitrary variable, it can be derived from the axioms", but "for each numeral" sounds as if one is invoking an infinite number of cases, and then we are back to the original problem.

Thank you also for the correction on the distinction between ω-completeness and ω-consistency. So, given that, the rest of my question should be reformulated as to the difference between ω-completeness and induction. I would be grateful if you or another contributor could answer the point about comparing starred statements with the substitution that should now refer to a correct formulation of ω-consistency rather than my original flawed formulation.

 

[andrewkirk]

In a context like this, we need to be clear about what language the propositions we write are expressed in.

I'll call your one and two star expressions 1S and 2S for short.

1S cannot be an expression in the language in which P is written, call it L, because the theory of languages only allows for expressions of finite length, and the LHS is infinitely long.

So 1S must be an expression in some meta language, call it L2, that can talk about the language L.

In contrast, 2S is an expression in the original language L.

I believe that, expressed both as sentences in L2, 1S and 2S are equivalent. You are already confident that 1S entails 2S. What about the other direction. For it not to hold we would require there to be some L-formula P for which 2S is true but 1S is not. For 1S to be falsified requires its antecedent to be true and its consequent false.

But the consequent of 1S is the same as that of 2S so the consequent of 2S is false also. Since 2S is true that means its antecedent must be false. Hence either P(0) is false or there is some n such that ##P(n)\wedge\neg P(n+1)## - either way there must be some n for which P(n) is false. But that gives us a contradiction, because the antecedent of 1S is true (see above), which means that P(n) is true for every n.

So, subject to the possibility that I've messed up somewhere, I conclude that 1S and 2S are equivalent, as L2 sentences.

 

[nomadreid]

Thanks, andrewkirk. Your conclusion seems correct to me.

Erland pointed out in post #2 as well that 1S could not be in L (which I admitted in my post #3). His answer seems to imply that he sees ω-completeness (which my 1S was stating, not ω-consistency as I had first erroneously stated) as a finitary statement (which, I notice,
https://www.encyclopediaofmath.org/index.php/Omega-completeness
does not seem to agree with); and hence expressible in L. I am still dubious on this point.

 

[stevendaryl]

"for each numeral" has always seemed to me to be a bit awkward. I understand that the meaning is "if P(n) is in a form such that, treating n as an arbitrary variable, it can be derived from the axioms", but "for each numeral" sounds as if one is invoking an infinite number of cases, and then we are back to the original problem.

The omega rule is about numerals. It's not about treating ##n## as a variable that can stand for an arbitrary integer.

The problem---if you want to call it a problem---with first-order axioms for arithmetic is that they give sufficient conditions for something to be a natural number, but not necessary conditions. From the Peano axioms, you know that

##0##
##S(0)##
##S(S(0))##
##S(S(S(0)))##
etc

(where ##S(x)## means "the successor of ##x##" or ##x+1##)

are all natural numbers. But the axioms don't say that every natural number is equal to one of those. You can't really say that in first-order logic. The induction axiom is an attempt to capture that, but it doesn't, as nonstandard models show. The omega-rule is a stronger attempt to say: "And that's all the naturals there are".

 

[stevendaryl]

I believe that, expressed both as sentences in L2, 1S and 2S are equivalent. You are already confident that 1S entails 2S. What about the other direction. For it not to hold we would require there to be some L-formula P for which 2S is true but 1S is not. For 1S to be falsified requires its antecedent to be true and its consequent false.

But the consequent of 1S is the same as that of 2S so the consequent of 2S is false also. Since 2S is true that means its antecedent must be false. Hence either P(0) is false or there is some n such that ##P(n)\wedge\neg P(n+1)## - either way there must be some n for which P(n) is false. But that gives us a contradiction, because the antecedent of 1S is true (see above), which means that P(n) is true for every n.

So, subject to the possibility that I've messed up somewhere, I conclude that 1S and 2S are equivalent, as L2 sentences.

They may be semantically equivalent, but they are not logically equivalent. Start with the standard axioms of arithmetic (including the axiom schema of induction). Add a new constant symbol, ##c## and add the infinite collection of axioms:

##c \neq 0##
##c \neq S(0)##
##c \neq S(S(0))##
etc.

This theory is consistent. But if you add the omega rule, it becomes inconsistent. So the omega rule is not logically equivalent to the axiom schema of induction.

 

[stevendaryl]

They may be semantically equivalent, but they are not logically equivalent. Start with the standard axioms of arithmetic (including the axiom schema of induction). Add a new constant symbol, ##c## and add the infinite collection of axioms:

##c \neq 0##
##c \neg S(0)##
##c \neg S(S(0))##
etc.

This theory is consistent. But if you add the omega rule, it becomes inconsistent. So the omega rule is not logically equivalent to the axiom schema of induction.

Concretely, we have the predicate ##P(x) \equiv x \neq c##. That does not contradict the axiom schema of induction, because it's false that

##\forall n, P(n) \rightarrow P(n+1)##

In particular, it's false when ##n = c-1##.

On the other hand, it does contradict the omega-logic statement, since ##P(0) \wedge P(1) \wedge ...## is true, but ##\forall n, P(n)## is false.

 

[andrewkirk]

##c \neq 0##
##c \neg S(0)##
##c \neg S(S(0))##

I think perhaps the 2nd and 3rd cases were supposed to be \neq rather than \neg, ie

##c \neq S(0)##
##c \neq S(S(0))##

Concretely, we have the predicate ##P(x) \equiv x \neq c##. That does not contradict the axiom schema of induction, because it's false that

##\forall n, P(n) \rightarrow P(n+1)##

In particular, it's false when ##n = c-1##.

Is there such a thing as ##c-1## in this system? We only have the non-negative integers, and operations of addition and multiplication, so it is not clear to me that ##c-1## is capable of being interpreted as a valid symbol string.

This can be fixed by making the predicate ##P(x)\equiv x\neq S(c)##. Then we have ##P(c)## and ##\neg P(S(c))##, so that the antecedent of the induction rule is not obtained, so we cannot prove the consequent. Hence the axiom schema of induction does not introduce inconsistency.

I am not sure that the system becomes inconsistent if we adapt it to make the omega rule true. That depends on exactly what the omega rule is, and the above version, with its ellipses, is too unclear to make a determination. I suspect the LHS is intended to say something like P(n) is true whenever n is one of the natural numbers that we all know and love (leaving aside the fact that almost all natural numbers have never been written, spoken or thought of by anybody), and that set is distinguished from ##\mathbb N##, which is the set of objects we have defined with our Peano axioms or such-like, which may include weird things like ##c## and its descendants.

I wonder if there's a non-circular way to refer to 'the natural numbers we know and love'. I thought of something like 'numbers that can be expressed as a finite number of applications of the S function to 0'. But I wonder whether that use of 'finite' is smuggling in our folk notion of natural number, and thereby circular. But maybe if we use the definition of finite that is 'not infinite' where the property of a set being infinite is that there exists a bijection to a proper subset of itself.

I suspect there may be no non-circular way of defining the natural numbers we know and love because if there was, I imagine it would have been used in the Peano axioms. Further, if there were such a way, and we called the set ##\mathbb S## then we can fix the axiom schema of induction to do the same thing as what we want the omega rule to do by just replacing the ##\mathbb N## in the antecedent by ##\mathbb S##.

 

[nomadreid]

Excellent points, both stephendaryl and andrewkirk. This raises some more questions:

the natural numbers we know and love

I understand that you mean by this only the standard natural numbers, but not the non-standard natural numbers.If so, I gather from

But the axioms don't say that every natural number is equal to one of those. You can't really say that in first-order logic.

that, if you mean a first-order way, then it would seem reasonable that "no": your suggestion

But maybe if we use the definition of finite that is 'not infinite' where the property of a set being infinite is that there exists a bijection to a proper subset of itself.

sounds like it is sneaking in a higher-order sentence. But in any case, what is to stop a non-standard natural number from being finite?

So the omega rule is not logically equivalent to the axiom schema of induction.

Ah, good, that settles that.

A formal theory T in the language of First Order Arithmetic is ω-complete if the following condition holds for each formula P(x) in T:

If the sentence P(n) is provable in T for each numeral n, then ∀xP(x) is provable in T.

So, can I say that the omega rule is equivalent to ω-completeness?

ω-consistency is a weaker condition: T (as above) is ω-consistent if the following condition holds for each formula P(x) in T:

If the sentence P(n) is provable in T for each numeral n, then not-∀xP(x) is not provable in T.

In Gödel's original proof of his First Incompleteness Theorem (before Rosser came around), he required that the system was ω-consistent; later one sometimes stated that it was only good for systems which had an axiom schema of induction. (Sorry, offhand I don't have a reference, but I am sure I can dig one up.) This would seem to indicate that if these two are not equivalent then one of them is a more basic condition than the other (more basic, not absolutely basic, as Robinson's Q pointed out). OK, I am sure something is wrong with the paragraph I just typed, so I await correction. If not, then which one is more basic?

 

[stevendaryl]

Is there such a thing as ##c-1## in this system?

The axioms of arithmetic imply that every number except zero has a predecessor, so yes.

We only have the non-negative integers, and operations of addition and multiplication, so it is not clear to me that ##c-1## is capable of being interpreted as a valid symbol string.

Subtraction is not a primitive operation, true, but it's definable. (Actually, we can define an operation ##-## with the property that ##x \geq y \rightarrow y + (x-y) = x##, but ##x \leq y \rightarrow x-y = 0##. That's not exactly subtraction, but it's good enough for most purposes when you're dealing with nonnegative integers.)

I suspect the LHS is intended to say something like P(n) is true whenever n is one of the natural numbers that we all know and love (leaving aside the fact that almost all natural numbers have never been written, spoken or thought of by anybody), and that set is distinguished from ##\mathbb N##, which is the set of objects we have defined with our Peano axioms or such-like, which may include weird things like ##c## and its descendants.

I wonder if there's a non-circular way to refer to 'the natural numbers we know and love'.

Second order logic allows you to specify them.

Let ##X## be any set. Let ##a## be any element of ##X##, and let ##f## be a function on ##X## such that:

• ##f(a) \neq a##
• ##f(x) = f(y) \rightarrow x=y##

Now, if ##Y## is any subset of ##X##, we call ##Y## "inductive" (with respect to ##a## and ##f##) if:

• ##a \in Y##
• ##x \in Y \rightarrow f(x) \in Y##

Finally, we define ##N(a,f)## to be the set of all ##x## such that for all ##Y##, if ##Y## is inductive with respect to ##a## and ##f##, then ##x \in Y##.

Then ##N(a,f)## is a model of the natural numbers, were we interpret 0 as ##a## and interpret ##S## as ##f##.

That's noncircular, although it is a higher-order definition.

 

[andrewkirk]

The axioms of arithmetic imply that every number except zero has a predecessor

Do you have a source for that? I am not aware of such a result. The axioms state that zero is not the successor of any number, and that the successor of any number is also a number, but neither of those says that every number is the successor of a number. Such a statement would have to be a proved theorem. I have a feeling that if such a proof exists, it will need to use the axiom of inequality that assert that ##<## is a total order on ##\mathbb N##, eg:
$$\forall x\forall y\ ((x<y)\vee (y<x) \vee (x=y))$$
and then somehow use arithmetical operations involving numbers that involve ##c## and numbers that don't, and inequalities between same.

Anyway, if you know of a proof that every nonzero element has a predecessor, I'd be grateful if you could share it.

Let ##X## be any set. Let ##a## be any element of ##X##, and let ##f## be a function on ##X## such that:

• ##f(a) \neq a##
• ##f(x) = f(y) \rightarrow x=y##

Now, if ##Y## is any subset of ##X##, we call ##Y## "inductive" (with respect to ##a## and ##f##) if:

• ##a \in Y##
• ##x \in Y \rightarrow f(x) \in Y##

Finally, we define ##N(a,f)## to be the set of all ##x## such that for all ##Y##, if ##Y## is inductive with respect to ##a## and ##f##, then ##x \in Y##.

Then ##N(a,f)## is a model of the natural numbers, were we interpret 0 as ##a## and interpret ##S## as ##f##.

That's noncircular, although it is a higher-order definition.

That's a nice construction. A couple of things I notice about it are.

(1) It looks to me that ##X## has to be infinite since ##N(a,f)##, which we want to be a model of ##\mathbb N##, is a subset of ##X##. So we'll need to use a definition of infinite, as well as to identify an infinite set, to get started.

(2) It relies on the existence of a function ##f## with the desired properties. Given that ##X## is infinite and has no structure specified, it looks like we'll need to use the Axiom of Choice to assert the existence of ##f##. For every ##x\in X## we need to choose ##f(x)## to be an element of ##X\smallsetminus\{x\}##.

How about this, that avoids both using Axiom of Choice and a definition of 'infinite'? We start with the Zermelo-Frankel axioms and choose a set ##X## whose existence is asserted by the Axiom of Infinity. This is the bit I'm unsure of. We are not making an infinite number of choices, so we are not using AC, but we are choosing a specific set even though we can't point to it, using an axiom that merely asserts the existence of such sets.

We then choose the empty set ##\emptyset## as our base element ##a##, which we know is in ##X##, and we choose as our function ##f## the successor function ##y\mapsto\{y,\{y\}\}##. We observe that this satisfies the two requirements of ##f##. We can then define a subset ##U## of the powerset of ##X## as the set of all inductive subsets of ##X##, viz:

$$U\triangleq \{s\in 2^X\ :\ \emptyset\in s\wedge \forall u\ (u\in s\to \{u,\{u\}\}\in s)\}$$

We then define ##\mathbb N## as the set of all ##x\in X## that are in all elements of ##U##, viz:

$$\mathbb N\triangleq \{x\in X\ :\ \forall s\ (s\in U \to x\in s)\}$$

The more I think about it, the more I feel that that first step of 'choosing' ##X## is dodgy. Yet we have to do it, otherwise we do not have a set that we can use as the superset of all the inductive subsets, of which we want to take the intersection. If we don't choose ##X## then we have to use the 'set of all sets' as our superset, and we know that that leads to contradiction and explosion via Russell's paradox (and hence is not possible in ZF).

It looks as though our inability to rigorously define the natural numbers without AC may be deep and fundamental, if it relates to Russell's paradox. The nub of the issue seems to be that we need an infinite set to kickstart the process but, while we have axioms that assert the existence of infinite sets, we cannot point to a specific one without circularity.

 

[andrewkirk]

Here is an attempt at formalising the 'Omega Rule'. It is written in a meta-language L2 that can refer to L and T and items therein. We also assume there is a meta-theory T2 in language L2, which will include Zermelo-Frankel set theory axioms and axioms asserting that the axioms of T and the logical axioms of L hold.

Then, assuming that in (L2,T2) we have managed to define a set ##\mathbb S## of equivalence classes (via the definition of '=' in L) of L-terms that are bijective to the natural numbers we are used to (see previous post for challenges and obstacles to doing this), we can write our Omega Rule as:
\begin{align*}
\forall p\forall v \Bigg(
free(v,p,L) \wedge
\forall g\forall n \bigg[
&(n\in\mathbb S) \wedge subst(g,n,v,p,L) \Rightarrow isTheorem(g,T,L)
\bigg]
\Rightarrow
\\&\forall f \forall w
\bigg[
%cat(f,f,y) \wedge
cat(f,"\forall",w) \wedge cat(w,v,p)
\Rightarrow isTheorem(f,T,L)
\bigg]
\Bigg)
\end{align*}
where:
##isTheorem## is a L2-formula with three free variables, that is a theorem of T2 iff the value of the 1st argument is a ##L'##-symbol string that is a theorem of the theory that is the value of the 2nd argument in the language ##L'## that is the value of the 3rd argument.

##free## is a L2-formula with three free variables, that is a theorem of T2 iff the value of the 1st argument is a ##L'##-symbol that is the only free variable in the 2nd argument which is a formula in the language ##L'## that is the value of the 3rd argument.

##cat## is a L2-formula with four free variables, that is a theorem of T2 iff the value of the 1st argument is a ##L'##-symbol string that is the concatenation of the values of the 2nd and 3rd arguments, where ##L'## is the language that is the value of the 4th argument.

##subst## is a L2-formula with five free variables, that is a theorem of T2 iff the value of the 1st argument is a ##L'##-symbol string that is the result of substituting the shortest ##L'##-symbol string for the number whose value is the 2nd argument, for the ##L'## variable symbol that is the value of the 3rd argument, in the ##L'##-symbol string that is the value of the 4th argument, where ##L'## is the language that is the value of the 5th argument.

That formulas with these properties can be written is demonstrated in this proof of Godel's theorem (the demonstration is on p13-18).

We note that the axiom schema of induction cannot achieve the same thing as this axiom. To do so we would want to write it as:

$$P(0) \wedge \forall x\ (x\in\mathbb S \wedge P(x) \to P(x+1)) \to \forall x\ P(x)$$But we cannot do that because the axioms must be written in L and that language has no way to refer to ##\mathbb S##. I don't yet understand whether we can even properly define ##\mathbb S## in the meta-language L2*, but I am pretty confident we cannot do it in L.

Thought to explore later: perhaps we can avoid circularity by using Russell's hierarchy of classes, so that in some way L2 can refer to the set of all sets in L, but not the set of all sets in L2, and thereby avoid explosion.

 

[Erland]

I have still not seen a statement of the omega rule in (semi-)informal language (sorry andrewkirk, too tired right now to read your formal defnition :) ), so I assume that it means the same as ω-completeness.

Now, it is an easy consequence of Gödel's first incompleteness theorem that any consistent extension of formal first order Peano Arithmetic is not ω-complete. Hence so is every subtheory of such a theory. Hence, for such a subtheory, it is trivially true that ω-completeness implies that each instance of the induction schema is provable, since a false statement implies anything. If the theory is inconsistent, this implication still holds.

The converse is false if formal first order PA is consistent, for then this theory gives an instance for which the (converse) implication is false.

 

[nomadreid]

Now, it is an easy consequence of Gödel's first incompleteness theorem that any consistent extension of formal first order Peano Arithmetic is not ω-complete. Hence so is every subtheory of such a theory. Hence, for such a subtheory, it is trivially true that ω-completeness implies that each instance of the induction schema is provable, since a false statement implies anything. If the theory is inconsistent, this implication still holds.

The converse is false if formal first order PA is consistent, for then this theory gives an instance for which the (converse) implication is false.

Thank you, Erland. That establishes that ω-completeness is a stronger principle than the induction schema. So, I now come back to my questions: which is a stronger principle: ω-consistency or the induction schema? If they are not equivalent, which one would be the minimum necessary for the original proof of Gödel's first theorem to go through?

 

[Erland]

Well, it is clear that if formal first order Peano arithmetic (PA) is consistent, then provability of all induction instances does not imply ω-consistency, for a theory with the language of PA. As a counterexample, take the theory PA + not-G, where G is the Gödel sentence of PA. The axioms of this theory are the axioms of PA plus the negation of G. Since G is not provable in PA, PA + not-G is consistent (provided that PA is). Now, all induction instances are provable in PA + not-G, since they are in PA.

Next, let P(x) be the predicate in this theory with interpretation "x is not the Gödel number of a proof of G in PA". Then P(n) is provable in PA, and hence in PA + not-G, for every numeral n. Now, ∀xP(x) is G itself, and its negation is not-G, which is trivially provable in PA + not-G. This means that PA + not-G is not ω-consistent.

So, provabilty of induction does not imply ω-consistency.

But I am not right now clear over whether ω-consistency implies provability of induction or not (for a theory in the language of PA).

EDIT: If PA is ω-consistent, then ω-consistency does not imply provability of induction either. Robinson Arithmetic (RA) is a theory which is the same as PA, which the induction scheme replaced with the weaker axiom

∀x(x=0 ∨ ∃y(Sy = x)).

RA is ω-consistent, since PA is (as we assumed). But induction in not provable in RA. If it was, then
∀x(Sx≠x) would be provable in RA, but it is not. This can be seen by observing that RA has a model where the latter is false, by adjoining an element ω to ℕ, and stipulating that Sω=ω, ω+x = x+ω = ω for all x, ω*0 = 0*ω = 0, and ω*x = x*ω = ω for all x≠0.