Given a φ independent of PA which is true in the standard model, will always (PA+ ¬φ) be ω-inconsistent?

Question

Given a φ independent of PA which is true in the standard model, will always (PA+ ¬φ) be ω-inconsistent? Does it mean that every such ¬φ can be used to prove that a Turing machine halts on a given C when it will actually never halt?

Answer 1

The usual definition of $\omega$ consistency is:

A theory $T$ is $\omega$-inconsistent if there is a formula $\psi$ such that $T$ proves $(\exists x)\psi(x)$, and $T$ also proves $\lnot \psi(n)$ separately for each standard natural number $n$.

$T$ is $\omega$-consistent if it is not $\omega$-inconsistent.

The property that "for every sentence $\psi$, if the theory proves $\psi$ then $\psi$ is true in the standard model" is called "arithmetical soundness" of the theory $T$. The statement "if $T$ proves that a Turing machine halts then it does halt" is a special case of soundness known as "1-consistency" which is formally defined using a certain classification of formulas. A formula in the language of arithmetic is called $\Sigma^0_1$ if it is of the form $(\exists x)\psi(x)$ where $\psi(x)$ has only bounded quantifiers. It turns out that for any Turing machine $m$, the statement "$m$ halts on input $x$" can be expressed as a $\Sigma^0_1$ formula $\psi(x)$, and vice versa. 1-consistency is defined as soundness for $\Sigma^0_1$ formulas.

Unfortunately, there is only a weak relationship between arithmetical soundness, 1-consistency and $\omega$-consistency:

• (1) Every sufficiently strong $\omega$-consistent theory is 1-consistent, that is, $\Sigma^0_1$ sound. "Sufficiently strong" here includes the assumption that the theory proves every true $\Sigma^0_1$ sentence - PA has this property.

The following examples show that we can't strengthen that statement very much:

• (2) There are theories that are $\omega$-consistent but not arithmetically sound: they prove sentences that are false in the standard model of arithmetic. Some of these theories are even of the form $PA + \lnot\phi$ for a sentence $\phi$ that is true in the standard model and independent of PA.

• (3) There are $1$-consistent theories (that is, $\Sigma^0_1$ sound) that are $\omega$-inconsistent. Some of these theories are even of the form $PA + \lnot\phi$ for a sentence $\phi$ that is true in the standard model and independent of PA.

Example (2) shows that it is not the case that $PA + \lnot \phi$ has to be $\omega$-inconsistent, which answers the first part of the question.

Example (3) shows that it is possible for $PA + \lnot \phi$ to be $\Sigma^0_1$ sound, in which case it never proves that a Turing machine halts unless the machine does halt. That answers the second part of the question.