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.
Definition Consider a first-order language that contains terms for the natural numbers 0 ¯ , 1 ¯ , 2 ¯ , … {\displaystyle {\bar {0}},{\bar {1}},{\bar {2}},\ldots } . For example, the standard language for Peano arithmetic contains the two symbols 0 , S {\displaystyle 0,S} , with which we can write down the terms for all the natural numbers: 0 , S 0 , S S 0 , … {\displaystyle 0,S0,SS0,\dots } . Let T {\displaystyle T} be a theory in the language. T {\displaystyle T} is ω-complete iff, for every formula φ ( x ) {\displaystyle \varphi (x)} with one free variable, T ⊢ φ ( n ¯ ) for every n ∈ ω ⟹ T ⊢ ∀ x φ ( x ) . {\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.
Examples It is possible for a theory to be ω-incomplete, because the theory may have a model M {\displaystyle {\mathcal {M}}} with non-standard integers. In the model, we can have M ⊨ φ ( 0 ¯ ) , M ⊨ φ ( 1 ¯ ) , … {\displaystyle {\mathcal {M}}\models \varphi ({\bar {0}}),{\mathcal {M}}\models \varphi ({\bar {1}}),\dots } , but nevertheless have M ⊭ φ ( c ) {\displaystyle {\mathcal {M}}\not \models \varphi (c)} for a certain non-standard integer c {\displaystyle c} in the model. A standard weak example is Robinson arithmetic Q {\displaystyle Q} . It proves each instance of 0 + n ¯ = n ¯ {\displaystyle 0+{\bar {n}}={\bar {n}}} , while the universal sentence ∀ x ( 0 + x = x ) {\displaystyle \forall x(0+x=x)} lies beyond its theorems. This can be computably demonstrated by building a computable nonstandard model of Q {\displaystyle Q} , in which 0 + c ≠ 0 {\displaystyle 0+c\neq 0} for a non-standard integer element c {\displaystyle c} . Accordingly, Q {\displaystyle Q} is ω-incomplete. 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 φ ( n ¯ ) {\displaystyle \varphi ({\bar {n}})} to mean "If number n {\displaystyle n} is a valid proof in PA, then its conclusion is not 0 = 1 {\displaystyle 0=1} ". Then, P A ⊢ φ ( 0 ¯ ) , P A ⊢ φ ( 1 ¯ ) , … {\displaystyle PA\vdash \varphi ({\bar {0}}),PA\vdash \varphi ({\bar {1}}),\dots } , but P A ⊬ ∀ x φ ( x ) {\displaystyle PA\not \vdash \forall x\varphi (x)} by incompleteness. This argument applies to any recursively axiomatized theory that contains PA.
Relation to nearby notions ω-completeness is closely related to ω-consistency. A theory is ω-consistent when no formula ψ ( x ) {\displaystyle \psi (x)} yields both the existential sentence ∃ x ψ ( x ) {\displaystyle \exists x\,\psi (x)} and every numeral instance ¬ ψ ( n ¯ ) {\displaystyle \neg \psi ({\bar {n}})} . 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, A ( 0 ) , A ( 1 ) , A ( 2 ) , … ⇒ ∀ n A ( n ) . {\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.
See also Gödel's incompleteness theorems Peano arithmetic ω-consistency ω-rule
References
Further reading "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.