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?
- Anybody can ask a question
- Anybody can answer
- The best answers are voted up and rise to the top
The usual definition of $\omega$ consistency is:
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:
The following examples show that we can't strengthen that statement very much:
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.