一階邏輯

一階邏輯（也稱為謂詞邏輯，量化邏輯和一階謂詞微積分）是用於數學，哲學，語言學和計算機科學的形式系統的集合。一階邏輯使用非邏輯對像上的量化變量，並允許使用包含變量的句子，因此，一個人可以以“蘇格拉底是一個人”（例如“蘇格拉底”是一個人”的命題，而是形式中的表達式“存在” x是蘇格拉底，x是一個人”，其中“存在”是一個量詞，而x是變量。這將其與不使用量詞或關係的命題邏輯區分開。從這個意義上講，命題邏輯是一階邏輯的基礎。

關於某個主題的理論，例如集合理論，群體理論或形式的算術理論，通常是一階邏輯，以及指定的話語領域（量化變量範圍），從中有限的許多功能。該域本身，有限的許多謂詞在該域上定義，並且一組被認為符合它們的公理。 “理論”有時從更正式的意義上被理解為一組一階邏輯中的句子。

術語“一階”將一階邏輯與高階邏輯區分開，其中有謂詞或函數作為參數，或允許對謂詞，函數或兩者進行量化。在一階理論中，謂詞通常與集合相關聯。在解釋的高階理論中，謂詞可以解釋為一組集。

有許多用於一階邏輯的演繹系統都是合理的，即所有可證明的語句在所有模型中都是正確的，並且完整，即所有模型中所有符合的語句都是可證明的。儘管邏輯後果關係僅是半確定的，但在一階邏輯中證明的自動定理已經取得了很大進展。一階邏輯還滿足了幾種使其在證明理論中分析的金屬定理，例如löwenheim-skolem定理和緊湊定理。

一階邏輯是將數學形式化為公理的標準，並在數學基礎中進行了研究。 Peano算術和Zermelo – Fraenkel集理論分別是數字理論和集合理論的公理化理論，分為一階邏輯。但是，沒有一階理論能夠唯一地描述具有無限域的結構，例如自然數或真實線。可以完全描述這兩種結構的公理系統，即分類公理系統，可以在更強的邏輯（例如二階邏輯）中獲得。

一階邏輯的基礎是由Gottlob Frege和Charles Sanders Peirce獨立開發的。有關一階邏輯的歷史及其在正式邏輯中的主導作用，請參見JoséFerreirós（2001）。

介紹

儘管命題邏輯涉及簡單的聲明性命題，但一階邏輯還涵蓋了謂詞和量化。謂詞對話語領域中的實體或實體評估對或錯。

考慮一下兩個句子“蘇格拉底是哲學家”，而“柏拉圖是哲學家”。在命題邏輯中，這些句子本身被視為研究個體，例如，可以用諸如p和q之類的變量表示。它們不被視為謂詞的應用，例如在話語領域中的任何特定對象，而是將它們視為純粹是真實或錯誤的話語。但是，在一階邏輯中，這兩個句子可能會被帶回去，即某個單個或非邏輯對象具有屬性的陳述。在此示例中，兩個句子恰好具有某些個體的共同形式，在第一句話中，變量x的值是“蘇格拉底”，在第二句話中，它是“柏拉圖”。由於能夠談論非邏輯個體以及原始邏輯連接劑，因此一階邏輯包括命題邏輯。

諸如“ X是哲學家”之類的公式的真理取決於X所表示的對象，以及對謂詞“是哲學家”的解釋。因此，“ X是哲學家”僅具有真實或錯誤的確定真實價值，並且類似於句子片段。謂詞之間的關係可以使用邏輯連接劑說明。例如，一階公式“如果X是哲學家，那麼X是學者”，是“ X是哲學家”的有條件陳述，作為其假設，而“ X是學者”作為結論，這再次再次需要X的規範以具有確定的真實價值。

量詞可以應用於公式中的變量。例如，可以普遍量化上一個公式中的變量X ，例如，“對於每個x ，如果x是哲學家，則x是學者”。本句話中的通用量化器“為每個”中的每個量化者表示這樣的觀念：主張“如果x是哲學家，則X是學者“為X的所有選擇都保留。

句子的否定為“每個X ，如果X是哲學家，那麼X是學者”在邏輯上等同於句子“存在X ，使X是哲學家，而X不是學者”。存在的量詞“存在”表達了這樣一種觀念，即主張“ X是哲學家， X不是學者”，可以選擇X。

謂詞“是哲學家”，“是學者”每個都有一個變量。通常，謂詞可以採用幾個變量。在第一階句子“蘇格拉底是柏拉圖的老師”中，謂詞是“佔領”的老師。

一階公式的解釋（或模型）指定每個謂詞的含義，以及可以實例化變量的實體。這些實體構成了話語或宇宙的領域，通常需要這是一個非空的集合。例如，在與所有人組成的話語領域的解釋中正如柏拉圖見證的那樣。

一階邏輯有兩個關鍵部分。語法確定符號的有限序列是一階邏輯中形成良好的表達式，而語義則確定這些表達式背後的含義。

句法

與英語之類的天然語言不同，一階邏輯的語言是完全正式的，因此可以機械地確定給定表達式是否形成很好。形成良好的表達式有兩種關鍵類型：術語，直覺代表對象和公式，它們直觀地表達可能是真實或錯誤的語句。一階邏輯的術語和公式是符號字符串，所有符號一起構成語言的字母。

字母

與所有形式語言一樣，符號本身的性質超出了形式邏輯的範圍。它們通常被視為字母和標點符號。

將字母的符號劃分為邏輯符號是通常的，這些符號總是具有相同的含義和非邏輯符號，其含義隨解釋而變化。例如，邏輯符號總是表示“和”；它永遠不會被解釋為“或”，它由邏輯符號表示。但是，諸如Phil（X）之類的非邏輯性謂詞符號可以解釋為“ X是哲學家”，“ X是一個名叫Philip的人”，或者取決於手頭的解釋。

邏輯符號

邏輯符號是一組因作者而異，但通常包括以下內容：

• 量詞符號： ∀用於通用定量， ∃用於存在定量
• 邏輯連接：∧用於連接，∨用於脫節，→為含義，↔對於雙條件，以否定。一些作者使用CPQ代替→和EPQ代替↔，尤其是在用於其他目的的上下文中。此外，馬蹄⊃可以更換→；三桿可能會替換↔; tilde（〜），np或fp可以替換¬;雙欄或APQ可以替換∨;以及一個＆，＆kpq或中間點走為∧可能會替換∧，特別是出於技術原因而無法使用這些符號時。 （上述符號CPQ，EPQ，NP，APQ和KPQ用於波蘭符號。）
• 括號，支架和其他標點符號符號。此類符號的選擇因上下文而異。
• 一組無限的變量，通常在字母x ， y ， z ，...的末端以小寫字母表示。下標通常用於區分變量： x ₀ ， x ₁ ， x ₂ ，...。
• 平等符號（有時，身份符號） = （請參閱下面的§等及其公理）。

並非所有這些符號都是一階邏輯所必需的。量化器之一以及否定，連詞（或分離），變量，括號和平等就足夠了。

其他邏輯符號包括以下內容：

• 真實常數：t，v或⊤為“ true”和f，o或⊥ （for“ false”）（V和O來自波蘭符號）。沒有任何價值0的邏輯運算符，這兩個常數只能使用量詞表示。
• 其他邏輯連接器，例如Sheffer Stroke ，D PQ （NAND）和獨家或J PQ 。

非邏輯符號

非邏輯符號代表謂詞（關係），函數和常數。在所有目的中，都使用固定的無限符號符號來使用固定的無限符號：

• 對於每個整數n≥0 ，都有n- ary或n-位置的謂詞符號的集合。因為它們代表n個元素之間的關係，所以它們也稱為關係符號。對於每個Arity n ，它們都有無限的供應：

  p ⁿ ₀ ， p ⁿ ₁ ， p ⁿ ₂ ， p ⁿ ₃ ，...

• 對於每個整數n≥0 ，都有無限的n個函數符號：

  f ⁿ ₀ ， f ⁿ ₁ ， f ⁿ ₂ ， f ⁿ ₃ ，...

當從上下文中清除謂詞符號或函數符號時，通常會省略上標n 。

在這種傳統方法中，只有一種一階邏輯的語言。這種方法仍然很普遍，尤其是在哲學上的書籍中。

一種最新的做法是根據人們的想法使用不同的非邏輯符號。因此，有必要命名特定應用程序中使用的所有非邏輯符號的集合。此選擇是通過簽名做出的。

數學中的典型簽名是{1，×}或組的{×}，或{0、1， +，×，<}的{ 0、1 ， +，×，<}。非邏輯符號的數量沒有限制。簽名可以是空的，有限的或無限的，甚至是無數的。例如，在Löwenheim -Skolem定理的現代證明中發生了無數簽名。

儘管在某些情況下，簽名可能意味著如何解釋非邏輯符號，但對簽名中非邏輯符號的解釋是分開的（不一定是固定的）。簽名涉及語法而不是語義。

在這種方法中，每個非邏輯符號都是以下類型之一：

• 一個大於或等於0的價值（或arity ，參數數）的謂詞符號（或關係符號）通常用大寫字母（例如p ， q和r ）表示。例子：
  • 在p （ x ）中， p是價1的謂詞象徵。一種可能的解釋是“ x是一個人”。
  • 在q （ x ， y ）中， q是價值2的謂詞符號。可能的解釋包括“ x大於y ”，“ x是y的父親”。
  • 價值0的關係可以通過命題變量來識別，這可以代表任何陳述。 R的一種可能解釋是“蘇格拉底是一個人”。
• 一個函數符號，一定的價大於或等於0。這些符號通常用小寫的羅馬字母（例如f ， g和h）表示。例子：
  • F （ x ）可以解釋為“ X的父親”。在算術中，它可能代表“ -x”。在集合理論中，它可能代表“ X的功率集”。
  • 在算術中， g （ x ， y ）可以代表“ x + y ”。在集合理論中，它可能代表“ X和Y的聯合”。
  • 價值0的功能符號稱為恆定符號，通常在字母開始時以小寫字母表示，例如a ， b和c 。符號A可能代表蘇格拉底。在算術中，它可能代表0。在集合理論中，它可能代表空集。

通過簡單地將“自定義”簽名指定為由非邏輯符號的傳統序列組成，可以在現代方法中恢復傳統方法。

編隊規則

<index>             ::= "" 
                      | <index> "'"
<variable>          ::= "x" <index>
<constant>          ::= "c" <index>
<unary function>    ::= "f1" <index>
<binary function>   ::= "f2" <index>
<ternary function>  ::= "f3" <index>
<unary predicate>   ::= "p1" <index>
<binary predicate>  ::= "p2" <index>
<ternary predicate> ::= "p3" <index>
<term>              ::= <variable> 
                      | <constant> 
                      | <unary function> "(" <term> ")" 
                      | <binary function> "(" <term> "," <term> ")" 
                      | <ternary function> "(" <term> "," <term> "," <term> ")"
<atomic formula>    ::= "TRUE" 
                      | "FALSE"
                      | <term> "=" <term>
                      | <unary predicate> "(" <term> ")" 
                      | <binary predicate> "(" <term> "," <term> ")" 
                      | <ternary predicate> "(" <term> "," <term> "," <term> ")"
<formula>           ::= <atomic formula> 
                      | "¬" <formula>
                      | <formula> "∧" <formula>
                      | <formula> "∨" <formula>
                      | <formula> "⇒" <formula>
                      | <formula> "⇔" <formula>
                      | "(" <formula> ")"
                      | "∀" <variable> <formula>
                      | "∃" <variable> <formula>

編隊規則定義了一階邏輯的術語和公式。當將術語和公式表示為符號字符串時，這些規則可用於為術語和公式編寫形式的語法。這些規則通常是無上下文的（每個生產在左側都有一個符號），只是可以允許符號集成為無限的符號，並且可能有許多啟動符號，例如變量在術語中。

術語

該術語集由以下規則定義：

• 變量。任何變量符號都是一個術語。
• 功能。如果f是n -ary函數符號，而t ₁ ，...， t _n是術語，則f （ t ₁ ，...， t _n ）是一個術語。特別是，表示單個常數的符號是​​無效函數符號，因此是術語。

只有通過規則1和2的許多應用程序才能獲得的表達方式是術語。例如，沒有涉及謂詞符號的表達是一個術語。

公式

一組公式（也稱為良好的公式或WFF ）由以下規則定義：

1. 謂詞符號。如果p是n- ary謂詞符號，而t ₁ ，...， t _n是術語，則p （ t ₁ ，...， t _n ）是公式。
2. 平等。如果將平等符號視為邏輯的一部分，而t ₁和t ₂是術語，則t ₁ = t ₂是一個公式。
3. 否定。如果是公式，則是公式。
4. 二元連接。如果是公式，則（）是一個公式。類似的規則適用於其他二進制邏輯連接。
5. 量詞。如果是一個公式，而x是一個變量，則（對於所有x，保留），並且（存在x，因此）是公式。

僅通過規則1-5的許多應用程序才能獲得的表達方式是公式。從前兩個規則中獲得的公式稱為原子公式。

例如：

是一個公式，如果f是一個單一函數符號，則p一個單一的謂詞符號和q a三元謂詞符號。但是，儘管它是字母內的一系列符號，但不是一個公式。

括號在定義中的作用是確保只能以一種方式獲得任何公式 - 遵循歸納定義（即，每個公式都有一個獨特的解析樹。該屬性被稱為公式的獨特可讀性。公式中使用括號的地方有很多慣例。例如，一些作者使用結腸或完整的停止代替括號，或更改插入括號的位置。每個作者的特定定義必須伴隨著獨特的可讀性證明。

公式的定義不支持定義if-else函數ite(c, a, b)，其中“ c”是一種表示為公式的條件，如果c為true，則會返回“ A”，如果是false，則“ b”。這是因為謂詞和函數都只能接受項作為參數，但是第一個參數是公式。某些基於一階邏輯（例如SMT-LIB 2.0）的語言添加。

符號慣例

為了方便起見，已經制定了關於邏輯運營商的優先次數的慣例，以避免在某些情況下編寫括號。這些規則類似於算術中的操作順序。一個共同的慣例是：

• 首先評估
• 並接下來評估
• 接下來對量詞進行評估
• 最後評估。

此外，可以插入定義不需要的額外標點符號，以使公式易於閱讀。因此公式：

可能寫為：

在某些字段中，通常將infix符號用於二進制關係和函數，而不是上面定義的前綴符號。例如，在算術中，通常寫“ 2 + 2 = 4”，而不是“ =（ +（2,2），4）”。通常將infix符號中的公式視為前綴符號中相應公式的縮寫，請參見。也是術語結構與表示形式。

上面的定義使用infix符號，例如。一個不太常見的慣例是波蘭語符號，其中一個人在其論點前而不是在他們之間的論點上寫下。該約定是有利的，因為它允許所有標點符號符號被丟棄。因此，波蘭符號緊湊而優雅，但在實踐中很少使用，因為人類很難閱讀。在波蘭符號中，公式：

變成“∀X∀Y→Pfx-→PXQFYXZ”。

免費和綁定變量

在公式中，變量可能會自由發生或綁定（或兩者）。該概念的一種形式化是由於quine引起的，首先定義了變量發生的概念，然後是變量發生的事件是免費的還是綁定的，然後是可變符號總體上是免費的還是綁定的。為了區分相同的符號x的不同出現，公式φ中的每次出現變量符號x都用φ的初始子字符串識別到符號x的上述實例的初始子字符串，然後出現符號。如果X的發生在至少一個或一個。最後，x在φ中的所有出現都綁定在φ中。PPP.142--143

直觀地，如果在公式中沒有量化的情況下，一個變量符號是免費的： ^pp.142---143在∀y p （ x ， y ）中，可變x的唯一出現是自由的，而y的b綁定。公式中的自由和綁定變量發生的歸納定義如下。

原子公式

如果φ是原子公式，則x在φ中自由出現，並且僅當x出現在φ中時。此外，在任何原子公式中都沒有結合變量。

否定

x在φ中僅出現在φ中時， x在€ φ中自由出現。 x發生在€ φ時，僅當x發生在φ中

二元連接

x在（ φ → ψ ）中自由出現，並且僅當x在φ或ψ中自由出現時。 x發生在（ φ → ψ ）中，並且僅當x發生在φ或ψ中時。同一規則適用於→→。

量詞

x在yφ中自由出現，並且僅當x在φ中自由出現並且x與y不同時。同樣， x發生在∀yφ時，並且僅當x是y或x發生在φ中時。相同的規則與∃代替∀ 。

例如，在∀x y （ p （ x ）→ q （ x ， f （ x ）， z ））中， x和y僅發生綁定， z僅出現，而w也不發生，因為它不在公式。

公式的自由和綁定變量不必脫節集：在公式p （ x ）→ ∀x q （ x ）中， x的第一次出現，作為p的參數，是免費的，而第二個是q的參數。 ，是綁定的。

一階邏輯中沒有自由變量出現的公式稱為一階句子。這些是在解釋下具有明確定義的真實價值的公式。例如，諸如phil（ x ）的公式是否為true必須取決於x所代表的。但是，在給定的解釋中，句∃x phil（ x ）將是真實的。

示例：訂購的阿貝利亞人群

在數學中，有序的Abelian組的語言具有一個常數符號0，一個單一函數符號 - ，一個二進制函數符號 +和一個二進制關係符號≤。然後：

• 表達式 +（ x ， y ）和 +（ x ， +（ y ， - （ z ）））是術語。這些通常寫為x + y和x + y - z 。
• 表達式 +（ x ， y ）= 0和≤（ +（ x ， +（ y ， - （ z ））））， +（ x ， y ））是原子公式。這些通常寫為x + y = 0和x + y - z≤x + y 。
• 該表達式是一個公式，通常寫為此公式具有一個自由變量，z。

有序的阿貝爾組的公理可以表示為語言中的一組句子。例如，公理表明該組通常是寫作的

語義

一階語言的解釋將該語言中的每個非邏輯符號（謂詞符號，函數符號或常數符號）分配。它還確定了一個指定量詞範圍的話語領域。結果是為每個項分配了一個代表的對象，每個謂詞被分配一個對象的屬性，每個句子都分配了一個真實值。這樣，一種解釋為語言的術語，謂詞和公式提供了語義含義。對形式語言的解釋的研究稱為正式語義。接下來是對一階邏輯的標準語義或塔斯基語義的描述。 （也可以為一階邏輯定義遊戲語義，但是除了需要選擇的公理外，遊戲語義與Tarskian Sentics的一階邏輯一致，因此在這裡不會詳細闡述遊戲語義。）

一階結構

指定解釋的最常見方法（尤其是在數學中）是指定結構（也稱為模型；見下文）。該結構由話語D的域和解釋函數I組成，I將非邏輯符號映射到謂詞，函數和常數。

話語d的領域是某種非空的“對象”集。直觀地，考慮到一種解釋，一階公式變成了有關這些對象的陳述。例如，說明謂詞p為真p的某些對象的存在（或更確切地說，通過解釋分配給謂詞符號p的謂詞是正確的）。例如，一個人可以用D作為整數。

非邏輯符號解釋如下：

• n- ary函數符號的解釋是從dn到D的函數。爭論。換句話說，符號F與此解釋相關聯是添加的。

• 對常數符號（ARITY 0的函數符號）的解釋是D0的函數（唯一成員是空元組的集合）d，可以簡單地用D中的對象識別。例如，解釋可能可以將值分配給常數符號。

• N- Ary謂詞符號的解釋是D元素的一組，給出了謂詞為真的參數。例如，對二進制謂詞符號p的解釋可能是成對的整數對，使第一個符號小於第二個整數。根據這種解釋，如果其第一個論點小於其第二個論點，則謂詞P將是正確的。同等地，謂詞符號可以從DN到。

真實價值觀的評估

在給定解釋和一個可變分配μ的情況下，公式評估為true或fals，該公式將話語領域元素與每個變量相關聯的變量分配μ。需要變量分配的原因是給具有自由變量的公式提供含義，例如。該公式的真實價值會根據x和y表示的值而變化。

首先，可變分配μ可以擴展到語言的所有術語，結果每個術語映射到話語域的一個元素。以下規則用於完成此任務：

• 變量。每個變量x評估為μ （ x ）
• 功能。給定已評估到話語領域元素的術語和n-ary函數符號f，該術語評估為術語。

接下來，為每個公式分配一個真實價值。用於進行此任務的歸納定義稱為T-Schema 。

• 原子公式（1）。公式是關聯的值，取決於術語的評估和解釋的評估在何處，通過假設為子集的術語和解釋。
• 原子公式（2）。 if並評估話語域的相同對象（請參見下面的平等部分）。
• 邏輯連接。如所討論的結締組織的真實表，對形式，形式等的公式進行了評估，如命題邏輯中。
• 存在量詞。根據m，一個公式是正確的，如果對x評估的變量進行了評估，並且根據解釋m和變量分配是正確的。此形式定義捕獲了當且僅當有一種方法選擇x值以使φ（x）滿足x值時。
• 通用量詞。一個公式根據m為true，如果φ（x）對於由解釋M組成的每個對組成的對（x）都是正確的，而某些可變分配的分配最多與x的值不同。如果每個可能選擇x的值會導致φ（x）是正確的，那麼這將捕捉到真實的想法。

如果公式不包含自由變量，則句子也是如此，則初始變量分配不會影響其真實價值。換句話說，根據m的句子，並且僅當根據m和其他所有變量分配是正確時，句子是正確的。

定義不依賴可變分配功能的真實價值的第二種常見方法。取而代之的是，給定解釋m ，首先將簽名添加到一個常數符號的集合中，其中一個用於M中的話語域的每個元素；說對於域中的每個d，常數符號c _d是固定的。解釋是擴展的，因此每個新常數符號都被分配給其域的相應元素。現在，一個人句法定義了真實的句法，如下所示：

• 存在量詞（替代量）。如果在話語的領域中有一些d，則根據m為true。這是替換CD代替每次自由出現X中的結果。
• 通用量詞（替代量）。根據M，根據M的每個D，根據M的每個D是正確的，則是正確的。

這種替代方法為所有句子提供了與通過變量分配的方法完全相同的真實價值。

有效性，滿意度和邏輯後果

如果一個句子φ在給定的解釋m下評估為true，則說m滿足φ。這是表示。如果有某種解釋，則可以滿足句子。這與模型理論的符號有些不同，其中表示模型中的性能，即“在s域中有一個合適的值分配到可變符號”。

具有自由變量的公式的滿意度更加複雜，因為解釋本身並不能決定這種公式的真實價值。最常見的慣例是，如果公式φ仍然是真實的，則具有自由變量的公式φ可以通過解釋來滿足。 。這與說一個公式φ在滿足其通用閉合時得到滿足的效果相同。

公式在邏輯上是有效的（或簡單地有效），如果在每個解釋中都是正確的。這些公式在命題邏輯中起著類似於重言式的作用。

公式φ是公式ψ的邏輯結果，如果每個使ψtrue的解釋也使得φ成真。在這種情況下，有人說φ在邏輯上被ψ暗示。

代數

一階邏輯語義的另一種方法通過抽象代數進行。這種方法概括了命題邏輯的Lindenbaum – Tarski代數。從一階邏輯中消除量化變量的三種方法不涉及用其他可變綁定術語運算符替換量詞：

• Alfred Tarski及其同事的圓柱代數；
• 保羅·霍爾莫斯（ Paul Halmos）的多核代數；
• 謂詞函子邏輯，主要是由於Willard Quine 。

這些代數都是正確擴展兩元素布爾代數的晶格。

Tarski and Givant（1987）表明，沒有原子句子的一階邏輯片段在三個以上的量詞的範圍內具有與關係代數相同的表達能力。該片段引起了極大的興趣，因為它足以滿足Peano算術和大多數公理設置理論，包括規範的ZFC 。他們還證明，具有原始有序對的一階邏輯等於具有兩個有序的對投影函數的關係代數。

一階理論，模型和基礎類

特定簽名的一階理論是一組公理，它們是由該簽名的符號組成的句子。公理集通常是有限的或遞歸枚舉的，在這種情況下，理論稱為有效。一些作者要求理論還包括公理的所有邏輯後果。公理被認為是在理論中含有的，並且可以得出該理論中所持的其他句子。

滿足給定理論中所有句子的一階結構被認為是理論的模型。小學類是滿足特定理論的所有結構的集合。這些課程是模型理論的主要研究主題。

許多理論都有預期的解釋，在研究理論時會牢記某種模型。例如，對Peano算術的預期解釋包括通常的自然數字，其通常的操作。但是，Löwenheim-Skolem定理表明，大多數一階理論也將具有其他非標準模型。

如果無法證明理論的公理矛盾，理論是一致的。如果對於簽名中的每個公式，該公式或否定是該理論公理的邏輯結果，那麼理論是完整的。戈德爾的不完整定理表明，包括自然數字理論的足夠部分的有效一階理論永遠不可能是一致的和完整的。

空域

上面的定義要求任何解釋的話語領域都必須是非空的。有設置，例如包容性邏輯，其中允許空域。此外，如果一類代數結構包含一個空結構（例如，有一個空的poset ），則如果允許空域或從類中刪除空結構，則只有一類在一階邏輯中是一個基本類。

但是，空地有幾個困難，但是：

• 僅當需要進行非空的領域時，許多常見的推論規則才有效。一個示例是說明x不是自由變量時的規則。該規則用於將公式放入Prenex正常形式中，在非空域中是合理的，但是如果允許空域，則不合時宜。
• 使用可變分配功能的解釋中的真理的定義不能與空域一起使用，因為沒有變量分配函數的範圍為空。 （同樣，一個人不能將解釋分配給常數符號。）此真相定義要求在可以定義的真實值之前，必須選擇一個變量分配函數（上面的μ）。然後，句子的真實價值被定義為任何變量分配下的真實價值，並且證明該真實價值並不取決於選擇哪個分配。如果根本沒有作業功能，此技術將不起作用。必須更改它以容納空域。

因此，當允許空域時，通常必須將其視為特殊情況。但是，大多數作者只是根據定義排除空白領域。

演繹系統

演繹系統用於以純粹的句法來證明一個公式是另一個公式的邏輯結果。有許多用於一階邏輯的系統，包括希爾伯特風格的演繹系統，自然扣除，序列微積分， tableaux方法和分辨率。這些共同的屬性是扣除是有限的句法對象；該對象的格式及其構造方式差異很大。這些有限扣除本身通常被稱為證明理論中的派生。它們通常也被稱為證明，但與自然語言數學證明不同。

如果系統可以在系統中得出的任何公式在邏輯上有效，則演繹系統是合理的。相反，如果每個邏輯上有效的公式都是可得出的，則具有演繹系統是完整的。本文討論的所有系統既有聲音又完整。他們還分享了可以有效驗證據稱有效扣除實際上是扣除的財產。這種扣除系統稱為有效。

演繹系統的關鍵特性是它們純粹是句法，因此可以在不考慮任何解釋的情況下驗證推導。因此，無論該解釋是關於數學，經濟學還是其他領域，無論是在對語言的每種可能解釋中都是正確的。

通常，一階邏輯中的邏輯後果僅是半確定的：如果句子在邏輯上暗示句子b，則可以發現（例如，通過搜索證明直到找到一個證明，使用一些有效，聲音，完整的證明系統）。但是，如果a在邏輯上不暗示b，這並不意味著邏輯上意味著B的否定。沒有有效的程序，即給定公式A和B，總是正確地決定是否邏輯上暗示B。

推理規則

一條推論規定，如果以特定屬性為假設的特定公式（或一組公式），則可以得出另一個特定的公式（或公式集）作為結論。如果規則在任何解釋滿足假設時，該規則都保留了有效性，則該規則是合理的（或保留真理）。

例如，一個共同的推論規則是替代規則。如果t是一個項，並且φ是可能包含變量x的公式，則φ[ t / x ]是在φ中替換x的所有自由實例的結果。替代規則指出，對於任何φ和任何術語t ，都可以從φ結論φ[ t / x ]，前提是在替換過程中t的自由變量沒有結合。 （如果t的某些自由變量被綁定，那麼要替換x ，首先有必要將φ的結合變量與t的自由變量不同。）

要了解為什麼需要對界變量的限制，請考慮在算術的（0,1，+，×，=）的簽名中給出的邏輯有效公式φ。如果t是術語“ x + 1”，則公式φ[t/y]為，這在許多解釋中都是錯誤的。問題在於，t的自由變量在替換過程中被綁定。可以通過將φ的界變量x重命名為Z（例如Z）來獲得預期的替換，以便替換後的公式是邏輯上有效的。

替代規則證明了推論規則的幾個共同方面。它完全是句法；可以判斷它是否正確應用，而無需上訴任何解釋。它具有（句法定義）何時可以應用，必須尊重它以保留派生的正確性。此外，就像通常情況下一樣，這些限制是必要的，因為在推斷規則中涉及的公式的句法操縱過程中，自由變量和綁定變量之間的相互作用。

希爾伯特風格的系統和自然扣除

希爾伯特風格的演繹系統中的扣除是公式的列表，每個公式都是邏輯公理，這是一種假設，該假設已被假定為手頭的推導或通過推論從先前的公式遵循。邏輯公理由邏輯上有效公式的幾個公理模式組成；這些包括大量的命題邏輯。推理規則可以操縱量詞。典型的希爾伯特風格系統具有少量的推理規則，以及邏輯公理的幾個無限模式。通常，只有實物席和普遍的概括作為推理規則。

自然扣除系統類似於希爾伯特風格的系統，因為扣除是公式的有限列表。但是，自然扣除系統沒有邏輯公理。他們通過添加其他推理規則來彌補，這些規則可用於操縱證明公式中的邏輯連接劑。

依次的演算

開發了序列的微積分來研究自然扣除系統的性質。它不是一次使用一個公式，而是使用順序，這是形式的表達式：

其中a1，...，an，b1，...，bk是公式，旋轉門符號用作標點符號，將兩半分開。直覺上，一個序列表達了暗示的想法。

tableaux方法

與剛剛描述的方法不同，Tableaux方法中的派生不是公式的列表。相反，推導是公式的樹。為了證明A公式A是可證明的，Tableaux方法試圖證明A的否定是不滿意的。派生的樹的根源；樹枝以一種反映公式結構的方式。例如，要證明這不滿意，就必須表明C和D每個人都不令人滿意；這對應於帶有父母和孩子C和D的樹中的一個分支點。

解決

分辨率規則是一個單一的推論規則，與統一一起，對於一階邏輯而言，它是合理的且完整的。與Tableaux方法一樣，通過證明該公式的否定不令人滿意來證明公式。分辨率通常用於自動定理證明。

該分辨率方法僅適用於原子公式的分析公式；必須首先通過Skolemization將任意公式轉換為此形式。決議規則指出，從假設和結論可以得出。

可證明的身份

可以證明許多身份，這些身份在特定公式之間建立了等價。這些身份可以通過將量詞移動到其他連接劑中，可以重新安排公式，並且可用於將公式以正常形式放置。一些可證明的身份包括：

（在哪裡不得自由發生）

（在哪裡不得自由發生）

平等及其公理

在一階邏輯中使用平等（或身份）有幾種不同的約定。最常見的慣例，稱為具有平等的一階邏輯，包括等效符號作為原始邏輯符號，始終將其解釋為話語領域成員之間的真實平等關係，因此“兩個”給定的成員是同一會員。這種方法還為所採用的演繹系統增加了有關平等的某些公理。這些平等公理是：

• 反射性。對於每個變量x ， x = x 。
• 替換功能。對於所有變量x和y ，以及任何函數符號f ，

  x = y → f （...， x ，...）= f （...， y ，...）。

• 替換公式。對於任何變量x和y和任何公式φ（ x ），如果通過用y替換任何數量的x中x的自由出現來獲得φ'，則這些x在用y中佔x，以便這些保持y的自由出現y ，則：

  x = y →（φ→φ'）。

這些是公理模式，每個模式都指定了無限的公理集。第三個架構被稱為萊布尼茲定律，“替代性原則”，“同卵形的不可分性性”或“替代特性”。涉及函數符號F的第二個模式是（等效於）第三個模式的特殊情況，使用公式：

x = y →（ f （...， x ，...）= z → f （...， y ，...）= z ）。

平等的許多其他特性是上述公理的後果，例如：

• 對稱。如果x = y，則y = x 。
• 傳遞性。如果x = y和y = z，則x = z 。

一階邏輯沒有平等

另一種方法將平等關係視為非邏輯符號。該慣例稱為一階邏輯，沒有平等。如果在簽名中包括平等關係，則現在必須將平等公理添加到所考慮的理論中，而不是被視為邏輯規則。這種方法與平等邏輯之間的主要區別在於，解釋現在可以將兩個不同的個體解釋為“平等”（儘管根據萊布尼茲定律，這些人將在任何解釋下都完全滿足相同的公式） 。也就是說，現在可以通過對話語領域的任意等價關係來解釋平等關係，而這種對等關係在解釋的功能和關係方面是一致的。

當遵循第二個慣例時，術語正常模型被用來指的是一種解釋，其中沒有不同的個體a和b滿足a = b 。在具有平等的一階邏輯中，只考慮了正常模型，因此除了正常模型以外，模型沒有其他術語。當研究沒有平等的一階邏輯時，有必要修改諸如löwenheim-Skolem定理之類的結果陳述，以便僅考慮正常模型。

一階邏輯通常是在二階算術和其他高階理論的背景下使用的，其中通常省略自然數集之間的平等關係。

在理論中定義平等

如果一種理論具有滿足反思性和萊布尼茲定律的二元公式A （ x ， y ），則該理論據說具有平等，或者是具有平等的理論。該理論可能沒有上述模式的所有實例作為公理，而是作為可衍生的定理。例如，在沒有函數符號和有限關係的理論中，可以通過將兩個術語s和t定義為平等來定義平等，如果通過將s更改為t到t中的s不變，則可以平等任何論點。

一些理論允許其他臨時定義平等的定義：

• 在一個關係符號≤的部分階階的理論中，可以將s = t定義為s≤t∧t≤s的縮寫。
• 在具有一個關係∈的集合理論中，一個人可以將s = t定義為∀x（s∈X↔T∈X）的縮寫（x∈Ss↔x∈T）。然後，平等的定義會自動滿足平等的公理。在這種情況下，應該替換通常的擴展性公理，可以用替代公式表示，該公理說，如果設置x和y具有相同的元素，則它們也屬於相同的集合。

金屬特性

使用一階邏輯而不是高階邏輯的一種動機是，一階邏輯具有許多更強邏輯沒有的金屬屬性。這些結果涉及一階邏輯本身的一般特性，而不是單個理論的特性。它們為建設一階理論的建設提供了基本工具。

完整性和不確定性

庫爾特·戈德爾（KurtGödel）在1929年證明的戈德爾（Gödel）的完整定理表明，有一個合理的，完整的，有效的推力系統用於一階邏輯，因此有限的可預訂性捕獲了一階邏輯後果關係。天真地，公式φ從邏輯上暗示公式ψ取決於每個模型的陳述。通常，這些模型將具有任意較大的基數性，因此無法通過檢查每個模型來有效驗證邏輯後果。但是，可以列舉所有有限的推導，並從φ中搜索ψ的派生。如果φ在邏輯上暗示了φ，則最終將找到這樣的派生。因此，一階邏輯後果是可以半完成的：可以對所有句子（φ，ψ）進行有效枚舉，使ψ是φ的邏輯結果。

與命題邏輯不同，一階邏輯是不確定的（儘管可以半確定），前提是該語言至少具有至少有2個謂詞（除了平等）。這意味著沒有決策過程可以確定任意公式在邏輯上是否有效。這一結果分別由1936年和1937年由Alonzo Church和Alan Turing獨立建立，對David Hilbert和Wilhelm Ackermann在1928年提出的Entscheidungsproblem構成了負面答案。他們的證明證明了他們的證據表明了對第一名決策問題的連接，這是第一名的決策問題之間的聯繫。訂購邏輯和停止問題的不可分析性。

系統比完整的一階邏輯要弱，邏輯後果關係是可以決定的。其中包括命題邏輯和monadic謂詞邏輯，該邏輯僅限於一階邏輯，僅限於一元謂詞符號和無函數符號。具有可決定性符號的其他邏輯是一階邏輯的守衛片段，以及兩變量的邏輯。伯爾尼 - 塞弗克爾的一階公式類也是可決定的。描述邏輯框架中還研究了一階邏輯的可決定子集。

Löwenheim– Skolem定理

löwenheim– Skolem定理表明，如果基數λ的一階理論具有無限模型，則它具有大於或等於λ的每個無限基數的模型。在模型理論中最早的結果之一，這意味著不可能在具有可計數的簽名的一階語言中表徵可數字或不可實數。也就是說，沒有一階公式φ（ x ），因此任意結構M滿足M時，並且僅當M的話語域是可計數的（或在第二種情況下是無數的）。

Löwenheim– Skolem定理意味著無限結構不能在一階邏輯中被絕對地進行公理。例如，沒有一階理論的唯一模型是真實的線：任何具有無限模型的一階理論也具有大於連續體的基數模型。由於實際線是無限的，因此某些非標準模型也滿足了真實線所滿足的任何理論。當Löwenheim– Skolem定理應用於一階集理論時，非直覺後果被稱為Skolem的悖論。

緊湊定理

緊湊性定理指出，當且僅當其每個有限子集都有模型時，一組一階句子具有模型。這意味著，如果公式是無限一組一階公理的邏輯結果，那麼這是這些公理數量有限數量的邏輯結果。該定理首先是由庫爾特·戈德爾（KurtGödel）證明，這是由於完整定理的結果，但隨著時間的流逝，已獲得了許多其他證據。它是模型理論中的中心工具，它提供了一種構建模型的基本方法。

緊湊型定理對一階結構的集合是基本類別具有限制效果。例如，緊湊度定理意味著任何具有任意大型有限模型的理論都有無限模型。因此，所有有限圖的類都不是基本類（對於許多其他代數結構，也是相同的）。

緊湊型定理也暗示了一階邏輯的更微妙的局限性。例如，在計算機科學中，許多情況都可以建模為有向狀態的狀態圖（節點）和連接（有向邊）。驗證這樣的系統可能需要表明從任何“良好”狀態都無法達到“不良”狀態。因此，人們試圖確定良好狀態和壞狀態是否位於圖的不同連接組件中。但是，緊湊型定理可以用來證明連接的圖不是一階邏輯中的基本類，並且在圖的邏輯中沒有一階邏輯的公式φ（x，y）表達想法是有從x到y的路徑。但是，連接性可以用二階邏輯表示，但不僅可以使用存在的集合量，也可以表現出緊湊性。

Lindström的定理

Perlindström表明，剛剛討論的金屬屬性實際上表徵了一階邏輯，從某種意義上說，也沒有更強大的邏輯也可以具有這些特性（Ebbinghaus and Flum 1994，第XIII章）。 Lindström定義了一類抽象的邏輯系統，以及對該類成員的相對強度的嚴格定義。他為這種類型的系統建立了兩個定理：

• 滿足Lindström定義的邏輯系統，其中包含一階邏輯並滿足Löwenheim-Skolem定理和緊湊定理的邏輯系統，必須等同於一階邏輯。
• 滿足Lindström定義的邏輯系統，具有半確定的邏輯後果關係並滿足Löwenheim-Skolem定理必須等同於一階邏輯。

限制

儘管一階邏輯足以使大部分數學形式化，並且通常用於計算機科學和其他領域，但它具有一定的局限性。這些包括對其表達性的局限性和可以描述的自然語言片段的局限性。

例如，一階邏輯是不可確定的，這意味著不可能有聲音，完整和終止的決策算法。這導致研究了有趣的可定義片段，例如具有兩個變量和計數量詞的C2：一階邏輯和。

表現力

löwenheim– Skolem定理表明，如果一階理論具有任何無限模型，那麼它具有每種基數的無限模型。特別是，沒有具有無限模型的一階理論可以分類。因此，沒有一階理論，其唯一的模型將自然數作為其域名集，或者其唯一的模型將實際數字集作為其域。一階邏輯的許多擴展，包括無限邏輯和高階邏輯，具有更大的表現力，因為它們確實允許自然數或實數的分類公理化。然而，這種表現力的成本是： lindström的定理，緊湊的定理和向下的löwenheim-skolem定理在任何邏輯上都不能比一階更強。

正式化天然語言

一階邏輯能夠以自然語言形式化許多簡單的量詞結構，例如“居住在澳大利亞的每個人”。因此，一階邏輯被用作知識表示語言的基礎，例如fo（。） 。

儘管如此，自然語言的複雜特徵仍無法用一階邏輯表達。 “任何作為用於分析自然語言的工具的邏輯系統都需要比一階謂詞邏輯更豐富的結構”。

限制，擴展和變化

一階邏輯有很多變化。其中一些並不十分是因為它們僅在不影響語義的情況下改變符號。其他人則通過通過其他量詞或其他新的邏輯符號擴展語義來更大程度地改變表達能力。例如，無限邏輯允許無限規模的公式，而模態邏輯增加了可能性和必要性的符號。

限制語言

一階邏輯可以用比上面描述的邏輯符號少的語言進行研究：

• 因為可以表示為，並且可以表示為兩個量詞中的任何一個，並且可以刪除。
• 由於可以表示為並可以表示為或可以刪除​​。換句話說，擁有和或作為唯一的邏輯連接是足夠的。
• 同樣，僅具有邏輯連接劑，或者僅具有Sheffer Stroke（NAND）或Peirce Arrow（NOR）操作員也足夠。
• 可以完全避免函數符號和恆定符號，以適當的方式通過謂詞符號重寫它們。例如，而不是使用常數符號，可以使用謂詞（解釋為）並替換所有謂詞。類似的函數將被解釋為。此更改需要在手頭的理論中添加其他公理，以便對所使用的謂詞符號的解釋具有正確的語義。

諸如此類的限制是減少演繹系統中推理規則或公理模式數量的技術，從而導致較短的金屬結果證明。限制的成本在於，在手頭正式系統中表達自然語言陳述變得更加困難，因為自然語言語句中使用的邏輯連接劑必須用其（更長）的定義代替，以限制收集邏輯連接。同樣，有限系統中的派生可能比包括其他連接器的系統中的推導更長。因此，在正式系統中的易用性與證明正式系統的結果的易用性之間存在權衡。

還可以在足夠表達的理論中限制功能符號和謂詞符號的敏銳度。原則上，可以完全用大於2的Arity功能分配，而在包括配對函數的理論中，Arity的謂詞大於1。這是Arity 2的函數，它採用了域的成對元素，並返回包含它們的有序對。具有兩個ARITY 2的謂詞符號也足以將投影功能從有序對到其組件定義。無論哪種情況，都必須滿足配對函數的天然公理及其投影。

多數邏輯

普通的一階解釋具有所有量詞範圍的話語領域。多組的一階邏輯允許變量具有不同的域，這些邏輯具有不同的域。這也稱為鍵入的一階邏輯，並且類型（如數據類型）與一階類型理論不同。二階算術研究經常使用多組的一階邏輯。

當理論中只有許多有限的方式時，可以將多組的一階邏輯還原為單排的一階邏輯。一個人介紹了單排理論中每種理論中每種類型的一個謂詞符號，並添加了一個公理，說這些一般的謂詞將話語的領域分開。例如，如果有兩種，則添加了謂詞符號和公理：

.

然後，滿足的元素被認為是第一種元素，而滿足的元素是第二種元素。一個人可以使用相應的謂詞符號來量化每種類型的量子，以限制定量範圍。例如，要說有一個滿足公式φ（x）的第一種元素，一個人寫道：

.

其他量化符

可以將其他量化器添加到一階邏輯中。

• 有時可以說“ P （ x ）完全持有一個X ”，這可以表示為∃！ X P （ X ） 。該符號（稱為唯一性定量）可以縮寫為諸如∃x （ p （ x ） ∧∀y （ p （ y ）→（ x = y ）））的公式。
• 帶有額外量化器的一階邏輯具有新的量詞qx ，...，含義“有很多x ，所以...”。另請參閱喬治·布洛斯（George Boolos）等人的分支量詞和複數量詞。
• 有限的量詞通常用於集合理論或算術研究。

無限邏輯

無限邏輯允許無限長的句子。例如，一個人可能允許無限多個公式的結合或脫節，或對無限多個變量進行定量。無限長的句子出現在數學領域，包括拓撲和模型理論。

無限邏輯概括了一階邏輯，以允許無限長度的公式。公式可以成為無限的最常見方式是通過無限的結合和析取。但是，還可以允許允許函數和關係符號具有無限的敏銳度，或者量詞可以綁定無限多個變量的通用簽名。因為無限公式不能由有限的字符串表示，所以有必要選擇其他公式的代表。在這種情況下，通常的表示是一棵樹。因此，從本質上講，公式是用他們的解析樹來識別的，而不是解析字符串。

最常見的無限邏輯是表示Lαβ _，其中α和β分別是基數或符號∞。在此表示法中，_普通的一階邏輯為LΩΩ 。在邏輯L∞Ω中，構建公式時允許任意連詞或分離_，並且有無限的變量供應。更一般而言，允許與小於κ組成的結合或分離_{的邏輯稱為LκΩ} 。例如， LΩ1Ω_允許可計數的結合和析取。

LκΩ公式中的一組自由變量嚴格地比κ具有任何基數，但是當一個公式以另一個量子為_單位的子形式出現時，只有有限的許多可以在任何量詞的範圍內。在其他無限邏輯中，副構件可能處於無限多個量詞的範圍。例如，在Lκ∞中，單個通用或存在的量詞可以同時任意結合_許多變量。同樣_，邏輯Lκλ允許在少於λ變量以及大小小於κ的結合和析取。

非古典和模態邏輯

• 直覺的一階邏輯使用直覺，而不是經典的推理；例如，€不必等於φ和€x.φφ通常不等於∃x.imφ。
• 一階模態邏輯允許人們描述我們所居住的其他可能的世界以及這個偶然的真實世界。在某些版本中，可能的世界一組取決於一個可能的世界居住。模態邏輯具有額外的模態算子，其含義可以非正式地表徵為“例如，在所有可能的世界中有必要”（在所有可能的世界中）和“可能在某些可能的世界中） 。使用標準的一階邏輯，我們有一個域，每個謂詞都會分配一個擴展。使用一階模態邏輯，我們具有一個域函數，可以為每個可能的世界分配其自身域，因此每個謂詞僅獲得相對於這些可能的世界的擴展。這使我們能夠建模案例，例如，亞歷克斯（Alex）是哲學家，但可能是數學家，並且可能根本不存在。在第一個可能的世界中， p （ a ）是正確的，在第二個p （ a ）中是錯誤的，在第三個可能的世界中，域中根本沒有一個。
• 一階模糊邏輯是命題模糊邏輯的一階擴展，而不是經典的命題計算。

FIXPOINT邏輯

FixPoint Logic通過在正算子的最小固定點下添加閉合來擴展一階邏輯。

高階邏輯

一階邏輯的特徵是可以量化個體，但不能進行謂詞。因此

是合法的一階公式，但

不是，在大多數一階邏輯的形式上。二階邏輯通過添加後一種量化來擴展一階邏輯。其他高階邏輯允許對比二階邏輯允許更高類型的量化。這些較高的類型包括關係之間的關係，從關係到關係之間的關係和其他高型對象之間的關係。因此，一階邏輯中的“第一”描述了可以量化的對象的類型。

與僅研究一種語義的一階邏輯不同，二階邏輯有幾種可能的語義。最常用的用於二階和高階邏輯的語義被稱為完整語義。這些量化器的其他量詞和完整語義的組合使高階邏輯比一階邏輯更強。特別是，二階和高階邏輯的（語義）邏輯後果關係是無法半決定的。在完整的語義下，沒有有效的二階邏輯推論系統。

具有完整語義的二階邏輯比一階邏輯更具表現力。例如，可以在二階邏輯中創建公理系統，以獨特地表徵自然數和實際線路。這種表現力的成本在於，二階和高階邏輯比一階邏輯具有更少的吸引力金屬特性。例如，當通過完整語義概括到高階邏輯時，löwenheim– skolem定理和一階邏輯的緊湊定理會變得錯誤。

自動定理證明和形式的方法

自動定理證明是指搜索和查找數學定理的推導（正式證明）的計算機程序的開發。尋找推導是一項艱鉅的任務，因為搜索空間可能很大。從理論上來說，詳盡的搜索是可能的，但對於許多數學感興趣的系統，在計算上是不可行的。因此，開發了複雜的啟發式功能，以試圖在較少的時間內找到比盲目搜索更少的推導。

自動證明驗證的相關領域使用計算機程序來檢查人類創建的證明是否正確。與復雜的自動定理拋棄不同，驗證系統可能足夠小，以至於可以通過自動軟件驗證手動檢查其正確性。需要對證明驗證者進行這種驗證，以確保將標記為“正確”的任何推導實際上都是正確的。

某些證明驗證符，例如metamath ，堅持將完全推導作為輸入。其他，例如Mizar和Isabelle ，請採用一個格式良好的證明草圖（可能仍然很長且詳細），並通過進行簡單的證明搜索或應用已知的決策程序來填充缺失的作品：然後由結果驗證由小核心“內核”。許多這樣的系統主要用於人類數學家的互動使用：這些系統被稱為證明助手。他們還可以使用比一階邏輯更強的形式邏輯，例如類型理論。由於對一階外扣系統中任何非平凡結果的全面推導將非常長，因此人類寫作的延長通常是形式化為一系列引理，為此可以單獨構建衍生作用。

自動定理掠奪者還用於在計算機科學中實施正式驗證。在這種情況下，定理掠奪者用於驗證程序和硬件（例如處理器的正式規範）的正確性。由於這種分析是耗時的，因此昂貴，因此通常保留給故障會帶來嚴重的人類或財務後果的項目。

對於模型檢查的問題，已知有效的算法可以確定輸入有限結構是否滿足一階公式，此外，除了計算複雜性界限外：請參閱模型檢查§§一階邏輯。

也可以看看