ω-complete theory

In mathematical logic, an ω-complete theory is a formal theory in first-order logic, containing arithmetics, such that whenever it proves every natural number instance of a formula, it also proves the corresponding universal sentence. A theory with the complementary property is called ω-incomplete. The ω in the name refers to the set of natural numbers.

The terminology was established in the 1958 paper The Classical and the ω-Complete Arithmetic by Andrzej Grzegorczyk, Andrzej Mostowski, and Czesław Ryll-Nardzewski.^[1]

Consider a first-order language that contains terms for the natural numbers ${\displaystyle {\bar {0}},{\bar {1}},{\bar {2}},\ldots }$. For example, the standard language for Peano arithmetic contains the two symbols ${\displaystyle 0,S}$, with which we can write down the terms for all the natural numbers: ${\displaystyle 0,S0,SS0,\dots }$.

Let ${\displaystyle T}$ be a theory in the language. ${\displaystyle T}$ is ω-complete iff, for every formula ${\displaystyle \varphi (x)}$ with one free variable,$${\displaystyle T\vdash \varphi ({\bar {n}}){\text{ for every }}n\in \omega \quad \Longrightarrow \quad T\vdash \forall x\,\varphi (x).}$$The implication may appear obvious. However, one must distinguish between ${\displaystyle \vdash }$, which is a consequence within the object-theory, and ${\displaystyle \implies }$, which is a consequence in the meta-theory. A theory is ω-complete if it can perform this consequence within the object-theory, rather than perform it outside in the meta-theory.

It is possible for a theory to be ω-incomplete, because the theory may have a model ${\displaystyle {\mathcal {M}}}$ with non-standard integers. In the model, we can have ${\displaystyle {\mathcal {M}}\models \varphi ({\bar {0}}),{\mathcal {M}}\models \varphi ({\bar {1}}),\dots }$, but nevertheless have ${\displaystyle {\mathcal {M}}\not \models \varphi (c)}$ for a certain non-standard integer ${\displaystyle c}$ in the model.

A standard weak example is Robinson arithmetic ${\displaystyle Q}$. It proves each instance of ${\displaystyle 0+{\bar {n}}={\bar {n}}}$, while the universal sentence ${\displaystyle \forall x(0+x=x)}$ lies beyond its theorems. This can be computably demonstrated by building a computable nonstandard model of ${\displaystyle Q}$, in which ${\displaystyle 0+c\neq 0}$ for a non-standard integer element ${\displaystyle c}$. Accordingly, ${\displaystyle Q}$ is ω-incomplete.^[2]

Peano arithmetic repairs many weak failures of that kind, yet standard incompleteness arguments still yield ω-incompleteness under the usual consistency assumption. In particular, Gödel's second incompleteness theorem provide an example. Consider a Gödel numbering of all proofs in PA, and let ${\displaystyle \varphi ({\bar {n}})}$ to mean "If number ${\displaystyle n}$ is a valid proof in PA, then its conclusion is not ${\displaystyle 0=1}$". Then, ${\displaystyle PA\vdash \varphi ({\bar {0}}),PA\vdash \varphi ({\bar {1}}),\dots }$, but ${\displaystyle PA\not \vdash \forall x\varphi (x)}$ by incompleteness. This argument applies to any recursively axiomatized theory that contains PA.^[3]

ω-completeness is closely related to ω-consistency. A theory is ω-consistent when no formula ${\displaystyle \psi (x)}$ yields both the existential sentence ${\displaystyle \exists x\,\psi (x)}$ and every numeral instance ${\displaystyle \neg \psi ({\bar {n}})}$.^[2] The two notions mark different syntactic patterns in the study of formal theories.

By the completeness theorem, a consistent theory is ω-incomplete if and only if it can be extended to a consistent but ω-inconsistent theory.

ω-completeness is also connected with the ω-rule,$${\displaystyle A(0),A(1),A(2),\ldots \;\Rightarrow \;\forall n\,A(n).}$$Proof systems using the ω-rule build the passage from all numeral instances to the universal conclusion directly into the proof system.

• Gödel's incompleteness theorems
• Peano arithmetic
• ω-consistency
• ω-rule

• "Gödel's Incompleteness Theorems". Stanford Encyclopedia of Philosophy. 2025-10-08. Retrieved 2026-04-17.
• Hájek, Petr; Pudlák, Pavel (1993). Metamathematics of First-Order Arithmetic. Berlin: Springer.