In mathematical logic, an ωconsistent (or omegaconsistent, also called numerically segregative^{[1]}) 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.^{[2]}
Contents

Definition 1

Examples 2

Consistent, ωinconsistent theories 2.1

Arithmetically sound, ωinconsistent theories 2.2

Arithmetically unsound, ωconsistent theories 2.3

ωlogic 3

Relation to other consistency principles 4

Notes 5

Bibliography 6
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 (necessarily nonstandard) natural number n such that P(n) fails. This may not lead directly to an outright contradiction, 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 Σ_{1}soundness. A theory T is Σ_{1}sound (or 1consistent, in another terminology) if every Σ^{0}_{1}sentence^{[3]} 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 computer program 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 Σ^{0}_{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) (since an inconsistent theory proves every sentence), 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 Σ_{1}, hence the system PA + ¬Con(PA) is in fact Σ_{1}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).
Σ_{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


\forall w\,[B(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\,[B(0,w)\land\forall x\,(B(x,w)\to B(x+1,w))\to B(n,w)]
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 (Σ_{3}unsound, to be precise), but ωconsistent. The argument is similar to the first example: a suitable version of the HilbertBernaysLö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.^{[4]} Let T be a theory in a countable language which 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 firstorder predicate logic, together with, for each Tformula 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 C. Smoryński:^{[5]}

T is ωconsistent if and only if T+\mathrm{RFN}_T+\mathrm{Th}_{\Pi^0_2}(\mathbb N) is consistent.
Here, \mathrm{Th}_{\Pi^0_2}(\mathbb N) is the set of all Π^{0}_{2}sentences valid in the standard model of arithmetic, and \mathrm{RFN}_T is the uniform reflection principle for T, which consists of the axioms

\forall x\,(\mathrm{Prov}_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_2sound.
Notes

^ W.V.O. Quine, Set Theory and its Logic

^ Smorynski, "The incompleteness theorems", Handbook of Mathematical Logic, 1977, p. 851.

^ The definition of this symbolism can be found at arithmetical hierarchy.

^ J. Barwise (ed.), Handbook of Mathematical Logic, NorthHolland, Amsterdam, 1977.

^ Craig Smoryński, Selfreference and modal logic, Springer, Berlin, 1985.
Bibliography
This article was sourced from Creative Commons AttributionShareAlike License; additional terms may apply. World Heritage Encyclopedia content is assembled from numerous content providers, Open Access Publishing, and in compliance with The Fair Access to Science and Technology Research Act (FASTR), Wikimedia Foundation, Inc., Public Library of Science, The Encyclopedia of Life, Open Book Publishers (OBP), PubMed, U.S. National Library of Medicine, National Center for Biotechnology Information, U.S. National Library of Medicine, National Institutes of Health (NIH), U.S. Department of Health & Human Services, and USA.gov, which sources content from all federal, state, local, tribal, and territorial government publication portals (.gov, .mil, .edu). Funding for USA.gov and content contributors is made possible from the U.S. Congress, EGovernment Act of 2002.
Crowd sourced content that is contributed to World Heritage Encyclopedia is peer reviewed and edited by our editorial staff to ensure quality scholarly research articles.
By using this site, you agree to the Terms of Use and Privacy Policy. World Heritage Encyclopedia™ is a registered trademark of the World Public Library Association, a nonprofit organization.