Consistency formula is strictly stronger in PA than PA-consistency

TL;DR

This paper shows that the standard consistency statement for PA is strictly stronger than the series of its finite approximations, clarifying their logical relationship within PA.

Contribution

It proves that Con(PA) is not equivalent to the series ConS(PA) in PA, establishing a strict strength difference between them.

Findings

Con(PA) is not equivalent to ConS(PA) in PA.

Con(PA) is strictly stronger than ConS(PA) in PA.

Unprovability of Con(PA) does not imply unprovability of PA's consistency.

Abstract

In this note, we show that, despite the widespread assumption, the consistency formula for Peano Arithmetic PA, Con(PA), "for all x, x is not a code of a derivation of (0=1)," is not equivalent in PA to the consistency of PA. Specifically, we demonstrate that "PA is consistent" is provably in PA equivalent to the series ConS(PA) of arithmetical sentences "n is not a code of a derivation of (0=1)" for n=0,1,2,.... Since Con(PA) is strictly stronger in PA than ConS(PA), the unprovability of Con(PA) in PA does not yield the unprovability of PA-consistency.

Equations

$$0,1,2,\dots ,n,\dots$$

$$P$$

$$D$$

$$n$$

$$\forall x(\neg x:\perp ).$$

$$\{\neg 0:\perp ,\neg 1:\perp ,\neg 2:\perp ,\neg 3:\perp \dots \}.$$

$$\mbox{\it each formula in ${\sf Con}^{S}_{\sf PA}$ holds}.$$

$$N(k)=\left\{\begin{array}[]{ll}n,&\mbox{\it if $k=\ulcorner{\neg n\!\!:\!\!\bot}\urcorner$}\\ 0,&\mbox{\it otherwise}.\end{array}\right.$$

$$\mathsf{PA}⊢\forall x(N[(\neg x:\perp {)}^{\bullet }]=x).$$

$$\mathsf{PA}⊢S(y)\leftrightarrow \exists x(y=(\neg x:\perp {)}^{\bullet }).$$

$$\mathsf{PA}⊢\phi (x)\leftrightarrow \text{mbox}{Tr}_1(\phi (x{)}^{\bullet }).$$

$$\forall x(\neg x:\perp ).$$

$$\forall y(S(y)\to \text{mbox}{Tr}_1(y)).$$

$$\mathsf{PA}⊢\forall xA(x)\leftrightarrow \forall xB(x)$$

$$\mathsf{PA}⊢A(f(x))\to B(x)\text{mbox}and\mathsf{PA}⊢B(h(x))\to A(x).$$

Full text

In [1], the PA-consistency in the form ${\sf Con}^{S}_{\sf PA}$ has been proven in PA.

1 Arithmetic: contentual vs. formal

We consider some fragment of contentual mathematics which, within this paper, we call Ar (for “Arithmetic”) which contains the set of natural numbers $\omega$

[TABLE]

and includes all primitive recursive operations on $\omega$.

We also consider the Peano Arithmetic PA, which is a formal first-order theory with the symbols and defining identities for all primitive recursive functions, one sort of variables to symbolically represent unspecified “natural numbers.” Along with logical axioms, PA has the Induction Principle represented by an infinite series of instances of induction for each arithmetical formula. PA has a unique standard model which is the structure with the domain $\omega$ in the language of PA satisfying all postulates of PA.

By Gödel’s Incompleteness Theorem, there are models of PA which are not isomorphic to the standard model. Simply speaking, there are (continuum many) countable nonstandard models of PA each of which, in addition to $\omega$, has so-called nonstandard numbers.

The domain of formal quantifiers $\forall x$ and $\exists x$ in PA is not specified and depends on a model. In nonstandard models, $\forall x$ and $\exists x$ do not range over $0,1,2,\ldots,n,\ldots$.

2 Contentual property vs. its formalization

Consider a contentual property $P$ of natural numbers expressible in Ar. Suppose that $P$ can be formalized as a formula $P_{f}$ in the language of PA by the following step-by-step formalization process: recursive operations on natural numbers in Ar are directly represented by PA-terms, propositional logic operations are straightforward, informal quantifiers “for all natural numbers $n$” and “exists a natural number $n$” are formalized as $\forall x$ and $\exists x$. We refer to $P_{f}$ as

[TABLE]

2.1 PA consistency vs. the consistency formula ${\sf Con}_{\sf PA}$

The consistency of a formal theory means that all its formal derivations are free of contradictions. For the case of PA,

[TABLE]

Derivations are finite syntactic objects, and their Gödel codes are all standard natural numbers. Such numbers can be identified with numerals, terms $\overline{0},\overline{1},\overline{2},\ldots,\overline{n}\ldots$ in the language of PA. We do not distinguish a syntactic object $X$ and its Gödel number $\ulcorner{X}\urcorner$, a natural number $n$, and the corresponding numeral $\overline{n}$ when safe. Let also $\bot$ denote the arithmetic formula $(0\!=\!1)$.

Let $x\!:\!y$ denote the standard primitive recursive proof predicate in PA,

[TABLE]

The proof predicate is represented by a quantifier-free PA-formula which we also call $x\!:\!y$.

Since the proof predicate is a direct copy of the definition of a formal proof, for each derivation $D$ and formula $\varphi$, the equivalence of “$D$ is a proof of $\varphi$” and $\ulcorner{D}\urcorner\!:\!\ulcorner{\varphi}\urcorner$ is a straightforward combinatorial observation about Gödel coding and it is uniformly provable in PA.

Following Gödel, we reformulate PA consistency (1) in an equivalent form in the contentual arithmetic Ar:

[TABLE]

This Gödelized definition (3) of PA-consistency is not yet in the language of PA since it contains an informal quantifier “for any natural number $n$” not expressible in PA.

The direct formalization of (3) is the consistency formula ${\sf Con}_{\sf PA}$, i.e.,

[TABLE]

It would be a mistake to assume a priori that the consistency formula ${\sf Con}_{\sf PA}$ (4) adequately represents PA-consistency property (3) in PA because of different quantifications in (3) and (4).

The direct mathematical comparison of (3) and (4) is not possible since (3) is a well-defined mathematical property whereas (4) is not; the formal quantifier “$\forall x$” in ${\sf Con}_{\sf PA}$ is not specified and its meaning depends on a choice of an arithmetical model. Comparing (3) and (4) formally within PA is also not possible since (3) is not in the language of PA. So, the choice of ${\sf Con}_{\sf PA}$ as representing “ PA is consistent” in PA has not had a mathematical justification.

As it follows from the results of the next Section 2.2, such a choice cannot be justified since, in PA, consistency formula ${\sf Con}_{\sf PA}$ is strictly stronger than PA-consistency.

2.2 PA-consistency is equivalent in PA to the consistency scheme

As we have already mentioned, the Gödelized definition (3) of PA-consistency contains an informal quantifier “for any natural number $n$” not expressible in PA. However, we can emulate quantifiers over standard numbers by sets of formulas in PA.

Consistency scheme is the set ${\sf Con}^{S}_{\sf PA}$ of PA-formulas

[TABLE]

Sets (sequences, schemes, etc.) of formulas are common objects in metamathematics of first-order theories. In particular, the induction principle is expressed in PA by the Induction Scheme, which is a primitive recursive set of PA-formulas. A set $X$ of PA–formulas holds under a given interpretation if each formula in $X$ holds.111The rigorous notion of a proof of a serial property in a theory was offered in [1] (selector proofs) and studied in [1, 2]. So, the rigorous reading of “${\sf Con}^{S}_{\sf PA}$ holds” is

[TABLE]

All formulas in ${\sf Con}^{S}_{\sf PA}$ are closed quantifier-free sentences and hence ${\sf Con}^{S}_{\sf PA}$ is a well-defined mathematical property. This allows us to compare (3) and (5) mathematically. Their comparison below amounts to a trivial observation, but we carry it on anyway to make sure it is formalizable in PA.

Proposition 1

PA*-consistency and ${\sf Con}^{S}_{\sf PA}$ are mathematically equivalent.*

Proof.

$(\Rightarrow)$. Suppose “PA is consistent,” i.e., (3). Pick an arbitrary natural number $n$, then, by (3), $\neg n\!\!:\!\!\bot$ holds, hence ${\sf Con}^{S}_{\sf PA}$ holds.

$(\Leftarrow)$. Suppose ${\sf Con}^{S}_{\sf PA}$ holds, then each $\neg n\!\!:\!\!\bot$ holds, hence (3).

$\Box$

The next step is to formalize this proof in PA.

Proposition 2

The proof of Proposition 1 is formalizable in PA.

Proof. This is a Gödelian formalization under which syntactic objects, such as numerals, terms, formulas, are represented by their Gödel numbers, operations and relations on these objects by primitive recursive terms and predicates. Furthermore, after Gödel, we use the PA-formula $x\!\!:\!\!y$ as a direct formal representation of the proof predicate (2).

Given an arithmetic formula $\varphi(x)$, consider the natural arithmetical term $\varphi(x)^{\bullet}$ for the primitive recursive function which for each $n$ returns $\ulcorner{\varphi(n)}\urcorner$. In particular, $(\neg x\!\!:\!\!\bot)^{\bullet}$ is a primitive recursive enumeration of ${\sf Con}^{S}_{\sf PA}$ which for each $n$ return the Gödel number of the $n$th formula in ${\sf Con}^{S}_{\sf PA}$.

Consider a function which is, in a sense, the converse of $(\neg x\!\!:\!\!\bot)^{\bullet}$. Let $N(y)$ be a natural arithmetical term for a primitive recursive function

[TABLE]

By the construction of $N(y)$,

[TABLE]

Consider a formula $S(y)$ which is $y=g(N(y))$ with $g(x)=(\neg x\!\!:\!\!\bot)^{\bullet}$. PA can prove that $S(y)$ is a characteristic function for the set of Gödel numbers of formulas from ${\sf Con}^{S}_{\sf PA}$, i.e.,

[TABLE]

Indeed, argue in PA. Suppose $S(y)$, i.e., $y=g(N(y))$, and take $a=N(y)$. Then $y=(\neg a\!\!:\!\!\bot)^{\bullet}$ hence $\exists x(y=(\neg x\!\!:\!\!\bot)^{\bullet})$. Now suppose for some $a$, $y=(\neg a\!\!:\!\!\bot)^{\bullet}$. By (7), $N(y)=a$, hence $y=g(N(y))$, i.e., $S(y)$.

Now we are back to proving Proposition 2. To convert Gödel numbers $\ulcorner{\neg n\!\!:\!\!\bot}\urcorner$ back to formulas $\neg n\!\!:\!\!\bot$ in PA, we use the truth predicate $\mbox{\it Tr}_{1}$ for $\Sigma_{1}$-formulas (cf. [1, 4]). This truth predicate satisfies Tarksi’s condition for a $\Sigma_{1}$-formula $\varphi$:

[TABLE]

The direct formalization of PA-consistency (3) is

[TABLE]

The direct formalization of “${\sf Con}^{S}_{\sf PA}$ holds” (6) is

[TABLE]

Now we are formalizing the proof of Proposition 1 in PA.

$(\Rightarrow)$. Suppose $\forall x(\neg x\!\!:\!\!\bot)$. Pick $y$ and suppose $S(y)$. By (8), there is $x$ such that $y=(\neg x\!\!:\!\!\bot)^{\bullet}$. Since $\neg x\!\!:\!\!\bot$ and (9), $\mbox{\it Tr}_{1}((\neg x\!\!:\!\!\bot)^{\bullet})$, hence $\mbox{\it Tr}_{1}(y)$.

$(\Leftarrow)$. Suppose $\forall y(S(y)\!\rightarrow\!\mbox{\it Tr}_{1}(y))$ and pick an arbitrary $x$. Take $y=(\neg x\!\!:\!\!\bot)^{\bullet}$. By (8), $S(y)$. By assumptions, $\mbox{\it Tr}_{1}(y)$, hence $\mbox{\it Tr}_{1}((\neg x\!\!:\!\!\bot)^{\bullet})$. By (9), $\neg x\!\!:\!\!\bot$. $\Box$

Comment. For the proof of Proposition 1 and its formalization in Proposition 2, we have chosen natural and easy versions. However, the argument supports a more technical, but more constructive formulation. In the current form, Proposition 2 proves that for appropriate $A$, $B$,

[TABLE]

The proof of Proposition 2 actually shows something slightly stronger. It builds primitive recursive functions $f(x)$ and $h(x)$ such that

[TABLE]

3 On Hilbert’s consistency program

Since ${\sf Con}^{S}_{\sf PA}$ is a mathematically justified way to represent the consistency of PA in PA, and ${\sf Con}_{\sf PA}$ is strictly stronger in PA than ${\sf Con}^{S}_{\sf PA}$ (an easy observation, cf. [1]), Gödel’s theorem stating the unprovability of ${\sf Con}_{\sf PA}$ does not answer the question of provability of PA-consistency in PA. The selector proof of the PA-consistency in the form ${\sf Con}^{S}_{\sf PA}$ in [1] provides a mathematically justified (affirmative) answer to the question of provability of PA-consistency in PA.

For many decades, Gödel’s Second Incompleteness Theorem, yielding the unprovability of ${\sf Con}_{\sf PA}$ in PA, has been regarded as mathematical evidence of the impossibility of Hilbert’s consistency program (cf., for example, [3, 5]). The aforementioned analysis of differences between the consistency formula ${\sf Con}_{\sf PA}$ and PA-consistency suggests that such cancelling of Hilbert’s consistency program has been premature.

For the recent progress in Hilbert’s program related to treating consistency as a serial property, including the disproof of the unprovability of consistency paradigm, cf. [1, 2].