直覺主義邏輯
直覺主義邏輯或構造性邏輯是最初由阿蘭德·海廷開發的為魯伊茲·布勞威爾的數學直覺主義計劃提供形式基礎的符號邏輯。這個系統保持跨越生成導出命題的變換的證實性而不是真理性。從實用的觀點，也有使用直覺邏輯的強烈動機，因為它有存在性質，這使它還適合其他形式的數學構造主義。
語法
直覺邏輯的公式的語法類似於命題邏輯或一階邏輯。但是直覺邏輯的連結詞不像經典邏輯那樣是可互定義的，因此它們的選擇是重要的。在直覺命題邏輯中通常使用 →, ∧, ∨, ⊥ 作為基本連結詞，把 ¬ 作為 ¬A = (A → ⊥) 的簡寫處理。在直覺一階邏輯中量詞 ∃, ∀ 都是需要的。
不同在於很多經典邏輯的重言式在直覺邏輯中不再是可證明的。例子不只包括排中律 P ∨ ¬P，還有皮爾士定律 ((P → Q) → P) → P，甚至還有雙重否定除去。在經典邏輯中，P → ¬¬P 和 ¬¬P → P 二者都是定理。在直覺邏輯中，只有前者是定理: 雙重否定可以介入但不能除去。
對很多經典有效重言式不是直覺邏輯的定理的觀察導致了弱化經典邏輯的證明論的想法。
相繼式演算
根岑發現簡單限制他的系統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)定義它們四個。類似的，在經典一階邏輯中，一個量詞可以依據另一個量詞和否定來定義。
這是二值原理的推論，它使得這種連結詞僅僅是布爾函數。二值原理在直覺邏輯中不成立，只有無矛盾律成立。作為結果沒有連結詞可以豁免，而上述公理都是必須的。多數經典恆等式只是直覺邏輯中在一個方向上的定理，儘管某些定理是兩個方向的。它們如下:
合取與析取:
合取與蘊涵:
析取與蘊涵:
全稱量詞與存在量詞:
所以，例如 「a 或 b」是比「如果非 a 則 b」更強的陳述，而在經典邏輯中它們是可互換的。
據 Alexander Kuznetsov 的證明，任一下述定義的連結詞可以充當直覺邏輯的自足算子:[1]
語義
語義要比經典邏輯更加複雜。其模型論可給出自海廷代數或等價的給出自克里普克語義。
海廷代數語義
在經典邏輯中，我們經常討論一個公式可能接受的真值。這種值通常被選擇為布爾代數的成員。在布爾代數中的交和並算子等同於∧和∨邏輯連結詞，所以形如A ∧ B的公式是在布爾代數中A的值和B的值的交。所以我們就有了一個有用的定理，一個公式是經典邏輯的有效的句子/斷定，若且唯若它的值對於任何賦值都是1---就是說，對它的變量的任何指派都是真。
對於直覺邏輯對應的法則也是真的，但是不再對每個公式指派（assign）來自布爾代數的值，而是使用來自海廷代數的值，布爾代數是它的特殊情況。公式在直覺邏輯中是有效的，若且唯若它對於在任何海廷代數上的任何賦值總是得到值1。
可以證實為了識別有效的公式，考慮其元素是實平面R2的開集的一個單一的海廷代數就足夠了。在這種代數中，∧和∨算子對應於集合的交集和併集，並且指派給公式A→B的值是 (AC ∪ B)o，它是B的值和A的值的補集的併集的內部。底元素是ø，頂元素是整個平面R2。¬A定義為A→ø，所以指派給它的值是ACo，這是A的值的補集的內部。通過這些指派，直覺上有效的公式正好就是被指派為整個平面的值的公式。
例如，公式¬(A ∧ ¬A)是有效的，因為不管為公式A選擇什麼集合X作為值，¬(A ∧ ¬A)的值總是被證實為整個平面：
- Value(¬(A ∧ ¬A)) =
- (Value(A ∧ ¬A))C° =
- (Value(A) ∩ Value(¬A))C° =
- (X ∩ (Value(A))C°)C° =
- (X ∩ XC°)C°
一個拓撲學定理告訴我們XC°是XC的子集，所以交集為空，因此：
- øC° =(R2)° = R2
所以這個公式的賦值是真，這個公式確實是有效的。
但是排中律A∨¬A，可以被證實是「無效的」，通過設定A的值是{y : y > 0 }。那麼¬A的值是{y : y ≤ 0 }的內部，它就是{y : y < 0 }，而公式的值是{y : y > 0 }和{y : y < 0 }的併集，這「不」是整個平面。
上面描述的無限海廷代數對所有直覺上有效的公式給出了真賦值，而不管為公式中的變量指派了什麼值。反過來說，對於每個無效的公式，都有來對變量的來自這個代數的一個值指派生成這個公式的一個假賦值。可以證實沒有有限的海廷代數有這個性質。
克里普克語義
建立在他關於模態邏輯的語義的工作之上，索爾·阿倫·克里普克為直覺邏輯建立了另一套語義，叫做克里普克語義或關係語義[2]。
數學的建構主義
在古典邏輯的語義中，無論我們是否擁有對任何命題其中敘述情況的直接證據，命題公式都是從僅有兩元素的集合 （即為「true」 和「false」）而評估其真值。這被稱之為「排中律」：因為它摒除了「為真」 或「為假」 之外的其它任何值存在的可能性。相較之下，直覺主義邏輯中的命題公式並不賦予明確的真值，只有在我們有直接證據時才被認為是 「真實的」，因此才具有證明。（我們也可說命題是由直接證據才據以成立，而並非命題公式本身的敘述就是「真」，它是由柯里-霍華德同構意義上的證據所支持的。）直覺主義邏輯中的操作因此保留了證據和可證明性方面的證據，而不單只執行真值的運算評估。
直覺邏輯是開發數學建構主義方法的常用工具。建構主義邏輯的使用在數學家和哲學家中，一直是個爭議話題（例如，參見 Brouwer-Hilbert 爭議）。共同反對使用它們的意見是上面引用的缺乏古典邏輯的兩個中心規則，即排中律和雙重否定的消除規則。這被認為對大衛·希爾伯特所寫的數學實踐非常重要：「從數學家那裏取走排中律不給他們使用，就像禁止望遠鏡給天文學家，或不允許拳擊手使用他的拳頭。禁止消除雙否的存在陳述和排中律，等於完全放棄數學。」
儘管直覺主義邏輯無法利用，排中律和雙重否定的消除這兩個對古典邏輯貢獻極大的規則，而面臨隨之而來的嚴峻挑戰，但直覺主義邏輯具有實際用途。其中一個原因是它所受的限制，反而因此產生了必須具備存在性的證據，使其也適用於其他形式的數學建構主義。非正式地，這意味着如果存在對象存在的建設性證據，則該構造性證據可用作生成該對象的示例算法，該原理即稱為證明和算法之間的柯里-霍華德同構。直覺邏輯這種特性如此有價值的原因，是它使研究者能夠使用廣泛的計算機化工具，稱為證明輔具。這些工具可以幫助用戶驗證（和生成）大規模的證據，這些證據的大小通常會排除發佈和審查數學證據的常規人工檢查。因此，使用證明輔具（例如 Agda 或 Coq）使現代數學家和邏輯學家能夠開發和證明極其複雜的系統，遠超出那些僅由手工創立和檢查的系統。在這些工具出現之前，無法驗證的著名範例是四色定理的證明。這個定理困擾了數學家一百多年，直到一個證據被開發出來，排除了大量可能的反例，但仍然留下可能性，需要一個計算機程序才能完成證明。這個證據在一段時間內引起爭議，但最終使用 Coq 進行了驗證。
參見
註釋
- ^ Alexander Chagrov, Michael Zakharyaschev, Modal Logic, vol. 35 of Oxford Logic Guides, Oxford University Press, 1997, pp. 58–59.
- ^ Intuitionistic Logic （頁面存檔備份，存於互聯網檔案館）. Written by Joan Moschovakis （頁面存檔備份，存於互聯網檔案館）. Published in Stanford Encyclopedia of Philosophy.
引用
- 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.