ω-consistent Theory

In mathematical logic, an ω-consistent (or omega-consistent, also called numerically segregative)W. V. O. Quine (1971), ''Set Theory and Its Logic''. theory is a theory (collection of sentences) that is not only (syntactically) consistent (that is, does not prove a contradiction), but also avoids proving certain infinite combinations of sentences that are intuitively contradictory. The name is due to Kurt Gödel, who introduced the concept in the course of proving the incompleteness theorem.

Definition

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'' (necessarily nonstandard in any model for ''T'') such that ''P''(''n'') ''fails''. 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''.

''T'' is ω-consistent if it is ''not'' ω-inconsistent.

There is a weaker but closely related property of Σ₁-soundness. A theory ''T'' is Σ₁-sound (or 1-consistent, in another terminology) if every Σ⁰₁-sentence 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, Σ₁-soundness is equivalent to demanding that whenever ''T'' proves that a Turing machine ''C'' halts, then ''C'' actually halts. Every ω-consistent theory is Σ₁-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 Σ⁰_''n'' 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

Consistent, ω-inconsistent theories

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 "For every natural number ''n'', ''n'' is not the Gödel number of a proof from PA that 0=1". (This formulation uses 0=1 instead of a direct contradiction; that gives the same result, because PA certainly proves ¬0=1, so if it proved 0=1 as well we would have a contradiction, and on the other hand, if PA proves a contradiction, then it proves anything, including 0=1.)

Now, assuming PA is really consistent, it follows that PA + Â¬Con(PA) is also consistent, for if it were not, then PA would prove Con(PA) (''reductio''), contradicting Gödel's second incompleteness theorem. However, PA + Â¬Con(PA) is ''not'' ω-consistent. This is because, for any particular natural number ''n'', PA + Â¬Con(PA) proves that ''n'' is not the Gödel number of a proof that 0=1 (PA itself proves that fact; the extra assumption ¬Con(PA) is not needed). 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 Σ₁, hence the system PA + Â¬Con(PA) is in fact Σ₁-unsound, not just ω-inconsistent.

Arithmetically sound, ω-inconsistent theories

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 $\exists x\,c=x$, and ''c'' â‰  ''n'' for every number ''n'').

Σ₁-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
::\forall w\, (0,w)\land\forall x\,(B(x,w)\to B(x+1,w))\to\forall x\,B(x,w)
If we denote the formula
::\forall w\, (0,w)\land\forall x\,(B(x,w)\to B(x+1,w))\to B(n,w)/math>
by ''P''(''n''), then for every natural number ''n'', the theory ''T'' (actually, even the pure predicate calculus) proves ''P''(''n''). On the other hand, ''T'' proves the formula $\exists x\,\neg P(x)$, because it is logically equivalent to the axiom ¬''A''. Therefore, ''T'' is ω-inconsistent.

It is possible to show that ''T'' is Π_''n'' + 3-sound. In fact, it is Π_''n'' + 3-conservative over the (obviously sound) theory ''I''Σ_''n''. The argument is more complicated (it relies on the provability of the Σ_''n'' + 2-reflection principle for ''I''Σ_''n'' in ''I''Σ_''n'' + 1).

Arithmetically unsound, ω-consistent theories

Let ω-Con(PA) be the arithmetical sentence formalizing the statement "PA is ω-consistent". Then the theory PA + Â¬Ï‰-Con(PA) is unsound (Σ₃-unsound, to be precise), but ω-consistent. The argument is similar to the first example: a suitable version of the Hilbert– Bernays– Löb derivability conditions holds for the "provability predicate" ω-Prov(''A'') = Â¬Ï‰-Con(PA + Â¬''A''), hence it satisfies an analogue of Gödel's second incompleteness theorem.

ω-logic

The concept of theories of arithmetic whose integers are the true mathematical integers is captured by ω-logic. Let ''T'' be a theory in a countable language that includes a unary predicate symbol ''N'' intended to hold just of the natural numbers, as well as specified names 0, 1, 2, ..., one for each (standard) natural number (which may be separate constants, or constant terms such as 0, 1, 1+1, 1+1+1, ..., etc.). Note that ''T'' itself could be referring to more general objects, such as real numbers or sets; thus in a model of ''T'' the objects satisfying ''N''(''x'') are those that ''T'' interprets as natural numbers, not all of which need be named by one of the specified names.

The system of ω-logic includes all axioms and rules of the usual first-order predicate logic, together with, for each ''T''-formula ''P''(''x'') with a specified free variable ''x'', an infinitary ω-rule of the form:
:From $P(0),P(1),P(2),\ldots$ infer $\forall x\,(N(x)\to P(x))$.

That is, if the theory asserts (i.e. proves) ''P''(''n'') separately for each natural number ''n'' given by its specified name, then it also asserts ''P'' collectively for all natural numbers at once via the evident finite universally quantified counterpart of the infinitely many antecedents of the rule. For a theory of arithmetic, meaning one with intended domain the natural numbers such as Peano arithmetic, the predicate ''N'' is redundant and may be omitted from the language, with the consequent of the rule for each ''P'' simplifying to $\forall x\,P(x)$.

An ω-model of ''T'' is a model of ''T'' whose domain includes the natural numbers and whose specified names and symbol ''N'' are standardly interpreted, respectively as those numbers and the predicate having just those numbers as its domain (whence there are no nonstandard numbers). If ''N'' is absent from the language then what would have been the domain of ''N'' is required to be that of the model, i.e. the model contains only the natural numbers. (Other models of ''T'' may interpret these symbols nonstandardly; the domain of ''N'' need not even be countable, for example.) These requirements make the ω-rule sound in every ω-model. As a corollary to the omitting types theorem, the converse also holds: the theory ''T'' has an ω-model if and only if it is consistent in ω-logic.

There is a close connection of ω-logic to ω-consistency. A theory consistent in ω-logic is also ω-consistent (and arithmetically sound). The converse is false, as consistency in ω-logic is a much stronger notion than ω-consistency. However, the following characterization holds: a theory is ω-consistent if and only if its closure under ''unnested'' applications of the ω-rule is consistent.

Relation to other consistency principles

If the theory ''T'' is recursively axiomatizable, ω-consistency has the following characterization, due to Craig Smoryński: Reviewed in
:''T'' is ω-consistent if and only if $T+\mathrm_T+\mathrm_(\mathbb N)$ is consistent.
Here, $\mathrm_(\mathbb N)$ is the set of all Π⁰₂-sentences valid in the standard model of arithmetic, and $\mathrm_T$ is the uniform reflection principle for ''T'', which consists of the axioms
:$\forall x\,(\mathrm_T(\ulcorner\varphi(\dot x)\urcorner)\to\varphi(x))$
for every formula $\varphi$ with one free variable. In particular, a finitely axiomatizable theory ''T'' in the language of arithmetic is ω-consistent if and only if ''T'' + PA is $\Sigma^0_2$-sound.

Notes

Bibliography

* Kurt Gödel (1931). 'Über formal unentscheidbare Sätze der Principia Mathematica und verwandter Systeme I'. In ''Monatshefte für Mathematik''. Translated into English as On Formally Undecidable Propositions of Principia Mathematica and Related Systems.

{{DEFAULTSORT:Omega consistent theory
Proof theory