Brouwer's views on the foundations of mathematics have inspired the study of intuitionistic logic, including the study of the intuitionistic propositional calculus and its extensions. The theory of these systems has become an independent branch of logic with connections to lattice theory, topology, modal logic and other areas. This paper aims to present a modern account of semantics for intuitionistic propositional systems. The guiding idea is that of a hierarchy of semantics, organized by increasing generality: from the least general Kripke (...) semantics on through Beth semantics, topological semantics, Dragalin semantics, and finally to the most general algebraic semantics. While the Kripke, topological, and algebraic semantics have been extensively studied, the Beth and Dragalin semantics have received less attention. We bring Beth and Dragalin semantics to the fore, relating them to the concept of a nucleus from pointfree topology, which provides a unifying perspective on the semantic hierarchy. (shrink)

We propose an extension of minimal intuitionistic predicate logic, based on delimited control operators, that can derive the predicate-logic version of the double-negation shift schema, while preserving the disjunction and existence properties.

Ranging from Alan Turing’s seminal 1936 paper to the latest work on Kolmogorov complexity and linear logic, this comprehensive new work clarifies the relationship between computability on the one hand and constructivity on the other. The authors argue that even though constructivists have largely shed Brouwer’s solipsistic attitude to logic, there remain points of disagreement to this day. Focusing on the growing pains computability experienced as it was forced to address the demands of rapidly expanding applications, the content maps the (...) developments following Turing’s ground-breaking linkage of computation and the machine, the resulting birth of complexity theory, the innovations of Kolmogorov complexity and resolving the dissonances between proof theoretical semantics and canonical proof feasibility. Finally, it explores one of the most fundamental questions concerning the interface between constructivity and computability: whether the theory of recursive functions is needed for a rigorous development of constructive mathematics. This volume contributes to the unity of science by overcoming disunities rather than offering an overarching framework. It posits that computability’s adoption of a classical, ontological point of view kept these imperatives separated. In studying the relationship between the two, it is a vital step forward in overcoming the disagreements and misunderstandings which stand in the way of a unifying view of logic. (shrink)

There is an ambiguity in the concept of deductive validity that went unnoticed until the middle of the twentieth century. Sometimes an inference rule is called valid because its conclusion is a theorem whenever its premises are. But often something different is meant: The rule's conclusion follows from its premises even in the presence of other assumptions. In many logical environments, these two definitions pick out the same rules. But other environments are context-sensitive, and in these environments the second notion (...) is stronger. Sorting out this ambiguity has led to profound mathematical investigations with applications in complexity theory and computer science. The origins of this ambiguity and the history of its resolution deserve philosophical attention, because our understanding of logic stands to benefit from their details. I am eager to examine together with you, Crito, whether this argument will appear in any way different to me in my present circumstances, or whether it remains the same, whet... (shrink)

Brouwer’s intuitionistic program was an intriguing attempt to reform the foundations of mathematics that eventually did not prevail. The current paper offers a new perspective on the scientific community’s lack of reception to Brouwer’s intuitionism by considering it in light of Michael Friedman’s model of parallel transitions in philosophy and science, specifically focusing on Friedman’s story of Einstein’s theory of relativity. Such a juxtaposition raises onto the surface the differences between Brouwer’s and Einstein’s stories and suggests that contrary to Einstein’s (...) story, the philosophical roots of Brouwer’s intuitionism cannot be traced to any previously established philosophical traditions. The paper concludes by showing how the intuitionistic inclinations of Hermann Weyl and Abraham Fraenkel serve as telling cases of how individuals are involved in setting in motion, adopting, and resisting framework transitions during periods of disagreement within a discipline. (shrink)

L.E.J. Brouwer famously took the subject’s intuition of time to be foundational and from there ventured to build up mathematics. Despite being largely critical of formal methods, Brouwer valued axiomatic systems for their use in both communication and memory. Through the Dutch Mathematical Society, Gerrit Mannoury posed a challenge in 1927 to provide an axiomatization of intuitionistic arithmetic. Arend Heyting’s 1928 axiomatization was chosen as the winner and has since enjoyed the status of being the _de facto_ formalization of intuitionistic (...) arithmetic. We argue that axiomatizations of intuitionistic arithmetic ought to make explicit the role of the subject’s activity in the intuitionistic arithmetical process. While Heyting Arithmetic is useful when we want to contrast constructed objects with platonistic ones, Heyting Arithmetic omits the contribution of the subject and thus falls short as a response to Mannoury’s challenge. We offer our own solution, Doxastic Heyting Arithmetic, or \({\textsf{DHA}}\), which we contend axiomatizes Brouwerian intuitionistic arithmetic. (shrink)

This book brings together philosophers, mathematicians and logicians to penetrate important problems in the philosophy and foundations of mathematics. In philosophy, one has been concerned with the opposition between constructivism and classical mathematics and the different ontological and epistemological views that are reflected in this opposition. The dominant foundational framework for current mathematics is classical logic and set theory with the axiom of choice. This framework is, however, laden with philosophical difficulties. One important alternative foundational programme that is actively pursued (...) today is predicativistic constructivism based on Martin-Löf type theory. Associated philosophical foundations are meaning theories in the tradition of Wittgenstein, Dummett, Prawitz and Martin-Löf. What is the relation between proof-theoretical semantics in the tradition of Gentzen, Prawitz, and Martin-Löf and Wittgensteinian or other accounts of meaning-as-use? What can proof-theoretical analyses tell us about the scope and limits of constructive and predicative mathematics? (shrink)

In this paper it is argued that the understanding of Brouwer as replacing truth conditions with assertability or proof conditions, in particular as codified in the so-called Brouwer-Heyting-Kolmogorov Interpretation, is misleading and conflates a weak and a strong notion of truth that have to be kept apart to understand Brouwer properly: truth-as-anticipation and truth- in-content. These notions are explained, exegetical documentation provided, and semi-formal recursive definitions are given.

The dissertation provides an analysis and elaboration of Michael Dummett's proof-theoretic notions of validity. Dummett's notions of validity are contrasted with standard proof-theoretic notions and formally evaluated with respect to their adequacy to propositional intuitionistic logic.

The use of the three labels to denote the three foundational schools of the early twentieth century are now part of literature. Yet, neither their number nor the...

The goal of this paper is to explore the significance of Montague’s paradox—that is, any arithmetical theory $T\supseteq Q$ over a language containing a predicate $P$ satisfying $P\rightarrow \varphi $ and $T\vdash \varphi \,\therefore\,T\vdash P$ is inconsistent—as a limitative result pertaining to the notions of formal, informal, and constructive provability, in their respective historical contexts. To this end, the paradox is reconstructed in a quantified extension $\mathcal {QLP}$ of Artemov’s logic of proofs. $\mathcal {QLP}$ contains both explicit modalities $t:\varphi $ (...) and also proof quantifiers $x:\varphi $. In this system, the basis for the rule NEC is decomposed into a number of distinct principles governing how various modes of reasoning about proofs and provability can be internalized within the system itself. A conceptually motivated resolution to the paradox is proposed in the form of an argument for rejecting the unrestricted rule NEC on the basis of its subsumption of an intuitively invalid principle pertaining to the interaction of proof quantifiers and the proof-theorem relation expressed by explicit modalities. (shrink)