茶年 · 中文维基百科

一阶逻辑

Wikipedia · 2026-06-01 维基百科 👁 1 阅读

一阶逻辑是使用於数学、哲学、语言学及電腦科學中的一种形式系统，也可以稱為：一阶斷言演算、低階斷言演算、量化理論或谓词逻辑。一階邏輯和命題邏輯的不同之處在於，一階邏輯包含量詞。

高階邏輯和一階邏輯不同之處在於，高階邏輯的斷言符號可以有斷言符號或函數符號當做引數，且容許斷言量詞或函數量詞。在一階邏輯的語義中，斷言被解釋為關係。而高階邏輯的語義裡，斷言則會被解釋為集合的集合。

在通常的語義下，一階邏輯是可靠（所有可證的敘述皆為真）且完備（所有為真的敘述皆可證）的。雖然一階邏輯的邏輯歸結只是半可判定性的，但還是有許多用於一階邏輯上的自動定理證明。一階邏輯也符合一些使其能通過證明論分析的元邏輯定理，如勒文海姆–斯科倫定理及緊緻性定理。

一階邏輯是數學基礎中很重要的一部份。許多常見的公理系統，如一階皮亞諾公理、冯诺伊曼-博内斯-哥德尔集合论和策梅洛-弗蘭克爾集合論都是一階理論。然而一階邏輯不能控制其無窮模型的基數大小，因根據勒文海姆–斯科倫定理和康托爾定理，可以構造出一種“病態”集合論模型，使整個模型可數，但模型內卻會覺得自己有「不可數集」。類似地，可以證明實數系的普通一階理論既有可數模型又有不可數模型。這類的悖論被稱為斯科倫悖論。但一階的直覺主義邏輯裡，勒文海姆–斯科倫定理不可證明，故不會有以上之現象。

簡介
基本符號
命題邏輯顧名思義，會將「蘇格拉底是哲學家」、「柏拉圖是哲學家」之類直觀上有真有假的敘述簡記為 p 及 q （也就是有真有假的命題），然後討論 \neg p（非p）、p \Rightarrow q（若p則q）、p \wedge q（p且q）與p \vee q（p或q）之間的推理關係。

但一階邏輯嘗試從一些比較基礎的詞彙去建構「句子」，比如說，可用符號 \text{Phil}(x) 代表 「 x 是哲學家」，也就是賦予斷言符號「\text{Phil}(x) 」語意的解釋。這個解釋預設一個「所有人類的群體」（也就是下面標準語義一節會說到的论域），并將變數 x 對應為自群體中取出來的某人。

以此類推，斷言符號可以包含一個以上的變數。例如：可以將 \text{Cp}(x,\,y) 解釋為「 x 與 y 是夫妻」。

一階邏輯類似於命題邏輯，可以將斷言符號與 \neg（非）、\Rightarrow（則）、\wedge（且）和 \vee（或）組成更複雜的敘述，例如：把斷言符號 \text{Schol}(x) 解釋成「 x 是學者」，那「若 x 為哲學家，則 x 為學者」可表示為：
:\text{Phil}(x)\Rightarrow \text{Schol}(x) \,

但相較之下，一階邏輯又加入了描述「所有」與「存在」的量詞，比如說「對所有 x ，若 x 為哲學家，則 x 為學者」可記為：
:\forall x [\text{Phil}(x) \Rightarrow \text{Schol}(x)]
也就是自左方開始閱讀，將 \forall x 解釋成「对所有 x 有…」。\forall 這個符號被称为全稱量詞。

而對於「有 x 是哲學家」这一叙述，一階邏輯則引入另一種量詞：
:\exists x [\text{Phil}(x)]
也就是自左方開始閱讀，將 \exists x 解釋成「存在 x 使…」。\exists 這個符號被称为存在量詞。

順帶一提「並非所有 x 不是哲學家」等價於「有 x 是哲學家」；且「不存在 x 不是學者」也等價於「所有的 x 是學者」。所以可以用「否定」和「全稱量詞」來組合出「存在量詞」。換句話說，可作以下的符號定義（\mathcal{A} 代表一段「敘述」）：
:\exists x \mathcal{A}:=\neg[\forall x (\neg\mathcal{A})]

相等
一階邏輯也考慮到「相等」這個概念在敘述中的重要性，例如想表達「若所有x是哲學家，那x的長子也會是哲學家」，可先把 \text{Son}(x) 解釋為 「 x 的長子」，那么這段敘述可記為：
:\forall x \text{Phil}(x) \Rightarrow \text{Phil}[\text{Son}(x)]
換句話說，\text{Son}(x) 被解釋成「與 x 有特定且唯一對應關係」的某對象（被稱為函數符號）。換句話話說，只要「x就是y」，那「x的長子也會是y的長子」。換句話說：
:(x = y)
\Rightarrow
[\text{Son}(x) = \text{Son}(y)]
這些性質被一階邏輯視為「理所當然」。

類似地，敘述中也有一些「不變的實體」，如苏格拉底，表示這些「實體」的符號被稱為常數符號。例如將 s 解釋為苏格拉底，那「苏格拉底為哲學家」就可以寫成：
:\text{Phil}(s)
所謂的「不變」隱含的代表：
:「蘇格拉底就是蘇格拉底」
:「對所有x，對所有y，如果x就是蘇格拉底，且y就是蘇格拉底，那x就是y」
換句話說
:(s = s)
:\forall x \forall y\{[(x = s) \wedge (y = s) ] \Rightarrow (x = y)\}
這兩個性質也被一階邏輯視為「理所當然」。

形式理論
一階邏輯的形式理論可分成幾個部份：
#：決定哪些符號組合是合式公式。（直觀上的“文法無誤的敘述”）
#推理規則：由合式公式符號組合出新合式公式的規則（直觀上的“推理”）
#公理：一套合式公式（直觀上的基本假設）
基本符號
一套理論能容許多少符號，取決於人類能運用物理定律來塑造多少符號，但目前無法確知宇宙是不是有限，或是以可無限制地分割。雖然所有的公理化集合論都以量詞的形式隱晦的承認跟自然數一樣多的無窮（如ZF集合論的無窮公理），甚至以這樣的可數無窮為基礎，去建構出不可數的實數，但將抽象的理論對應到現實時，還是需要回答物理上有沒有可數或不可數的無窮。所以謹慎起見，如果沒有特別申明的話，以下各種類符號的數目上限都是有限的。

邏輯符號
一階邏輯通常擁有以下的符號：

#量化符號 \forall 及 \exists
#*某些作者會把 \exists 符號定義為 \exists x\mathcal{A}:= \neg[\forall x(\neg\mathcal{A})]，如此便只需要 \forall 做為基礎符號。
#邏輯聯結詞：以下為可能的表示符號（关于波蘭表示法下的邏輯連接詞，請參見逻辑运算的波兰记法）：
#*否定： \neg 或 \sim 或－
#*條件：\Rightarrow 或 \rightarrow 或 \supset
#*且：\land 或 \&
#或：\lor 或 ||*
#*雙條件：\Leftrightarrow 或 \harr
#*某些作者會作如下的符號定義：
#::\mathcal{A}\wedge\mathcal{B}:=\neg(\mathcal{A}\Rightarrow(\neg\mathcal{B})),
#::\mathcal{A}\vee\mathcal{B}:=(\neg\mathcal{A})\Rightarrow\mathcal{B},
#::\mathcal{A}\Leftrightarrow\mathcal{B}:=(\mathcal{A}\Rightarrow\mathcal{B})\wedge(\mathcal{B}\Rightarrow\mathcal{A}),
#::如此一來只需要否定和條件做為基礎符號。
#標點符號：括號、逗號及其他，依作者的喜好有所不同。
#*為了更有效的將括號做配對，通常還會採用大括號{ }跟中括號[ ]。
#至多跟自然數一樣多的變數，通常標記為英文字母末端的小寫字母x、y、z、…，也常會使用下標（或上標、上下標兼有）來區別不同的變數：x0、x1、x2、…（特別注意c有時候會被當成常數符號而引起混淆）。
#等式符號：=
#*有作者會因為語義上对“相等”的不同解释，而將等式符號視為雙元斷言符號、甚至是某種合式公式的簡寫。
#符號相等：\asymp
#*某些作者會額外採用這個符號來表示符號辨識上的等同以便與等式符號作區別。

並非所有的符號都不可或缺的，像謝費爾豎線「 | 」（或異或）可以用來定義量詞以外的所有邏輯符號，換句話說：
{{math_theorem
| name = 符號定義
| math_statement =

(\neg \mathcal{A}) := (\mathcal{A} | \mathcal{A})

(\mathcal{A} \Rightarrow \mathcal{B}) := \mathcal{A} | (\mathcal{B} | \mathcal{B})

(\mathcal{A} \wedge \mathcal{B}) := [\,(\mathcal{A} | \mathcal{B}) |(\mathcal{A} | \mathcal{B})\,]

(\mathcal{A} \vee \mathcal{B}) := [\,(\mathcal{A} | \mathcal{A}) |(\mathcal{B} | \mathcal{B})\,]
}}
另外，一些作者不區分語義解釋和形式理論，所以會將表示真值的符號納入形式理論裡，也就是說，用 T 、Vpq 或 \top 來表示「真」，並用 F 、 Opq 或 \bot 來表示「假」。

斷言符號
「他們兩人是夫妻」，是一個關於兩個“對象”的斷言，而「他是人」、「三點共線」则表明斷言容許一個或者多個對象。所以對於自然數 n 、j 約定：
:A^n_j(x_1,\,x_2,\,...,\,x_n)
為一階邏輯的合法詞彙。它在直觀上表示一個有 n 個“對象”的斷言，稱為 n 元斷言符號。下標的自然數 j 只是拿來和其他同為 n 元的斷言符號作區別。

實用上只要有申明，不至於和其他詞彙引起混淆的話，可以用任意的形式簡寫一個斷言符號。如：公理化集合論裡的雙元斷言符號 A^2_1(x,\,y) 也可以表示为 x\in y 。

函數符號
「物體的顏色」、「夫妻的長子」这种断言說明了一组對象所唯一對應的對象。但不同的夫妻有不同的長子；不同的物體有不同的顏色。據此，形式上對於自然數 n 、j 約定：
:f^n_j(x_1,\,x_2,\,...,\,x_n)
為一階邏輯的合法詞彙，直觀上表示 n 個“對象”所對應到的東西，稱它為 n 元函數符號。需要特別注意，這種“唯一對應”的直觀想法，必須配上關於“等式”的性質（詳見下面的等式定理章节），才能在形式理論中被實現。

与斷言符號一样，只要不引起混淆，就可以用任何的形式簡寫函數符號。如：公理化集合論裡的 x\cup y 是依據聯集公理而定義的新函數符號（請參見下面函數符號與唯一性章節），也可以冗長的表記為 f^2_j(x,\,y) 。

常數符號
「刻度0」、「原點」、「蘇格拉底」是直觀上＂唯一不變＂的對象。據此，對自然數 j 約定
:c_j
為一階邏輯的合法詞彙，直觀上表示一個“唯一不變”的對象，稱為常數符號。同樣的。“常數的不變性”需配上等式的性質（詳見下面等式定理）才能被實現。

為了不和變數的表記混淆，常數符號一樣可以用任何的形式簡寫，如公理化集合論裡的 \varnothing 是根據空集公理和函數符號與唯一性，而定義的新常數符號。亦可冗長的表示為 c_j 。

語法
和自然語言（如英語）不同，一階邏輯的語言以明確的遞迴定義判斷一個給定的詞彙是否合法。大致上來說，一階邏輯以「項」代表討論的對象，而對「項」的斷言組成了最基本的原子（合式）公式；而原子公式和邏輯符號組成了更複雜的合式公式（也就是“敘述”）。

項
「那對夫妻的長子的職業」、「(x+y)\times z」、「x\cup\varnothing」代表變數可以與函數符號組成更一般的物件。據此形式，遞迴地規定一類合法詞彙——項為：

習慣上以大寫的西方字母（如英文字母、希伯來字母、希臘字母）代表項，如果變數不得不採用大寫字母，而可能跟項引起混淆的話，需額外規定分辨的辦法。

原子公式
為了比較簡潔地規定甚麼是合式公式，先規定原子公式為：（若 T_1,\,....,\,T_n 是項）
:A^n_j(T_1,\,....,\,T_n)
這樣的形式。

公式
一階邏輯的合式公式（簡稱公式或 wf ）以下面的規則遞迴地定義：

{{math_theorem
| name = 遞迴定義
| math_statement =

#原子公式為公式。（美觀起見，在原子公式外面包一層括弧也是公式）
#若 \mathcal{A} 為公式，則 (\neg\mathcal{A}) 為公式。
#若 \mathcal{A} 與 \mathcal{B} 為公式，則 (\mathcal{A}\Rightarrow\mathcal{B}) 為公式。
#若 \mathcal{A} 為公式， x 為任意變數，則 (\forall x\mathcal{A}) 為公式。 （美觀起見 (\forall x)\mathcal{A}:=\forall x\mathcal{A}，也就是裡面的量詞有無外包括弧都是公式）
#合式公式只能通过以上四點，於有限步驟內建構出來。
}}

另外成對的中括弧跟大括弧，符號辨識上視為成對的小括弧，而草書的大寫西方字母為公式的代號。

舉例來說，
:\{(\forall y)A^2_1[x,\,f^1_1(y)]\}
是公式而
:\forall x\, x \Rightarrow
則不是公式。

而接下來只要對任意公式\mathcal{A} 、 \mathcal{B} 與變數 x，做以下符號定義

{{math_theorem
| name = 符號定義
| math_statement =

(\mathcal{A}\wedge\mathcal{B}):=\{\neg[\mathcal{A}\Rightarrow(\neg\mathcal{B})]\}

(\mathcal{A}\vee\mathcal{B}):=[(\neg\mathcal{A})\Rightarrow\mathcal{B}]

(\mathcal{A}\Leftrightarrow\mathcal{B}):=[(\mathcal{A}\Rightarrow\mathcal{B})\wedge(\mathcal{B}\Rightarrow\mathcal{A})]

(\exists x\mathcal{A}):=\{\neg[\forall x(\neg\mathcal{A})]\} （同樣美觀起見 (\exists x)\mathcal{A}:=\exists x\mathcal{A}）
}}

這樣所有的邏輯連接詞與量詞就納入了合式公式的規範。

施用
所謂的施用/作用，是以下公式形式的口語說法：（其中 \mathcal{A} 與 \mathcal{B} 都是公式）

*(\neg\mathcal{A}) 稱為 \neg 施用於 \mathcal{A} 上。
*(\mathcal{A}\Rightarrow\mathcal{B}) 稱為 \Rightarrow 施用於 \mathcal{A} 和 \mathcal{B} 上。
*(\mathcal{A}\wedge\mathcal{B}) 稱為 \wedge 施用於 \mathcal{A} 和 \mathcal{B} 上。
*(\mathcal{A}\vee\mathcal{B}) 稱為 \vee 施用於 \mathcal{A} 和 \mathcal{B} 上。
*(\mathcal{A}\Leftrightarrow\mathcal{B}) 稱為 \Leftrightarrow 施用於 \mathcal{A} 和 \mathcal{B} 上。
*(\forall x\mathcal{A}) 稱為 \forall x 施用於 \mathcal{A} 上。
*(\exists x\mathcal{A}) 稱為 \exists x 施用於 \mathcal{A} 上。

就类似于運算子作用在它們身上。

自由變數和約束變數
量詞所施用的公式被稱為量詞的範圍（scope）。同一個變數在公式一般來說不只出現一次，若變數 x 出現在 \forall x 的範圍內，稱這樣出現的 x 為不自由/被約束的 x （not free/bounded）；反過來說，不出現在 \forall x 的範圍內的某個 x 被稱為自由的 x。

例如，對於公式：
:\{(\forall x)[A^1_1(x)\Rightarrow A^1_2(y)]\}
[A^1_1(x)\Rightarrow A^1_2(y)] 就是量詞 \forall x 的範圍；而 A^1_1(x) 裡的 x 就是不自由的；反之 A^1_2(y) 裡的 y 就是自由的。

說 x 於公式 \mathcal{A} 完全自由，意為於 \mathcal{A} 出現的 x 都是自由的；反之，說 x 於公式 \mathcal{A} 完全不自由/完全被約束，意為 \mathcal{A} 內根本沒有 x ，或是 \mathcal{A} 內沒有自由的 x 。若 \mathcal{A} 內所有的變數都完全不自由，\mathcal{A} 特稱為封閉公式/句子（closed formula/sentence）。

括弧的簡寫
括弧是為了保證語意解釋符合預期，但太多的括弧書寫不易，為此規定以下的“重構法”（反過來就是“簡寫法”），從表面上不合法的一串符號找出作者原來想表達的公式：
*若整串符號的括弧不成對，直接視為無法重構。
*以\lnot,\,\land,\,\lor,\,\forall,\,\exists,\,\Rightarrow,\,\Leftrightarrow（左至右）的施用順序重構括弧。
*相鄰的邏輯連接詞或量詞無法決定施用順序的話，以右邊為先。
*重構施用的順序，以被成對括弧包住的部分為優先施用，其次才是落單的斷言符號。

舉例來說
:\lnot [\forall x A^1_1(x)] \Rightarrow \exists x \lnot A^1_2(x)
的重構過程如下
:#\{\lnot [\forall x A^1_1(x)]\} \Rightarrow \exists x [\lnot A^1_2(x)] （優先施用 \lnot）
:#\{\lnot [\forall x A^1_1(x)]\} \Rightarrow \{\exists x [\lnot A^1_2(x)]\} （施用 \exists）
:#\{\{\lnot [\forall x A^1_1(x)]\} \Rightarrow \{\exists x [\lnot A^1_2(x)]\}\} （最後施用 \Rightarrow）

可以被重構為公式的一串符號則寬鬆的認定為“合式公式”。（最明顯的例子就是合式公式最外層的括弧可以省略）

波蘭表示法
波蘭表示法將邏輯連接詞前置於被施用的公式而非傳統的中間。如果沿用以上的＂施用順序＂，這個表示法允許捨棄所有括弧。如公式
:\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]\}\}
轉成波蘭表示法的過程如下
:\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 （轉成波蘭表示法的順序）
:\Pi x\Pi y\text{C} A^1_1 f^1_1 x\text{N}\text{C} A^1_1 x A^3_1 f^1_1 y x z （邏輯連結詞的符號轉換）

推理规则
一階邏輯通常只有以下的推理規則（因為將普遍化視為推理規則會有不直觀的限制）
{{math_theorem
|name=MP律
|math_statement=
對於公式 \mathcal{A} 和 \mathcal{B} 有
:\mathcal{A}\Rightarrow\mathcal{B} 和 \mathcal{A} 組合出 \mathcal{B}。
}}
直觀意義非常明顯，就是p=>q且p可以推出q。

在只以謝費爾豎線「 | 」為基礎邏輯連接詞的公理系统裡，MP律會被改寫成
{{math_theorem
|name=修改的MP律
|math_statement=
對於公式 \mathcal{A} 、\mathcal{B} 和 \mathcal{C} 有
\mathcal{A} | (\mathcal{C} | \mathcal{B}) 和 \mathcal{A} 組合出 \mathcal{B}。
}}
公理
邏輯公理
{{math_theorem
|name=公理
|math_statement=
如果\mathcal{B}、\mathcal{C}、\mathcal{D}都是公式，則：
*（A1） \mathcal{B}\Rightarrow(\mathcal{C}\Rightarrow\mathcal{B})
*（A2） [\mathcal{B}\Rightarrow(\mathcal{C}\Rightarrow\mathcal{D})]\Rightarrow[(\mathcal{B}\Rightarrow\mathcal{C})\Rightarrow(\mathcal{B}\Rightarrow\mathcal{D})]
*（A3） [(\neg\mathcal{B})\Rightarrow(\neg\mathcal{C})]\Rightarrow[(\neg\mathcal{B}\Rightarrow\mathcal{C})\Rightarrow\mathcal{B}]
都是公理。
}}
它们实际上是公理模式，代表著“跟自然數一樣多”條的公理。

在有（A1）與（A2）的前提下，（A3）等價於以下的公理模式：（證明請參見下面否定一節。）
{{math_theorem
|name=（T1）
|math_statement=
[\,(\neg \mathcal{B}) \Rightarrow (\neg \mathcal{C})\,]
\Rightarrow
(\mathcal{B} \Rightarrow \mathcal{C})
}}
另外，在只以謝費爾豎線「 | 」為基礎邏輯連接詞的公理系统裡，上面三條公理模式等價於下面這條公理模式

一阶逻辑的限制
所有数学概念都有它的强项和弱点；下面列出一阶逻辑的一些问题。

难于表达if-then-else
带有等式的FOL不包含或允许定义if-then-else斷言或函数if（c,a,b），这裡的c是表达为公式的条件，而a和b是要么都是项要么都是公式，并且它的结果是a如果c为真，或者b如果它为假。问题在于FOL中，斷言和函数二者只接受（“非布尔类型”）项作为参数，而条件的明确表达是（“布尔类型”）公式。这是不幸的，因为很多数学函数是依据if-then-else而方便的表达的，而if-then-else是描述大多数计算机程序的基础。

在数学上，有可能重定义匹配公式算子的新函数的完备集合，但是这是非常笨拙的。
斷言if（c,a,b）如果重写为(c \wedge a) \lor (\neg c \wedge b)就可以在FOL中表达，但是如果条件c是复杂的这就是笨拙的。很多人扩展FOL增加特殊情况斷言叫做“if（条件，a, b）”（这里a和b是公式）和／或函数“ite（条件，a, b）”（这裡的a和b是项），它们都接受一个公式作为条件，并且等于a如果条件为真，或b如果条件为假。这些扩展使FOL易于用于某些问题，并使某类自动定理证明更容易。
其他人进一步扩展FOL使得函数和斷言可以在任何位置接受项和公式二者。

类型（种类）
除了在公式（“布尔类型”）和项（“非布尔类型”）之间的区别之外，FOL不包括类型（种类）到自身的概念中。
某些人争辩说缺乏类型是巨大优点
，而很多其他人发觉了定义和使用类型（种类）的优点，比如帮助拒绝某些错误或不想要的规定
。
想要指示类型的那些人必须使用在FOL中可获得的符号来提供这种信息。这么做使得这种表达更加复杂，并也容易导致错误。

单一参数斷言可以用来在合适的地方实现类型的概念。例如：
:\forall x (Man(x) \rightarrow Mortal(x))，
斷言Man（x）可以被认为是一类“类型断言”（就是说，x必须是男人）。
斷言还可以同指示类型的“存在”量词一起使用，但这通常应当转而与逻辑合取算子一起来做，比如：
:\exists x (Man(x) \wedge Mortal(x))（“存在既是男人又是人类的事物”）。
容易写成\exists x Man(x) \rightarrow Mortal(x)，但这将等价与\exists x \neg Man(x) \lor \exists x Mortal(x)（“存在不是男人的事物或者存在是人类的事物”），这通常不是想要的。类似的，可以做一个类型是另一个类型的子类型的断言，比如：
:\forall x (Man(x) \rightarrow Mammal(x))（“对于所有x，如果x是男人，则x是哺乳动物）。

难于刻画模型大小
从Löwenheim–Skolem定理得出在一阶逻辑中不可能刻画有限性或可数性。若一階理論有任意有限大的模型，則也有無窮大的模型，所以說不能刻劃有限性。而若理論有某個無窮基數大小的模型，則也必有任意更大的模型，所以不能刻劃可數性。另一個例子，是無法用一階語言將實數系公理化，因為不論用何種一階理論描述，既然該理論有實數系此種無窮模型（大小為2^{\aleph_0}），所以必有比實數系更大（比如2^{2^{\aleph_0}}）的另一個模型，從而該理論不是（唯一地）刻劃實數系的性質。實數系滿足的公理中，有上确界性质一項，它声称实数的所有有界的、非空集合都有上确界。一階邏輯祗能對元素量化，但此公理中，要對模型的全部子集量化，这就需要二阶逻辑了。

图可及性不能表达
很多情况可以被建模为节点和有向连接（边）的图。例如，效验很多系统要求展示不能从“好”状态触及到“坏”状态，而状态的相互连接经常可以建模为图。但是，可以证明这种可及性不能用斷言逻辑完全表达。换句话说，没有斷言逻辑公式f，带有u和v作为它的唯一自由变量，而R作为它唯一的（2元）斷言符号，使得f在一个有向图中成立，如果在这个图中存在从关联于u的节点到关联于v的节点的路径。

参见

  • 真值表
  • 逻辑等价
  • 逻辑条件
  • 逻辑与非
  • 逻辑或非
  • 数理逻辑
  • 零阶逻辑
  • 一阶语言
  • 二階邏輯
  • 布尔函数
  • 推理规则列表
  • 哥德尔完备性定理
  • 哥德尔不完备定理

参考文献
引用
来源

  • Jon Barwise and John Etchemendy，2000. Language Proof and Logic. CSLI (University of Chicago Press) and New York: Seven Bridges Press.
  • David Hilbert and Wilhelm Ackermann 1950. Principles of Theoretical Logic（English translation）. Chelsea. The 1928 first German edition was titled Grundzüge der theoretischen Logik.
  • Wilfrid Hodges, 2001, "Classical Logic I: First Order Logic", in Lou Goble, ed., The Blackwell Guide to Philosophical Logic. Blackwell.

外部链接

#數理邏輯 #形式逻辑系统

评论 (0)

  • 还没有评论，来抢沙发吧。