ω协调性

又称ω无矛盾性，形式(算术)系统的一个性质。一个形式系统称为ω协调的，如果没有一个公式A(x)使得下列各公式

A(0)，A(1)，…，A(n)，…；xA(x)

都在系统中可证。相反的情况，即：对每个自然数n，A(n)可证，又xA(x)也可证，称该系统为ω不协调的。

ω协调性概念的出现是与哥德尔不完全性定理相联系的。正是在形式算术系统是ω协调的假定下，哥德尔证明了它是不完全的。ω协调性是一种比简单协调性(即：不是每一个公式都是在系统中可证明的)更强的性质。ω协调性蕴涵简单协调性，因为如果A为任何一个不含自由变元的可证公式，则可把它写成“A(x)”，x为一变元，这时所有A(0)，A(1)，A(2)，…都是可证的(这些都简单地就是A)；因此如果这系统是ω协调的，则xA(x)就是一个不可证明的公式。一个形式系统可能是简单协调的而未必是ω协调的。