are provable. ω-consistency is a stronger property than consistency. Suppose that is a formula with one free variable . In order to be ω-consistent, the theory cannot prove both while also proving for each natural number .

The theory is assumed to be effective, which means that the set of axioms must be recursively enumerable. This means that it is theoretically possible to write a finite-length computer program that, if allowed