查看“︁直觉主义逻辑”︁的源代码

'''直觉主义逻辑'''或'''构造性逻辑'''是最初由[[阿蘭德·海廷]]开发的为[[鲁伊兹·布劳威尔]]的[[数学直觉主义]]计划提供形式基础的[[符号逻辑]]。这个系统保持跨越生成导出命题的变换的[[证实理论|证实性]]而不是[[真理|真理性]]。从实用的观点，也有使用直觉逻辑的强烈动机，因为它有[[存在性质]]，这使它还适合其他形式的[[数学构造主义]]。

==语法==
[[File:Rieger-Nishimura.svg|thumb|right|280px| Rieger-Nishimura 格。它的節點是不別直覺邏輯等價之異的一元命題公式，按直覺邏輯蘊含排序。]]
直觉逻辑的公式的[[语法]]类似于[[命题逻辑]]或[[一阶逻辑]]。但是直覺邏輯的連結詞不像[[經典邏輯]]那樣是可互定義的，因此它們的選擇是重要的。在直覺命題邏輯中通常使用 →, ∧, ∨, ⊥ 作為基本連結詞，把 ¬ 作為 {{nowrap|1=¬''A'' = (''A'' → ⊥)}} 的簡寫處理。在直覺一階邏輯中量詞 ∃, ∀ 都是需要的。

不同在于很多经典逻辑的[[重言式]]在直觉逻辑中不再是可证明的。例子不只包括[[排中律]] ''P'' ∨ ¬''P''，还有[[皮尔士定律]] ((''P'' → ''Q'') → ''P'') → ''P''，甚至还有[[双重否定除去]]。在经典逻辑中，''P'' → ¬¬''P'' 和 ¬¬''P'' → ''P'' 二者都是定理。在直觉逻辑中，只有前者是定理: 双重否定可以介入但不能除去。

对很多经典有效重言式不是直觉逻辑的定理的观察导致了弱化经典逻辑的证明论的想法。

=== 相继式演算 ===
{{main|相继式演算}}
[[格哈德·根岑|根岑]]发现简单限制他的系统LK（他的经典逻辑的相继式演算）就导致了关于直觉逻辑的一个可靠和完备的系统。他称之为系统LJ。

=== 希尔伯特式演算 ===

推理规则是[[肯定前件]]，公理有:
* THEN-1: φ → (χ → φ)
* THEN-2: (φ → (χ → ψ)) → ((φ → χ) → (φ → ψ))
* AND-1: φ ∧ χ → φ
* AND-2: φ ∧ χ → χ
* AND-3: φ → (χ → (φ ∧ χ))
* OR-1: φ → φ ∨ χ
* OR-2: χ → φ ∨ χ
* OR-3: (φ → ψ) → ((χ → ψ) → (φ ∨ χ → ψ))
* NOT-1: (φ → χ) → ((φ → ¬χ) → ¬ φ)
* NOT-2: φ → (¬φ → χ)

对于一阶逻辑系统还要加上[[普遍化|普遍化规则]]，和如下公理:

* PRED-1: (∀''x'' ''Z''(''x'')) → ''Z''(''t'')
* PRED-2: ''Z''(''t'') → (∃''x'' ''Z''(''x''))
* PRED-3: (∀''x'' (''W'' → ''Z''(''x''))) → (''W'' → ∀''x'' ''Z''(''x''))
* PRED-4: (∀''x'' (''Z''(''x'') → ''W'')) → (∃''x'' ''Z''(''x'') → ''W'')

=== 算子的不可互定义性 ===

在经典命题逻辑中，有可能选取[[逻辑合取|合取]]、[[逻辑析取|析取]]或[[实质蕴涵|蕴涵]]中的一个作为原始的，并依据它和[[逻辑否定|否定]]来定义另两个，比如在[[扬·武卡谢维奇]]的[[命题逻辑#简单的公理系统|命题逻辑三公理]]中。甚至可以依据[[自足算子]]比如[[皮尔士箭头]](NOR)或[[Sheffer竖线]](NAND)定义它们四个。类似的，在经典一阶逻辑中，一个量词可以依据另一个量词和否定来定义。

这是[[二值原理]]的推论，它使得这种连结词仅仅是[[布尔函数]]。二值原理在直觉逻辑中不成立，只有[[无矛盾律]]成立。作为结果没有连结词可以豁免，而上述公理都是必须的。多数经典恒等式只是直觉逻辑中在一个方向上的定理，尽管某些定理是两个方向的。它们如下:

合取与析取:
* <math>(\phi \wedge \psi) \to \neg (\neg \phi \vee \neg \psi)</math> 
* <math>(\phi \vee \psi) \to \neg (\neg \phi \wedge \neg \psi)</math>
* <math>(\neg \phi \vee \neg \psi) \to \neg (\phi \wedge \psi)</math>
* <math>(\neg \phi \wedge \neg \psi) \leftrightarrow \neg (\phi \vee \psi)</math>
合取与蕴涵:
* <math>(\phi \wedge \psi) \to \neg (\phi \to \neg \psi)</math>
* <math>(\phi \to \psi) \to \neg (\phi \wedge \neg \psi)</math>
* <math>(\phi \wedge \neg \psi) \to \neg (\phi \to \psi)</math>
* <math>(\phi \to \neg \psi) \leftrightarrow \neg (\phi \wedge \psi) </math>
析取与蕴涵:
* <math>(\phi \vee \psi) \to (\neg \phi \to \psi)</math>
* <math>(\neg \phi \vee \psi) \to (\phi \to \psi)</math>
* <math>\neg (\phi \to \psi) \to \neg (\neg \phi \vee \psi)</math>
* <math>\neg (\phi \vee \psi) \leftrightarrow \neg (\neg \phi \to \psi)</math>
全称量词与存在量词:
* <math>(\forall x \ \phi(x)) \to \neg (\exist x \ \neg \phi(x))</math>
* <math>(\exist x \ \phi(x)) \to \neg (\forall x \ \neg \phi(x))</math>
* <math>(\exist x \ \neg \phi(x)) \to \neg (\forall x \ \phi(x))</math>
* <math>(\forall x \ \neg \phi(x)) \leftrightarrow \neg (\exist x \ \phi(x))</math>

所以，例如 “a 或 b”是比“如果非 a 则 b”更强的陈述，而在经典逻辑中它们是可互换的。

據 [[Alexander Kuznetsov]] 的證明，任一下述定義的連結詞可以充當直覺邏輯的自足算子:<ref>Alexander Chagrov, Michael Zakharyaschev, ''Modal Logic'', vol. 35 of Oxford Logic Guides, Oxford University Press, 1997, pp. 58–59.</ref>
* <math>((p\lor q)\land\neg r)\lor(\neg p\land(q\leftrightarrow r)),</math>
* <math>p\to(q\land\neg r\land(s\lor t)).</math>

==语义==
语义要比经典逻辑更加复杂。其模型论可给出自[[海廷代数]]或等价的给出自[[克里普克语义]]。

===海廷代数语义===

在经典逻辑中，我们经常讨论一个公式可能接受的[[真值]]。这种值通常被选择为[[布尔代数]]的成员。在布尔代数中的交和并算子等同于∧和∨逻辑连结词，所以形如''A'' ∧ ''B''的公式是在布尔代数中''A''的值和''B''的值的交。所以我们就有了一个有用的定理，一个公式是经典逻辑的有效的句子/断定，当且仅当它的值对于任何[[賦值 (邏輯)|賦值]]都是1---就是说，对它的变量的任何指派都是真。

对于直觉逻辑对应的法则也是真的，但是不再对每个公式指派（assign）来自布尔代数的值，而是使用来自[[海廷代数]]的值，布尔代数是它的特殊情况。公式在直觉逻辑中是有效的，当且仅当它对于在任何海廷代数上的任何賦值总是得到值1。

可以证实为了识别有效的公式，考虑其元素是实平面''R''<sup>2</sup>的[[开集]]的一个单一的海廷代数就足够了。在这种代数中，∧和∨算子对应于集合的交集和并集，并且指派给公式''A''→''B''的值是 (''A''<sup>C</sup> ∪ B)<sup>o</sup>，它是B的值和A的值的[[补集]]的并集的[[内部]]。底元素是ø，顶元素是整个平面''R''<sup>2</sup>。¬''A''定义为''A''→ø，所以指派给它的值是''A''<sup>C</sup><sup>o</sup>，这是''A''的值的补集的[[内部]]。通过这些指派，直觉上有效的公式正好就是被指派为整个平面的值的公式。

例如，公式¬(''A'' ∧ ¬''A'')是有效的，因为不管为公式''A''选择什么集合''X''作为值，¬(''A'' ∧ ¬''A'')的值总是被证实为整个平面：

: Value(¬(''A'' ∧ ¬''A'')) =
: (Value(''A'' ∧ ¬''A''))<sup>''C''</sup>° =
: (Value(''A'') ∩ Value(¬''A''))<sup>''C''</sup>° =
: (''X'' ∩ (Value(''A''))<sup>''C''</sup>°)<sup>''C''</sup>° =
: (''X'' ∩ ''X''<sup>''C''</sup>°)<sup>''C''</sup>°

一个[[拓扑学]]定理告诉我们''X''<sup>''C''</sup>°是''X''<sup>''C''</sup>的子集，所以交集为空，因此：

: ø<sup>''C''</sup>° =(''R''<sup>2</sup>)° = ''R''<sup>2</sup>

所以这个公式的賦值是真，这个公式确实是有效的。

但是排中律''A''∨¬''A''，可以被证实是“无效的”，通过设定''A''的值是{''y'' : ''y'' > 0 }。那么¬''A''的值是{''y'' : ''y'' ≤ 0 }的内部，它就是{''y'' : ''y'' < 0 }，而公式的值是{''y'' : ''y'' > 0 }和{''y'' : ''y'' < 0 }的并集，这“不”是整个平面。

上面描述的无限海廷代数对所有直觉上有效的公式给出了真賦值，而不管为公式中的变量指派了什么值。反过来说，对于每个无效的公式，都有来对变量的来自这个代数的一个值指派生成这个公式的一个假賦值。可以证实没有有限的海廷代数有这个性质。

===克里普克语义===
{{main|關係語義}}
建立在他关于[[模态逻辑]]的语义的工作之上，[[索尔·阿伦·克里普克]]为直觉逻辑建立了另一套语义，叫做'''克里普克语义'''或'''关系语义'''<ref name=Mosch-IntLog>[http://www.seop.leeds.ac.uk/archives/spr2004/entries/logic-intuitionistic/ Intuitionistic Logic] {{Wayback|url=http://www.seop.leeds.ac.uk/archives/spr2004/entries/logic-intuitionistic/ |date=20160304075623 }}. Written by [http://www.math.ucla.edu/~joan/ Joan Moschovakis] {{Wayback|url=http://www.math.ucla.edu/~joan/ |date=20210210234438 }}. Published in Stanford Encyclopedia of Philosophy.</ref>。

== 數學的建構主義 ==
在古典邏輯的語義中，無論我們是否擁有對任何命題其中敘述情況的直接證據，命題公式都是從僅有兩元素的集合 <math>\{\top, \bot\}</math>（即為“true” 和“false”）而評估其[[真值]]。這被稱之為“[[排中律]]”：因為它摒除了“為真” 或“為假” 之外的其它任何值存在的可能性。相較之下，直覺主義邏輯中的命題公式並不賦予明確的真值，只有在我們有直接證據時才被認為是 “真實的”，因此才具有證明。（我們也可說命題是由直接證據才據以成立，而並非命題公式本身的敘述就是“真”，它是由[[柯里-霍华德同构]]意義上的證據所支持的。）直覺主義邏輯中的操作因此保留了證據和可證明性方面的證據，而不單只執行真值的運算評估。

直覺邏輯是開發數學建構主義方法的常用工具。[[数学构成主义|建構主義]]邏輯的使用在數學家和哲學家中，一直是個爭議話題（例如，參見 Brouwer-Hilbert 爭議）。共同反對使用它們的意見是上面引用的缺乏古典邏輯的兩個中心規則，即排中律和雙重否定的消除規則。這被認為對[[大卫·希尔伯特]]所寫的數學實踐非常重要：“從數學家那裡取走排中律不給他們使用，就像禁止望遠鏡給天文學家，或不允許拳擊手使用他的拳頭。禁止消除雙否的存在陳述和排中律，等於完全放棄數學。”

儘管直覺主義邏輯無法利用，排中律和雙重否定的消除這兩個對古典邏輯貢獻極大的規則，而面臨隨之而來的嚴峻挑戰，但直覺主義邏輯具有實際用途。其中一個原因是它所受的限制，反而因此產生了必須具備存在性的證據，使其也適用於其他形式的數學建構主義。非正式地，這意味著如果存在對象存在的建設性證據，則該構造性證據可用作生成該對象的示例算法，該原理即稱為證明和算法之間的柯里-霍华德同构。直覺邏輯這種特性如此有價值的原因，是它使研究者能夠使用廣泛的計算機化工具，稱為證明輔具。這些工具可以幫助用戶驗證（和生成）大規模的證據，這些證據的大小通常會排除發布和審查數學證據的常規人工檢查。因此，使用證明輔具（例如 Agda 或 Coq）使現代數學家和邏輯學家能夠開發和證明極其複雜的系統，遠超出那些僅由手工創立和檢查的系統。在這些工具出現之前，無法驗證的著名範例是[[四色定理]]的證明。這個定理困擾了數學家一百多年，直到一個證據被開發出來，排除了大量可能的反例，但仍然留下可能性，需要一個計算機程序才能完成證明。這個證據在一段時間內引起爭議，但最終使用 Coq 進行了驗證。

==参见==
* [[直觉主义]]
* [[BHK释义]]
* [[直觉类型论]]
* [[经典逻辑]]
* [[中间逻辑]]
* [[线性逻辑]]
* [[构造性证明]]
* [[Curry-Howard对应]]
* [[可计算性逻辑]]
* [[博弈语义]]

== 注释 ==
{{reflist}}

==引用==
* [[Dirk van Dalen|Van Dalen, Dirk]], 2001, "Intuitionistic Logic," in Goble, Lou, ed., ''The Blackwell Guide to Philosophical Logic''. Blackwell.
* Morten H. Sørensen, Pawel Urzyczyn, 2006, ''Lectures on the Curry-Howard Isomorphism'' (chapter 2: "Intuitionistic Logic").  Studies in Logic and the Foundations of Mathematics vol. 149, Elsevier.

==外部链接==

* [http://plato.stanford.edu/entries/logic-intuitionistic/ Stanford Encyclopedia of Philosophy entry] {{Wayback|url=http://plato.stanford.edu/entries/logic-intuitionistic/ |date=20210426013615 }}

{{Authority control}}
[[Category:數理邏輯|Z]]
[[Category:形式逻辑系统]]