構造邏輯是一種非經典的邏輯系統。它主要由對數學持直覺主義、構造主義或致力於構造性數學研究和發展的數學家和邏輯學家建立和使用。在數理邏輯和數學基礎中，“構造性”一詞有幾種不同的理解並在幾種不同的意義下使用，其共同之處在於它們都滿足下列構造性要求：①對存在命題ヨxAx的一個證明是構造性的，如果從這個證明能找到（構造出）一個特殊的對象x，它滿足A；②不能無條件地使用排中律。按照構造性觀點，對於p∨塡p,只有在有一個方法能判明p與塡p中哪一個是真的情況下，才能承認它是真的，而不承認任一命題非真即假。按照這些構造性觀點建立的邏輯就是構造邏輯。
基本介紹
- 中文名：構造邏輯
- 1：一種非經典的邏輯系統
- 2：對數學持直覺主義
- 3：證明是構造性的
實例
說明經典邏輯和構造邏輯之間的對照的一個簡單例子，是考慮所謂肯定的蘊涵演算，這個演算只有一個邏輯常項，即蘊涵詞，它有兩個公理和一條推理規則：
A1.A→(B→A)；
A2.(A→(B→C))→((A→B)→(A→C))；
規則E.如果A並且A→B，那么B。從構造性數學觀點看，這個系統是足夠的。但是，它並沒有在下述意義上刻劃出作為一個真值函項的蘊涵，即A→B是真的若且唯若 A假或者B真。例如,【((A→B)→A)→A】（即Peirce律）是一個重言式，但它在這個系統中是不能證明的。如果在該系統中增加以下兩個關於否定的公理，能得到就蘊涵和否定而言的構造命題演算。這兩個關於否定的公理為：
A3.(A→塡A)→塡A；
A4.塡A→(A→B)。
但要得到經典命題演算，則需要在上面系統中再增一條公理
A5.塡塡A→A。和排中律一樣，該公理在構造邏輯中也是不成立的。
在構造邏輯中，對於邏輯聯結詞塡（非）、∧（並且）、∨（或者）、→（如果,則，）和量詞ヨx（存在一個 x，有一個x）、凬 x（所有x）的理解如下：①對A∧B的一個證明由A的一個證明和B的一個證明一起構成；②對 A∨B的一個證明由特別指定的A的一個證明或者由特別指定的 B的一個證明構成；③對A→B的一個證明由一個構造c構成，構造c可把A的任一證明轉換成B的一個證明，即構造 c具有如果d是A的一個證明，把c與d結合起來就產生 B的一個證明這種性質；④以符號⊥表示一個不可證的命題,對塡A的一個證明由一個構造c構成,構造c把對A的任一證明轉換成對⊥的一個證明；⑤如果個體變元x取值於某個“基本的”個體域D，則對凬xA(x)的一個證明由一個構造c組成,當把構造c套用於域D中的任一個體d時,就產生對A(d)的一個證明c(d)；⑥如果個體變元x取值於某個“基本的”個體域D，則對ヨ xA(x)的一個證明由一個構造 c和域D中的一個個體d構成，並且構造 c是對A(d)的一個證明。
在構造邏輯中，各個聯結詞和量詞都是彼此獨立、不能相互定義的。
從20世紀30年代以來，構造邏輯已建立了多個形式系統。其中，K.哥德爾在1958年構作的系統為：
①A,A→B崊B;
②A→B,B→C崊A→C;
③A∨A→A,A→A∧A;
④A→A∨B,A∧B→A;
⑤A∨B→B∨A,A∧→B∧A;
⑥A→B崊C∨A→C∨B;
⑦A∧B→C崊A→(B→C)
⑧A→(B→C)崊A∧B→C;
⑨⊥→A;
⑩B→A(x)崊B→凬xA(x)（x在 B中不自由出現）；
?凬xA(x)→A(t)（t對於A中的x自由）；
?A(t)→ヨxA(x)（t對於A中的x自由）；
?A(x)→B崊ヨxA(x)→B（x在 B中不自由出現），其中的崊為元數學符號。
