一阶逻辑 是使用於数学 、哲学 、语言学 及電腦科學 中的一种形式系统 ，也可以稱為：一阶斷言演算 、低階斷言演算 、量化理論 或谓词逻辑 。一階邏輯和命題邏輯 的不同之處在於，一階邏輯包含量詞 。
高階邏輯 和一階邏輯不同之處在於，高階邏輯的斷言符號可以有斷言符號或函數符號當做引數，且容許斷言量詞或函數量詞[1] 語義 中，斷言被解釋為關係 。而高階邏輯的語義裡，斷言則會被解釋為集合的集合。
在通常的語義下，一階邏輯是可靠 （所有可證的敘述皆為真）且完備 （所有為真的敘述皆可證）。雖然一階邏輯的邏輯歸結 只是半可判定性 的，但還是有許多用於一階邏輯上的自動定理證明 。一階邏輯也符合一些使其能通過證明論 分析的元邏輯 定理，如勒文海姆–斯科倫定理 及緊緻性定理 。
一階邏輯是數學基礎 中很重要的一部份。許多常見的公理系統，如一階皮亞諾公理 、冯诺伊曼-博内斯-哥德尔集合论 和策梅洛-弗蘭克爾集合論 都是一階理論。然而，一階定理並沒有能力去完整描述及範疇性地 （「唯一地」）刻劃如自然數 或實數 之類無限的概念。這些結構的公理系統可以由如二階邏輯 之類更強的邏輯來取得。
簡介 以下通俗的介紹一階邏輯。
在命題邏輯裡，「蘇格拉底是哲學家」、「柏拉圖是哲學家」只能簡單標記為
p
{\displaystyle p}
q
{\displaystyle q}
而在一階邏輯，我們先將符號
Phil
(
x
)
{\displaystyle \text{Phil}(x)}
x
{\displaystyle x}
s
{\displaystyle s}
b
{\displaystyle b}
Phil
(
s
)
{\displaystyle \text{Phil}(s)}
p
{\displaystyle p}
Phil
(
b
)
{\displaystyle \text{Phil}(b)}
q
{\displaystyle q}
斷言符號 「
Phil
(
x
)
{\displaystyle \text{Phil}(x)}
語意的解釋 ，而這個解釋預設一個「所有人類的群體」(也就是我們一階邏輯語義的論域 )，將變數
x
{\displaystyle x}
事實上斷言符號可以包含不只一個的變數，比如說我們可以把
Cp
(
x
,
y
)
{\displaystyle \text{Cp}(x,\,y)}
x 與y 是夫妻」，這樣
Cp
(
s
,
y
)
{\displaystyle \text{Cp}(s,\,y)}
就可以解釋為「蘇格拉底和y 是夫妻」。
進一步的，斷言符號和變數還可以和邏輯符號組合成更複雜的敘述。例如將斷言符號
Schol
(
x
)
{\displaystyle \text{Schol}(x)}
x
{\displaystyle x}
x 為哲學家，則x 為學者」可以表示為
Phil
(
x
)
⇒
Schol
(
x
)
{\displaystyle \text{Phil}(x)\Rightarrow \text{Schol}(x) \,}
而「對所有x ，若x 為哲學家，則x 為學者」之類的敘述，我們寫為
∀
x
(
Phil
(
x
)
⇒
Schol
(
x
)
)
{\displaystyle \forall x ( \text{Phil}(x) \Rightarrow \text{Schol}(x))}
也就是自左方開始閱讀，以
∀
x
{\displaystyle \forall x}
x 」；將敘述理解為「對所有的x ，
∀
x
{\displaystyle \forall x}
∀
x
{\displaystyle \forall x}
x
{\displaystyle x}
全稱量詞
但全稱量詞直觀上，會有「若所有x 是哲學家，那x 的長子也會是哲學家」這樣的敘述，為此我們將
Son
(
x
)
{\displaystyle \text{Son}(x)}
x 的長子」，這樣前面的敘述可以寫為
∀
x
Phil
(
x
)
⇒
Phil
[
Son
(
x
)
]
{\displaystyle \forall x \text{Phil}(x) \Rightarrow \text{Phil}[\text{Son}(x)]}
這種解釋為成與
x
{\displaystyle x}
函數符號 。而事實上這段直觀為真的敘述，經過適當的擴展以後就是一階邏輯其中的一條公理 。
而對於「有x 是哲學家」，我們引入另一種量詞而表記為：
∃
x
(
Phil
(
x
)
)
{\displaystyle \exists x ( \text{Phil}(x))}
自左方開始閱讀，以
∃
x
{\displaystyle \exists x}
x 」；也就是解釋為「有x 使
∃
x
{\displaystyle \exists x}
∃
x
{\displaystyle \exists x}
x
{\displaystyle x}
存在量詞 。全稱量詞和存在量詞一起被簡稱為量詞
而直觀上，「並非所有x 不是哲學家」，和「有x 是哲學家」是等價的；且「並非有x 不是學者」也跟「所有的x 是學者」在直觀上也是等價的。所以只要有「否定」這個邏輯概念，那一階邏輯就只需要一種量詞。據此，並且為了使邏輯公理的敘述更加簡潔，一般會以全稱量詞 為基礎，作以下的符號定義(
¬
{\displaystyle \neg}
A
{\displaystyle \mathcal{A}}
∃
x
A
:=
¬
[
∀
x
(
¬
A
)
]
{\displaystyle \exists x \mathcal{A}:=\neg[\forall x (\neg\mathcal{A})]}
而將存在量詞定義為全稱量詞的衍伸符號。
在通常的一階邏輯語意解釋 上，需要一個量詞所提及物件所組成的非空集合，稱為論域 。例如，
∃
x
Phil
(
x
)
{\displaystyle \exists x \text{Phil}(x)}
集合論 基礎，但一般的嚴謹的公理化集合論 都是以一階邏輯的語言來敘述（如策梅洛-弗蘭克爾集合論 ）。這不免讓一階邏輯語義淪為"具有集合論公理的一階邏輯理論的一套元定理 "，用來有效的檢驗一段"敘述"(合式公式 )是否為這個一階邏輯理論的定理 。
形式理論 一階邏輯的形式理論 可分成幾個部份：
語法 ：決定哪些符號組合是合法表示式 。推理規則：一種針對合式公式的符號組合規則(對應於直觀上的"推理")
公理：一套合式公式(對應於直觀理解上，一個理論的基本假設。邏輯公理縮小形式系統與直觀邏輯的差距。) 語法 基本詞彙 一套理論到底能容許多少符號，取決於人類以物理定律 的手段能塑造和容下多少的符號。但以目前所知是無法確知宇宙是不是有限，或是是否可無限制分割。雖然所有的公理化集合論 都以量詞的形式隱晦的承認無窮的存在(如ZF集合論的無窮公理 )，甚至以這樣自然數 意義上的無窮為基礎，去建構出不可數 的實數。但將之對應到現實，還是會遇到同樣的物理問題。
謹慎起見，以下各種類的符號沒有特別聲明，數量將會是有限個。
邏輯符號 詞彙表中存在若干個邏輯符號，通常包括：
量化符號
∀
{\displaystyle \forall}
∃
{\displaystyle \exists}
某些作者[2]
∃
{\displaystyle \exists}
∃
x
A
:=
¬
[
∀
x
(
¬
A
)
]
,
{\displaystyle \exists x\mathcal{A}:= \neg[\forall x(\neg\mathcal{A})],}
如此只需要
∀
{\displaystyle \forall}
邏輯聯結詞 ：以下為可能的表示符號，而波蘭表示法下的邏輯連接詞請參見逻辑运算的波兰记法
否定 ：
¬
{\displaystyle \neg}
∼
{\displaystyle \sim}
條件 ：
⇒
{\displaystyle \Rightarrow}
→
{\displaystyle \rightarrow}
⊃
{\displaystyle \supset}
且 ：
∧
{\displaystyle \land}
&
{\displaystyle \&}
或 ：
∨
{\displaystyle \lor}
|| 雙條件 ：
⇔
{\displaystyle \Leftrightarrow}
↔
{\displaystyle \harr}
某些作者[3]
A
∧
B
:=
¬
(
A
⇒
(
¬
B
)
)
,
{\displaystyle \mathcal{A}\wedge\mathcal{B}:=\neg(\mathcal{A}\Rightarrow(\neg\mathcal{B})),}
A
∨
B
:=
(
¬
A
)
⇒
B
,
{\displaystyle \mathcal{A}\vee\mathcal{B}:=(\neg\mathcal{A})\Rightarrow\mathcal{B},}
A
⇔
B
:=
(
A
⇒
B
)
∧
(
B
⇒
A
)
,
{\displaystyle \mathcal{A}\Leftrightarrow\mathcal{B}:=(\mathcal{A}\Rightarrow\mathcal{B})\wedge(\mathcal{B}\Rightarrow\mathcal{A}),}
如此一來只需要否定 和條件 作为基礎符號。 標點符號：括號、逗號及其他，依作者的喜好有所不同。
為了更有效的將括號做配對，通常還會採用大括號{ } 跟中括號[ ] 。
至多跟自然數 一樣多的變數 ，通常標記為英文字母末端的小寫字母x 、y 、z 、…，也常會使用下標（或上標、上下標兼有）來區別不同的變數：x 0 、x 1 、x 2 、…。(特別注意c有時候會被當成常數符號而引起混淆)
等式符號：
=
{\displaystyle =}
有作者會因為語義上解釋"相等"的不同，而將等式符號視為雙元斷言符號、甚至是某類合式公式的簡寫。詳見下面的「等式」一節。
符號相等：
≍
{\displaystyle \asymp}
為了將詞彙於符號辨識上為等同 和等式符號做區隔，某些作者[4] 注意並非所有的符號都需要，比如說比較極端的理論，因謝費爾豎線 (或異或 )的布林代數 完備性使得所有不含量詞的邏輯公理可以以謝費爾豎線表述，而大幅減少基礎的邏輯聯結詞。
另外，一些作者並沒有將語義學 和形式理論 劃分清楚，而會將真值常數納入符號的一環；用T、Vpq 或
⊤
{\displaystyle \top}
pq 或
⊥
{\displaystyle \bot}
斷言符號 「他們兩人是夫妻」，代表一個關於兩個"對象"的斷言，而「他是人」、「三點共線」顯示了斷言是容許一個──甚至多個對象，所以對於自然數
n
{\displaystyle n}
j
{\displaystyle j}
A
j
n
(
x
1
,
x
2
,
.
.
.
,
x
n
)
{\displaystyle A^n_j(x_1,\,x_2,\,...,\,x_n)}
為一階邏輯的合法詞彙，它在直觀上表示一個有
n
{\displaystyle n}
n
{\displaystyle n}
元斷言符號 。下標的自然數
j
{\displaystyle j}
n
{\displaystyle n}
實用上只要有申明，不至於和其他詞彙引起混淆的話，我們可以用任意的形式簡寫一個斷言符號，如公理化集合論 裡的
x
∈
y
{\displaystyle x\in y}
A
1
2
(
x
,
y
)
{\displaystyle A^2_1(x,\,y)}
函數符號 「物體的顏色」、「夫妻的長子」說明了一列對象所唯一 對應的對象。但不同的夫妻有不同的長子；不同的物體有不同的顏色，所以對於自然數
n
{\displaystyle n}
j
{\displaystyle j}
f
j
n
(
x
1
,
x
2
,
.
.
.
,
x
n
)
{\displaystyle f^n_j(x_1,\,x_2,\,...,\,x_n)}
為一階邏輯的合法詞彙，它在直觀上表示
n
{\displaystyle n}
n
{\displaystyle n}
元函數符號 。但特別注意這種＂唯一對應＂的直觀想法，必須要有量詞的公理配上下面「等號」的章節以後，才能被實現。
就像斷言符號，不引起混淆的話我們可以用任何的形式簡寫函數符號，如公理化集合論 裡的
x
∪
y
{\displaystyle x\cup y}
聯集公理 而定義的新函數符號(請參見下面「函數符號與唯一性」的章節)，也可以冗長的表記為
f
j
2
(
x
,
y
)
{\displaystyle f^2_j(x,\,y)}
常數符號 「刻度0」、「原點」、「蘇格拉底 」這種(至少在作者的)直觀上"唯一不變"的對象，使我們對自然數
j
{\displaystyle j}
c
j
{\displaystyle c_j}
為一階邏輯的合法詞彙，它在直觀上表示一個"唯一不變"的對象。稱為常數符號 ，同樣的"常數的不變"要等到下面「等號」的章節才能被實現。
為了不和變數的表記混淆，常數符號一樣可以用任何的形式簡寫，如公理化集合論 裡的
∅
{\displaystyle \varnothing}
空集公理 和「函數符號與唯一性」的章節，而定義的新常數符號。亦可冗長的表示為
c
j
{\displaystyle c_j}
形成規則 和自然語言(如英語 )不同，一階邏輯的語言以明確的遞迴定義判斷一個給定的詞彙是否合法。大致上來說，一階邏輯以「項」代表討論的對象，而對「項」的斷言組成了最基本的原子(合式)公式 合式公式 (也就是"敘述")。
項 「那對夫妻的長子的職業」、「
(
x
+
y
)
×
z
{\displaystyle (x+y)\times z}
x
∪
∅
{\displaystyle x\cup\varnothing}
項 為：
變數 和常數 是項。若
T
1
,
.
.
.
.
,
T
n
{\displaystyle T_1,\,....,\,T_n}
f
j
n
(
T
1
,
.
.
.
.
,
T
n
)
{\displaystyle f^n_j(T_1,\,....,\,T_n)}
項只能透過以上兩點，於有限步驟內建構出來。 我們習慣用大寫的西方字母(如英文 字母、希伯來 字母、希臘字母 )代表項，如果變數不得不採用大寫字母，而跟會項引起混淆的話，需額外規定分辨的辦法。
原子公式 為了比較簡潔的規定甚麼是合式公式 ，我們先規定原子公式 為：（若
T
1
,
.
.
.
.
,
T
n
{\displaystyle T_1,\,....,\,T_n}
A
j
n
(
T
1
,
.
.
.
.
,
T
n
)
{\displaystyle A^n_j(T_1,\,....,\,T_n)}
這樣的形式。
公式 一階邏輯的合式公式
w
f
{\displaystyle wf}
原子公式為公式。(美觀起見，在原子公式外面包一層括弧也是公式)
若
A
{\displaystyle \mathcal{A}}
(
¬
A
)
{\displaystyle (\neg\mathcal{A})}
若
A
{\displaystyle \mathcal{A}}
B
{\displaystyle \mathcal{B}}
(
A
⇒
B
)
{\displaystyle (\mathcal{A}\Rightarrow\mathcal{B})}
若
A
{\displaystyle \mathcal{A}}
x
{\displaystyle x}
(
∀
x
A
)
{\displaystyle (\forall x\mathcal{A})}
(
∀
x
)
A
:=
∀
x
A
{\displaystyle (\forall x)\mathcal{A}:=\forall x\mathcal{A}}
合式公式只能透過以上四點，於有限步驟內建構出來。 另外成對的中括弧跟大括弧，符號辨識上我們視為成對的小括弧。我們習慣以草書的大寫西方字母 為公式的代號。
舉例來說，
{
(
∀
y
)
A
1
2
[
x
,
f
1
1
(
y
)
]
}
{\displaystyle \{(\forall y)A^2_1[x,\,f^1_1(y)]\}}
是公式而
∀
x
x
⇒
{\displaystyle \forall x\, x \Rightarrow}
則不是公式。
而接下來我們只要對任意公式
A
{\displaystyle \mathcal{A}}
B
{\displaystyle \mathcal{B}}
x
{\displaystyle x}
(
A
∧
B
)
:=
{
¬
[
A
⇒
(
¬
B
)
]
}
{\displaystyle (\mathcal{A}\wedge\mathcal{B}):=\{\neg[\mathcal{A}\Rightarrow(\neg\mathcal{B})]\}}
(
A
∨
B
)
:=
[
(
¬
A
)
⇒
B
]
{\displaystyle (\mathcal{A}\vee\mathcal{B}):=[(\neg\mathcal{A})\Rightarrow\mathcal{B}]}
(
A
⇔
B
)
:=
[
(
A
⇒
B
)
∧
(
B
⇒
A
)
]
{\displaystyle (\mathcal{A}\Leftrightarrow\mathcal{B}):=[(\mathcal{A}\Rightarrow\mathcal{B})\wedge(\mathcal{B}\Rightarrow\mathcal{A})]}
(
∃
x
A
)
:=
{
¬
[
∀
x
(
¬
A
)
]
}
{\displaystyle (\exists x\mathcal{A}):=\{\neg[\forall x(\neg\mathcal{A})]\}}
(
∃
x
)
A
:=
∃
x
A
{\displaystyle (\exists x)\mathcal{A}:=\exists x\mathcal{A}}
這樣所有的邏輯連接詞與量詞就納入了合式公式的規範。
施用 所謂的施用 /作用 ，是以下公式形式的口語說法：(其中
A
{\displaystyle \mathcal{A}}
B
{\displaystyle \mathcal{B}}
(
¬
A
)
{\displaystyle (\neg\mathcal{A})}
¬
{\displaystyle \neg}
A
{\displaystyle \mathcal{A}}
(
A
⇒
B
)
{\displaystyle (\mathcal{A}\Rightarrow\mathcal{B})}
⇒
{\displaystyle \Rightarrow}
A
{\displaystyle \mathcal{A}}
B
{\displaystyle \mathcal{B}}
(
A
∧
B
)
{\displaystyle (\mathcal{A}\wedge\mathcal{B})}
∧
{\displaystyle \wedge}
A
{\displaystyle \mathcal{A}}
B
{\displaystyle \mathcal{B}}
(
A
∨
B
)
{\displaystyle (\mathcal{A}\vee\mathcal{B})}
∨
{\displaystyle \vee}
A
{\displaystyle \mathcal{A}}
B
{\displaystyle \mathcal{B}}
(
A
⇔
B
)
{\displaystyle (\mathcal{A}\Leftrightarrow\mathcal{B})}
⇔
{\displaystyle \Leftrightarrow}
A
{\displaystyle \mathcal{A}}
B
{\displaystyle \mathcal{B}}
(
∀
x
A
)
{\displaystyle (\forall x\mathcal{A})}
∀
x
{\displaystyle \forall x}
A
{\displaystyle \mathcal{A}}
(
∃
x
A
)
{\displaystyle (\exists x\mathcal{A})}
∃
x
{\displaystyle \exists x}
A
{\displaystyle \mathcal{A}}
就好似運算子作用在它們身上。
自由變數和約束變數 量詞所施用的公式被稱為量詞的範圍 (scope)。同一個變數在公式一般來說不只出現一次，若變數
x
{\displaystyle x}
∀
x
{\displaystyle \forall x}
x
{\displaystyle x}
不自由 /被約束的
x
{\displaystyle x}
∀
x
{\displaystyle \forall x}
x
{\displaystyle x}
自由的
x
{\displaystyle x}
例如，對於公式：
(
∀
x
)
[
A
1
1
(
x
)
⇒
A
2
1
(
y
)
]
{\displaystyle (\forall x)[A^1_1(x)\Rightarrow A^1_2(y)]}
[
A
1
1
(
x
)
⇒
A
2
1
(
y
)
]
{\displaystyle [A^1_1(x)\Rightarrow A^1_2(y)]}
∀
x
{\displaystyle \forall x}
A
1
1
{\displaystyle A^1_1}
x
{\displaystyle x}
A
2
1
{\displaystyle A^1_2}
y
{\displaystyle y}
說
x
{\displaystyle x}
A
{\displaystyle \mathcal{A}}
A
{\displaystyle \mathcal{A}}
x
{\displaystyle x}
x
{\displaystyle x}
A
{\displaystyle \mathcal{A}}
A
{\displaystyle \mathcal{A}}
x
{\displaystyle x}
A
{\displaystyle \mathcal{A}}
x
{\displaystyle x}
A
{\displaystyle \mathcal{A}}
A
{\displaystyle \mathcal{A}}
封閉公式/句子
括弧的簡寫 括弧是為了保證語意解釋符合預期，但太多的括弧書寫不易，為此我們規定以下的"重構法"(反過來就是"簡寫法")，從表面上不合法的一串符號找出作者原來想表達的公式：
若整串符號的括弧不成對，直接視為無法重構 。
以
¬
,
∧
,
∨
,
∀
,
∃
,
⇒
,
⇔
{\displaystyle \lnot,\,\land,\,\lor,\,\forall,\,\exists,\,\Rightarrow,\,\Leftrightarrow}
相鄰的邏輯連接詞或量詞無法決定施用順序的話，以右邊為先。
重構施用的順序，以被成對括弧包住的部分為優先施用，其次才是落單的斷言符號。 舉例來說
¬
[
∀
x
A
1
1
(
x
)
]
⇒
∃
x
¬
A
2
1
(
x
)
{\displaystyle \lnot [\forall x A^1_1(x)] \Rightarrow \exists x \lnot A^1_2(x)}
的重構過程如下
{
¬
[
∀
x
A
1
1
(
x
)
]
}
⇒
∃
x
[
¬
A
2
1
(
x
)
]
{\displaystyle \{\lnot [\forall x A^1_1(x)]\} \Rightarrow \exists x [\lnot A^1_2(x)]}
¬
{\displaystyle \lnot}
{
¬
[
∀
x
A
1
1
(
x
)
]
}
⇒
{
∃
x
[
¬
A
2
1
(
x
)
]
}
{\displaystyle \{\lnot [\forall x A^1_1(x)]\} \Rightarrow \{\exists x [\lnot A^1_2(x)]\}}
∃
{\displaystyle \exists}
{
{
¬
[
∀
x
A
1
1
(
x
)
]
}
⇒
{
∃
x
[
¬
A
2
1
(
x
)
]
}
}
{\displaystyle \{\{\lnot [\forall x A^1_1(x)]\} \Rightarrow \{\exists x [\lnot A^1_2(x)]\}\}}
⇒
{\displaystyle \Rightarrow}
可以被重構為公式的一串符號，我們寬鬆的認定為"合式公式"。(最明顯的例子就是合式公式最外層的括弧可以"省略")
波蘭表示法 波蘭表示法 將邏輯連接詞前置於被施用的公式 而非傳統的中間。如果沿用以上的"施用順序"，這個表示法允許捨棄所有括弧。如公式
∀
x
∀
y
{
A
1
1
[
f
1
1
(
x
)
]
⇒
¬
{
A
1
1
(
x
)
⇒
A
1
3
[
f
1
1
(
y
)
,
x
,
z
]
}
}
{\displaystyle \forall x\forall y\{A^1_1[f^1_1(x)]\Rightarrow\neg\{A^1_1(x)\Rightarrow A^3_1[f^1_1(y),x,z]\}\}}
的波蘭表示法為
∀
x
∀
y
⇒
A
1
1
f
1
1
x
¬
⇒
A
1
1
x
A
1
3
f
1
1
y
x
z
{\displaystyle \forall x\forall y\Rightarrow A^1_1 f^1_1 x\neg\Rightarrow A^1_1 x A^3_1 f^1_1 y x z}
推理规则 對於公式
A
{\displaystyle \mathcal{A}}
B
{\displaystyle \mathcal{B}}
A
⇒
B
{\displaystyle \mathcal{A}\Rightarrow\mathcal{B}}
A
{\displaystyle \mathcal{A}}
B
{\displaystyle \mathcal{B}}
直觀意義非常明顯，就是p =>q 且p 可以推出q 。
公理 邏輯公理 如果
B
{\displaystyle \mathcal{B}}
C
{\displaystyle \mathcal{C}}
D
{\displaystyle \mathcal{D}}
(A1)
B
⇒
(
C
⇒
B
)
{\displaystyle \mathcal{B}\Rightarrow(\mathcal{C}\Rightarrow\mathcal{B})}
(A2)
[
B
⇒
(
C
⇒
D
)
]
⇒
[
(
B
⇒
C
)
⇒
(
B
⇒
D
)
]
{\displaystyle [\mathcal{B}\Rightarrow(\mathcal{C}\Rightarrow\mathcal{D})]\Rightarrow[(\mathcal{B}\Rightarrow\mathcal{C})\Rightarrow(\mathcal{B}\Rightarrow\mathcal{D})]}
(A3)
[
(
¬
B
)
⇒
(
¬
C
)
]
⇒
[
(
¬
B
⇒
C
)
⇒
B
]
{\displaystyle [(\neg\mathcal{B})\Rightarrow(\neg\mathcal{C})]\Rightarrow[(\neg\mathcal{B}\Rightarrow\mathcal{C})\Rightarrow\mathcal{B}]}
都是公理。
它们实际上是公理模式 ，代表著"無限多"條的公理。
量词公理 以下的
x
{\displaystyle x}
B
{\displaystyle \mathcal{B}}
C
{\displaystyle \mathcal{C}}
(A4)
T
{\displaystyle T}
t
{\displaystyle t}
T
{\displaystyle T}
B
{\displaystyle \mathcal{B}}
∀
t
{\displaystyle \forall t}
x
{\displaystyle x}
B
{\displaystyle \mathcal{B}}
T
{\displaystyle T}
x
{\displaystyle x}
[
(
∀
x
)
B
(
x
)
]
⇒
[
B
(
T
)
]
{\displaystyle [(\forall x)\mathcal{B}(x)]\Rightarrow[\mathcal{B}(T)]}
為公理
其中
B
(
T
)
{\displaystyle \mathcal{B}(T)}
B
{\displaystyle \mathcal{B}}
x
{\displaystyle x}
T
{\displaystyle T}
(A5)如果
x
{\displaystyle x}
B
{\displaystyle \mathcal{B}}
[
(
∀
x
)
(
B
⇒
C
)
]
⇒
[
B
⇒
(
∀
x
C
)
]
{\displaystyle [(\forall x)(\mathcal{B}\Rightarrow\mathcal{C})]\Rightarrow[\mathcal{B}\Rightarrow(\forall x\mathcal{C})]}
為公理 (A6)
[
(
∀
x
)
(
B
⇒
C
)
]
⇒
[
(
∀
x
B
)
⇒
(
∀
x
C
)
]
{\displaystyle [(\forall x)(\mathcal{B}\Rightarrow\mathcal{C})]\Rightarrow[(\forall x\mathcal{B})\Rightarrow(\forall x\mathcal{C})]}
(A7) 若
B
{\displaystyle \mathcal{B}}
(
∀
x
)
B
{\displaystyle (\forall x)\mathcal{B}}
也是公理。 它们实际上是公理模式 。
定理與證明 以下介紹一些理解公理所需的基本用語和符號
在一階邏輯理論
L
{\displaystyle \mathcal{L}}
⊢
L
A
{\displaystyle \vdash_{\mathcal{L}}\mathcal{A}}
C
i
(
1
≤
i
≤
n
)
{\displaystyle \mathcal{C}_i\,\,(1\leq i\leq n)}
C
n
{\displaystyle \mathcal{C}_n}
A
{\displaystyle \mathcal{A}}
C
1
{\displaystyle \mathcal{C}_1}
L
{\displaystyle \mathcal{L}}
若
1
<
k
<
n
{\displaystyle 1 < k < n}
C
k
{\displaystyle \mathcal{C}_k}
C
k
{\displaystyle \mathcal{C}_k}
L
{\displaystyle \mathcal{L}}
存在
i
,
j
<
k
{\displaystyle i,\,j < k}
C
i
{\displaystyle \mathcal{C}_i}
(
C
j
⇒
C
k
)
{\displaystyle (\mathcal{C}_j\Rightarrow\mathcal{C}_k)}
而口語上會稱公式
A
{\displaystyle \mathcal{A}}
⊢
L
A
{\displaystyle \vdash_{\mathcal{L}}\mathcal{A}}
L
{\displaystyle \mathcal{L}}
定理 (theorem)。而這列
C
i
(
1
≤
i
≤
n
)
{\displaystyle \mathcal{C}_i\,\,(1\leq i\leq n)}
⊢
L
A
{\displaystyle \vdash_{\mathcal{L}}\mathcal{A}}
例如定理
⊢
L
B
⇒
B
{\displaystyle \vdash_{\mathcal{L}}\mathcal{B}\Rightarrow\mathcal{B}}
C
1
{\displaystyle \mathcal{C}_1}
{
B
⇒
[
(
B
⇒
B
)
⇒
B
]
}
⇒
{
[
B
⇒
(
B
⇒
B
)
]
⇒
(
B
⇒
B
)
}
{\displaystyle \{\mathcal{B}\Rightarrow[(\mathcal{B}\Rightarrow\mathcal{B})\Rightarrow\mathcal{B}]\}\Rightarrow\{[\mathcal{B}\Rightarrow(\mathcal{B}\Rightarrow\mathcal{B})]\Rightarrow(\mathcal{B}\Rightarrow\mathcal{B})\}}
C
2
{\displaystyle \mathcal{C}_2}
B
⇒
[
(
B
⇒
B
)
⇒
B
]
{\displaystyle \mathcal{B}\Rightarrow[(\mathcal{B}\Rightarrow\mathcal{B})\Rightarrow\mathcal{B}]}
C
3
{\displaystyle \mathcal{C}_3}
B
⇒
(
B
⇒
B
)
{\displaystyle \mathcal{B}\Rightarrow(\mathcal{B}\Rightarrow\mathcal{B})}
C
4
{\displaystyle \mathcal{C}_4}
[
B
⇒
(
B
⇒
B
)
]
⇒
(
B
⇒
B
)
{\displaystyle [\mathcal{B}\Rightarrow(\mathcal{B}\Rightarrow\mathcal{B})]\Rightarrow(\mathcal{B}\Rightarrow\mathcal{B})}
C
1
{\displaystyle \mathcal{C}_1}
C
2
{\displaystyle \mathcal{C}_2}
C
5
{\displaystyle \mathcal{C}_5}
B
⇒
B
{\displaystyle \mathcal{B}\Rightarrow\mathcal{B}}
C
4
{\displaystyle \mathcal{C}_4}
C
3
{\displaystyle \mathcal{C}_3}
直觀上的證明，總是會有一些"前提假設"，對此，若我們以
Γ
{\displaystyle \Gamma}
Γ
⊢
L
A
{\displaystyle \Gamma\vdash_{\mathcal{L}}\mathcal{A}}
C
i
(
1
≤
i
≤
n
)
{\displaystyle \mathcal{C}_i\,\,(1\leq i\leq n)}
C
n
{\displaystyle \mathcal{C}_n}
A
{\displaystyle \mathcal{A}}
若
k
<
n
{\displaystyle k < n}
C
k
{\displaystyle \mathcal{C}_k}
C
k
{\displaystyle \mathcal{C}_k}
L
{\displaystyle \mathcal{L}}
C
k
{\displaystyle \mathcal{C}_k}
Γ
{\displaystyle \Gamma}
存在
i
,
j
<
k
{\displaystyle i,\,j < k}
C
i
{\displaystyle \mathcal{C}_i}
(
C
j
⇒
C
k
)
{\displaystyle (\mathcal{C}_j\Rightarrow\mathcal{C}_k)}
這樣我們稱
C
i
(
1
≤
i
≤
n
)
{\displaystyle \mathcal{C}_i\,\,(1\leq i\leq n)}
Γ
{\displaystyle \Gamma}
A
{\displaystyle \mathcal{A}}
若要特別凸顯
Γ
{\displaystyle \Gamma}
B
{\displaystyle \mathcal{B}}
Γ
,
B
⊢
L
A
{\displaystyle \Gamma,\,\mathcal{B}\vdash_{\mathcal{L}}\mathcal{A}}
Γ
{\displaystyle \Gamma}
B
1
,
.
.
.
,
B
n
{\displaystyle \mathcal{B}_1,...,\mathcal{B}_n}
B
1
,
.
.
.
,
B
n
⊢
L
A
{\displaystyle \mathcal{B}_1,...,\mathcal{B}_n\vdash_{\mathcal{L}}\mathcal{A}}
以上的記號，在引用哪個理論很顯然的情況下，
⊢
L
{\displaystyle \vdash_{\mathcal{L}}}
L
{\displaystyle \mathcal{L}}
從公理(A1)和(A2)會得出一條很直觀的元定理：
一階邏輯理論
L
{\displaystyle \mathcal{L}}
Γ
,
B
⊢
L
C
{\displaystyle \Gamma,\mathcal{B}\vdash_{\mathcal{L}}\mathcal{C}}
Γ
⊢
L
B
⇒
C
{\displaystyle \Gamma\vdash_{\mathcal{L}}\mathcal{B}\Rightarrow\mathcal{C}}
等式和它的公理 在一阶逻辑中对使用等式（或恒等式）有多种不同的约定。本节总结其中主要的。不同的约定对同样的工作给出本质上相同的结果，区别主要在术语上。
对等式的最常见的约定是把等号包括为基本逻辑符号，并向一阶逻辑增加等式的公理。等式公理是 x = x x = y → f (...,x ,...) = f （...,y ,...）对于任何函数f x = y →（P (...,x ,...) → P （...,y ,...））对于任何关系P （包括 = 自身）其次常见的约定是把等号包括为理论的关系之一，并向这个理论的公理增加等式的公理。在实际中这是同前面约定最难分辨的，除了在没有等式概念的不常见情况下。公理是一样的，唯一的区别是把它叫做逻辑公理还是这个理论的公理。
在没有函数和有有限数目个关系的理论中，有可能以关系的方式定义等式，通过定义两个项s 和t 是相等的，如果任何关系通过把s 改变为t 在任何讨论下都没有改变。例如，在带有一个关系∈的集合论中，我们可以定义s = t 为∀x (s ∈ x ↔ t ∈ x ) ∧ ∀x （x ∈ s ↔ x ∈ t ）的缩写。这个等式定义接着自动的满足了关于等式的公理。
在某些理论中有可能给出特别的等式定义。例如，在带有一个关系 ≤的偏序的理论中，我们可以定义s = t 为s ≤ t ∧ t ≤ s 的缩写。 語義 一階語言的解釋 會對語言內的所有非邏輯常數賦予上意義，同時也決定能指明量化範圍的論域 。其結果為，每個項都會被賦予其代表的元件，每個句子也都會被賦予上一個真值。這樣，解釋即對語言內的項及公式提供了語義。研究形式語言的解釋的學科稱為形式語義學 。
論域D 是由某種類型的「物件」所組成的非空集合。直觀上來看，一階公式是有關這些物件的敘述。例如，
∃
x
P
(
x
)
{\displaystyle \exists x P(x)}
x ，能使得指涉此物件的斷言P 為真。論域即是此類考量的物件的集合，例如可取D 為整數的集合。
函數符號的解釋是函數。舉例來說，若論域由整數所組成，則一個2元的函數符號f 能解釋為給出其參數之和的函數。換句話說，符號f 和在此解釋下為加法的函數I(f) 是相關連的。
常數符號的解釋是一個從單元素集合D 0 映射至D 的函數，也可簡單視為是D 內的一個物件。例如，一個解釋可將值
I
(
c
)
=
10
{\displaystyle I(c)=10}
c
{\displaystyle c}
n 元斷言符號的解釋是由論域中的元素所組成的n 對有序集。這意味著，給定一個解釋、一個斷言符號及論域中的n 個元素，則可依給定的解釋判斷這些元素的斷言是否為真。例如，一個2元斷言符號P 的解釋I(P) 可以是一對整數，能使得第一個整數小於第二個整數。依據這個解釋，斷言P 在其第一個參數小於第二個參數時為真。
一階結構 指定一個解釋的最常見方法是指定一個結構 （或稱做模型 ，見下文）。結構包括一個由論域及標識內的非邏輯項的解釋I 所組成的非空集合。這個解釋自身是個函數：
每個n 元函數符號f 都會賦予一個從
D
n
{\displaystyle D^n}
D
{\displaystyle D}
I(f) 。特別地是，每個標識內的常數符號都會被賦予論域中的一個個體。
每個n 元斷言符號P 都會賦予一個在
D
n
{\displaystyle D^n}
I(P) （或等價地說，一個從
D
n
{\displaystyle D^n}
{
t
r
u
e
,
f
a
l
s
e
}
{\displaystyle \{true,false\}}
D 上的布林值函數 所解釋。 真值的賦值 一個公式由給定的解釋及將論域中的元素與每個變數相關連的變數賦值 μ來決定為真或為假。需要變數賦值的原因是為了給予具自由變數的公式（如
y
=
x
{\displaystyle y = x}
x 和y 是否標記著相同的個體。
首先，變數賦值μ可以擴展到語言內的所有項，使每個項都能映射至論域中的單一元素。下列的規則被用來得到賦值：
變數 。每個變數x 皆可得到μ(x )。函數 。給定一組項
t
1
,
…
,
t
n
{\displaystyle t_1, \ldots, t_n}
d
1
,
…
,
d
n
{\displaystyle d_1, \ldots, d_n}
n 元函數符號f ，則項
f
(
t
1
,
…
,
t
n
)
{\displaystyle f(t_1, \ldots, t_n)}
(
I
(
f
)
)
(
d
1
,
…
,
d
n
)
{\displaystyle (I(f))(d_1,\ldots,d_n)}
再來，每個公式皆可賦予一個真值。用來得到賦值的遞歸性定義稱為T-模式 。
原子公式（1） 。公式
P
(
t
1
,
…
,
t
n
)
{\displaystyle P(t_1,\ldots,t_n)}
⟨
v
1
,
…
,
v
n
⟩
∈
I
(
P
)
{\displaystyle \langle v_1,\ldots,v_n \rangle \in I(P)}
v
1
,
…
,
v
n
{\displaystyle v_1,\ldots,v_n}
t
1
,
…
,
t
n
{\displaystyle t_1,\ldots,t_n}
I
(
P
)
{\displaystyle I(P)}
P
{\displaystyle P}
原子公式（2） 。公式
t
1
=
t
2
{\displaystyle t_1 = t_2}
t
1
{\displaystyle t_1}
t
2
{\displaystyle t_2}
邏輯聯結詞 。
¬
ϕ
{\displaystyle \neg \phi}
ϕ
→
ψ
{\displaystyle \phi \rightarrow \psi}
真值表 （如命題邏輯一般）來賦值的。存在量化 。公式
∃
x
ϕ
(
x
)
{\displaystyle \exists x \phi(x)}
M 和變數賦值μ為真，若存在一個只和μ在對x 的賦值上有所不同的變數賦值μ'，能使得φ根據解釋M 和變數賦值μ'為真。此一形式定義是由「
∃
x
ϕ
(
x
)
{\displaystyle \exists x \phi(x)}
x 的方法，使得φ(x )為真」的這個概念來的。全稱量化 。公式
∀
x
ϕ
(
x
)
{\displaystyle \forall x \phi(x)}
M 和變數賦值μ為真，若φ(x )根據每個只和μ在對x 的賦值上有所不同的變數賦值μ'及解釋M 為真。此一形式定義是由「
∀
x
ϕ
(
x
)
{\displaystyle \forall x \phi(x)}
x 的方法，皆能使φ(x )為真」的這個概念來的。若一個公式不包含自由變數，即為一個句子，則一開始的變數賦值不會影響其真值。換句話說，一個句子根據M 及
μ
{\displaystyle \mu}
M 及其他的變數賦值
μ
′
{\displaystyle \mu'}
還有第二種常見的做法可以定義真值，而且不需要依靠變數賦值函數。給定一個解釋M ，首先將一組常數符號加至標識之中，每一個在M 中的論域的元素對應一個常數符號：稱對每個域論中的元素d ，都會固定有一個常數符號c d
存在量化 。公式
∃
x
ϕ
(
x
)
{\displaystyle \exists x \phi(x)}
M 為真，若存在某些在論域中的d ，使得
ϕ
(
c
d
)
{\displaystyle \phi(c_d)}
ϕ
(
c
d
)
{\displaystyle \phi(c_d)}
c d x 所得到的公式。全稱量化 。公式
∀
x
ϕ
(
x
)
{\displaystyle \forall x \phi(x)}
M 為真，若對每個論域中的d ，根據M 的
ϕ
(
c
d
)
{\displaystyle \phi(c_d)}
這個做法對所有的句子會給出和使用變數賦值的做法一樣的真值。
有效性、可滿足性及邏輯結論 若句子φ在一給定解釋M 下為真，則稱M 滿足 φ，標記為
M
⊨
ϕ
{\displaystyle M \vDash \phi}
可滿足的 ，若存在某个解釋使其為真。
具自由變數的公式的可滿足性就較為複雜了，因為只用解釋並無法決定此類公式的真值。一個常見的慣例是稱一個具自由變數的公式在一個解釋下為可滿足的，若不論如何將論域中的個體賦予其自由變數，這個公式皆為真。這等價於稱公式為可從足的，若且唯若其全稱閉包 為可滿足的。
一個公式是邏輯有效的 （或簡單稱為有效的 ），若在每一個解釋之下皆為真。此類的公式和命題邏輯中的重言式 扮演著相似的角色。
一個公式φ是公式ψ的邏輯結論 ，若每個使得ψ為真的解釋皆會使得φ為真。在此一狀況下，稱φ被ψ邏輯蘊涵著。
代數化 另一種賦予一階邏輯語義的方法可經由抽象代數 處理。這種方法是將命題邏輯的林登鮑姆-塔斯基代數 擴展而成。有如下幾種類型：
這些代數 都是純粹擴展兩元素布林代數 而成的格 。
塔斯基和葛范德於1987年證明，沒有超過包在三個以上的量化內的原子句子 的部份一階邏輯，其表示力和關係代數 相同。上述部份一階邏輯令人十分地感到有興趣，因為它已足夠表示皮亞諾算術 和公理化集合論 ，包括典型的ZFC 。他們亦證明了，具有簡單有序對 的一階邏輯和具有兩個有序的投影函數 的關係代數等價。
一階理論、模型及基本類 一階理論 公理 所組成的。公理所組成的集合通常是有限的或遞歸可枚舉 的，此類的理論稱為是有效的 。有些作者要求理論也要包括所有由公理導出的邏輯結論。
滿足給定理論內的所有句子的一階結構稱為此理論的模型 。基本類 是由所有滿足特定理論的結構所組成的集合。這些類是類型論 裡的研究主題。
許多理論都有一個預期解釋 ，即一個在研究理論時會在意的某種模型。例如，皮亞諾公理 的預期解釋 是由一般的自然數 和其一般的運算所組成的。不過，勒文海姆–斯科倫定理證明，大多數的一階理論也都會有其他的非標準模型 。
一個理論是相容的 完備的 哥德爾不完備定理 證明，有效的一階理論只要它強到足以蘊涵自然數的理論，即無法同時是相容且完備的。
空論域 上述定義需要任何一個解釋的論域均為非空集合。但在如自由邏輯 之中，設定空論域是被允許的。更甚之，若代數結構的類包含一個空結構（如空偏序集 ），當允許空論域時，這個類只能是一階邏輯中的一個基本類，不然就要將空結構由類中移除。
不過，空論域存在著一些難點：
許多常見的推理規則只在論域被要求是非空時才為有效的。一個例子為，當x 不是
ϕ
{\displaystyle \phi \,}
ϕ
∨
∃
x
ψ
{\displaystyle \phi \lor \exists x \psi}
∃
x
(
ϕ
∨
ψ
)
{\displaystyle \exists x (\phi \lor \psi)}
前束範式 的規則在非空論域中是可靠的，但在允許空論域時則是不可靠的。
在使用變數賦值函數的解釋中，真值的定義不能和空論域一起運作，因為不存在範圍為空的變數賦值函數。（相似地，也無法將解釋賦予上常數符號。）在甚至是原子公式的真值可被定義之前，都必須選定一個變數賦值函數。然後一個句子的真值即可在任一個變數賦值之下定義出其真值，且可證明其真值不依選定的賦值而變。這個做法在賦值函數不存在時不能運作；除非將其改成配上空論域。 因此，若空論域是被允許的，通常也必須被視成特例。不過，大多數的作家會簡單地將空論域由定義中排除。
常用的定理 斷言演算是命题演算 的扩展，它定义了哪些一阶逻辑的陈述是可证明的。它是用来描述数学理论的形式系统 。如果命题演算用一组合适的公理和一个单一的推理规则肯定前件 来定义（可以有很多不同的方式），则斷言演算可以通过增加一些补充的公理和补充的推理规则"全称普遍化"来定义。更精确地说，斷言演算采用的公理有：
来自命题演算的所有重言式（命题变量被替代为公式）。
上面给出的量词公理。
上面给出的等式公理，如果等式被认为是逻辑概念的话。 一个句子被定义为是在一阶逻辑中可证明 的，如果可以通过从斷言演算的公理开始并重复应用推理规则"肯定前件"和"全称普遍化"来得出它。
如果我们有一个理论T （在某些语言中叫做公理的陈述的集合），则一个句子φ被定义为是在理论T 中可证明 的，如果
a ∧ b ∧ ... → φ在一阶逻辑中对于理论T 的某个公理a , b ,...的有限集合是可证明的。
可证明性的一个明显问题是它好像非常特别：我们采用了显然随机的公理和推理规则的搜集，不清楚是否意外的漏掉了某个关键的公理或规则。哥德尔完备性定理 确保这实际上不是问题：这个定理声称在所有模型中为真的任何陈述在一阶逻辑中都是可证明的。特别是，在一阶逻辑中"可证明性"的任何合理定义都必须等价于上述定义（尽管在不同的可证明性的定义下证明的长度可能有巨大差别）。
有很多不同（但等价）的方式来定义可证明性。前面的演算是"希尔伯特风格 "演算的一个典型例子，它有许多不同的公理但只有非常少的推理规则。"根岑风格" 斷言演算有非常少的公理但有许多推理规则。
文法上说斷言演算在现存的命题演算上增加了“斷言-主词结构”和量词 。主词是给定的个体群组（集合 ）的一个成员的名字，而斷言 是在这个群组上的关系 ，一元斷言在哲学中称为性质 ，在数学中称为指示函数 ，在数理逻辑 中称为布尔值函数 。
可证明的恒等式
¬
∀
x
P
(
x
)
⇔
∃
x
¬
P
(
x
)
{\displaystyle \neg \forall x P(x) \Leftrightarrow \exists x \neg P(x)}
¬
∃
x
P
(
x
)
⇔
∀
x
¬
P
(
x
)
{\displaystyle \neg \exists x P(x) \Leftrightarrow \forall x \neg P(x)}
∀
x
∀
y
P
(
x
,
y
)
⇔
∀
y
∀
x
P
(
x
,
y
)
{\displaystyle \forall x \forall y P(x,y) \Leftrightarrow \forall y \forall x P(x,y)}
∃
x
∃
y
P
(
x
,
y
)
⇔
∃
y
∃
x
P
(
x
,
y
)
{\displaystyle \exists x \exists y P(x,y) \Leftrightarrow \exists y \exists x P(x,y)}
∀
x
P
(
x
)
∧
∀
x
Q
(
x
)
⇔
∀
x
(
P
(
x
)
∧
Q
(
x
)
)
{\displaystyle \forall x P(x) \land \forall x Q(x) \Leftrightarrow \forall x (P(x) \land Q(x)) }
∃
x
P
(
x
)
∨
∃
x
Q
(
x
)
⇔
∃
x
(
P
(
x
)
∨
Q
(
x
)
)
{\displaystyle \exists x P(x) \lor \exists x Q(x) \Leftrightarrow \exists x (P(x) \lor Q(x)) }
可能增加的推理规则
∃
x
∀
y
P
(
x
,
y
)
⇒
∀
y
∃
x
P
(
x
,
y
)
{\displaystyle \exists x \forall y P(x,y) \Rightarrow \forall y \exists x P(x,y)}
∀
x
P
(
x
)
∨
∀
x
Q
(
x
)
⇒
∀
x
(
P
(
x
)
∨
Q
(
x
)
)
{\displaystyle \forall x P(x) \lor \forall x Q(x) \Rightarrow \forall x (P(x) \lor Q(x)) }
∃
x
(
P
(
x
)
∧
Q
(
x
)
)
⇒
∃
x
P
(
x
)
∧
∃
x
Q
(
x
)
{\displaystyle \exists x (P(x) \land Q(x)) \Rightarrow \exists x P(x) \land \exists x Q(x)}
∃
x
P
(
x
)
∧
∀
x
Q
(
x
)
⇒
∃
x
(
P
(
x
)
∧
Q
(
x
)
)
{\displaystyle \exists x P(x) \land \forall x Q(x) \Rightarrow \exists x (P(x) \land Q(x)) }
一阶逻辑的元定理 下面列出了一些重要的元逻辑定理。
不像命题演算 ，一阶逻辑是不可判定性的。对于任意的公式P，可以证实没有判定过程 ，判定P是否有效，（参见停机问题 ）。（结论独立的来自于邱奇 和图灵 。）
有效性 的判定问题是半可判定的。按哥德尔完备性定理 所展示的，对于任何有效的 公式P, P是可证明的。一元斷言逻辑 （就是说，斷言只有一个参数的斷言逻辑）是可判定的。转换自然语言到一阶逻辑 用自然语言表达的概念必须在一阶逻辑（FOL）可以为为其效力之前必须被转换到FOL，而在这种转换中可能有一些潜在的缺陷。在FOL中，
p
∨
q
{\displaystyle p \lor q}
[5]
一阶逻辑的限制 所有数学概念都有它的强项和弱点；下面列出一阶逻辑的一些问题。
难于表达if-then-else 带有等式的FOL不包含或允许定义if-then-else斷言或函数if（c,a,b），这裡的c是表达为公式的条件，而a和b是要么都是项要么都是公式，并且它的结果是a如果c为真，或者b如果它为假。问题在于FOL中，斷言和函数二者只接受（“非布尔类型”）项作为参数，而条件的明确表达是（“布尔类型”）公式。这是不幸的，因为很多数学函数是依据if-then-else而方便的表达的，而if-then-else是描述大多数计算机程序的基础。
在数学上，有可能重定义匹配公式算子的新函数的完备集合，但是这是非常笨拙的。[6]
(
c
∧
a
)
∨
(
¬
c
∧
b
)
{\displaystyle (c \wedge a) \lor (\neg c \wedge b)}
[7]
类型（种类） 除了在公式（“布尔类型”）和项（“非布尔类型”）之间的区别之外，FOL不包括类型（种类）到自身的概念中。
某些人争辩说缺乏类型是巨大优点
[8] [9]
单一参数斷言可以用来在合适的地方实现类型的概念。例如：
∀
x
(
M
a
n
(
x
)
→
M
o
r
t
a
l
(
x
)
)
{\displaystyle \forall x (Man(x) \rightarrow Mortal(x))}
斷言Man(x)可以被认为是一类“类型断言”（就是说，x必须是男人）。
斷言还可以同指示类型的“存在”量词一起使用，但这通常应当转而与逻辑合取算子一起来做，比如：
∃
x
(
M
a
n
(
x
)
∧
M
o
r
t
a
l
(
x
)
)
{\displaystyle \exists x (Man(x) \wedge Mortal(x))}
容易写成
∃
x
M
a
n
(
x
)
→
M
o
r
t
a
l
(
x
)
{\displaystyle \exists x Man(x) \rightarrow Mortal(x)}
∃
x
¬
M
a
n
(
x
)
∨
∃
x
M
o
r
t
a
l
(
x
)
{\displaystyle \exists x \neg Man(x) \lor \exists x Mortal(x)}
∀
x
(
M
a
n
(
x
)
→
M
a
m
m
a
l
(
x
)
)
{\displaystyle \forall x (Man(x) \rightarrow Mammal(x))}
难于刻画模型大小 从Löwenheim–Skolem定理 得出在一阶逻辑中不可能刻画有限性或可数性。若一階理論有任意大的模型，則也有無窮大的模型，所以說不能刻劃有限性。[10] :1 而若理論有某個無窮基數大小的模型，則也必有任意更大的模型，所以不能刻劃可數性。[11] :45 另一個例子，是無法用一階語言將實數系 公理化，因為不論用何種一階理論描述，既然該理論有實數系此種無窮模型（大小為
2
ℵ
0
{\displaystyle 2^{\aleph_0}}
2
2
ℵ
0
{\displaystyle 2^{2^{\aleph_0}}}
上确界 性质一項，它声称实数的所有有界的、非空集合都有上确界 。一階邏輯祗能對元素量化，但此公理中，要對模型的全部子集量化，这就需要二阶逻辑 了。[12] :30
图可及性不能表达 很多情况可以被建模为节点和有向连接（边）的图 。例如，效验很多系统要求展示不能从“好”状态触及到“坏”状态，而状态的相互连接经常可以建模为图。但是，可以证明这种可及性不能用斷言逻辑完全表达。换句话说，没有斷言逻辑公式f，带有u和v作为它的唯一自由变量，而R作为它唯一的（2元）斷言符号，使得f在一个有向图中成立，如果在这个图中存在从关联于u的节点到关联于v的节点的路径。[13]
参考文献 引用
↑ Mendelson, Elliott. Introduction to Mathematical Logic. Van Nostrand Reinhold. 1964: 56. ↑ Elliott Mendelson. Introduction to Mathematical Logic - 6th Edition , p.48 ISBN 978-1482237726
↑ Elliott Mendelson. Introduction to Mathematical Logic - 6th Edition , p.29 ISBN 978-1482237726
↑ Stephen Cole Kleene Introduction to Metamathematics , p.252 ISBN 978-0923891572
↑ Suber, Peter, Translation Tips , [2007-09-20 ] ↑ Otter Example if.in , [2007-09-21 ] ↑
Manna, Zohar, Mathematical Theory of Computation, McGraw-Hill Computer Science Series, New York, New York: McGraw-Hill Book Company: 77–147, 1974, ISBN 0-07-039910-7
↑ Leslie Lamport, Lawrence C. Paulson.
Should Your Specification Language Be Typed?
ACM Transactions on Programming Languages and Systems.
1998.
http://citeseer.ist.psu.edu/71125.html
↑ Rushby, John. Subtypes for Specification. 1997. Proceedings of the Sixth European Software Engineering Conference (ESEC/FSE 97). http://citeseer.ist.psu.edu/328947.html
↑ Mahesh Viswanathan. Finite Model Theory (PDF) . ↑ David Marker. Model Theory: An Introduction. Graduate Texts in Mathematics 217 . Springer. 2002. ↑ Johnstone, P. T. Notes on logic and set theory. Cambridge University Press . 1987. doi:10.1017/CBO9781139172066 ↑
Huth, Michael; Ryan, Mark, Logic in Computer Science, 2nd edition: 138–139, 2004, ISBN 0-521-54310-X
来源 外部链接 参见
背景
分主题
应用
相关主题
人物
关键的语义网组织
标准
语法及支持技术
模式、本体和规则
语义标注
公共词表
