In mathematical logic, an ω-consistent (or omega-consistent, also called numerically segregative)[1] theory is a theory (collection of sentences) that is not only (syntactically) consistent[2] (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.
[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").
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).
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.
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.
Let IΣn be the subtheory of PA with the induction schema restricted to Σn-formulas, for any n > 0.
We can assume that A is an instance of the induction schema, which has the form If we denote the formula by P(n), then for every natural number n, the theory T (actually, even the pure predicate calculus) proves P(n).
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.
[8] 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.).
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: 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.
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.
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.
If the theory T is recursively axiomatizable, ω-consistency has the following characterization, due to Craig Smoryński:[9] Here,
In particular, a finitely axiomatizable theory T in the language of arithmetic is ω-consistent if and only if T + PA is