一階邏輯 是使用於數學 、哲學 、語言學 及電腦科學 中的一種形式系統 ，也可以稱為：一階斷言演算 、低階斷言演算 、量化理論 或謂詞邏輯 。一階邏輯和命題邏輯 的不同之處在於，一階邏輯包含量詞 。
高階邏輯 和一階邏輯不同之處在於，高階邏輯的斷言符號可以有斷言符號或函數符號當做引數，且容許斷言量詞或函數量詞[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
來源 外部連結 參見
背景
分主題
應用
相關主題
人物
關鍵的語意網組織
標準
語法及支援技術
模式、本體和規則
語意標註
公共詞表
