【SEP】数学与哲学直觉主义（一） (11-5)

A∧B→A A∧B→B A→A∨B B→A∨B

A→(B→A) ∀xA(x)→A(t) A(t)→∃xA(x) ⊥→A

(A→(B→C)) →((A→B)→(A→C))

A→(B→A∧B)

(A→C)→((B→C)→(A∨B→C))

∀x(B→A(x)) →(B→∀xA(x))

∀x(A(x)→B) →(∃xA(x)→B)

伴随着最后两个公理的通常侧面条件，以及“模因”规则，

从A和（A→B）推出 B

作为推理的唯一规则，自从海廷提出直觉主义逻辑以来，它一直是研究的对象。在命题层面上，它已经有了许多不同于经典逻辑的特性，比如说析取属性：

(DP) IQC ⊢ A∨B implies IQC ⊢ A or IQC ⊢ B.

这个原则显然是与经典逻辑相冲突的，因为经典逻辑对独立于其的公式也证明了(A∨¬A)，即对A和¬A都不是同义词。把“Ex Falso Sequitur Quodlibet (⊥→A)”这一原则纳入到直觉主义逻辑中，是研究布劳威尔关于这个问题的言论的讨论点。在van Atten 2008中，有人认为这一原则在直觉主义中是无效的，根据布劳威尔的观点，有效的逻辑原则是相关性逻辑的原则。关于布劳威尔和Ex Falso Sequitur Quodlibet的更多信息，见van Dalen 2004。

尽管到今天为止，直觉主义推理中使用的所有逻辑都包含在IQC中，但在原则上可以想象，在某些时候会发现一个从直觉主义观点来看可以接受的原则，而这个逻辑却没有涵盖到。对于大多数形式的建构主义来说，被普遍接受的观点是，这种情况永远不会出现，因此，IQC被认为是建构主义的逻辑。对于直觉主义来说，情况就不太清楚了，因为不能排除在某个时候，我们的直觉主义理解可能会引导我们找到我们之前没有掌握的新的逻辑原则。

直觉主义逻辑被广泛使用的原因之一是它在证明理论和模型理论的角度都表现良好。它有许多证明系统，如根岑（Gentzen）计算法和自然演绎系统，以及各种形式的语义学，如克里普克模型、贝斯模型、海廷矩阵、拓扑语义学和分类模型。然而，这些语义中的几个只是研究直觉主义逻辑的经典手段，因为可以证明，关于它们的直觉主义完全性证明是不存在的(Kreisel 1962)。然而，已经证明有一些替代性的但不那么自然的模型，对于这些模型，完全性确实是建构性的(Veldman 1976)。直观逻辑的建构性特征在库里-霍华德同构中变得特别明显，该同构在逻辑中的派生与简单类型的λ-微积分中的术语之间建立了对应关系，也就是说，在证明与计算之间。这种对应关系保留了结构，因为术语的减少对应于证明的规范化。

3.3 自然数

自然数的存在是由直觉主义的第一个规定给出的，即通过对时间运动的感知，以及将生命的瞬间分解成两个不同的东西：过去的东西1，和现在的东西2，以及从那里到3，4……与古典数学相反，在直觉主义中，所有的无穷被认为是潜无穷。特别是自然数的无穷大就是这种情况。因此，对这个集合进行量化的声明必须谨慎对待。另一方面，从直觉的角度来看，归纳法的原则是完全可以接受的。

数学联邦政治世界观提示您：看后求收藏（同人小说网http://tongren.me），接着再看更方便。