遮帕麻與遮米麻

[拼音]：gouzao luoji

[英文]：constructive logic

一種非經典的邏輯系統。它主要由對數學持直覺主義、構造主義或致力於構造性數學研究和發展的數學家和邏輯學家建立和使用。在數理邏輯和數學基礎中，“構造性”一詞有幾種不同的理解並在幾種不同的意義下使用，其共同之處在於它們都滿足下列構造性要求：

（1）對存在命題ヨxAx的一個證明是構造性的，如果從這個證明能找到（構造出）一個特殊的物件x，它滿足A；

（2）不能無條件地使用排中律。按照構造性觀點，對於p∨塡p，只有在有一個方法能判明p與塡p中哪一個是真的情況下，才能承認它是真的，而不承認任一命題非真即假。按照這些構造性觀點建立的邏輯就是構造邏輯。

從構造性觀點看不可接受的證明的例子，如定理：

存在兩個無理數a和b，使得a b 是有理數。該定理的一個非構造性證明是：

或者是有理數或者是無理數，假若

是有理數，取a=b=匇，因匇是無理數，故所取的a和b滿足定理；假若匇是無理數，取

，b=匇，則a和b是無理數且

是有理數，故所取的a和b滿足定理。於是定理得證。從經典的邏輯和數學的觀點看，該證明是無懈可擊的，因而該定理確是成立的。但從構造性的觀點來看，這個證明僅是根據排中律肯定

或者是有理數或者是無理數而作出的，但沒有任何方法指明

究竟是有理數還是無理數，因而也沒有指出究竟怎樣去構造出滿足定理的a和b。因此這個證明不是構造性的，不承認這個定理已經有一個證明。

說明經典邏輯和構造邏輯之間的對照的一個簡單例子，是考慮所謂肯定的蘊涵演算，這個演算只有一個邏輯常項，即蘊涵詞，它有兩個公理和一條推理規則：

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）的理解如下：

（1）對A∧B的一個證明由A的一個證明和B的一個證明一起構成；

（2）對 A∨B的一個證明由特別指定的A的一個證明或者由特別指定的 B的一個證明構成；

（3）對A→B的一個證明由一個構造c構成，構造c可把A的任一證明轉換成B的一個證明，即構造 c具有如果d是A的一個證明，把c與d結合起來就產生 B的一個證明這種性質；

（4）以符號⊥表示一個不可證的命題，對塡A的一個證明由一個構造c構成，構造c把對A的任一證明轉換成對⊥的一個證明；

（5）如果個體變元x取值於某個“基本的”個體域D，則對凬xA(x)的一個證明由一個構造c組成，當把構造c應用於域D中的任一個體d時，就產生對A(d)的一個證明c(d)；

（6）如果個體變元x取值於某個“基本的”個體域D，則對ヨ xA(x)的一個證明由一個構造 c和域D中的一個個體d構成，並且構造 c是對A(d)的一個證明。

在構造邏輯中，各個聯結詞和量詞都是彼此獨立、不能相互定義的。

從20世紀30年代以來，構造邏輯已建立了多個形式系統。其中，K.哥德爾在1958年構作的系統為：