合式公式語言表達式

合式公式語言表達式，即形式系統中按一定規則構成的表達式。按照模型論中一種通行習慣，語言F中的合式公式定義如下：1.原子公式是合式公式； 2.若φ和ψ是合式公式，則(φ∧ψ)及(ᒣφ)是合式公式； 3.若φ是合式公式，而x是變元,則(ᗄx)φ是合式公式；4.有限次地套用1—3所得到的符號序列是合式公式。合式公式有時簡稱公式，如果一個公式φ中的自由變元都屬於集合x₁，x₂，…，xₑ，則φ也可以記為φ(x₁，x₂，…，xₑ)，不含量詞、自由變元的合式公式，分別稱為開公式和閉公式，後者又稱語句，例如R(x，y)為開公式，ᗄxR(x)是一個語句，由原子公式及聯結詞∧，∨，ᗄ，∃構成語句 稱為正語句。

如果一階邏輯中的恆真(恆假)公式，要求所有解釋I均滿足(弄假)該公式，而解釋I依賴一個非空個體集合D，又集合D可以是無窮集合，而集合D的“數目”也可以有無窮多個，因此，所謂公式的“所有”解釋，實際上是很難考慮的，這就使得一階邏輯中公式的恆真、恆假性的判定異常困難。Church和Turing分別於1936年獨立地證明了：對於一階邏輯，判定問題是不可解的，即不存在一個統一的算法A，該算法與謂詞公式無關，使得對一階邏輯中的任何謂詞公式G，A能夠在有限步內判定公式G的類型。

但是，一階邏輯是半可判定的，即如果謂詞公式G是恆真的，有算法在有限步內檢驗出G的恆真性。