Definition[edit]
A theory T is said to interpret the language of arithmetic if there is a translation of formulas of arithmetic into the language of T so that T is able to prove the basic axioms of the natural numbers under this translation.
A T that interprets arithmetic is ω-inconsistent if, for some property P of natural numbers (defined by a formula in the language of T), T proves P(0), P(1), P(2), and so on (that is, for every standard natural number n, T proves that P(n) holds), but T also proves that there is some natural number n such that P(n) fails.[2] This may not generate a contradiction within T because T may not be able to prove for any specific value of n that P(n) fails, only that there is such an n. In particular, such n is necessarily a nonstandard integer in any model for T (Quine has thus called such theories "numerically insegregative").[4]
T is ω-consistent if it is not ω-inconsistent.
There is a weaker but closely related property of Σ1-soundness. A theory T is Σ1-sound (or 1-consistent, in another terminology)[5] if every Σ01-sentence[6] provable in T is true in the standard model of arithmetic N (i.e., the structure of the usual natural numbers with addition and multiplication).
If T is strong enough to formalize a reasonable model of computation, Σ1-soundness is equivalent to demanding that whenever T proves that a Turing machine C halts, then C actually halts. Every ω-consistent theory is Σ1-sound, but not vice versa.
More generally, we can define an analogous concept for higher levels of the arithmetical hierarchy. If Γ is a set of arithmetical sentences (typically Σ0n for some n), a theory T is Γ-sound if every Γ-sentence provable in T is true in the standard model. When Γ is the set of all arithmetical formulas, Γ-soundness is called just (arithmetical) soundness.
If the language of T consists only of the language of arithmetic (as opposed to, for example, set theory), then a sound system is one whose model can be thought of as the set ω, the usual set of mathematical natural numbers. The case of general T is different, see ω-logic below.
Σn-soundness has the following computational interpretation: if the theory proves that a program C using a Σn−1-oracle halts, then C actually halts.
Examples[edit]
Consistent, ω-inconsistent theories[edit]
Write PA for the theory Peano arithmetic, and Con(PA) for the statement of arithmetic that formalizes the claim "PA is consistent". Con(PA) could be of the form "No natural number n is the Gödel number of a proof in PA that 0=1".[7] Now, the consistency of PA implies the consistency of PA + ¬Con(PA). Indeed, if PA + ¬Con(PA) was inconsistent, then PA alone would prove ¬Con(PA)→0=1, and a reductio ad absurdum in PA would produce a proof of Con(PA). By Gödel's second incompleteness theorem, PA would be inconsistent.
Therefore, assuming that PA is consistent, PA + ¬Con(PA) is consistent too. However, it would not be ω-consistent. This is because, for any particular n, PA, and hence PA + ¬Con(PA), proves that n is not the Gödel number of a proof that 0=1. However, PA + ¬Con(PA) proves that, for some natural number n, n is the Gödel number of such a proof (this is just a direct restatement of the claim ¬Con(PA)).
In this example, the axiom ¬Con(PA) is Σ1, hence the system PA + ¬Con(PA) is in fact Σ1-unsound, not just ω-inconsistent.
Arithmetically sound, ω-inconsistent theories[edit]
Let T be PA together with the axioms c ≠ n for each natural number n, where c is a new constant added to the language. Then T is arithmetically sound (as any nonstandard model of PA can be expanded to a model of T), but ω-inconsistent (as it proves , and c ≠ n for every number n).
Σ1-sound ω-inconsistent theories using only the language of arithmetic can be constructed as follows. Let IΣn be the subtheory of PA with the induction schema restricted to Σn-formulas, for any n > 0. The theory IΣn + 1 is finitely axiomatizable, let thus A be its single axiom, and consider the theory T = IΣn + ¬A. We can assume that A is an instance of the induction schema, which has the form
