直觉主义逻辑的发展 intuitionistic logic (Mark van Atten)

首次发表于 2008 年 7 月 10 日；实质修订于 2022 年 5 月 4 日。

"直觉主义逻辑" 是一个不幸越来越流行的术语；它传达了一个完全错误的直觉主义数学观点。——弗洛伊登塔尔 1937 年

直觉主义逻辑是 L.E.J.布劳尔直觉主义数学的一个分支。普遍存在一个误解，即直觉主义逻辑是布劳尔直觉主义的基础逻辑；相反，直觉主义是逻辑的基础，被构建为将直觉主义数学应用于语言的一种方式。直觉主义数学包括进行某种类型的心智构建的行为。这些构建本质上并不是语言性质的，但是当构建行为及其结果用语言描述时，描述可能呈现出语言模式。直觉主义逻辑是对这些模式的数学研究，特别是那些表征有效推理的模式。如果推理规则中的前提陈述描述了直觉主义数学的真理，那么可以找到一种构建，使得应用该规则得到的陈述为真。因此，逻辑原则需要保持的不是像经典逻辑那样的与心智无关的真理，而是心智可构建性。各种经典逻辑原则，尤其是排中律原则，因此变得不够有根据，甚至某些经典定理出现了矛盾。在直觉主义逻辑中，形式上与经典定理相矛盾的定理依赖于与经典数学不兼容的直觉主义数学元素；这说明在直觉主义中，逻辑是基于数学而不是反过来。

直觉主义逻辑的系统解释和形式化始于布劳尔的学生阿伦德·海廷在 1928 年。这里的“解释”是对人们在理解和正确使用逻辑连接词时所知道的内容的解释。自 1970 年代以来，海廷的解释及其变体被称为“证明解释”，因为在古典逻辑的解释中，独立于思维的真理所起的作用在这里由证明所扮演。对海廷来说，证明首先是布劳尔意义上的数学构造，其次是对其的语言描述。但事实证明，证明解释也可以基于其他证明概念。以更一般的意义理解的证明解释在其历史起源之外找到了许多应用，尤其是在其他建构性但非直觉主义形式的数学、哲学、计算机科学和语言学中。这种应用范围的扩大是可能的，因为最初的证明解释主要依赖于直觉主义数学真理概念具有验证主义性质的事实，因此在其他领域中广泛的验证主义理论允许对其逻辑进行类似的解释。

在本文中，主要关注的是直觉主义数学中证明解释的发展及其原始背景。第 1 节对术语进行评论。第 2 节考察了布劳尔在早期著作中对逻辑概念的基础。第 3 节介绍了他后来的改进，以及他对希尔伯特计划、哥德尔不完备定理以及 20 世纪 20 年代数学基础领域的争论的看法。第 4 节讨论了直觉主义逻辑的形式化，这在证明解释明确之前就已经开始，并简要介绍了所获得形式化的数学解释。第 5 节讨论了海廷在 1930 年至 1956 年间的著作中对证明解释的解释。直觉主义逻辑对数学构造的确切概念的敏感性是直觉主义内部对证明解释的某些部分提出强烈反对的根源。这些在第 6 节中进行了讨论。最后，列出了将在未来更新中添加的主题的简短列表。

1. 引言

1.1 证明解释

直觉主义逻辑的标准解释是 BHK-解释（“Brouwer, Heyting, Kolmogorov”的缩写），或者是 Troelstra 和 van Dalen 在《数学中的构造主义》（Troelstra & van Dalen 1988: 9）中提出的证明解释。

(H1)给出了一个证明 A∧B 的证明，其中给出了 A 的证明和 B 的证明。
(H2)给出了一个证明 A∨B 的证明，其中给出了 A 的证明或 B 的证明（加上我们希望将所给出的证明视为 A∨B 的证据的规定）。
(H3)证明 A→B 的证明是一种构造，它使我们能够将任何 A 的证明转化为 B 的证明。
(H4)荒谬 ⊥（矛盾）没有证明；对 ¬A 的证明是一种将任何假设的 A 的证明转化为矛盾证明的构造。
(H5)∀xA(x)的证明是一种将 d∈D（D 是变量 x 的预期范围）的证明转化为 A(d)的证明的构造。
(H6)∃xA(x)的证明是通过提供 d∈D 和 A(d)的证明来给出的。

诸如“构建”、“呈现”和“转化”等概念可以有不同的理解方式，事实上也确实如此。同样地，对于如何证明 H3 和 H4 子句的具体实例确实适用于任何（可能是假设的）前提证明，也存在不同的观点。在这些概念的某种理解上有效的逻辑原则在另一种理解上可能无效。正如 Troelstra 和 van Dalen 所指出的，甚至可以以一种使这些子句验证经典逻辑原则的方式来理解它们（Troelstra 和 van Dalen 1988: 9, 32–33；参见 Sundholm 2004 和 Sato 1997）。在直觉主义和构造主义的基础计划背景下，当然所有概念都被理解为有效；但即使在这种情况下，仍然存在理解上的差异。这种差异可能会产生数学上的后果。在某些理解上，直觉主义逻辑在形式上被证明是经典逻辑的一个子系统（即，没有排中律的经典逻辑）。但这并不是直觉主义数学家的理解，他们在分析中构造了直觉上有效的 ¬∀x(Px∨¬Px)模式的实例，而在经典逻辑中则不存在（请参见下面的“强反例和创造主体”（3.3）部分）。

Troelstra 和 van Dalen 指出，子句 H1-H6 可以追溯到 Heyting 在 1934 年的解释（因此称为“H”）。Heyting 的目标是澄清 Brouwer 在数学基础计划中的逻辑概念，这促使添加以下子句：

（H0）对于一个原子命题 A 的证明是通过呈现一个在 Brouwer 的意义上使 A 成立的数学构造来给出的。

实际上，正如我们将看到的那样，证明解释的一个版本已经隐含在布劳尔在 1907 年和 1908 年的早期著作中，并且在他在 1924 年和 1927 年的杆定理证明中被他显著地使用，这些著作早于海廷关于逻辑的论文。因此，我们将从布劳尔的思想开始介绍直觉主义逻辑的历史发展，然后展示如何通过海廷和其他人，得到了现代证明解释。

1.2 解释、理论和名称

正如桑德霍姆（1983: 159）指出，在“BHK-解释”和“证明解释”的术语中，将“解释”替换为“理论”是合适的。因为在逻辑数学的背景下，“解释”已经成为指一个形式理论在另一个形式理论中的解释。一个形式系统 U 在形式系统 V 中的解释是通过将 U 的公式翻译为 V 的公式，并保持可证性来给出的。

如果 U⊢A，则 V⊢A′

暂时地，我们注意到 BHK-解释或证明解释并不是在数学意义上的解释，而是一种意义上的解释；我们将在补充文件《转向 Heyting 的形式逻辑和算术》的第 2 节中回到这样的解释和它们与解释的区别。

虽然接受 Sundholm 的观点，我们保留这些术语本身，考虑到它们可能已经变得太常见而无法更改。下面的第 5.3 节是解释我们对“证明解释”优于“BHK-解释”的偏好的适当位置。

Heyting 在 1930 年代和之后发表的解释，其名称“Proof Interpretation”似乎只在 1973 年首次出现在印刷物上，由 van Dalen 和 Kleene 在同一次会议上发表的论文中提出（van Dalen 1973a; Kleene 1973）。Heyting 本人只是简单地称之为“interpretation”（1958A: 107; 1974: 87）或“the intuitionistic interpretation”（1958A: 110）。

“BHK-Interpretation”这个名称是由 Troelstra（1977: 977）创造的，其中“K”最初代表“Kreisel”（因为 Kreisel 1962），后来代表“Kolmogorov”，例如在 Troelstra 1990: 6 中；这个替换是根据 Sundholm 的观点进行的修正。

2. Brouwer 在 1907 年和 1908 年对逻辑的观点

2.1 数学、语言和逻辑

在他的博士论文（1907 年）中，布劳尔提出了他对数学、语言和逻辑之间关系的看法。直觉主义对逻辑的观点本质上是贫瘠的，以及直觉主义逻辑中存在与古典逻辑不兼容的结果，这两者都基本上依赖于这种观念。

对于布劳尔来说，纯数学主要是进行某些心智构建的行为（Brouwer 1907: 99n.1 [1975: 61n.1]）。[3] 这些构建的出发点是时间流动的直觉。[4] 当这种直觉剥离了所有感性内容时，我们能够感知到“一物再物，以及两者之间的连续体”的形式。布劳尔将这种将离散和连续统一起来的形式称为“空的二元性”。这是数学的基本直觉；离散不能归约为连续，连续也不能归约为离散（Brouwer 1907: 8 [1975: 17]）。

随着时间的流逝，一个空的二元性可以被视为新的二元性的一部分，依此类推。直觉主义数学的发展在于探索空的二元性及其自我展开或迭代允许哪些具体构造，以及不允许哪些构造：

数学的唯一可能基础必须在这种构造中寻找，同时要仔细观察直觉允许哪些构造，以及不允许哪些构造。（布劳尔 1907: 77 [1975: 52]）

或者用海廷的话来说，

[布劳尔] 直觉主义数学的构建不过是对智力在自我展开中所能达到的极限的探究。(Heyting 1968A: 314)

布劳尔和其他直觉主义者已经展示了如何基于这一基础构建算术、实分析和拓扑学。此外，布劳尔认为，任何不是数学本身的确切思想都是数学的应用。因为每当我们有意识地以确切的方式思考两个事物，即将它们在保持分离的同时思考在一起，我们就是通过将一个空的二元性的离散部分投射到它们上来实现这一点的(Brouwer 1907: 179n.1 [1975: 97n.1])。

布劳尔认为时间的直觉属于语言前意识。因此，数学本质上是无语言的。它是从非语言性的东西中进行非语言性构建的活动。使用语言，我们可以描述我们的数学活动，但这些活动本身并不依赖于语言元素，数学构建活动的真实性也不依赖于某种语言事实。诸如公理这样的语言对象可以用来描述一个心理构建，但它们不能使其产生。因此，直觉主义者拒绝了某些来自古典数学的公理，比如实数的完备性公理，该公理声称如果一个非空的实数集有一个上界，那么它有一个最小上界：我们不知道有什么一般的方法可以使我们在心理上构建出这个公理所声称的最小上界。

正如布劳尔后来所说，“形式语言就像巴赫的交响乐或亨德尔的神剧伴随着数学”。（布劳尔等人 1937 年：262；译者注）[5] 相应地，建立形式系统的属性可能有很多用途，但对数学基础没有根本意义。在 1923 年的一次讲座中，布劳尔对希尔伯特的证明理论表示乐观，但否认它对数学的意义：

我们绝不必对实现形式化数学一致性证明的目标感到绝望，但这并不会带来任何数学价值：即使一个不正确的理论不能被任何能够驳斥它的矛盾所抑制，它仍然是不正确的，就像一个犯罪政策即使不能被任何能够限制它的法庭所抑制，它仍然是犯罪的。（布劳尔 1924N：3 [van Heijenoort 1967: 336]）

同时，布劳尔也很清楚语言在实践中的需求，既是为了将数学结果传达给他人，也是为了帮助我们记住和重构以前的结果（布劳尔 1907 年：169 [1975 年：92]）。只有具有完美和无限记忆力的理想数学家才能在不借助语言的情况下进行纯粹数学的实践（布劳尔 1933A2：58 [van Stigt 1990：427]）。显然，鉴于语言的这两个实际功能，语言越精确越好。

逻辑学在这个框架中寻求并系统化我们数学构建活动的语言记录中的某些模式。它是将数学应用于数学语言的一种方式。具体而言，逻辑学研究表征有效推理的模式。其目的是建立适用于关于数学构建的陈述的一般规则，以便如果原始陈述（前提）传达了数学真理，则应用该规则得到的陈述（结论）也将传达数学真理（布劳尔 1949C：1243）。因此，从给定前提到结论的推理中所保留的不是像经典逻辑中那样可能超越证据的真理，而是可构建性。这种观点在布劳尔的博士论文中已经非常明确（布劳尔 1907：125-132，159-160 [1975：72-75，88]），但更值得记忆的是 1908 年的论文中的一段话：

在纯数学构建和转换的情况下，是否可以暂时忽略已经建立的数学系统的呈现，并在伴随的语言建筑中移动，遵循三段论、矛盾和排中律的原则，始终确信通过对这种推理建议的数学构建的呈现的瞬间召唤，可以证明论述的每个部分？（布劳尔 1908C：4 [van Atten＆Sundholm 2017：40]）

（然后他继续论证，对于三段论和矛盾原则，答案是“是”，但对于排中律（PEM）来说，一般来说是“否”；关于此问题的更多内容，请参见下文第 2.4 节。）

但是，如果某个数学构造可以由另一个数学构造构建出来，这是一个纯粹的数学事实，因此与逻辑无关。因此，逻辑是描述性的而不是创造性的：通过使用逻辑，人们永远不会得到通过直接数学构造无法获得的数学真理（布劳尔 1949C：1243）。因此，在直觉主义数学的发展中，逻辑永远不能起到重要的作用。布劳尔的观点表明，逻辑是从属于数学的。传统观点认为数学从属于逻辑，这与纯粹逻辑没有特定主题或领域，并且优先于一切的观点密切相关。从这个角度来看，布劳尔对逻辑依赖于数学的观念似乎过于限制。但对于布劳尔来说，逻辑总是预设数学，因为在他看来，它像任何精确的思想一样，是数学的应用。

逻辑学的结果语言系统可以在数学上进行研究，甚至可以独立于最初从中抽象出来的数学活动及其记录。通过迭代这个过程，会产生一个无限的层次结构，包括数学活动、它们的语言记录以及对这些记录作为语言对象的数学研究，而不考虑它们最初的意义。布劳尔在他的论文结尾（布劳尔 1907: 173ff）中对这个层次结构进行了更详细的描述，并批评希尔伯特没有尊重它。布劳尔特别关注的是他对数学和“二阶数学”之间的区别（布劳尔 1907: 99n.1, 173 [1975: 61n.1, 94]），其中后者的一个实例是对前者语言的数学研究，抽象出其原始意义；这样，布劳尔完全明确了数学和（后来被称为）元数学之间的区别（例如，希尔伯特 1923: 153）。后来，布劳尔声称对这个区别有优先权，并在一个脚注中补充说，他在 1909 年的一系列对话中向希尔伯特解释了这一点（布劳尔 1928A2: 375 [Mancosu 1998: 44n.1]）。

2.2 假设性判断

布劳尔（1907: 125–128 [1975: 72–73]）意识到，假设性判断似乎对他对逻辑的观点提出了问题。布劳尔说，假设性判断的特殊之处在于，在那里，数学优先于逻辑的优先级似乎被颠倒了。他提到的例子包括阿波罗尼斯的初等几何问题的证明。以下是其中之一：给定三个由它们的圆心和半径定义的圆，构造一个与这三个给定圆都相切的第四个圆。通常的解决方法是首先假设存在这样一个第四个圆，然后建立表达它与三个给定圆之间关系的方程，然后通过代数运算和逻辑推理，得出所需圆的圆心和半径的明确定义，从而得出相应的数学构造。因此，似乎在这里首先必须假设所需圆的存在，然后使用逻辑对其进行各种判断，只有这样才能得出它的数学构造。

然而，布劳尔认为，实际情况并非如此。他对这类情况的一般解释如下。首先指出逻辑推理伴随或反映了至少在概念上优先于该推理的数学活动，布劳尔接着说：

有一个特殊情况 [...] 似乎确实预设了逻辑的假设判断。这种情况发生在一个结构中定义了某种关系，但并不立即清楚如何实现其构造。在这种情况下，似乎假设已经完成了所需的构造，并从这个假设中推导出一系列假设性判断。但实际上并非如此；在这种情况下，实际上是这样做的：首先构建一个满足部分所需关系的系统，并试图通过 tautologies 的方式从这些关系中推导出其他关系，以便最终推导出的关系与尚未使用的关系相结合，得到一组适合作为所需系统构建的起点的条件。只有通过这种构建，才能证明原始条件确实可以满足。(Brouwer 1907: 126–127 [1975: 72; translation modified])

对这个简洁段落的不同解读已经被提出。根据其中一种解读，Brouwer 的段落与 A→B 的关系如下：

(α)Brouwer 在上述行中指出，如果给出了 A 的条件和规范，那么我们会尝试以一种方式添加更多信息，以便在一定程度的构造活动之后，我们可以真正进行一个符合规范的 A 的构造。一旦这个目标实现，我们可以转向“蕴涵”构造 B，从而得到 B 的构造以及将 A 的结构嵌入到 B 的结构中所需的嵌入。(van Dalen 2004: 250–251)

根据解释 α，A→B 只是意味着 A∧B，并附加了一个信息，即 B 的构造是从 A 的构造中获得的。在这种解读下，只有在找到 A 的构造之后才能断言 A→B。这个想法很明确：即通过坚持提供证明前提的构造来避免假设性构造和它们所需的逻辑使用。（正如在补充文件《对证明解释的反对意见》的第 2.1 节中将解释的那样，Freudenthal（1937b）也提出了这个策略，尽管其动机与 Brouwer 的论文中的这段话不同。）但是，正如 van Dalen 也注意到的那样，在一般情况下，人们不知道是否存在 A 的构造，这实际上也是对假设性判断的拒绝。

另一种解读是 β：

（β）为了建立 A→B，必须将 A 和 B 视为构造的条件，并展示从 A 指定的条件到 B 指定的条件的转换，其组合保持数学可构造性：如果假设已经进行了 A 的构造，那么我们可以进行 B 的构造（van Atten 2009: 128）。

在这种解释下，布劳尔对假设判断的解释避免了假设性结构和相应的逻辑使用，而是通过考虑对结构的条件而不是结构本身来进行。我们并不是在进行“一系列假设性判断”，而是在进行一系列变换，其中从给定的关系（即给定的条件）推导出进一步的关系。当然，这些变换必须保持数学可构造性，并且这种保持本身是直观知道的。条件的作用在布劳尔在其出版生涯的另一端所发表的一篇论文中得到了明确的阐述：

[T] 数学定理的措辞只有在指示对一个实际的数学实体的构造或者对一个假设的数学系统施加的某种构造条件（例如，空的二元与空的一元的等同性）的构造时才有意义。（布劳尔 1954A：3）

布劳尔并不是说通过一个假设的数学系统构造出的不相容性，而是通过对其构造的某种条件构造出的。

不管怎样，从 A 到 B 的可构建性的保持对于阅读 α 和阅读 β 都是必要的，因此在任何一种情况下，布劳尔在 1907 年已经考虑到了蕴涵的证明解释。有关布劳尔在假设判断上的进一步讨论以及这里提到的两种解读，请参见 Kuiper 2004，van Dalen 2004，van Dalen 2008 和 van Atten 2009。

2.3 否定

直觉主义地说，说一个命题 A 是真的，主要是说我们已经进行了一个被 A 正确描述的构造；这个命题 A 是通过这个构造变为真的。在一定程度上理想化，我们说如果我们拥有一个构造方法，当实施时，将会产生一个被 A 正确描述的构造，那么 A 就是真的。根据布劳尔的观点，说一个命题 A 是假的，那么就意味着无法进行一个合适的构造；记作 ¬A。这种不可能性可以立即被认识到（例如，无法区分 1 个单位和 2 个单位的不可能性）或者间接地被认识到。在前一种情况下，人们直接观察到一个预期的构造被阻止了；它“无法进行”（布劳尔 1907 年：127 [1975 年：73]）。在后一种情况下，人们通过将命题 A 归约为已知的假命题来证明 A 是矛盾的，例如，人们证明 A→1=2（布劳尔 1954A：3）。在实践中，人们定义 ¬A:=A→1=2（因此 ¬1=2 被视为 A→A 的一个特例）。

“否定即不可能”的概念被称为“强否定”。人们谈论 A 的“弱否定”是为了表达迄今为止没有找到 A 的证明。这既不排除找到 A 的证明，也不排除以后找到 ¬A 的证明。因此，断言 A 的弱否定并不是为其分配真和假之外的真值；Barzin 和 Errera（见下文 4.3 节）声称它对否定的处理使得布劳尔的逻辑变成了一个三值逻辑是毫无根据的。弱否定和强否定的区别对于所谓的“弱反例”是重要的。

2.4 弱反例（“不可靠性”）和排中律

由于逻辑的规则是在语言对象上操作的，而这些语言对象可以被单独考虑，不需要提供它们所描述的真理的精确数学背景，因此可以应用逻辑规则并获得新的语言对象，而无需为后者提供精确的数学背景。换句话说，逻辑原则可以在不指定应用它们的上下文的情况下陈述，并因此暗示着上下文无关性，但它们的正确性对上下文是敏感的。没有一般性的保证，逻辑原则在一个上下文中有效，在另一个上下文中同样有效。这就是布劳尔在谈到“逻辑原则的不可靠性”时的意思，这也是他的重要论文《布劳尔 1908C》的标题和主题；另请参阅布劳尔 1949A：1243。

在 1908 年的论文中，布劳尔从他对逻辑的一般观点中得出了一个他在他的论文中忽视的结论：PEM，A∨¬A，是无效的。它的建设性有效性意味着我们有一种方法，对于任何 A，要么给出 A 的构造，要么显示这样的构造是不可能的。但我们没有这样的一般决策方法，数学中存在许多未解决的问题。布劳尔将“每个数是有限的或无限的”作为一个例子，迄今为止还没有找到建设性的证明。因此，他说，目前还不确定是否可以解决以下问题：

在 π 的十进制展开中，是否存在一个数字比其他任何数字出现得更频繁？
在 π 的十进制展开中，是否存在无限多对相等的连续数字？（布劳尔 1908C：7 [van Atten＆Sundholm 2017：44]）

实际上，布劳尔（Brouwer）的意思是，我们可以断言这些问题中所表达的命题的弱否定；因此，这些命题被称为“布劳尔反例”或“弱反例”对于 PEM（排中律）来说。在 PEM 的建设性阅读中，当然任何尚未解决的问题都是 PEM 的弱反例。布劳尔在国际期刊上才在更晚的时候（1921A，1924N，1925E）开始发表 PEM 的弱反例。

布劳尔在 1908 年的论文中指出，PEM 无效并不意味着它是错误的：¬（A∨¬A）意味着 ¬A∧¬¬A，这是一个矛盾。换句话说，¬¬（A∨¬A）是正确的。布劳尔得出结论，使用 PEM 始终是一致的，但并不总是导致真理。在后一种情况下，诉诸 PEM 的论证建立的不是真理，而是其结论的一致性。布劳尔建议将通常被认为已被证明的定理分为真实的和非矛盾的（Brouwer 1908C：7n.2 [van Atten＆Sundholm 2017：44n.14]）。这并不是说存在三个真值，真，非矛盾，假；因为一个非矛盾的命题可能有一天会被证明，从而变为真。

布劳尔指出，PEM 在一个数学背景下是有效的，即在给定有限域中是否可能存在给定有限特征的构造的问题。在这样的背景下，只有有限次尝试该构造，每次尝试都会在有限的步骤中成功或失败（为了清晰起见，这里的措辞不是布劳尔 1908C 的措辞，而是布劳尔 1955 的措辞）。因此，基于这些理由，A∨¬A 成立，其中 A 是陈述该构造存在的命题。

Brouwer 将对 PEM 普遍有效性的信念归因于从有限情况（特别是从有限数学应用于日常现象中产生的情况）到无限的不合理投射。[6]

在他 1907 年的论文中，Brouwer 仍然将 PEM 视为一个重言式，（误）将 A∨¬A 误解为 ¬A→¬A（Brouwer 1907: 131, 160 [1975: 75, 88]）。[7] 有趣的是，他同时意识到没有证据表明每个数学命题都是可证明的或可证伪的（Brouwer 1907: 142n.3 [1975: 101]）；这个原则是 PEM 的建设性正确阅读。在 1908 年的论文中，他纠正了自己对 PEM 的早期理解：

现在是第三排除原则：这要求每个假设在数学上要么正确要么不正确：对于每个假设的系统在某种程度上的相互适应，要么可以构造出终止，要么可以构造出不可能的阻塞。（Brouwer 1908C: 5 [van Atten & Sundholm 2017: 42]）

2.5 没有绝对不可决命题

布劳尔继续引用最后一句话如下：

由此可知，第三排斥原则的有效性问题等同于无解数学问题是否存在的问题。对于这种信念，没有一丝证据，有时候会提出这种观点（布劳尔在脚注中提到了希尔伯特 1900 年的观点），即不存在无解数学问题。

在这里，他似乎忽视了一个事实，即在建设性的意义上，每个数学问题都是可解的这一主张与没有绝对不可解问题的较弱主张之间存在着差异。前者等同于 A∨¬A，后者等同于 ¬¬(A∨¬A)；而布劳尔在同一篇论文中证明了后者的直觉主义有效性。实际上，在布劳尔的档案中，有一份大约在 1907 年至 1908 年期间的笔记，明确指出了这一点：

一个命题能否被证明永远无法决定？不，因为这将需要通过反证法来证明。因此，我们必须这样说：假设命题在意义 a 下已经被决定，并从中推导出矛盾。但是，这样就证明了非 a 是真的，而命题毕竟是被决定的。（van Dalen 2001b: 174n.a；翻译为我的）

布劳尔从未发表过这份笔记。1926 年，瓦夫尔提出了一个特定情况的论证，明显看到了一般的观点：

为了同时给出一个人们不知道它是代数的还是超越的数字的例子，以及一个在进一步的信息到来之前既不是前者也不是后者的数字的例子，只需给出一个数字的例子就足够了。但是，另一方面，我觉得想要定义一个既不是代数的也不是超越的数字是徒劳的，因为唯一能够证明它不是代数的方法就是证明它是荒谬的，那么这个数字就是超越的。（Wavre 1926: 66; 翻译为我的）

在 Heyting 1934: 16 中明确观察到 ¬¬(A∨¬A)的意思是没有绝对无解的问题可以被指出。

3. 布劳尔的后期改进和应用，1921-1955 年

3.1 直觉主义的隐式证明解释

可以举出三个例子，表明到了 20 世纪 20 年代中期，布劳尔在实践中使用了假设判断和证明解释中的蕴涵子句（后来发表）：命题逻辑中的等价性、杆定理的证明以及他对排序公理的阅读。

3.1.1 命题逻辑中的等价性

在 1923 年的一次讲座中，布劳尔提出了 ¬¬¬A↔¬A 的证明（布劳尔 1925E: 253 [Mancosu 1998: 291）[8]。这个等价式是布劳尔在命题逻辑中发表的唯一定理。论证从指出 A→B 蕴含着 ¬B→¬A 开始（因为 ¬B 是 B→⊥，而且这两个蕴含可以组合，因为一个的结论是另一个的前提）。如果在当时，布劳尔必须在蕴含的证明条件中有一个前提的证明，那么他就不可能进行这个推理，因为这样一来，A→B 的证明将导致 B 的证明，从而使得通过证明其前提 ¬B 来开始建立第二个蕴含的过程变得不可能。

后来，布劳尔指出了 ¬¬¬A↔¬A 的有效性的以下推论：反证法的证明方法可以用来建立否定命题 ¬A（布劳尔 1929A: 163 [Mancosu 1998: 52]）。因为如果假设 ¬¬A 导致矛盾，即 ¬¬¬A，那么这个等价式允许将其简化为 ¬A。另一方面，一般情况下，反证法不能用来建立肯定命题 A；从假设 ¬A 推导出矛盾只能得到 ¬¬A，而在直觉主义中，¬¬A 比 A 更弱。

3.1.2 条的证明

Brouwer 的条形定理对直觉主义分析至关重要；有关所涉及概念和 Brouwer 的证明的详细解释，请参见 Heyting 1956（第 3 章），Parsons 1967 和 van Atten 2004b（第 4 章）。在这里，我们更关注逻辑学方面。

Brouwer 在 1924 年证明的条形定理（证明的后续版本出现在 1927 年和 1954 年）证明了一个形式为“如果已经证明了 A，则 B 是可证明的”的陈述（Brouwer 1924D1，1927B，1954A）。如果将后者理解为将 A 的证明条件转化为 B 的证明条件的蕴含 A→B，那显然不是这样，因为在前一种情况下，有额外的信息，即根据假设，A 已经被证明。换句话说，我们假设手头上有一个具体的 A 的证明。（然而，两者都是假设性判断，即都不要求我们实际上已经证明了 A。）可能可以利用这个额外的信息，下面将指出 Brouwer 是如何做到这一点的。（Heyting 在 1956 年也选择以这种更强的意义理解蕴含，即以断言条件为基础；请参见下面的第 5.4 节。）

条形定理的一个简单但相关的版本（对于自然数上的通用树 T）将是：

如果已经证明了通过 T 的每条路径都与给定的节点集合 B 相交，那么可以证明通过 T 的每条路径都与一个可以被良序排列的节点集合 B'有一个共同的节点。[9]

像 B 和 B'这样的集合被称为 bar。布劳威尔首先为可能找到的命题“树 T 包含一个 bar”的任何证明制定了一个条件。这个条件是，该命题的任何证明必须可以分析成某种规范形式。然后，布劳威尔给出了一种方法，将任何这样的证明，当分析成该规范形式时，转化为一个数学构造，使命题“T 包含一个良序的 bar”成立，从而建立了结果。这个策略清楚地表明，布劳威尔对 A→B 的操作性解释是引言中所阐述的证明解释的一个版本，如果我们将该条款中的“proof”理解为“demonstration”。

要获得一个规范形式，需要对前提进行一个具体的或假设的证明。原因是，命题 A 的一个规范证明的存在不能从 A 的纯粹的证明条件中逻辑地推导出来，因为这样一个规范证明的形式可能取决于 A 的具体非逻辑细节的数学构造。

在布劳尔证明条定理中，将变换方法应用于前提的任何证明的可行性是由他所制定的条件是一个必要条件这一事实所保证的。布劳尔通过利用他的观念中数学对象，特别是树和条的心智对象的事实来获得这个必要条件；这打开了这样的可能性，即对这些对象及其属性在心智行为中的构建方式进行反思，可以提供关于它们的信息，这些信息可以在数学上得到应用，特别是如果这些信息包含对这些构建行为的限制。这就是布劳尔得出他的规范形式的方式。实际上，布劳尔对条定理的论证是一种超验论证。在其他数学观念中，这些考虑可能不被接受，事实上，在其他形式的建构性数学中（其中条归纳要么被接受为公理，这也是布劳尔曾经提出的可能性（布劳尔 1927B: 63n.7 [van Heijenoort 1967: 460n.7]），要么不被接受，如马尔科夫学派），没有已知的（经典有效的）条定理的证明。

关于这个问题的更详细讨论，请参见 Sundholm 和 van Atten 2008 年的论文。

3.1.3 排序公理

大约在 1925 年，布劳尔引入了“虚拟排序”的概念。如果一个（部分）排序<是虚拟的，那么它满足以下公理（布劳尔 1926A: 453）：

关系 r=s，rs 是互斥的。
从 r=u，s=v 和 r<s 可以推出 u<v。
从关系 r>s 和 r=s 同时失败可以推出 r<s。
从关系 r>s 和 r<s 同时失败可以推出 r=s。
从 r<s 和 s<t 可以推出 r<t。

在 1925 年的一个关于序类型的讲座课程中，David van Dantzig 的笔记保存在 Brouwer 档案中，Brouwer 评论道：

公理 II 到 V 应以建设性意义理解：如果公理的前提得到满足，虚拟有序集应为结论中的顺序条件提供一个构造。（van Dalen 2008: 19）

这是证明解释中蕴涵子句的明确实例。请注意，Brouwer 在发表的论文（1926A）中没有包含这一阐述，也没有在后来的演讲中提及。

3.2 扩大弱反例的范围

正如我们在上面看到的，布劳尔在 1908 年的论文中给出了对 PEM 的弱反例。在 1920 年代，布劳尔发展了一种通用技术，用于构造弱反例，这也使得扩大它们的范围并包括分析原理成为可能。这一发展始于 1921 年，当时布劳尔给出了一个关于每个实数都有一个十进制展开的命题的弱反例（布劳尔 1921A）。该论证通过定义实数，其十进制展开依赖于关于 π 的十进制展开的特定开放问题。布劳尔观察到，如果这些开放问题得到解决，那么可以定义其他没有十进制展开的实数（布劳尔 1921A: 210 [Mancosu 1998: 34]）。这一通用技术在 1923 年的一次讲座中得到明确阐述（布劳尔 1924N: 3 和脚注 4 [van Heijenoort 1967: 337 和脚注 5]），并在 1928 年第一次维也纳讲座中达到了完善（布劳尔 1929A: 161 [Mancosu 1998: 51]）。该方法涉及将一个数学原理的有效性归约为以下类型的一个开放问题的可解性：我们有一个可判定的属性 P（定义在自然数上），对于这个属性，我们既没有显示出 ∃xP(x)，也没有显示出 ∀x¬P(x)。这种归约是以这样一种方式进行的，即它仅仅使用了 P 诱导出这种类型的一个开放问题的事实，并且不依赖于 P 的确切定义；也就是说，如果这个开放问题得到解决，那么可以简单地用同类型的另一个问题替换它，而且完全相同的归约仍然有效。这种一致性意味着，只要存在这种类型的开放问题（而这在任何时候几乎是确定的），就没有直觉主义证明所涉及的一般数学原理。在 1920 年代，布劳尔构建了以下一般数学命题的弱反例，其中包括（其中 R 代表直觉主义实数集，Q 代表有理数集）：

连续体是完全有序的（布劳尔 1924N）
每个集合要么是有限的，要么是无限的（布劳尔 1924N）
Heine-Borel 定理（Brouwer 1924N）
∀x∈R(x∈Q∨x∉Q)（Brouwer 1925E）
欧几里得平面上的任意两条直线要么平行，要么重合，要么相交（Brouwer 1929A）
每个正数的无限序列要么收敛，要么发散（布劳威尔 1929A）

3.3 强反例和创造性主体

一个弱反例表明我们目前无法证明某个命题，但它并没有真正驳斥它；从这个意义上说，它不是一个真正的反例。从 1928 年开始，布劳威尔设计了一些强反例来反驳经典有效的命题，也就是说，他证明了这些命题是矛盾的。这应该理解为：如果我们坚持经典原则的字面意义，但在解释中用直觉主义概念替代它们的经典对应物，我们就会直觉地得出一个矛盾。因此，布劳威尔的强反例与他的弱反例一样，并不是严格意义上的反例（但原因不同）。看待强反例的一种方式是将它们视为不可解释的结果。

解释如下，强有力的反例可以解释为经典原理的可能性。如前所述，根据直觉主义的理解，逻辑学是数学的从属，而在经典逻辑学中则相反。因此，如果直觉主义数学包含在经典数学中不存在的对象和原则，那么直觉主义逻辑学，也依赖于这些非经典元素，可能不是经典逻辑学的一个合适的部分。

布劳尔的第一个强有力的反例发表于布劳尔 1928A2 中，他在其中展示了：

¬∀x∈R(x∈Q∨x∉Q)

这是对 1923 年相应的弱反例的加强，但论证完全不同。强反例依赖于直觉主义分析中的定理，该定理于 1924 年获得，并于 1927 年改进，即所有的全函数 [0,1]→R 都是一致连续的。该定理中的非经典元素是将连续体看作选择序列的传播以及基于此的杆定理（有关这一概念的进一步解释，请参见 Heyting 1956（第 3 章）和 van Atten 2004b（第 3 章和第 4 章））。[10]

从 1948 年开始，布劳尔还发表了基于所谓的“创造主体方法”的反例。（他在布劳尔 1948A 中提到，他自 1927 年以来一直在讲座中使用这种方法。）它们的特点是明确引用进行数学构造的主体，引用其活动的时间结构以及该结构与直觉主义真理观念的关系。这些方法可以用来生成弱反例和强反例。（在早期用于生成弱反例的“振荡数”方法中，未明确引用创造主体。）

使用创造主体方法，布劳尔例如展示了

¬∀x∈R(¬¬x>0→x>0)(Brouwer 1949A)¬∀x∈R(x≠0→x <0∨x> 0)(Brouwer 1949B)

使用这些方法的实际论证本身并没有引入任何新的逻辑现象——其他方法也可以给出弱反例和强反例。暂时我们参考文献以获取更多细节：Brouwer 1949A, 1949B, 1954F; Heyting 1956: 117–120; Myhill 1966; Dummett 2000: 244–245; van Atten 2018。但我们在这里要注意这种方法的一个特定方面。它似乎引入了进一步的否定概念，即接受如果已知创造主体永远不会证明 A，则 A 为假。但这实际上与否定作为不可能性的概念没有区别。从启发式的角度来看，可以如下理解：鉴于创造主体构造任何可能的自由度，显示主体无法证明 A 的方式是证明 A 本身是不可能的。该原则的一个实际证明是：如果创造主体证明了命题 A，那么它是在某个特定的时刻 n 证明的；因此，根据逆否命题，如果存在一个时刻 n 使得主体证明 A 是矛盾的，则 A 是矛盾的。[11]

3.4 命题的分类

在 Brouwer 1955 年的论文中，明确指出了命题 α 在任何特定时刻可能处于的四种可能情况：

α 已被证明为真；
α 已被证明为假，即荒谬；
α 既未被证明为真，也未被证明为荒谬，但已知存在一种算法，可以得出结论，要么 α 为真，要么 α 为荒谬；
α 既未被证明为真，也未被证明为荒谬，也没有已知的算法可以得出结论，要么 α 为真，要么 α 为荒谬。

在 1951 年的一次讲座中，布劳尔仅列出了上述列表中的 1、2 和 4 情况，并补充说第 3 种情况“显然可以归约为第一和第二种情况”（布劳尔 1981A：92）。这一备注强调了直觉主义数学中允许的重要理想化：我们可以理想化地认为，一旦我们获得了一个特定命题的决策方法，我们也知道它的结果。

布劳尔还补充说，对于满足第 4 种情况的命题，可能会在某个时刻转移到另一种情况，要么是因为我们在此期间找到了决策方法，要么是因为与命题 α 相关的对象在此期间获得了进一步的属性，从而允许做出决策（这可能发生在关于选择序列的命题中）。

3.5 布劳尔对形式主义计划和哥德尔不完备定理的看法

1908 年，布劳尔已经证明了 ¬¬(A∨¬A)；1923 年，当希尔伯特的计划全面展开时，这个结果激发了布劳尔说：“我们绝对不必对达到这个目标（形式化数学的一致性证明）感到绝望”；详见上文第 2.1 节的完整引文。（当时，布劳尔怀疑 ¬¬A→A 比 PEM 要弱；伯奈斯很快在给布劳尔的一封信中纠正了这个印象（布劳尔 1925E: 252n.4 [Mancosu 1998: 292n.4]）。）

在 1928 年，他在这个基础上增加了 PEM 实例的有限合取的一致性，并认为这些结果为形式主义的一致性证明项目提供了“一些鼓励”（布劳尔 1928A2: 377 [曼科苏 1998: 43]）[12]。基于这些结果，他在 1928 年第一次维也纳讲座结束时发表了最强烈的声明：

因此，这种直觉主义非矛盾数学语言的适当机械化应该恰好能够实现形式主义学派设定的目标。（布劳尔 1929A: 164；译者注）

但是，出于上述原因，这样的一致性证明对布劳尔来说没有数学价值；根据布劳尔所描绘的观点，一个古典数学家所做的最好的事情就是提供相对一致性证明。

哥德尔的不完备定理表明，希尔伯特计划在其最雄心勃勃的形式下无法成功。布劳尔的助手胡雷维奇在一个研讨会上讨论了不完备定理（van Dalen 2005: 674n.7）。布劳尔对哥德尔的第一个定理没有发表评论；另一方面，当他在 1952 年写道时，他显然有第二个定理在心中：

最初由旧形式主义者培养的希望，按照他们的原则建立的数学科学将有一天以非矛盾性的证明而告终，从未实现，并且现在，鉴于过去几十年的某些调查结果，我认为这种希望已经放弃了。（布劳尔 1952B：508）

郝王报告：

1961 年春天，我拜访了布劳尔的家。他广泛地演讲了许多主题。他说，他认为 G 的不完备性结果并不像海廷的直觉推理形式化那样重要，因为对他来说，G 的结果是显而易见的（显然是真的）。（王 1987：88）[13]

关于第一个不完备性定理，布劳尔的反应是可以理解的。在他的论文中，他已经指出所有可能的数学构造的总体是“可数未完成的”；他的意思是我们永远无法以明确定义的方式构造出超过可数子集的元素，但是当我们构造出这样的子集时，我们可以立即根据一些先前定义的数学过程从中推导出被计入原始集合的新元素。（布劳尔 1907：148 [1975：82]）

we can never construct in a well-defined way more than a denumerable subset of it, but when we have constructed such a subset, we can immediately deduce from it, following some previously defined mathematical process, new elements which are counted to the original set. (Brouwer 1907: 148 [1975: 82])

在他的论文之前的一本笔记本中，他曾经说过：“数学定理的总体是一个可数但永远不会完成的集合”[14]。

的确，根据卡尔纳普的说法，正是布劳威尔的一个论点激发了哥德尔找到了第一个定理。在 1929 年 12 月 12 日的日记中，卡尔纳普说哥德尔当天与他交谈

关于数学的无穷性（见另一张纸）。他受到布劳威尔在维也纳的演讲的启发。数学并不完全可形式化。他似乎是对的。（王 1987：84）

在“独立的纸张”上，卡尔纳普写下了哥德尔告诉他的内容：

我们承认将关于经验的语言的语法进行数学化是合法的。如果我们试图形式化这样的数学，那么每个形式化都会遇到问题，这些问题可以用普通语言理解和表达，但不能用给定的形式化语言表达。这就导致了（布劳威尔的观点）数学是无穷尽的：我们必须始终从“直觉之泉”中汲取新的东西。因此，整个数学没有普遍的特征，也没有整个数学的决策过程。在每种封闭的语言中，只有可数多个表达式。连续体只出现在“整个数学”中...如果我们只有一种语言，并且只能对其进行“阐明”，那么这些阐明是无穷尽的，它们总是需要一些新的直觉。（引自王 1987 年的翻译，第 50 页）

这份记录特别包含了布劳威尔在维也纳的两次讲座中的元素，哥德尔所提到的论证就在其中：一方面，完整的连续体在先验直觉中给出，而另一方面，它不能被具有可数多个表达式的语言所穷尽（布劳威尔 1930A: 3, 6 [Mancosu 1998: 56, 58]）。

另一方面，第二不完全性定理一定让布劳尔感到惊讶，考虑到他在 20 世纪 20 年代对形式主义学派实现证明形式化古典数学一致性的目标持乐观态度（见本小节开头的引文）。

在他最后一篇原创发表的论文（1955 年）中，布劳尔以自己的方式对古典逻辑的研究持非常积极的态度。在证明了逻辑代数传统中的各种原则（例如布尔、施罗德）在直觉上是矛盾的之后，他继续说道：

幸运的是，古典逻辑代数在其适用于数学的问题之外也有其优点。它不仅作为常识思维技术的形式化形象达到了高度的完善，而且作为一种思维建筑本身，它是一种异常和谐美丽的事物。事实上，它的继任者，即 20 世纪华丽的符号逻辑，目前不断提出最迷人的问题并做出最令人惊讶和深入的发现，同样在很大程度上是为了自身的缘故而培养的。（布劳尔 1955 年：116）

3.6 布劳尔的逻辑与格伦德拉根斯特莱特争论

布劳尔的逻辑在格伦德拉根斯特莱特争论（基础辩论）中只起到了作为经典逻辑片段的作用。在这个意义上的建设性逻辑是成功的，并且（以不同的意义）也成为希尔伯特计划的基础。另一方面，布劳尔对逻辑的完整构想中特有的现象，特别是强反例，在基础辩论中没有起到任何作用。这主要原因可能是，它们依赖于选择序列，使用了在经典数学中不可接受的对象。（一个更微妙的问题是它们在希尔伯特的有限性数学中是否可接受。根据伯奈斯的说法，希尔伯特从未对选择序列表态（哥德尔 2003a：279），并且从更一般的角度来看，从未阅读过布劳尔的论文（范·达伦 2005：637）[15]。）此外，布劳尔并没有大声或争论性地宣布强反例的存在；当他在 1954 年最终发表了一篇标题争议性的英文论文《经典函数理论中的矛盾性例子》时，基础辩论在社会意义上早已结束。直觉主义逻辑和数学已被广泛接受，可以被视为经典数学的建设性部分，而典型的直觉主义创新则被忽视。因此，不足为奇的是，20 世纪 50 年代对强反例的呈现并没有导致辩论的重新开启。有关此问题的进一步讨论，请参见 Hesseling 2003 和 van Atten 2004a。

4. 早期部分形式化和元数学

由于布劳尔对发展纯数学比对发展逻辑学更感兴趣，对他来说逻辑学是一种应用数学形式，他从未对后者进行过广泛的研究。特别是，他从未对直觉主义逻辑和经典逻辑进行系统比较，例如在《数学原理》（怀特海德和罗素 1910 年）或希尔伯特学派（希尔伯特 1923 年；希尔伯特和阿克曼 1928 年）中形式化。其他人进行这种比较的动机是布劳尔在国际期刊上发表了一些弱反例，显示出这些反例也影响到非常普遍的数学原理，例如实数的三分律（见上文第 3.2 节）。

显然，要进行系统比较，需要在一个形式系统中对直觉主义逻辑进行编码。根据直觉主义观点，这是不可能的，因为逻辑与其依赖的数学一样是开放的。但是可以对直觉主义逻辑的片段进行形式化。相关的论文包括科尔莫戈洛夫 1925 年、海廷 1928 年（未发表）、格利文科 1928 年、格利文科 1929 年和海廷 1930 年 [16]。但也许最早对这个问题进行系统思考的是保罗·伯纳斯。在 1930 年 11 月 5 日写给海廷的一封信中，他写道：

当时布劳尔教授在哥廷根（首次）[1924 年（范·达伦 2001：305）] 举行的讲座引发了我对如何分离出布劳尔命题逻辑的问题，并得出结论，可以通过省略单个公式 ¬¬a⊃a（在你的符号中）来实现这一点。我还写信给布劳尔教授 [纠正了布劳尔当时对这个公式比 PEM 弱的印象]。（特罗尔斯特拉 1990：8）[17]

（在证明阶段，伯恩斯的修正被包含在布劳尔的论文中（1925E: 252n.4 [Mancosu 1998: 292n.4]）。然而，伯恩斯没有发表他关于布劳尔逻辑的想法。（科尔莫戈洛夫在 1925 年发表了相同的想法；请参见下文。）

在建立一个形式系统来捕捉布劳尔基础中的逻辑（尽管必然只能部分捕捉），自然需要一些先前获得的意义解释作为直觉主义有效性的标准。然而，科尔莫戈洛夫、海廷和格利文科所提到的论文中，没有一个明确对直觉主义逻辑的意义解释做出贡献。正如我们将看到的，这些论文中给出的解释（这不一定是各自作者所考虑的全部）对此太过模糊。也许并不奇怪，这些系统并不等价；值得注意的是，科尔莫戈洛夫拒绝了“假”的存在，而海廷和格利文科接受了它。我们现在将依次讨论这些论文。

4.1 科尔莫戈洛夫 1925

1925 年，22 岁的安德烈·科尔莫戈洛夫发表了直觉主义逻辑的第一篇（部分）形式化，并在一篇名为《论排中律》的论文中与形式化的古典逻辑进行了广泛比较。正如范·达伦所建议的（赫塞林 2003：237），科尔莫戈洛夫可能是通过亚历山德罗夫或乌里索恩与布劳威尔的亲密朋友接触到直觉主义的。科尔莫戈洛夫无论如何都非常了解情况，甚至引用了仅出现在荷兰语《Verhandelingen》中的论文（布劳威尔 1918B，1919A，1921A）。

该论文中科尔莫戈洛夫设定的任务是解释为什么“在布劳威尔的著作中揭示的‘排中律的非法使用’尚未导致矛盾，以及为什么这种非法性经常被忽视”（范·海耶诺特 1967：416）。实际上，正如其他段落所清楚表明的（范·海耶诺特 1967：429-430），（未实现的）目标是显示古典数学可翻译为直觉主义数学，并从而相对于直觉主义数学给出古典数学的一致性证明。

该论文中建立的技术结果是：古典命题逻辑可以在直觉主义可接受的片段中进行解释。这个直觉主义片段被称为 B（可能是为了“布劳威尔”）。

(1)(2)(3)(4)(5)A→(B→A)(A→(A→B))→(A→B)(A→(B→C))→(B→(A→C))(B→C)→((A→B)→(A→C))(A→B)→((A→¬B)→¬A)

该系统 H（可能是指“希尔伯特”）由 B 和附加公理组成

(6)¬¬A→A

在这两个系统中，规则是假言推理和替换。

然后，科尔莫戈洛夫指出并部分证明了 H 与希尔伯特在 1923 年提出的经典命题逻辑系统等价。然后科尔莫戈洛夫设计了以下的翻译 ∗：

对于原子命题 A，A∗=¬¬A；对于复合公式 AF(ϕ1,ϕ2,…,ϕk)，∗=¬¬F(ϕ∗1,ϕ∗2,…,ϕ∗k)。

并证明了这个可解释性结果：

如果 U⊢Hϕ，则 U∗⊢Bϕ∗

其中 U 是 H 的公理集，而 U∗ 是其翻译的集合（Kolmogorov 证明可在 B 中推导出）。

科尔莫戈洛夫的技术结果预示了哥德尔和根岑的算术“双重否定翻译”（见下文），尤其是因为他还提出了如何处理谓词逻辑的具体建议。然而，正如赫塞林（2003 年：239）指出的那样，将科尔莫戈洛夫的结果视为直觉主义数学的翻译与他自己的看法略有不同。科尔莫戈洛夫将其视为对“伪数学”领域的翻译；尽管他没有明确将其视为直觉主义数学的一部分，但他本可以这样做。

科尔莫戈洛夫获得形式化直觉主义逻辑的（片段）的策略是从一个经典系统出发，从中分离出一个直觉上可接受的系统。（请注意，尽管科尔莫戈洛夫提到了《数学原理》，但他并没有以此为出发点。）这可以（粗略地）描述为划掉的方法，这也是海廷在 1928 年所做的（见下文）。鉴于科尔莫戈洛夫设定的任务，这是一种自然的方法。科尔莫戈洛夫保留公理的标准是命题是否具有“直观基础”或“具有直观明显性”（范·海延诺特 1967 年：421, 422）；关于蕴涵，他说，

符号 A→B 的意义仅仅在于，一旦我们确信 A 的真实性，我们也必须接受 B 的真实性。（范·海延诺特 1967 年：420）

没有给出更精确的指示，因此从这个意义上说，这篇论文很少解释了直觉主义逻辑的含义。

Ex Falso 被从这个片段中排除了：科尔莫戈洛夫说，就像 PEM 一样，Ex Falso“没有直观的基础”（van Heijenoort 1967: 419）。特别是，他说 Ex Falso 是不可接受的，因为它断言了关于不可能的事物后果的某些内容（van Heijenoort 1967: 421）。请注意，这是一个非常强烈的拒绝：它不仅排除了 Ex Falso 的全部普遍性，还排除了特定的实例，例如“如果 3.15 是 π 的一个初始段，那么 3.1 是 π 的一个初始段”。它还指出了科尔莫戈洛夫立场上的不一致性：一个人不能同时接受 A→（B→A）作为公理，并否认关于不可能的 B 的任何内容。

正如范·达伦所指出的，不知道科尔莫戈洛夫是否将他的论文寄给了布劳尔（van Dalen 2005: 555）。这篇论文的内容似乎在苏联以外的地方多年来一直不为人所知。格利文科在 1928 年 10 月 13 日的一封给海廷的信中提到了这篇论文，科尔莫戈洛夫在 1933 年或之后的一封给海廷的信中也提到了这篇论文（Troelstra 1990: 16）；但在海廷 1934 年的论文中，与科尔莫戈洛夫 1932 年后的论文不同，它既没有讨论也没有包含在参考文献中。涵盖 1925 年的《数学进展年鉴》的卷，其中包括了列宁格勒的 V·斯米尔诺夫对科尔莫戈洛夫 1925 年的一个非常简短的通知，实际上直到 1932 年才出版（斯米尔诺夫 1925）。

4.2 Heyting 1928

尽管科尔莫戈洛夫的工作在西方不为人知，但在 1927 年，荷兰数学学会独立发起了直觉主义逻辑和数学形式化的倡议，当时该学会选择为其年度竞赛提出以下问题：

由于其本质，布劳尔的集合论不能与某种帕西格拉夫系统（即通用符号系统）中形式推导出的结论等同。然而，布劳尔用来表达他的数学直觉的语言中可以观察到某些规律；这些规律可以在一个形式化的数学系统中进行编码。要求解释这些规律。
构建这样一个系统，并指出它与布劳尔的理论的偏差；
调查是否可以通过（形式上）交换排中律和矛盾律来获得一个对偶系统。（Troelstra 1990: 4）

这个问题是由布劳尔的朋友、同事和前任教师格里特·曼努里提出的，在一封信中事先向布劳尔征求了他的意见（布劳尔当时在柏林）；[18] 不幸的是，没有找到布劳尔的回复，但最终的表述与曼努里的信中相同。

布劳尔的前学生阿伦德·海廷（Arend Heyting）在 1925 年以直觉主义投影几何学的论文（优等毕业）毕业后，写了一篇后来被证明是唯一的论文（Hesseling 2003: 274）。原始手稿似乎已经不存在，但众所周知，它的标语是“石头换面包”[19]。1928 年，评审团加冕了海廷的作品 [20]，称其为“以最有见识和令人钦佩的毅力进行的形式化”（Hesseling 2003: 274；翻译已修改）。

海廷的论文涵盖了命题逻辑、谓词逻辑、算术和布劳尔的集合论或分析。人们可能会认为，为了能够实现这一点，海廷必须对如何直观地解释逻辑连接词有相当明确的想法。然而，海廷与弗罗伊登塔尔在 1930 年的通信显示，在 1930 年之前，海廷尚未达到在解释蕴涵时明确要求转换过程的要求（见下文第 5.1 节的引文）。

由于原始手稿似乎未能保存下来，对海廷的工作的讨论必须以 1930 年修订和出版的版本为出发点；请参见下文。

Heyting 将他的手稿寄给了 Brouwer，后者在 1928 年 7 月 17 日的一封信中回复说他发现它“非常有趣”，并继续说：

到目前为止，我已经开始非常欣赏你的工作，我想请求你将其用德语修订后发表在《数学年刊》上（最好是稍微扩展而不是缩短）[21]。

有趣的是，Brouwer 还建议（着眼于选择序列理论的形式化）

而且，根据第 13 节的观点，也许“法则”的概念可以被形式化。

然而，海廷似乎没有在那个方向上做出努力。

海廷的论文确实在 1930 年不久后发表了；不过并非在《数学年刊》上，因为那时候布劳尔已经不在其编辑委员会上，而是在普鲁士科学院的会议记录中。然而，海廷的工作在发表之前就已经为人所知。海廷在 1928 年与格利文科的通信中提到了它（见下文），塔斯基和卢卡谢维奇在 1928 年的博洛尼亚会议上与伯奈斯谈到了它，而且丘奇在 1929 年给埃雷拉的信中也提到了它（Hesseling 2003: 274）。

4.3 Glivenko 1928 年和 1929 年

作为对 Barzin 和 Errera 的反应，他们认为 Brouwer 的逻辑是三值的，并且这导致它不一致，Valerii Glivenko [22] 在 1928 年通过形式手段试图证明他们是错误的。他给出了直觉主义命题逻辑的以下公理列表：

(1)(2)(3)(4)(5)(6)(7)(8)(9)p→p(p→q)→((q→r)→(p→r))(p∧q)→p(p∧q)→q(r→p)→((r→q)→(r→(p∧q)))p→(p∨q)q→(p∨q)(p→r)→((q→r)→((p∨q)→r))(p→q)→((p→¬q)→¬p)

从这些公理出发，他随后证明了

(1)(2)(3)¬¬(p∨¬p)¬¬¬p→¬p((¬p∨p)→¬q)→¬q

前两个已经在布劳尔（1908C，1925E）进行了非正式的论证；第三个是新的。现在假设在直觉主义逻辑中，一个命题可以是真的（p 成立），假的（¬p 成立），或者有第三个真值（p′成立）。显然，p→¬p′和 ¬p→¬p′，因此(¬p∨p)→¬p′；但是，根据上述引理中的第三个和列表中的公理 8，得到 ¬p′。由于 p 是任意的，这意味着没有命题具有第三个真值。（1932 年，哥德尔将证明，更一般地说，直觉主义命题逻辑对于任何自然数 n 都不是 n 值逻辑；请参见补充文档《转向海廷的形式化逻辑和算术》的第 1 节。）

像科尔莫戈洛夫在 1925 年和，正如我们将看到的，海廷在 1930 年一样，格利文科没有对这些公理的直觉有效性提供详细的解释。

格利文科随即继续这一研究方向，发表了第二篇简短论文，即格利文科 1929 年的论文，其中他展示了在一个更丰富的直觉主义命题逻辑系统中：

如果 p 在经典命题逻辑中是可证的，则在直觉主义命题逻辑中 ¬¬p 是可证的；
如果在经典命题逻辑中可以证明 ¬p，则在直觉主义命题逻辑中也可以证明。

第一个定理不是通常意义上的翻译（像科尔莫戈洛夫的那样），因为它不翻译 p 的子公式；但它足够强大，可以显示所讨论的经典和直觉主义系统是等价的。

直觉主义命题逻辑系统比格利文科先前的论文更丰富，因为现在已经添加了以下四个公理：

(A)(B)(C)(D)(p→(q→r))→(q→(p→r))(p→(p→r))→(p→r)p→(q→p)¬q→(q→p)

有趣的是，Glivenko 在他的论文中提到：“正是 A. Heyting 先生让我看到了 Brouwer 逻辑中 C 和 D 两个公理的适用性”（Mancosu 1998: 304–305n.3）。当 Glivenko 1928 年的论文发表后，两人开始通信，Heyting 给 Glivenko 写了一封信（Troelstra 1990: 11）。Kolmogorov 在 1925 年明确拒绝了 Ex Falso，因为它没有“直观基础”。根据 1928 年 10 月 13 日 Glivenko 写给 Heyting 的信，我们知道 Glivenko 是知道这一点的（Troelstra 1990: 12）。然而，在他后来完成的论文中，他根本没有提到 Kolmogorov。相反，他引用了上述关于 Heyting 的话，并通过说它是(p∨¬q)→(q→p)原则的结果来证明 D，他认为这个原则的可接受性是“非常明显的”[ 23]。然而，从 Brouwer 的观点来看，这个原则和 Ex Falso 一样令人反感 [ 24]。值得注意的是，当 Heyting 在 Heyting 1956: 102 中为 Ex Falso 辩护时，他并没有引用 Glivenko 使用的原则（Kolmogorov 在 1932 年也没有）。从 1928 年 10 月 18 日 Glivenko 的信中，人们会得到这样的印象，这个原则并不是 Heyting 实际上用来说服他的论据：

我现在被你的理由说服了，直觉主义数学不需要拒绝那个公理，因此所有反对那个公理的考虑可能超出了我们目前的主题范围。（Troelstra 1990: 12；翻译为我的）

Heyting 已经告知 Glivenko 计划在 Mathematische Annalen 上发表他（修订和翻译后的）1928 年的奖励论文。1928 年 10 月 30 日，Glivenko 问 Heyting 是否也打算包括这样一个结果：如果 p 在经典命题逻辑中是可证明的，那么在直觉主义命题逻辑中 ¬¬p 也是可证明的；因为如果是这样的话，Glivenko 就没有必要发表自己的手稿了。两周后，Glivenko 改变了主意，于 11 月 13 日写信给 Heyting 说，尽管这个结果“只是一个几乎平凡的观点”，“它的严格证明有点长”，他想独立发表它，而不依赖于 Heyting 的论文。事实上，Glivenko 的论文先于 Heyting 的论文发表，其中宣布了 Heyting 的形式化的发表；当 Heyting 在 1930 年发表他的论文时，他引用了 Glivenko 1929 年的两个定理，并承认了来自 Glivenko 1928 年的结果的使用。Heyting 在 1930 年的笔记《关于直觉主义逻辑》中，也首先提到了 Glivenko 1928 年和 1929 年的“两篇优秀文章”。

4.4 Heyting 1930

Heyting 在 Heyting 1930 年、Heyting 1930A 和 Heyting 1930B 中对直觉主义逻辑和数学进行了（部分）形式化，就逻辑部分而言，这可能是有影响力的直觉主义出版物，与他 1956 年的著作《直觉主义：一种介绍》一起。

Heyting 的形式化包括直觉主义命题和谓词逻辑、算术和分析，全部都在一个大系统中（只有任意对象的变量）。与分析有关的部分，在其预期的解释（涉及选择序列）和形式上都不是其古典对应物的子系统；这解释了为什么当时没有引起普遍兴趣。（我们上面提到的一个结果是，Brouwer 的强反例从未影响到辩论。）因此，Heyting 的形式化的这部分被基础辩论中的其他参与者忽略了。[25] 与逻辑和算术有关的部分则不同。从形式上讲，忽略它们的预期解释，可以从中提取出它们的古典对应物的子系统，其中只缺少了 PEM（或双重否定消除）。毫无疑问，这鼓励许多人给这些系统赋予了决定性的特征，正如 Heyting 在他的论文开头所指出的，根据直觉主义逻辑的观念，它们不能具备这种特征：

直觉主义数学是一种思维活动 [“Denktätigkeit”]，对于它来说，包括形式主义语言在内的任何语言都只是一种交流工具。原则上不可能建立一个与直觉主义数学等价的公式系统，因为思维的可能性不能被归纳为预先设定的有限规则的数量。正因为如此，试图重现形式语言的最重要部分，仅仅是为了其相对于普通语言更加简洁和明确；而这些特性有助于深入理解直觉主义概念并将这些概念应用于研究中。（Heyting 1930: 42 [Mancosu 1998: 311]）

然而，Heyting 本人在大约五十年后写道，

我很遗憾，我的名字今天主要与这些论文 [Heyting 1930, 1930A, 1930B] 联系在一起，这些论文非常不完善，包含许多错误。它们对我一生致力于的斗争几乎没有帮助，即更好地理解和欣赏布劳尔的思想。它们将注意力从基本思想转移到了形式系统本身上。（Heyting 1978: 15）

实际上，在这三篇论文中的第一篇中确实表达了这种注意力可能被转移的担忧：

第 4 节 [关于否定] 与经典逻辑有很大不同。在这里，我无法避免给人一种印象，即在这一节中凸显出来的差异构成了直觉主义者和形式主义者之间最重要的冲突点（这一说法已经被上面引用的话所驳斥）；这种印象的产生是因为形式主义无法表达更基本的冲突点。（Heyting 1930: 44 [Mancosu 1998: 313]）

对于包括谓词逻辑和分析的完整系统，读者可参考海廷的原始论文。海廷对直觉主义命题逻辑的公理是：

(1)(2)(3)(4)(5)(6)(7)(8)(9)(10)(11)a→(a∧a)(a∧b)→(b∧a)(a→b)→((a∧c)→(b∧c))((a→b)∧(b→c))→(a→c)b→(a→b)(a∧(a→b))→ba→(a∨b)(a∨b)→(b∨a)((a→c)∧(b→c))→((a∨b)→c)¬a→(a→b)((a→b)∧(a→¬b))→¬a

在给奥斯卡·贝克尔的一封信中，海廷描述了获得这些公理的方法，以及谓词逻辑的公理如下：

我筛选了《数学原理》的公理和定理，并在找到可接受的那些基础上，寻找了一个独立公理的系统。鉴于《数学原理》的相对完备性，我认为这样可以以最好的方式确保我的系统的完备性。实际上，从原则上讲，不可能确定一个形式系统中是否捕捉到了所有可接受的推理方式。（Heyting 致 Becker，1933 年 9 月 23 日（草稿）[van Atten 2005: 129]，原文斜体，翻译为本人所作）

正如 Heyting 在这里强调的，必须也要考虑《数学原理》的定理，因为一个定理在经典证明不可行的情况下，可能在直觉主义上是可接受的。值得注意的是，Heyting 使用了划掉的方法，就像 Kolmogorov 一样，而不是直接从布劳尔的数学构造的一般考虑中确定逻辑。（在某种程度上，Kreisel 在 20 世纪 60 年代试图系统地做到这一点。）在他关于直觉主义射影几何公理化的论文中，Heyting 已经通过以经典公理系统为指导并进行调整的方式获得了开发直觉主义系统的经验。

在 Mints 2006 年（第 2 节）中观察到，Russell 1903 年（第 18 节）通过识别 Peirce 的定律并将其用于分离暗示 PEM 的原则，预见了直觉主义命题逻辑。似乎 Heyting 当时没有意识到这一点；在 Heyting 1930 年的参考文献中，没有提到 Russell 的书。

Heyting 通过 Bernays（1926）提供的方法展示了他的公理的独立性；这种对于元数学目的使用非预期解释的方法，Heyting 毫不犹豫地接受了，但他指出这种元数学对于我们（直觉主义者）来说“不如将所有公式视为有意义的命题的方法重要”（Heyting 1930: 43 [Mancosu 1998: 312]）。

Heyting 陈述了 Glivenko 在 1929 年提出的两个定理，但没有给出证明。

与 Kolmogorov 不同，但与 Glivenko（被 Heyting 说服）相似，Heyting 接受了 Ex Falso（上述公理 10）。他对这一点进行了更详细的阐述：

公式 a→b 通常意味着：“如果 a 是正确的，则 b 也是正确的”。如果 a 和 b 是关于其正确性无需了解的常量命题，则此命题是有意义的... 可以想象的情况是，在以指定的意义证明了命题 a→b 之后，结果发现 b 始终是正确的。一旦被接受，公式 a→b 就必须保持正确；也就是说，我们必须赋予符号→一个意义，使得 a→b 仍然成立。在后来发现 a 始终为假的情况下，也可以做出同样的观察。出于这些原因，公式 [5] 和 [10] 被接受。（Heyting 1930: 44 [Mancosu 1998: 313]）

然而，这个论证是不完整的。毫无争议的是，一旦证明了 a→b，当之后证明了 ¬a 时，它应该保持不变。但是，如果 a→b 尚未被证明，为什么仅仅通过建立 ¬a 就可以使其成为可证明的呢？（Johansson 在 1935 年写信给 Heyting 时提出了这个问题；[28] 参见补充文件 Objections to the Proof Interpretation 的第 1 节）。显然，对直觉主义逻辑的解释还需要进一步的工作。

在 Heyting 发表了一系列论文之后，有三条道路可以选择，而且确实被选择了（参见 Posy 1992）：

解释和发展引发 Heyting 系统的意义解释；
从 Heyting 系统中提炼出的形式系统进行元数学研究；
寻找与直觉主义者独立但在某种程度上也具有建设性的（例如 Lorenzen 的对话语义）Heyting 系统的替代动机（部分）。

总的来说，这三条道路通向非常不同的领域，相应地有着不同的历史，其中没有统一的解释可以期望。（然而，在戈德尔 [1958 年，1970 年，1972 年] 提出并理解的辩证解释中，它们彼此接近。）遵循本解释的主题，我们的话题将保持直觉主义逻辑的意义解释。但是，在这份补充文件中，还介绍了一些形式转向的早期亮点：

转向海廷的形式化逻辑和算术

5. 显式地进行证明解释

5.1 Heyting 1930, 1931

Heyting 告诉范·达伦，他在 1927 年制定直觉主义逻辑和数学的形式化时，脑海中有（直觉主义）构造的概念来指导他。在他的形式化版本中，他并没有详细阐述连接词的含义；他只是解释了关于 a→b 的一般含义：“如果 a 是正确的，那么 b 也是正确的”（Heyting 1930: 44 [Mancosu 1998: 313]）。1930 年 Heyting 与 Freudenthal 之间的通信表明，直到那时 Heyting 手头上还没有更精细的解释；我们将在本节稍后回到这个问题。

Heyting 开始在 1930 年的两篇论文中详细阐述连接词的含义。第一篇是 Heyting 1930C，同年发表，第二篇是他在 1930 年 9 月在 Königsberg 的演讲文本，于次年发表（Heyting 1931）。

第一篇论文是对 Barzin 和 Errera 声称 Brouwer 的逻辑是三值的反应（Barzin＆Errera 1927）。 Heyting 的论文中解释连接词含义的相关要点如下。首先，给出了断言的解释：

在这里，Brouwerian 对 p 的断言如下：已知如何证明 p。我们将用 ⊢p 表示。 “证明”一词必须理解为“通过构造证明”。[原文斜体]（Heyting 1930C：959 [Mancosu 1998：307]）

然后是直觉主义否定：

⊢¬p 将意味着：“已知如何将 p 归约为矛盾”。（Heyting 1930C: 960 [Mancosu 1998: 307]）

Heyting 继续解释说，尽管在这些解释中除了 ⊢p 和 ⊢¬p 之外还有第三种情况，即既不知道如何证明 p 也不知道如何反驳它的情况，但这并不意味着存在第三个真值：

这种情况可以用 p′ 表示，但必须意识到 p′ 几乎永远不会是一个明确的陈述，因为必须考虑到将来可能成功证明 p 或 ¬p 的可能性。如果不希望冒险撤回已经说过的话，在 p′ 的情况下应该不说任何话。（Heyting 1930C: 960 [Mancosu 1998: 307]）

这驳斥了 Barzin 和 Errera 的争论。请注意，这些观点在 Brouwer 的著作中也都有。事实上，Heyting（1932: 121）反对 Barzin 和 Errera 的术语“Heyting 的逻辑”，称“那个逻辑的所有基本思想都来自 Brouwer”（翻译为我的）。但是 Heyting 的论文比 Brouwer 的论文更广为人知。反过来，Brouwer 对 Heyting 1930C 的论文非常肯定，并写信给了它发表的期刊的编辑（Brouwer to de Donder，1930 年 10 月 9 日）：

在为比利时皇家学院通报凭直觉主义的一篇笔记做准备时，我惊喜地看到我的学生 Heyting 先生发表了一篇笔记，以权威的方式阐明了我自己想要阐明的观点。我相信在 Heyting 的笔记之后，几乎没有什么需要说的了。（van Dalen 2005: 676）

Heyting 还提出了一个可证明运算符+，其中+p 表示“p 是可证明的”。如果有人认为（至少有些）命题独立于我们的数学活动而是真或假的，那么 p 和+p 之间的区别是相关的。在这种情况下，可以继续发展可证明逻辑，例如 Gödel 所做的（参见补充文件《转向 Heyting 的形式化逻辑和算术》第 1 节）。这不是直觉主义的概念，Heyting 指出，如果 p 的实现需要一个构造，那么 p 和+p 之间没有区别。他补充说，在直觉主义对否定的解释中，¬p 和+¬p 确实没有区别，因为 ¬p 的证明被定义为将 p 归约为矛盾的构造。但是 Heyting 没有将这个观点推广到所有直觉主义逻辑。本文的最后一节是对可证明运算符逻辑的进一步讨论，特别是它与否定的相互作用（例如，⊢¬+p 是 p 不可证明的断言）。但是 Heyting 最后说道，由于直觉主义者的任务是重建所有数学，同时迄今为止还没有找到任何需要使用这个可证明运算符来表达其状态（例如，表达绝对不可判定性）的命题的例子，因此不能要求直觉主义者发展这个逻辑（Heyting 1930C: 963 [Mancosu 1998: 309–310）

1930 年的 Königsberg 演讲在 1931 年发表，明确了 p、¬p 和 p∨q 的含义。这次 Heyting 明确地与现象学建立了联系：

我们在这里区分命题 [Aussagen] 和断言 [Sätze]。断言是对命题的肯定。数学命题表达了一定的期望。例如，命题“欧拉常数 C 是有理数”表达了我们可以找到两个整数 a 和 b，使得 C=a/b 的期望。也许“意图”这个词，由现象学家创造，更好地表达了这里的意思...对命题的肯定意味着意图的实现。(Heyting 1931: 113 [Benacerraf & Putnam 1983: 58–59])

与 1930 年撰写的早期论文相比，关于可证明运算符的观点被放大了：

一旦在 p 本身中打算进行构造，p 和+p 之间的区别就消失了，因为只有通过实际执行才能证明构造的可能性。如果我们仅限于那些需要构造的命题，那么可证明性的逻辑功能根本不会出现。我们可以通过仅处理“p 是可证明的”形式的命题来施加这种限制，或者换句话说，将每个意图视为具有构造意图以实现其实现的意图。就这个意义而言，直觉主义逻辑，只要没有使用+函数，就必须被理解。(Heyting 1931: 115 [Benacerraf & Putnam 1983: 60; translation modified])

在 Königsberg 讲座中，对析取的解释是：

“p∨q”表示只有当至少有一个意图 p 和 q 被实现时才能实现的意图。（Heyting 1931: 114 [Benacerraf & Putnam 1983: 59]）

而对于否定：

贝克尔（Becker）在赫斯尔（Husserl）的基础上，非常清楚地描述了它的意义。对他来说，否定是完全积极的，即原始意图中包含的矛盾意图。因此，“C 不是合理的”这个命题意味着期望能够从假设 C 是合理的这一前提中推导出矛盾。需要注意的是，命题的否定总是指导致矛盾的证明过程，即使原始命题没有提及证明过程。（Heyting 1931: 113 [Benacerraf & Putnam 1983: 59]）

Heyting 指出，这些关于析取和否定的解释，综合起来，立即反对了 PEM 的可接受性，因为需要一种通用方法，应用于任何给定的命题 p，要么产生 p 的证明，要么产生 ¬p 的证明。Heyting 在这里没有将否定的这种解释推广到蕴涵的解释。此外，需要注意的是，该过程不是基于 p 的证明，而是仅仅基于假设 p，这通常提供的信息较少。这两个问题不久之后得到了解决。在 1930 年 10 月 25 日给弗洛伊登塔尔的一封信中，Heyting 写道：

从你的言论中，我明白了“当我思考 a 时，我必须思考 b”对 a→b 的简单解释是站不住脚的；这个想法无论如何都太不确定，不能作为逻辑的基础。但是你的表述：“当 a 被证明时，b 也被证明”对我来说也不完全令人满意；当我问自己你可能是什么意思时，我相信 a→b 和否定一样，应该指的是一个证明过程：“我拥有一个构造，它可以从每个 a 的证明中推导出一个 b 的证明”。在接下来的内容中，我将坚持这种解释。因此，a→b 和+a→+b 之间没有区别。（Troelstra 1983: 206–207；翻译为本人所作）

这个解释的蕴涵，即成为标准的那个，只在 Heyting 1934: 14 中以印刷形式引入；在他的论文 1932C 中，Heyting 使用了 Kolmogorov 1932 中给出的解释（见下文）。

Heyting 的这两篇论文都没有对 Ex Falso 的有效性进行论证。

5.2 Heyting 的影响

一些影响（或可能的影响）导致 Heyting 提出证明解释的理论。以下是 Heyting 在 1927 年之前看到的出版物，因为他在他的论文中提到了它们（1925 年：93-94）：

Brouwer 1907 年（第 3 章）和 Brouwer 1908C，强烈强调直觉主义逻辑关注可构造性的保持。（见上文 2.1 节。）
Brouwer 在 1924 年提出的杆定理的证明，于 1924 年 3 月 29 日提交（Brouwer 1924D1：189 [Mancosu 1998：36]），以及可能也包括 1927 年的后续版本，该版本的手稿于 1926 年 4 月 28 日提交（Brouwer 1927B：75 [van Heijenoort 1967：446]）；两者都展示了如何在数学上将证明作为对象进行操作。（见上文 3.1.2 节。）
Weyl 1921，在那里，普遍和存在的定理被认为根本不是真正的判断，而是“Urteilsanweisungen”（判断指令）和“Urteilsabstrakte”（判断抽象），从而强调这样的定理为了其合理化需要通过一种构造方法来支持。布劳尔在对韦伊尔的论文的注释中表示同意，他说：“这只是一个名称问题，当然不反映我对此缺乏洞察力”（Mancosu 1998: 122）。

另一个可能的影响是布劳尔对虚拟排序公理的未发表阐述（见上文 3.1.3 节）。Dirk van Dalen（个人通信）怀疑，虽然海廷可能没有参加这个讲座，但他在其他场合听布劳尔发表类似的评论（例如在 1922 年至 1925 年期间，海廷在布劳尔指导下撰写论文时，也考虑了直觉主义排序）。

5.3 科尔莫戈洛夫 1932 年和海廷 1934 年

1932 年，科尔莫戈洛夫提出了一个关于问题及其解决方案的逻辑，并指出这个解释所验证的逻辑在形式上等同于海廷于 1930 年提出的直觉主义命题和谓词逻辑。此外，他认为这提供了比海廷更好的解释。

科尔莫戈洛夫的想法是这样的：

如果 a 和 b 是两个问题，那么 a∧b 表示“解决问题 a 和问题 b”，而 a∨b 表示“解决问题 a 和问题 b 中至少一个”。此外，a⊃b 表示“给出 a 的解决方案的前提下解决 b”，或者等价地说，“将 b 的解决方案归约为 a 的解决方案”……¬a 表示“在给出 a 的解决方案的前提下得到矛盾”……(x)a(x)通常表示“为每个 x 的单个值提供 a(x)的一般解决方法”。（科尔莫戈洛夫 1932 年：59 [Mancosu 1998 年：329）

然后，他列举了 Heyting 的命题逻辑公理（使用 Heyting 的编号），并通过讨论一个例子，明确指出当将其解释为关于问题及其解决方案的陈述时，这些公理都成立。他还指出，a∨¬a 是问题的解释/理论

为了给出一种通用方法，对于每个问题 a，要么找到 a 的解决方案，要么从 a 的解决方案的存在中推导出矛盾！
特别是，如果问题 a 是一个命题的证明，则必须拥有一种通用方法，要么证明该命题，要么将其归约为矛盾。（Kolmogorov 1932: 63 [Mancosu 1998: 332]）。

在他的论文的第二部分中，科尔莫戈洛夫认为，鉴于直觉主义的认识论原则，

直觉主义逻辑应该被问题演算所取代，因为它的对象实际上不是理论命题，而是问题。（科尔莫戈洛夫 1932 年：58 [Mancosu 1998 年：328]）

他认为他的解释是对海廷的一种替代，并且是一种更可取的替代，这一点在附加的证明中再次强调：

这种对直觉主义逻辑的解释与海廷先生在《认识论》第 2 卷（1931 年：106）中提出的观点密切相关 [Heyting 1931]；然而，在海廷的观点中，命题和问题之间缺乏明确的区分。（科尔莫戈洛夫 1932：65 [Mancosu 1998: 334]）

但是，海廷是否愿意进行这种区分并不清楚。如果我们将命题的概念理解为命题在我们对其真假的认识之外是独立于真或假的，那么海廷将很乐意同科尔莫戈洛夫一起认为命题与问题是不同的；但是，一旦我们采纳了命题表达了我们的数学构造所实现（使命题成为真）或者失望（使命题成为假）的意图的观点，而这正是海廷实际持有的观点，那么命题和问题之间似乎就没有本质区别了。科尔莫戈洛夫本人已经指出问题可能包括找到命题的证明；利用这一点，我们可以得出以下两个命题概念是相同的结论：

命题表达了对构造的意图
命题提出了需要通过进行构造来解决的问题

基本思想是，意义 1 中的命题引发了寻找满足表达意图的构造的问题，而在意义 2 中提出的问题的解决方案也用于满足解决该问题的构造的意图；这在 Martin-Löf 的一个小论证中得到了充分的明确，详细介绍在 Sundholm 1983: 158–159 中。

在 1931 年 10 月 12 日写给 Heyting 的一封信中，Kolmogorov 实际上同意 Heyting 和他之间的区别主要是一个术语问题（Troelstra 1990: 15）。

Heyting 后来声称 Kolmogorov 的意义解释和他自己的解释是相同的（Heyting 1958C: 107）。到 1937 年，Kolmogorov 似乎也相信了这一点，在 Zentralblatt 的一篇评论中，评论了 Freudenthal 和 Heyting 之间的交流（在补充文件 Objections to the Proof Interpretation 的第 1 节中讨论），他一直谈到“意图或问题”（Kolmogorov 1937）。在这个交流中，Freudenthal（1937: 114）曾说 Heyting 和 Kolmogorov 的解释之间“没有本质区别”。最后，Oskar Becker 在 1934 年 9 月写给 Heyting 的一封信中指出，Heyting 的解释是 Kolmogorov 的一般化，因为“问题”和“解决方案”是意图和实现的特例。“直觉主义逻辑因此是一种‘意图的演算’”。[ 30]

然而，对于 Heyting 和 Kolmogorov 对逻辑的解释的认同存在一个复杂性，这是由于 Kolmogorov 在特定情况下也接受了不涉及具体构造的解决方案。Kolmogorov 说“一旦 ¬a 得到解决，那么 a 的解决就是不可能的，而问题 a→b 就没有内容”（Kolmogorov 1932: 62 [Mancosu 1998: 331]），并提出“证明一个问题没有内容 [由于一个不可能的假设] 将始终被视为它的解决方案”（Kolmogorov 1932: 59: [Mancosu 1998: 329]）。综合起来，这就为 Ex Falso，¬a→(a→b)提供了一个理由。

以这种方式扩展术语“解决方案”的含义似乎并不完全不合理，因为与具体解决方案一样，不可能性证明也提供了所谓的“认识闭合性”：就像具体解决方案一样，它提供了一个完全令人信服的理由来停止解决某个问题。（这种“高阶”解决方案也可以从希尔伯特的计划中找到，例如，希尔伯特 1900 年：51。）请注意，这种对 Ex Falso 的辩护并没有试图描述一个反事实的数学构造过程；因此，科尔莫戈洛夫在 1932 年的辩护实际上与他在 1925 年拒绝 Ex Falso 的理由并不矛盾，即不能建设性地断言不可能的事物的后果。相反，1932 年的解决方案引入了一个规定，以实现逻辑理论的完整性。

另一方面，尽管科尔莫戈洛夫的规定既不是不合理的，也不是没有动机的，但在布劳威尔的逻辑描述观念中，显然没有规定的位置。因此，“证明解释”似乎比“BHK 解释”更适合作为布劳威尔逻辑的解释名称。

然而，在海廷的解释中，与科尔莫戈洛夫的 Ex Falso 的辩护类似的辩护似乎是不可能的：当显示出一个解决方案是不可能的时，一个问题可能会找到一个“高阶”解决方案，但说一个意图找到“高阶”实现当显示它无法实现时是没有意义的。解决方案的概念似乎允许一个合理的扩展，而实现的概念则不允许。在他 1934 年的著作中，海廷用科尔莫戈洛夫的术语而不是他自己的术语解释了 Ex Falso。在陈述了公理 ¬a⊃(a⊃b)之后，他说：

适当地解释“减少”的概念是这样的，即证明无法同时解决问题 a 的不可能性，将任何问题的解决都简化为问题 a 的解决。（Heyting 1934: 15; 本文翻译）

显然，Kolmogorov 自己的解释与 Heyting 在 Kolmogorov 的术语中的解释之间存在差异。Heyting 说，¬a 的证明建立了将任何问题的解决简化为问题 a 的解决，而 Kolmogorov 则说，它证明了将任何问题的解决简化为问题 a 的解决已经没有内容。人们有这样的印象，Heyting 在对 Ex Falso 的解释中尽可能接近于在前提和结论之间具体建设性联系方面对普通蕴涵的解释；这在他在 1956 年对 Ex Falso 的解释中更加清楚（见下文 5.4 节）。（请注意，Heyting 和 Kolmogorov 从未通过给出 1929 年 Glivenko 论文中也提到的传统论证（基于析取三段论）来证明 Ex Falso；请参见上文 4.3 节。）

更一般地说，Heyting 1934 年对逻辑的解释在很大程度上采用了 Kolmogorov 的风格，而不是 Heyting 自己的意图和实现的解释。（后者仅在解释蕴涵时提到（Heyting 1934: 14）。）也许这是因为 Heyting（1934: 14）同意 Kolmogorov（1932: 58）的观点，即用问题和解决方案的术语进行解释为非直觉主义者提供了有用的解释，同时对于直觉主义者来说，它们是一样的。在他的短文 1932C 中，题为“将直觉主义逻辑应用于逻辑演算的完备性定义”，Heyting 使用了 Kolmogorov 的解释而不是他自己的解释。考虑到主题，这是可以预料的。

5.4 Heyting 1956

在他 1956 年的重要著作《直觉主义导论》中，Heyting 将逻辑连接词解释如下（97-98，102）：

“数学命题 p 总是要求进行具有一定给定属性的数学构造；只要进行了这样的构造，就可以断言它”。
"当且仅当 p 和 q 都可以断言时，可以断言 p∧q"。
"当且仅当 p 和 q 中至少有一个命题可以断言时，可以断言 p∨q"。
"当且仅当我们拥有一个从假设一个构造 p 被执行导致矛盾的构造时，可以断言 ¬p"。
“当且仅当我们拥有一个构造 r，该构造与任何证明 p 的构造（假设后者已完成）结合在一起，将自动产生一个证明 q 的构造时，可以断言蕴含 p→q。”
“⊢(∀x)p(x)意味着对于 Q 中的每个 x，p(x)都为真；换句话说，我们拥有一种通用的构造方法，如果选择了 Q 的任何元素 a，通过特化可以得到构造 p(a)。”
“当且仅当已经构造出 Q 的一个元素 a，使得 p(a)为真时，(∃x)p(x)将为真。”

注意，这些解释不是基于证明条件，而是基于断言条件。这可能在解释蕴含的特定情况下有所不同，其中，我们不仅可以根据某种条件来判断某事物是否是 p 的证明，还可以考虑到，根据假设，已经实现了 p 的具体构造。正如我们在 3.1.2 节中所看到的，能够这样做对于布劳尔的 Bar 定理的证明至关重要。

在同样的页面上，Heyting 还给出了对 Ex Falso 的以下解释：

公理 X [¬p→(p→q)] 可能在直觉上不太清晰。事实上，它增加了对蕴含定义的精确性。你还记得，只有当我们拥有一个与构造 p 相结合的构造，才能断言 p→q。现在假设 ⊢¬p，也就是说，我们从假设 p 被执行中推导出了一个矛盾。那么，在某种意义上，这可以被视为一种构造，它与 p 的证明（这是不存在的）相结合，导致了 q 的证明。（Heyting 1956: 102）

人们很容易认识到 Heyting 试图尽可能地解释 Ex Falso，就像其他蕴涵一样，即通过提供一个具体的构造，从前提到结论。在试图“在某种意义上”提供一个构造的过程中，这种解释显然与 Kolmogorov 在 1932 年的规定不同。但它也不符合 Heyting 最初关于逻辑的解释，即以意图指向构造和实现这种意图的方式。因为要实现对特定构造的意图，我们必须展示该构造；我们必须展示一个将 p 的任何证明转化为 q 的构造。但是，一个从假设 p 到达矛盾的构造，因此一般而言不会到达 q，如何能够导致 q 呢？不能说这样的构造在某种意义上存在。Heyting 在这里使用的“在某种意义上”是没有构造的。

即使在直觉主义运动中，也并非每个人都同意 Heyting 对逻辑的解释。这在一份补充文件中讨论：

对证明解释的反对意见

最后，本文尚未讨论布劳尔的前辈，布劳尔“强反例”的更复杂方面，对循环性和非预言性的证明解释的反对意见，以及对证明解释的后期发展。这些将成为未来更新的主题。

Bibliography

Brouwer’s writings are referred to according to the scheme in the bibliography van Dalen 1997a; Gödel’s, according to the bibliography in Gödel 1986, Gödel 1990, Gödel 1995 (except for Gödel 1970); Heyting’s, according to the bibliography Troelstra et al. 1981 (except for Heyting 1928).

Apostel, L., 1972, “Negation: The tension between ontological positivity (negationless positivity) and anthropological negativity (positively described)”, Logique et Analyse, 15(57–58): 209–317. [Apostel 1972 available online]
Artemov, Sergei N., 2001, “Explicit provability and constructive semantics”, Bulletin of Symbolic Logic, 7(1): 1–36. doi:10.2307/2687821
Arruda, Ayda Ignez, 1978, “Some remarks on Griss’ logic of negationless intuitionistic mathematics”, in Mathematical Logic, Proceedings of the 1st Brazilian Conference on Mathematical Logic, Campinas 1977 (Lecture Notes in Pure and Applied Mathematics 39), A.I. Arruda, N.C.A. da Costa, R. Chuaqui (eds.), 9–29.
van Atten, Mark, 2004a, “Review of Dennis E. Hesseling, Gnomes in the Fog. The Reception of Brouwer’s Intuitionism in the 1920s”, Bulletin of Symbolic Logic, 10(3): 423–427. doi:10.2307/3185194
–––, 2004b, On Brouwer, Belmont, CA: Wadsworth.
–––, 2005, “The correspondence between Oskar Becker and Arend Heyting”, in Oskar Becker und die Philosophie der Mathematik, V. Peckhaus (ed.), München: Wilhelm Fink, 119–142.
–––, 2009, “The hypothetical judgement in the history of intuitionistic logic”, in Logic, Methodology, and Philosophy of Science 13: Proceedings of the 2007 International Congress in Beijing, C. Glymour, W. Wang, and D. Westerståhl, eds., London: King’s College Publications, 122–136.
–––, 2018, “The Creating Subject, the Brouwer-Kripke Schema, and infinite proofs”, Indagationes Mathematicae, 29: 1565–1636. doi: 10.1016/j.indag.2018.06.005
van Atten, Mark, Göran Sundholm, Michel Bourdeau, and Vanessa van Atten, 2014, “‘Que les principes de la logique ne sont pas fiables.’ Nouvelle traduction française annotée et commentée de l’article de 1908 de L.E.J. Brouwer”, Revue d’Histoire des Sciences, 67(2): 257–281. doi:10.3917/rhs.672.0257
van Atten, Mark, Pascal Boldini, Michel Bourdeau, and Gerhard Heinzmann (eds.), 2008, One Hundred Years of Intuitionism (1907–2007). The Cerisy Conference, Basel: Birkhäuser. doi:10.1007/978-3-7643-8653-5
van Atten, Mark and Göran Sundholm, 2017, “L.E.J. Brouwer’s ‘Unreliability of the logical principles’: A new translation, with an introduction”, History and Philosophy of Logic, 38(1): 24–47. doi:10.1080/01445340.2016.1210986
Barzin, M. and A. Errera, 1927, “Sur la logique de M. Brouwer”, Académie Royale de Belgique, Bulletin de la classe des sciences, 13: 56–71.
Bazhanov, Valentin A., 2003, “The Scholar and the ‘Wolfhound Era’: The Fate of Ivan E. Orlov’s Ideas in Logic, Philosophy, and Science”, Science in Context, 16(4): 535–550. doi:10.1017/S0269889703000954
Becker, Oskar, 1927, “Mathematische Existenz. Untersuchungen zur Logik und Ontologie mathematischer Phänomene”, Jahrbuch für Philosophie und phänomenologische Forschung, 8: 439–809.
–––, 1930, “Zur Logik der Modalitäten”, Jahrbuch für Philosophie und phänomenologische Forschung, 11: 497–548.
Benacerraf, Paul and Hilary Putnam (eds.), 1983, Philosophy of Mathematics: Selected Readings, second edition, Cambridge: Cambridge University Press. doi:10.1017/CBO9781139171519
Bergson, Henri, 1907, L’Évolution Créatrice, Paris: Félix Alcan.
Bernays, Paul, 1926, “Axiomatische Untersuchung des Aussagen-Kalküls der ‘Principia Mathematica’”, Mathematische Zeitschrift, 25: 305–320. doi:10.1007/BF01283841
–––, 1967, “Hilbert, David”, in The Encyclopedia of Philosophy, vol. 3, Paul Edwards (ed.), New York: Macmillan.
Beth, Evert W., 1956, “Semantic Construction of Intuitionistic Logic”, Mededelingen der Koninklijke Nederlandse Akademie van Wetenschappen. Afdeling Letterkunde, 19(11): 357–388.
–––, 1966, The Foundations of Mathematics: A Study in the Philosophy of Science, second revised edition, New York: Harper & Row.
Blaschek, Günther, 1994, Object-Oriented Programming: with Prototypes, Berlin: Springer. doi:10.1007/978-3-642-78077-6
Borwein, Jonathan M., 1998, “Brouwer-Heyting Sequences Converge”, Mathematical Intelligencer, 20(1): 14–15. doi:10.1007/BF03024393
Brouwer, L.E.J., 1907, Over de Grondslagen der Wiskunde (On the Foundations of Mathematics), Ph.D. thesis, Universiteit van Amsterdam. English translation in Brouwer 1975: 11–101.
–––, 1908C, “De onbetrouwbaarheid der logische principes” (The Unreliability of the Logical Principles), Tijdschrift voor Wijsbegeerte, 2: 152–158. English translation in Van Atten and Sundholm 2017. An older English translation is in Brouwer 1975: 107–111. doi:10.1016/B978-0-7204-2076-0.50009-X
–––, 1918B, “Begründung der Mengenlehre unabhängig vom logischen Satz vom ausgeschlossenen Dritten. Erster Teil, Allgemeine Mengenlehre”, KNAW Verhandelingen, 5: 1–43. Also in Brouwer 1975: 150–190 (in German). doi:10.1016/B978-0-7204-2076-0.50015-5
–––, 1919A, “Begründung der Mengenlehre unabhängig vom logischen Satz vom ausgeschlossenen Dritten. Zweiter Teil, Theorie der Punktmengen”, KNAW Verhandelingen, 7: 1–33. Also in Brouwer 1975: 191–221 (in German). doi:10.1016/B978-0-7204-2076-0.50016-7
–––, 1919D, “Intuitionistische Mengenlehre”, Jahresbericht D.M.V., 28: 203–208. English translation in Mancosu 1998: 23–27.
–––, 1921A, “Besitzt jede reelle Zahl eine Dezimalbruchentwicklung?”, Mathematische Annalen, 83(3–4): 201–210. English translation in Mancosu 1998: 28–35. doi:10.1007/BF01458382
–––, 1924D1, “Bewijs dat iedere volle functie gelijkmatig continu is”, KNAW verslagen, 33: 189–193. English translation in Mancosu 1998: 36–39.
–––, 1924N, “Über die Bedeutung des Satzes vom ausgeschlossenen Dritten in der Mathematik, insbesondere in der Funktionentheorie”, Journal für die reine und angewandte Mathematik, 154: 1–7. English translation in van Heijenoort 1967: 335–341.
–––, 1925E, “Intuitionistische Zerlegung mathematischer Grundbegriffe”, Jahresbericht D.M.V., 33: 251–256. English translation in Mancosu 1998: 287–289 (sections 2–4), 290–292 (section 1).
–––, 1926A, “Zur Begründung der intuitionistischen Mathematik, II”, Mathematische Annalen, 95: 453–472. doi:10.1007/BF01206621
–––, 1926B2, “Intuitionistische Einführung des Dimensionsbegriffes”, Proceedings Koninklijke Akademie van Wetenschappen Amsterdam, 29: 855–873.
–––, 1927B, “Über Definitionsbereiche von Funktionen”, Mathematische Annalen, 97: 60–75. English translation of sections 1–3 in van Heijenoort 1967: 457–463. doi:10.1007/BF01447860
–––, 1928A2, “Intuitionistische Betrachtungen über den Formalismus”, Proceedings Koninklijke Akademie van Wetenschappen Amsterdam, 31: 374–379. English translation in Mancosu 1998: 40–44. [Brouwer 1928A2 available online]
–––, 1929A, “Mathematik, Wissenschaft und Sprache”, Monatshefte für Mathematik und Physik, 36: 153–164. English translation in Mancosu 1998: 45–53. doi:10.1007/BF02307611
–––, 1930A, Die Struktur des Kontinuums, Wien: Komitee zur Veranstaltung von Gastvorträgen ausländischer Gelehrter der exakten Wissenschaften. English translation in Mancosu 1998: 54–63.
–––, 1933A2, “Willen, weten, spreken” (Volition, Knowledge, Language), in De Uitdrukkingswijze der Wetenschap, L.E.J. Brouwer et al., Groningen: Noordhoff, 45–63. English translation in van Stigt 1990: 418–431. Partial English translation in Brouwer 1975: 443–446.
–––, 1942A, “Zum freien Werden von Mengen und Funktionen”, Proceedings Nederlandse Akademie van Wetenschappen Amsterdam, 45: 322–323. Also Indagationes Mathematicae, 4 (1942): 107–108.
–––, 1942B, “Die repräsentierende Menge der stetigen Funktionen des Einheitskontinuums”, Proceedings Nederlandse Akademie van Wetenschappen Amsterdam, 45: 443. Also Indagationes Mathematicae, 4 (1942): 154.
–––, 1948A, “Essentieel negatieve eigenschappen” (Essentially Negative Properties), Proceedings Koninklijke Nederlandse Akademie van Wetenschappen Amsterdam, 51: 963–964. Also Indagationes Mathematicae, 10 (1948): 322–323. English translation in Brouwer 1975: 478–479. doi:10.1016/B978-0-7204-2076-0.50053-2
–––, 1949A, “De non-aequivalentie van de constructieve en de negatieve orderelatie in het continuum” (The Non-Equivalence of the Constructive and the Negative Order Relation on the Continuum), Proceedings Koninklijke Nederlandse Akademie van Wetenschappen Amsterdam, 52:122–124. Also Indagationes Mathematicae, 11 (1949): 37–39. English translation in Brouwer 1975: 495–496. doi:10.1016/B978-0-7204-2076-0.50055-6
–––, 1949B, “Contradictoriteit der elementaire meetkunde” (Contradictority of Elementary Geometry), Proceedings Koninklijke Nederlandse Akademie van Wetenschappen Amsterdam, 52: 315–316. Also Indagationes Mathematicae, 11 (1949): 89–90. English translation in Brouwer 1975: 497–498. doi:10.1016/B978-0-7204-2076-0.50056-8
–––, 1949C, “Consciousness, Philosophy and Mathematics”, Proceedings of the 10th International Congress of Philosophy, Amsterdam 1948, Amsterdam: North-Holland, 3: 1235–1249.
–––, 1952B, “Historical Background, Principles and Methods of Intuitionism”, South African Journal of Science, 49: 139–146.
–––, 1954A, “Points and Spaces”, Canadian Journal of Mathematics, 6: 1–17. doi:10.4153/CJM-1954-001-9
–––, 1954F, “An Example of Contradictority in Classical Theory of Functions”, Proceedings Koninklijke Nederlandse Akademie van Wetenschappen Amsterdam, 57: 204–205. Also Indagationes Mathematicae, 16 (1954): 204–205. doi:10.1016/S1385-7258(54)50030-2
–––, 1955, “The Effect of Intuitionism on Classical Algebra of Logic”, Proceedings of the Royal Irish Academy, 57: 113–116.
–––, 1975, Collected Works. I: Philosophy and Foundations of Mathematics, Arend Heyting (ed.), Amsterdam: North-Holland.
–––, 1977, Collected Works. II: Geometry, Analysis, Topology and Mechanics, H. Freudenthal (ed.), Amsterdam: North-Holland.
–––, 1981A, Brouwer’s Cambridge Lectures on Intuitionism, Cambridge: Cambridge University Press.
Brouwer, L.E.J., Fred. van Eeden, J. van Ginneken, and S.J.G. Mannoury, 1937, “Signifiese dialogen”, Synthese, 2: 168–174, 261–268, 316–324. doi:10.1007/BF00880415 doi:10.1007/BF00880431 doi:10.1007/BF00880440
–––, 1939, Signifische dialogen, Utrecht: Erven J. Bijleveld. Partial English translation in Brouwer 1975: pp. 447–452.
Chronique générale, 1949. “Chronique générale”, Revue Philosophique de Louvain, 47(15): 432–436. [Chronique générale 1949 available online]
Colacito, Almudena, Dick de Jongh, and Ana Lucia Vargas, 2017, “Subminimal Negation”, Soft Computing, 2(1): 165–174. doi:10.1007/s00500-016-2391-8
Colson, Loïc, and David Michel, 2007, “Pedagogical Natural Deduction Systems: the Propositional Case”, Journal of Universal Computer Science, 13(10): 1396–1410. [Colson & Michel 2007 available online]
–––, 2008, “Pedagogical Second-order Propositional Calculi”, Journal of Logic and Computation, 18(4): 669–695. doi:10.1093/logcom/exn001
–––, 2009, “Pedagogical Second-order λ-calculus”, Theoretical Computer Science, 410(42): 4190–4203. doi:10.1016/j.tcs.2009.04.020
van Dalen, Dirk, 1973, “Lectures on intuitionism”, in Mathias & Rodgers 1973: 1–94. doi:10.1007/BFb0066771
–––, 1997, “A Bibliography of L.E.J. Brouwer”, Utrecht Logic Group Preprint Series, no. 175 [van Dalen 1997 updated preprint available from Universiteit Utrecht]. Updated version in van Atten et al. 2008: 343–390. doi:10.1007/978-3-7643-8653-5_22
–––, 1999, Mystic, Geometer, and Intuitionist. The Life of L.E.J. Brouwer. 1: The Dawning Revolution, Oxford: Clarendon Press.
–––, 2001a, L.E.J. Brouwer 1881–1966. Een Biografie. Het Heldere Licht van de Wiskunde, Amsterdam: Bert Bakker.
–––, 2001b, L.E.J. Brouwer en de Grondslagen van de Wiskunde, Utrecht: Epsilon.
–––, 2004, “Kolmogorov and Brouwer on constructive implication and the Ex Falso rule”, Russian Mathematical Surveys, 59(2): 247–257. doi:10.1070/RM2004v059n02ABEH000717
–––, 2005, Mystic, Geometer, and Intuitionist. The Life of L.E.J. Brouwer. 2: Hope and Disillusion, Oxford: Clarendon Press.
–––, 2008, “Another look at Brouwer’s dissertation”, in van Atten et al. 2008: 3–20. doi:10.1007/978-3-7643-8653-5_1
––– (ed.), 2011, The Selected Correspondence of L.E.J. Brouwer, London: Springer. An online supplement (link and password on the copyright page of the book) presents most of the extant correspondence, but without English translations. doi:10.1007/978-0-85729-537-8
van Dalen, Dirk and Volker R. Remmert, 2007, “Ce périodique foncièrement international: the birth and youth of Compositio Mathematica”, Nieuw Archief voor Wiskunde 5th series, 8(3): 178–189. [van Dalen & Remmert 2007 available online]
van Dantzig, D., 1947a, “On the principles of intuitionistic and affirmative mathematics. I”, Proceedings Koninklijke Nederlandse Akademie van Wetenschappen Amsterdam, 50: 918–929. Also Indagationes Mathematicae, 9: 429–440.
–––, 1947b, “On the principles of intuitionistic and affirmative mathematics. II”, Proceedings Koninklijke Nederlandse Akademie van Wetenschappen Amsterdam, 50:1092–1103. Also Indagationes Mathematicae, 9: 506–517.
–––, 1949, “Comments on Brouwer’s Theorem on Essentially-negative predicates”, Proceedings Koninklijke Nederlandse Akademie van Wetenschappen Amsterdam, 52: 949–957. Also Indagationes Mathematicae, 11: 347–355.
–––, 1951, “Mathématique stable et mathématique affirmative”, Congrès International de Philosophie des Sciences, 1949, II Logique (Actualités scientifiques et industrielles 1134), Paris: Hermann & Cie, pp. 123–135.
Demange, Vincent, 2015, “Pedagogical lambda-cube: the λ² case”, Journal of Logic and Computation, 25(3): 743–779. doi: 10.1093/logcom/exu049
Dequoy, Nicolle, 1952 [1955], Axiomatique intuitionniste sans négation de la géométrie projective, PhD thesis, Université de Paris. Published in 1955, Paris:Gauthier-Villars (Collection de logique mathématique ; sér. A, 6).
Destouches-Février, Paulette, 1945a, “Rapports entre le calcul des problèmes et le calcul des propositions”, Comptes Rendus de l’Académie des sciences, 220: 484–486. [Destouches-Février 1945a available online]
–––, 1945b, “Logique adaptee aux théories quantiques”, Comptes Rendus de l’Académie des sciences, 221: 287–288. [Destouches-Février 1945b available online]
–––, 1947a, “Sur la notion d’adequation et le calcul minimal de Johannsson”, Comptes Rendus de l’Académie des sciences, 224: 545–547. [Destouches-Février 1947a available online]
–––, 1947b, “Esquisse d’une mathématique intuitioniste positive”, Comptes Rendus de l’Académie des sciences, 225: 1241–1243. [Destouches-Février 1947b available online]
–––, 1948, “Logique de l’intuitionisme sans négation et logique de l’intuitionisme positif”, Comptes Rendus de l’Académie des sciences, 226: 38–39. [Destouches-Février 1948 available online]
–––, 1949, “Connexions entre les calculs des constructions, des problèmes, des propositions”, Comptes Rendus de l’Académie des sciences, 228: 31–33. [Destouches-Février 1949 available online]
–––, 1951, “Sur l’intuitionnisme et la conception strictement constructive”, Proceedings Koninklijke Nederlandse Akademie van Wetenschappen Amsterdam, 54: 80–86. doi:10.1016/S1385-7258(51)50012-4
Došen, Kosta, 1992, “The First Axiomatization of Relevant Logic”, Journal of Philosophical Logic, 21(4): 339–356. doi:10.1007/BF00260740
Dummett, Michael A.E., 1973, “The Justification of Deduction”, British Academy, London. Page references to reprint in Dummett 1978: 290–318. [Dummett 1973 available online]
–––, 1978, Truth and Other Enigmas, Cambridge MA: Harvard University Press.
–––, 2000, Elements of Intuitionism, second revised edition, Oxford: Clarendon Press.
Ewald, William Bragg, 1996, From Kant to Hilbert: A Source Book in the Foundations of Mathematics, 2 vols, Oxford: Oxford University Press.
Fitting, Melvin Chris, 1969, Intuitionistic Logic, Model Theory and Forcing, (Studies in Logic and the Foundations of Mathematics, 54), Amsterdam: North-Holland.
Fraenkel, Abraham A., Yehoshua Bar-Hillel, and Azriel Levy, 1973, Foundations of Set Theory, second revised edition, (Studies in Logic and the Foundations of Mathematics, 67), Amsterdam: North-Holland. The revision of the chapter on intuitionism (4) was done by Dirk van Dalen.
Franchella, Miriam, 1994a, “Heyting’s contribution to the change in research into the foundations of mathematics”, History and Philosophy of Logic, 15(2): 149–172. doi:10.1080/01445349408837229
–––, 1994b, “Brouwer and Griss on intuitionistic negation”, Modern Logic, 4(3): 256–265. [Franchella 1994b available online]
–––, 1995, “L.E.J. Brouwer towards intuitionistic logic”, Historia Mathematica, 22(3): 304–322. doi:10.1006/hmat.1995.1026
–––, 2008, Con gli occhi negli occhi di Brouwer, Monza: Polimetrica.
Freudenthal, Hans, 1937a, “Zum intuitionistischen Raumbegriff”, Compositio Mathematica, 4: 82–111. [Freudenthal 1937a available online]
–––, 1937b, “Zur intuitionistischen Deutung logischer Formeln”, Compositio Mathematica, 4: 112–116. [Freudenthal 1937b available online]
–––, 1937c, “Nachwort”, Compositio Mathematica, 4: 118. [Freudenthal 1937c available online]
–––, 1973, Mathematics as an Educational Task, Dordrecht:Reidel.
Gentzen, Gerhard, 1934, “Untersuchungen über das logische Schliessen”, Mathematische Zeitschrift, 39: 176–210, 405–431. English translation in Gentzen 1969: 68–131. doi:10.1007/BF01201353
–––, 1969, The Collected Papers of Gerhard Gentzen, M.E. Szabo (ed. and trans.), Amsterdam: North-Holland.
Georgacarakos, G.N., 1982, “The Semantics of Minimal Intuitionism”, Logique et Analyse, 25(100): 383–397. [Georgacarakos 1982 available online]
Gilmore, P.C., 1953a, “The effect of Griss’ criticism of the intuitionistic logic on deductive theories formalized within the intuitionistic logic. I”, Proceedings Koninklijke Nederlandse Akademie van Wetenschappen Amsterdam, 56: 162–174. Also Indagationes Mathematicae, 15: 162–174. doi:10.1016/S1385-7258(53)50022-8
–––, 1953b, “The effect of Griss’ criticism of the intuitionistic logic on deductive theories formalized within the intuitionistic logic. II”, Proceedings Koninklijke Nederlandse Akademie van Wetenschappen Amsterdam, 56: 175–186. Also Indagationes Mathematicae, 15: 175–186. doi:10.1016/S1385-7258(53)50023-X
–––, 1953c, “Griss’ criticism of the intuitionistic logic and the theory of order”, Proceedings of the 11th International Congress of Philosophy, Brussels 1953, Amsterdam: North-Holland, 5: 98–104.
–––, 1956, “Mathématique stable et Mathématique affirmative, by D. van Dantzig”, Journal of Symbolic Logic, 21(3): 323–324. doi:10.2307/2269134
Glivenko, V., 1928, “Sur la logique de M. Brouwer”, Académie Royale de Belgique, Bulletin de la classe des sciences, 14: 225–228.
–––, 1929, “Sur quelques points de la logique de M. Brouwer”, Académie Royale de Belgique, Bulletin de la classe des sciences, 5(15): 183–188. English translation in Mancosu 1998: 301–305.
Gödel, Kurt, 1932, “Zum intuitionistischen Aussagenkalkül”, Anzeiger der Akademie der Wissenschaften in Wien, 69: 65–66. Also, with English translation, in Gödel 1986: 222–225.
–––, 1932f, “Heyting, Arend: Die intuitionistische Grundlegung der Mathematik”, Zentralblatt für Mathematik und ihre Grenzgebiete, 2: 321–322. Also, with English translation, in Gödel 1986: 246–247.
–––, 1933e, “Zur intuitionistischen Arithmetik und Zahlentheorie”, Ergebnisse eines mathematischen Kolloquiums, 4: 34–38. Also, with English translation, in Gödel 1986: 286–295.
–––, 1933f, “Eine Interpretation des intuitionistischen Aussagenkalküls”, Ergebnisse eines mathematischen Kolloquiums, 4: 39–40. Also, with English translation, in Gödel 1986: 300–303.
–––, *1933o, “The present situation in the foundations of mathematics”, text of a lecture in Cambridge, MA, in Gödel 1995: 45–53.
–––, *1941, “In what sense is intuitionistic logic constructive?”, text of a lecture at Yale, in Gödel 1995: 189–200.
–––, 1958, “Über eine bisher noch nicht benutzte Erweiterung des finiten Standpunktes”, Dialectica, 12(3–4): 280–287. Also, with English translation, in Gödel 1990: 240–251. doi:10.1111/j.1746-8361.1958.tb01464.x
–––, 1970, “On an extension of finitary mathematics which has not yet been used”, Circulated earlier version of Gödel 1972.
–––, 1972, “On an extension of finitary mathematics which has not yet been used”, Revised and expanded translation of Gödel 1958, first published in Gödel 1990: 271–280.
–––, 1986–, Collected Works, Solomon Feferman et al. (eds.), Oxford: Oxford University Press.
- –––, 1986, I: Publications 1929–1936
- –––, 1990, II: Publications 1938–1974
- –––, 1995, III: Unpublished Essays and Lectures
- –––, 2003a, IV: Correspondence A–G
- –––, 2003b, V: Correspondence H–Z
Griss, G.F.C., 1944, “Negatieloze intuitïonistische wiskunde”, Verslagen Nederlandse Akademie van Wetenschappen Amsterdam, 53: 261–268.
–––, 1946, “Negationless intuitionistic mathematics”, Proceedings Koninklijke Nederlandse Akademie van Wetenschappen Amsterdam, 49: 1127–1133. Also Indagationes Mathematicae, 8: 675–681.
–––, 1947, Idealistische Filosofie, Arnhem: Van Loghum Slaterus.
–––, 1948a, “Sur la négation (dans les mathématiques et la logique)”, Synthese, 7(1/2): 71–74.
–––, 1948b, “Logique des mathématiques intuitionistes sans négation”, Comptes Rendus de l’Académie des sciences, 227: 946–948. [Griss 1948b available online]
–––, 1950, “Negationless intuitionistic mathematics. II”, Proceedings Koninklijke Nederlandse Akademie van Wetenschappen Amsterdam, 53: 456–463. Also Indagationes Mathematicae, 12: 108–115.
–––, 1951a, “Negationless Intuitionistic Mathematics. III”, Proceedings Koninklijke Nederlandse Akademie van Wetenschappen Amsterdam, 54: 193–199. Also Indagationes Mathematicae, 13: 193–199. doi:10.1016/S1385-7258(51)50027-6
–––, 1951b, “Negationless Intuitionistic Mathematics. IVa”, Proceedings Koninklijke Nederlandse Akademie van Wetenschappen Amsterdam, 54: 452–462. Also Indagationes Mathematicae, 13: 452–462. doi:10.1016/S1385-7258(51)50064-1
–––, 1951c, “Negationless Intuitionistic Mathematics. IVb”, Proceedings Koninklijke Nederlandse Akademie van Wetenschappen Amsterdam, 54: 463–471. Also Indagationes Mathematicae, 13: 463–471. doi:10.1016/S1385-7258(51)50065-3
–––, 1951d, “Logic of Negationless Intuitionistic Mathematics”, Proceedings Koninklijke Nederlandse Akademie van Wetenschappen Amsterdam, 54: 41–49. Also Indagationes Mathematicae, 13: 41–49. doi:10.1016/S1385-7258(51)50007-0
van Heijenoort, Jean (ed.), 1967, From Frege to Gödel: A Sourcebook in Mathematical Logic, 1879–1931, Cambridge, MA: Harvard University Press.
Hazen, A.P., 1995, “Is Even Minimal Negation Constructive?”, Analysis, 55(2): 105–107. doi:10.1093/analys/55.2.105
Herbrand, Jacques, 1931, “Sur la non-contradiction de l’arithmétique”, Journal für die reine und angewandte Mathematik, 166: 1–8. Also Herbrand 1968: 221–232. English translation in van Heijenoort 1967: 620–628, reprint in Herbrand 1971: 284–297.
–––, 1968, Écrits logiques, Jean van Heijenoort (ed.), Paris: Presses Unversitaires de France.
–––, 1971, Logical Writings, Warren D. Goldfarb (ed.), Cambridge, MA: Harvard University Press.
Hesseling, Dennis E., 2003, Gnomes in the Fog. The Reception of Brouwer’s Intuitionism in the 1920s, Basel: Birkhäuser.
Heyting, Arend, 1925, Intuïtionistische axiomatiek der projectieve meetkunde, Ph.D. thesis, Universiteit van Amsterdam.
–––, 1928, [Prize essay on the formalization of intuitionistic logic]. Expanded and revised version published as Heyting 1930, Heyting 1930A, Heyting 1930B.
- –––, 1930, “Die formalen Regeln der intuitionistischen Logik I”, Sitzungsberichte der Preussischen Akademie der Wissenschaften, 42–56. English translation in Mancosu 1998: 311–327.
- –––, 1930A, “Die formalen Regeln der intuitionistischen Logik II”, Sitzungsberichte der Preussischen Akademie der Wissenschaften, 57–71.
- –––, 1930B, “Die formalen Regeln der intuitionistischen Logik III”, Sitzungsberichte der Preussischen Akademie der Wissenschaften, 158–169.
–––, 1930C, “Sur la logique intuitionniste”, Académie Royale de Belgique, Bulletin de la Classe des Sciences, 16: 957–963. English translation in Mancosu 1998: 306–310.
–––, 1931, “Die intuitionistische Grundlegung der Mathematik” (The Intuitionist Foundations of Mathematics), Erkenntnis, 2: 106–115. English translation in Benacerraf & Putnam 1983: 52–61. doi:10.1017/CBO9781139171519.003 and doi:10.1007/BF02028143
–––, 1932, “A propos d’un article de MM. Barzin et Errera”, Enseignement Mathématique, 31: 121–122.
–––, 1932C, “Anwendung der intuitionistischen Logik auf die Definition der Vollständigkeit eines Kalküls”, in Verhandlungen des Internationalen Mathematikerkongresses Zürich 1932, W. Saxer (ed.), Zürich: Orell Füssli, vol. 2, 344–345.
–––, 1934, Mathematische Grundlagenforschung, Intuitionismus, Beweistheorie, Berlin: Springer.
–––, 1937, “Bemerkungen zu dem Aufsatz von Herrn Freudenthal ‘Zur intuitionistischen Deutung logischer Formeln’”, Compositio Mathematica, 4: 117–118. [Heyting 1937c available online]
–––, 1955, Les fondements des mathématiques. Intuitionnisme. Théorie de la démonstration, Paris: Gauthier-Villars. Updated version of Heyting 1934, translated into French by P. Destouches-Février.
–––, 1953–1955, “G. F. C. Griss and His Negationless Intuitionistic Mathematics” Synthese, 9: 91–96. doi:10.1007/BF00567395
–––, 1956, Intuitionism, an Introduction, Amsterdam: North–Holland.
–––, 1958A, “Blick von der intuitionistischen Warte”, Dialectica, 12(3–4): 332–345. doi:10.1111/j.1746-8361.1958.tb01468.x
–––, 1958C, “Intuitionism in Mathematics”, in La philosophie au milieu du vingtième siècle, Raymond Klibansky (ed.), Firenze: La nuova Italia, vol. 1, 101–115.
–––, 1968A, “L.E.J. Brouwer”, in Logic and Foundations of Mathematics, (Contemporary Philosophy. A Survey, Vol.1), Raymond Klibansky (ed.), Firenze: La Nuova Italia editrice, 308–315.
–––, 1974, “Intuitionistic views on the nature of mathematics”, Synthese, 27(1–2): 79–91. doi:10.1007/BF00660890
–––, 1978, “History of the Foundations of Mathematics”, Nieuw Archief voor Wiskunde, 3rd series, 26(3): 1–21.
Hilbert, David, 1900, “Mathematische Probleme. Vortrag, gehalten auf dem internationalen Mathematiker-Kongress zu Paris 1900” (Mathematical Problems), Archiv der Mathematik und Physik (3), 1: 44–63,213–237. English translation in the Bulletin of the American Mathematical Society, 8(10): 437–479, 1902. doi:10.1090/S0002-9904-1902-00923-3
–––, 1922, “Neubegründung der Mathematik (Erste Mitteilung)”, Abhandlungen aus dem Mathematischen Seminar der Hamburgischen Universität, 1: 157–177. English translation in Mancosu 1998: 198–214.
–––, 1923, “Die logischen Grundlagen der Mathematik”, Mathematische Annalen, 88(1–2): 151–165. English translation in Ewald 1996: 1134–1148. doi:10.1007/BF01448445
Hilbert, D. and W. Ackermann, 1928, Grundzüge der theoretischen Logik, Berlin: Springer. doi:10.1007/978-3-642-52789-0
Imai, Yasuyuki and Kiyoshi Iseki, 1966, “On Griss Algebra. I”, Proceedings of the Japan Academy, 42(3): 213–216. doi:10.3792/pja/1195522077
de Iongh, J.J., 1949, “Restricted Forms of Intuitionistic Mathematics”, Proceedings of the 10th International Congress of Philosophy, Amsterdam 1948, Amsterdam: North-Holland, 2: 744–748. doi:10.5840/wcp1019492207
Johansson, Ingebrigt, 1937, “Der Minimalkalkül, ein reduzierter intuitionistischer Formalismus”, Compositio Mathematica, 4: 119–136. [Johansson 1937 available online]
Joosten, Joost Johannes, 2004, Interpretability Formalized, Ph.D. thesis, Utrecht University. Quaestiones Infinitae vol. XLIX, [Joosten 2004 available from Universiteit Utrecht/Universiteitsbibliotheek].
Kennedy, Juliette, 2007, “Kurt Gödel”, in The Stanford Encyclopedia of Philosophy, Winter 2007 Edition, Edward N. Zalta (ed.), URL = https://plato.stanford.edu/archives/win2007/entries/goedel/.
Kleene, Stephen Cole, 1945, “On the Interpretation of Intuitionistic Number Theory”, Journal of Symbolic Logic, 10(4): 109–124. doi:10.2307/2269016
–––, 1952, Introduction to Metamathematics, Amsterdam: North-Holland.
–––, 1973, “Realisability: A Retrospective Survey”, in Mathias & Rodgers 1973: 95–112. doi:10.1007/BFb0066772
Kleene, Stephen Cole and Richard Eugene Vesley, 1965, The Foundations of Intuitionistic Mathematics, Especially in Relation to Recursive Functions, (Studies in logic and the foundations of mathematics, 39), Amsterdam: North-Holland.
Kolmogorov, A., 1925, “O principe tertium non datur”, Matematiceskij Sbornik, 32: 646–667. English translation in van Heijenoort 1967: 416–437.
–––, 1932, “Zur Deutung der Intuitionistischen Logik”, Mathematische Zeitschrift, 35: 58–65. English translation in Mancosu 1998: 328–334. doi:10.1007/BF01186549
–––, 1937, “Freudenthal, Hans: Zur intuitionistischen Deutung logischer Formeln. Heyting, A.: Bemerkungen zu dem Aufsatz von Herrn Freudenthal ‘Zur intuitionistischen Deutung logischer Formeln’”, Zentralblatt für Mathematik und ihre Grenzgebiete, 0015.24201.
Korevaar, Jaap., 2016, “Enkele persoonlijke herinneringen aan L.E.J. Brouwer”, (“Some personal memories of L.E.J. Brouwer”), Nieuw Archief voor Wiskunde, 5th series, 17(4): 247–249. [Korevaar 2016 available online]
Kreisel, G., 1962, “Foundations of Intuitionistic Logic”, in Logic, Methodology and Philosophy of Science: Proceedings of the 1960 International Congress, Ernst Nagel, Patrick Suppes, and Alfred Tarski (eds.), Stanford: Stanford University Press, 198–210. doi:10.1016/S0049-237X(09)70587-7
–––, 1987, “Gödel’s Excursions into Intuitionistic Logic”, in Gödel Remembered, P. Weingartner and L. Schmetterer (eds.), Napoli: Bibliopolis, 67–179.
Kripke, Saul A., 1965, “Semantical Analysis of Intuitionistic Logic I”, in Formal Systems and Recursive Functions, (Studies in Logic and the Foundations of Mathematics, 40), J.N. Crossley and M. Dummett (eds.), Amsterdam: North-Holland, 92–130. doi:10.1016/S0049-237X(08)71685-9
Krivtsov, Victor N., 2000a, “A Negationless Interpretation of Intuitionistic Theories”, Erkenntnis, 53(1–2): 155–172. doi:10.1023/A:1005618302941
–––, 2000b, “A Negationless Interpretation of Intuitionistic Theories. I”, Studia Logica, 64(3): 323–344. doi:10.1023/A:1005233526469
–––, 2000c, “A Negationless Interpretation of Intuitionistic Theories. II”, Studia Logica, 65(2): 155–179. doi:10.1023/A:1005207512630
Kuiper, Johannes John Carel, 2004, Ideas and Explorations. Brouwer’s Road to Intuitionism, Ph.D. thesis, Utrecht University. Quaestiones Infinitae vol. XLVI [Kuiper 2004 available from Universiteit Utrecht/Universiteitsbibliotheek].
Lewis, C.I., 1914, “The Calculus of Strict Implication”, Mind, New Series, 23(90): 240–247. doi:10.1093/mind/XXIII.1.240
Mancosu, Paolo (ed.), 1998, From Brouwer to Hilbert. The Debate on the Foundations of Mathematics in the 1920s, Oxford: Oxford University Press.
Mathias, A.R.D. and H. Rodgers (eds.), 1973, Cambridge Summer School in Mathematical Logic 1971, (Lecture Notes in Mathematics, 337), Heidelberg: Springer. doi:10.1007/BFb0066770
McKinsey, J.C.C., 1939, “Proof of the Independence of the Primitive Symbols of Heyting’s Calculus of Propositions”, Journal of Symbolic Logic, 4(4): 155–158. doi:10.2307/2268715
Mendez, José M., 1988, “A Note on the Semantics of Minimal Intuitionism”, Logique et Analyse, 31(123–124): 371–377. [Mendez 1988 available online]
Michel, David, 2008, Systèmes formels et systèmes fonctionnels pédagogiques, Ph.D. thesis, Université Metz. [Michel 2008 available from Université de Lorraine].
Mints, Grigori, 2006, “Notes on Constructive Negation”, Synthese, 148(3): 701–717. doi:10.1007/s11229-004-6294-3
van der Molen, Tim, 2016, “The Johansson/Heyting letters and the birth of minimal logic”, ILLC Publications, Technical Notes Series, X-2016-04 [van der Molen 2016 available online from ILLC].
Moschovakis, Joan, 2007, “Intuitionistic Logic”, in The Stanford Encyclopedia of Philosophy, Spring 2007 Edition, Edward N. Zalta (ed.), URL=https://plato.stanford.edu/archives/spr2007/entries/logic-intuitionistic/.
Myhill, John, 1966, “Notes Towards An Axiomatization of Intuitionistic Analysis”, Logique et Analyse, 9(35–36): 280–297. [Myhill 1966 available online]
Nelson, David, 1966, “Non-Null Implication”, Journal of Symbolic Logic, 31(4): 562–572. doi:10.2307/2269691
Parsons, Charles, 1967, [Introduction to the translation of sections 1–3 of Brouwer 1927B], in van Heijenoort 1967: 446–457.
Pieri, Mario, 1898, “I principii della geometria di posizione composti in sistema logico deduttivo”, Memorie della Reale Accademia delle Scienze di Torino, series II, 48: 1–62.
Plisko, V.E., 1988, “The Kolmogorov calculus as a part of minimal calculus”, Russian Mathematical Surveys, 43(6): 95–110. doi:10.1070/RM1988v043n06ABEH001993
Pos, H.J., 1953–1954, “G.F.C. Griss als wijsgerig humanist en als mens”, De Nieuwe Stem, 8: 654–663.
Posy, Carl J., 1992, “Review: Dirk van Dalen, Intuitionistic Logic; Walter Felscher, Dialogues as a Foundation for Intuitionistic Logic”, Journal of Symbolic Logic, 57(2): 754–756. doi:10.2307/2275309
Prawitz, Dag, 1965, Natural Deduction. A Proof-Theoretical Study, Stockholm: Almqvist & Wiksell.
Prawitz, D. and P.-E. Malmnäs, 1968, “A Survey of Some Connections Between Classical, Intuitionistic and Minimal Logic”, in Contributions to Mathematical Logic, (Studies in Logic and the Foundations of Mathematics, 50), H. Arnold Schmidt, K. Schütte, and H.-J. Thiele (eds.), Amsterdam: North-Holland, pp. 215–229. doi:10.1016/S0049-237X(08)70527-5
Rasiowa, Helena, 1974, An Algebraic Approach to Non-Classical Logics, (Studies in logic and the foundations of mathematics, 78), Amsterdam: North-Holland/
Ruitenburg, Wim, 1991, “The Unintended Interpretations of Intuitionistic Logic”, in Perspectives on the History of Mathematical Logic, Thomas Drucker (ed.), Basel: Birkhäuser, 134–160. doi:10.1007/978-0-8176-4769-8_10
van Rootselaar, B., 1953–1954, “In memoriam Dr. G.F.C. Griss”, Euclides, 29(1): 42–45.
Russell, Bertrand, 1903, The Principles of Mathematics, London: Allen & Unwin.
Sato, Masahiko, 1997, “Classical Brouwer-Heyting-Kolmogorov interpretation”, RIMS Kokyuroku, 1021: 28–47.
Smirnov, V.J., 1925 [published 1932], “Kolmogorov, A.N.: Über das Prinzip tertium non datur”, Jahrbuch über die Fortschritte der Mathematik 51.0048.01.
van Stigt, Walter P., 1990, Brouwer’s Intuitionism, (Studies in the history and philosophy of mathematics, 2), Amsterdam: North-Holland.
Stone, Marshall Harvey, 1937, “Topological Representations of Distributive Lattices and Brouwerian Logics”, Časopis pro pěstování matematiky a fysiky, 67(1): 1–25.
Sundholm, Göran, 1983, “Constructions, Proofs and the Meaning of Logical Constants”, Journal of Philosophical Logic, 12(2): 151–172. doi:10.1007/BF00247187
–––, 2004, “The Proof-Explanation of Logical Constants is Logically Neutral”, Revue Internationale de Philosophie, 58(4): 401–410.
Sundholm, Göran and Mark van Atten, 2008, “The proper explanation of intuitionistic logic: on Brouwer’s proof of the Bar Theorem”, in van Atten et al. 2008: 60–77. doi:10.1007/978-3-7643-8653-5_5
de Swart, H.C.M., 1976, “Another Intuitionistic Completeness Proof”, Journal of Symbolic Logic, 41(3): 644–662. doi:10.1017/S0022481200051215
–––, 1977, “An Intuitionistically Plausible Interpretation of Intuitionistic Logic”, Journal of Symbolic Logic, 42(4): 564–578. doi:10.2307/2271877
Tarski, Alfred, 1938, “Der Aussagenkalkül und die Topologie”, Fundamentae Mathematicae, 31: 103–134. English translation in Tarski 1956, pp. 421–454.
–––, 1953, “A General Method in Proofs of Undecidability”, in Undecidable Theories, A. Tarski, A. Mostowski, and R. Robinson (eds.), Amsterdam: North-Holland, 3–35.
–––, 1956, Logic, Semantics, Metamathematics. Papers from 1923 to 1938, J.H. Woodger (trl.), Clarendon Press.
Troelstra, A.S., 1977, “Aspects of constructive mathematics”, in Handbook of Mathematical Logic, (Studies in Logic and the Foundations of Mathematics, 90), Jon Barwise (ed.), Amsterdam: North-Holland, 973–1052. doi:10.1016/S0049-237X(08)71127-3
–––, 1983, “Logic in the Writings of Brouwer and Heyting”, in Atti del Convegne Internazionaledi Storia della Logica. San Gimignano, 4–8 dicembre 1982, V. Abrusci, E. Casari, and M. Mugnai, eds., Bologna: CLUEB, 193–210.
–––, 1990, “On the Early History of Intuitionistic Logic”, in Mathematical Logic, Petio P. Petkov (ed.), New York: Plenum Press, 3–17.
Troelstra, A.S., J. Niekus, and H. van Riemsdijk, 1981, “Bibliography of A. Heyting”, Nieuw Archief voor Wiskunde, 3rd series, 29: 24–35.
Troelstra, A.S. and D. van Dalen, 1988, Constructivism in Mathematics, 2 vols., (Studies in Logic and the Foundations of Mathematics, 121 & 123), Amsterdam: North-Holland.
Valpola, Veli, 1955, “Ein system der negationlosen Logik mit ausschliesslich realisierbaren Prädicaten”, Acta Philosophica Fennica, 9: 1–247.
Veldman, Wim, 1976, “An Intuitionstic Completeness Theorem for Intuitionistic Predicate Logic”, Journal of Symbolic Logic, 41(1): 159–166. doi:10.1017/S0022481200051859
–––, 1982, “On the Continuity of Functions in Intuitionistic Real Analysis. Some Remarks on Brouwer’s Paper: ‘Ueber Definitionsbereiche von Funktionen’”, Tech. Rep. 8210, Mathematisch Instituut, Katholieke Universiteit Nijmegen.
–––, 2008, “The Borel Hierarchy Theorem from Brouwer’s Intuitionistic Perspective”, Journal of Symbolic Logic, 73(1): 1–64. doi:10.2178/jsl/1208358742
Vesley, Richard, 1980, “Intuitionistic Analysis: the Search for Axiomatization and Understanding”, in The Kleene Symposium, (Studies in Logic and the Foundations of Mathematics, 101), J. Barwise, H. J. Keisler, and K. Kunen (eds.), Amsterdam: North-Holland, 317–331. doi:10.1016/S0049-237X(08)71265-5
Vredenduin, P.G.J., 1953, “The Logic of Negationless Mathematics”, Compositio Mathematica, 11: 204–277. [Vredenduin 1953 available online]
–––, 1956, “G.F.C. Griss and his Negationaless Intuitionistic Mathematics, by A. Heyting”, Journal of Symbolic Logic, 21(1): 91. doi:10.2307/2268511
Wajsberg, Mordchaj, 1938, “Untersuchungen über den Aussagenkalkül [von A. Heyting]”, Wiadomosci Matematyczne, (old series) 46: 45–101.
Wang, Hao, 1987, Reflections on Kurt Gödel, Cambridge MA: MIT Press.
Wavre, Rolin, 1924, “Y a-t-il une crise des mathématiques? A propos de la notion d’existence et d’une application suspecte du principe du tiers exclu”, Revue de Métaphysique et de Morale, 31(3) 435–470.
–––, 1926, “Logique formelle et logique empirique”, Revue de Métaphysique et de Morale, 33(1): 65–75.
Weyl, Hermann, 1921, “Über die neue Grundlagenkrise der Mathematik”, Mathematische Zeitschrift, 10(1–2): 39–79. English translation in Mancosu 1998: 86–118. doi:10.1007/BF02102305
Whitehead, Alfred North, 1906, The Axioms of Projective Geometry, Cambridge: Cambridge University Press.
Whitehead, Alfred North and Bertrand Russell, 1910, Principia Mathematica, vol. 1, Cambridge: Cambridge University Press.

Academic Tools

Other Internet Resources

Acknowledgments

I am grateful to Dirk van Dalen and Göran Sundholm for discussions of some of the issues involved. Helpful comments by the editors and Rosalie Iemhoff led to various improved formulations, corrections, and clarifications. Van Dalen kindly granted permission to quote from materials in the Brouwer Archive (at Utrecht at the time, now at the Noord-Hollands Archief in Haarlem). Thanks also to van Dalen and Eckhart Menzler-Trott for their search for Bernays’ letter to Brouwer, and to Sundholm and Michael Hegarty for a copy of de Iongh 1949. In section 3.6 I have drawn on van Atten 2004a; I thank the Association for Symbolic Logic for granting permission to do so.

上一页一阶逻辑的出现 first-order logic (William Ewald)下一页现代模态逻辑的起源 modal logic (Roberta Ballarin)

最后更新于7小时前