哥德尔转换

将古典逻辑CQC嵌入直觉主义逻辑IQC中的一种“否定性转换”(即，结果公式中不出现∨和、并且原子公式在其中只以否定形式出现的一种转换)。最初由K．哥德尔在1933年的论文中提出，用来建立古典一阶算术PA和直觉主义一阶算术HA之间的一种联系，证明了它们之间的相对协调性。哥德尔转换还被推广到更强的数学理论，例如二阶海廷算术HAS、类型论和集合论。

哥德尔转换将古典逻辑中的任意公式A变成直觉主义逻辑中的公式Ag，具体的递归定义如下：

(1)对于原子公式p，p是p；

(2)(B∧C)是B∧C；

(3)(B→C)是B→C；

(4)(xB)是xB；

(5)(xB)是xB；

(6)(B∨c)是(B∧C)；

这里，假定CQC和IQC都以∧，∨，→，⊥，，为初始符号，否定号则按通常方式由→和上来定义(A即A→⊥)。定义中的(1)可作如下修改：

⊥是⊥；但对于并非⊥的原子公式p，

p仍是p。

在这样的修改下，(A)将是A。利用归纳法，可以证得下面的定理：

定理．对于一切公式A，

(1)┝AA；

(2)Γ┝A当且仅当Γ┝A，这里Γ=｛B∶B∈Γ｝。

MQC指极小谓词逻辑，也就是从CQC中去掉公理A→A或与其等价的规则而得的逻辑系统。称一公式为否定性的，如果它不出现∨和，并且原子公式在其中只以否定形式出现。由上面的定理可知，古典逻辑和直觉主义逻辑关于否定性公式是等价的；也就是说，对于任意的否定性公式，CQC┝A当且仅当IQC┝A。由于CQC中的任意公式都等价于某个否定性公式，CQC也就在某种意义上被含于IQC。

在上述哥德尔转换g的递归定义中增加一条：

()(t=s)是t=s；

就得到将古典一阶算术嵌入直觉主义一阶算术的转换。对此，有下面的定理：

定理 对于一切公式A，

(1)PA┝A当且仅当HA┝A；

　 PA┝AA；

(2)如果A中不出现∨和，那么

　 HA┝A当且仅当PA┝A。

由此可知，古典一阶算术和直觉主义一阶算术是相对协调的。定理中的(2)还表明，有许多在PA中能证明的定理可以毫无困难地直接转到HA中。