ω完全性

形式算术系统的一个性质。一个形式系统称为ω完全的，如果对任何公式A(x)，从A(0)，A(1)，A(2)，…都是可证的，就能得出xA(x)是可证的。反之，称这系统是ω不完全的。哥德尔不完全性定理证明了形式算术系统是ω不完全的，即在系统中有一个公式A(x)，使得A(0)，A(1)，…都是在系统中可证的，但公式xA(x)是不可证的。由于发现了一系统可以是ω不完全的，因此也揭示了一系统很可能是ω不协调的而未必是简单不协调的。