Luitzen Egburtus Jan Brouwer founded a school of thought whose aim was to include mathematics within the framework of intuitionistic philosophy; mathematics was to be regarded as an essentially free development of the human mind. What emerged diverged considerably at some points from tradition, but intuitionism has survived well the struggle between contending schools in the foundations of mathematics and exact philosophy. Originally published in 1981, this monograph contains a series of lectures dealing with most of the fundamental topics (...) such as choice sequences, the continuum, the fan theorem, order and well-order. Brouwer's own powerful style is evident throughout the work. (shrink)

It is argued that Brouwer’s philosophy of mathematics makes perfect sense if viewed from an Eastern philosophical perspective, as a mathematics in what Erich Fromm called “the being mode of existence.” The difficulty Western philosophers have accepting its validity under Brouwer’s own justifications is that mathematics is one of the highest prized treasures of Western philosophy (those footnotes to Plato’s dialogues).

Dutch Mathematician Luitzen Egbertus Jan Brouwer (1881-1966) was a rebel. His doctoral thesis... was the manifesto of an angry young man taking on the mathematical establishment on all fronts. In a short time he established a world-wide reputation for himself; his genius and originality were acknowledged by the great mathematicians of his time... The Intuitionist-Formalist debate became a personal feud between the mathematical giants Brouwer and Hilbert, and ended in 1928 with the expulsion of Brouwer from the editorial board of (...) the Mathematische Annalen by dictat of Hilbert. Forsaken, humiliated and disillusioned Brouwer abandoned his Intuitionist Programme and withdrew into silence just about the time when the Formalist Programme appeared to be fundamentally flawed and major opposition collapsed... This book attempts to follow the `genetic' development of Brouwer's ideas, linking the man Brouwer, his Weltanschauung, his philosophy of mathematics and his reconstruction of mathematics. Brouwer's own writings, his publications as well as his unpublished papers, are its immediate and main source of reference. It is the second volume in the new series Studies in the History and Philosophy of Mathematics, and is written for the specialist as well as for the general reader interested in mathematics and the interpretation of its status and function. (shrink)

We investigate which part of Brouwer’s Intuitionistic Mathematics is finitistically justifiable or guaranteed in Hilbert’s Finitism, in the same way as similar investigations on Classical Mathematics already done quite extensively in proof theory and reverse mathematics. While we already knew a contrast from the classical situation concerning the continuity principle, more contrasts turn out: we show that several principles are finitistically justifiable or guaranteed which are classically not. Among them are: fan theorem for decidable fans but arbitrary bars; continuity principle (...) and the axiom of choice both for arbitrary formulae; and $\Sigma _2$ induction and dependent choice. We also show that Markov’s principle MP does not change this situation; that neither does lesser limited principle of omniscience LLPO ; but that limited principle of omniscience LPO makes the situation completely classical. (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)

The Curry-Howard isomorphism states an amazing correspondence between systems of formal logic as encountered in proof theory and computational calculi as found in type theory. For instance, minimal propositional logic corresponds to simply typed lambda-calculus, first-order logic corresponds to dependent types, second-order logic corresponds to polymorphic types, sequent calculus is related to explicit substitution, etc. The isomorphism has many aspects, even at the syntactic level: formulas correspond to types, proofs correspond to terms, provability corresponds to inhabitation, proof normalization corresponds to (...) term reduction, etc. But there is more to the isomorphism than this. For instance, it is an old idea---due to Brouwer, Kolmogorov, and Heyting---that a constructive proof of an implication is a procedure that transforms proofs of the antecedent into proofs of the succedent; the Curry-Howard isomorphism gives syntactic representations of such procedures. The Curry-Howard isomorphism also provides theoretical foundations for many modern proof-assistant systems (e.g. Coq). This book give an introduction to parts of proof theory and related aspects of type theory relevant for the Curry-Howard isomorphism. It can serve as an introduction to any or both of typed lambda-calculus and intuitionistic logic. Key features - The Curry-Howard Isomorphism treated as common theme - Reader-friendly introduction to two complementary subjects: Lambda-calculus and constructive logics - Thorough study of the connection between calculi and logics - Elaborate study of classical logics and control operators - Account of dialogue games for classical and intuitionistic logic - Theoretical foundations of computer-assisted reasoning · The Curry-Howard Isomorphism treated as the common theme. · Reader-friendly introduction to two complementary subjects: lambda-calculus and constructive logics · Thorough study of the connection between calculi and logics. · Elaborate study of classical logics and control operators. · Account of dialogue games for classical and intuitionistic logic. · Theoretical foundations of computer-assisted reasoning. (shrink)

(2005). Being and Time and Brouwer's Intuitionism. Angelaki: Vol. 10, continental philosophy and the sciences the german traditionissue editor: damian veal, pp. 181-186.

In intuitionistic analysis, "Brouwer's Continuity Principle" implies, together with an "Axiom of Countable Choice", that the positively Borel sets form a genuinely growing hierarchy: every level of the hierarchy contains sets that do not occur at any lower level.

The paper examines Andrei A. Markov’s critical attitude towards L.E.J. Brouwer’s intuitionism, as is expressed in his endnotes to the Russian translation of Heyting’s Intuitionism, published in Moscow in 1965. It is argued that Markov’s algorithmic approach was shaped under the impact of the mathematical style and values prevailing in the Petersburg mathematical school, which is characterized by the proclaimed primacy of applications and the search for rigor and effective solutions.

The lives of few mathematicians offer the drama that is presented by the life of L. E. J. Brouwer, correctly identified on the cover of this book as a topologist, intuitionist, and philosopher, and before we go any further, it will be worth indicating why.It is not just that Brouwer would rank high among mathematicians for his work in topology alone: he set standards for rigour and created a theory of dimension for topological spaces, and his fixed-point theorem is of (...) great importance. Nor is it just that his philosophy of intuitionism created a new and vibrant branch of logic, that is, arguably, the only viable alternative to naïve, classical logic outside the enclave of professional logicians. Rather, it is that there is a tension, popularly taken to amount to a contradiction, in the fundamental ideas behind his topology and his intuitionism. Added to that, he took a highly principled stand on mathematical issues that led him into confrontations with major figures and a certain degre .. (shrink)

Luitzen Egburtus Jan Brouwer founded a school of thought whose aim was to include mathematics within the framework of intuitionistic philosophy; mathematics was to be regarded as an essentially free development of the human mind. What emerged diverged considerably at some points from tradition, but intuitionism has survived well the struggle between contending schools in the foundations of mathematics and exact philosophy. Originally published in 1981, this monograph contains a series of lectures dealing with most of the fundamental topics (...) such as choice sequences, the continuum, the fan theorem, order and well-order. Brouwer's own powerful style is evident throughout the work. (shrink)

Review of a van Stigt's book Brouwer's intuitionism.

We try to translate the intuitionistic propositional logic INT into Brouwer's modal logic KTB. Our translation is motivated by intuitions behind Brouwer's axiom p →☐◊p The main idea is to interpret intuitionistic implication as modal strict implication, whereas variables and other positive sentences remain as they are. The proposed translation preserves fragments of the Rieger-Nishimura lattice which is the Lindenbaum algebra of monadic formulas in INT. Unfortunately, INT is not embedded by this mapping into KTB.

My first aim in this paper is to use time diagrams in the style of Brentano to analyze constructions in Brouwer's separable mathematics more precisely. I argue that constructions must involve not only pairing and projecting as basic operations guaranteed by the intuition of twoity, as sometimes assumed in the literature, but also a recalling operation. My second aim is to argue that Brouwer's views on the intuition of twoity and arithmetic lead to an ontological explosion. Redeveloping the (...) constructions of natural numbers and systems sketched in an appendix to Brouwer's Cambridge lectures, I observe that the only plausible way he can make some elementary arithmetic in his separable mathematics is by allowing for the same canonical number to be determined by multiple separable entities, resulting in an overabundant mathematical ontology. (shrink)

Brouwer's demonstration of his Bar Theorem gives rise to provocative questions regarding the proper explanation of the logical connectives within intuitionistic and constructivist frameworks, respectively, and, more generally, regarding the role of logic within intuitionism. It is the purpose of the present note to discuss a number of these issues, both from an historical, as well as a systematic point of view.

This book examines the role of acts of choice in classical and intuitionistic mathematics. Featuring fifteen papers - both new and previously published - it offers a fresh analysis of concepts developed by the mathematician and philosopher L.E.J. Brouwer, the founder of intuitionism. The author explores Brouwer's idealization of the creative subject as the basis for intuitionistic truth, and in the process he also discusses an important, related question: to what extent does the intuitionistic perspective succeed in avoiding (...) the classical realistic notion of truth? The papers detail realistic aspects in the idealization of the creative subject and investigate the hidden role of choice even in classical logic and mathematics, covering such topics as bar theorem, type theory, inductive evidence, Beth models, fallible models, and more. In addition, the author offers a critical analysis of the response of key mathematicians and philosophers to Brouwer's work. These figures include Michael Dummett, Saul Kripke, Per Martin-Löf, and Arend Heyting. This book appeals to researchers and graduate students with an interest in philosophy of mathematics, linguistics, and mathematics. (shrink)

The paper is a contribution to intuitionistic reverse mathematics. We introduce a formal system called Basic Intuitionistic MathematicsBIM, and then search for statements that are, over BIM, equivalent to Brouwer’s Fan Theorem or to its positive denial, Kleene’s Alternative to the Fan Theorem. The Fan Theorem is true under the intended intuitionistic interpretation and Kleene’s Alternative is true in the model of BIM consisting of the Turing-computable functions. The task of finding equivalents of Kleene’s Alternative is, intuitionistically, a nontrivial extension (...) of the task of finding equivalents of the Fan Theorem, although there is a certain symmetry in the arguments that we shall try to make transparent. We introduce closed-and-separable subsets of Baire space N\documentclass[12pt]{minimal} \usepackage{amsmath} \usepackage{wasysym} \usepackage{amsfonts} \usepackage{amssymb} \usepackage{amsbsy} \usepackage{mathrsfs} \usepackage{upgreek} \setlength{\oddsidemargin}{-69pt} \begin{document}$${\mathcal{N}}$$\end{document} and of the set R\documentclass[12pt]{minimal} \usepackage{amsmath} \usepackage{wasysym} \usepackage{amsfonts} \usepackage{amssymb} \usepackage{amsbsy} \usepackage{mathrsfs} \usepackage{upgreek} \setlength{\oddsidemargin}{-69pt} \begin{document}$${\mathcal{R}}$$\end{document} of the real numbers. Such sets may be compact and also positively noncompact. The Fan Theorem is the statement that Cantor space C\documentclass[12pt]{minimal} \usepackage{amsmath} \usepackage{wasysym} \usepackage{amsfonts} \usepackage{amssymb} \usepackage{amsbsy} \usepackage{mathrsfs} \usepackage{upgreek} \setlength{\oddsidemargin}{-69pt} \begin{document}$${\mathcal{C}}$$\end{document}, or, equivalently, the unit interval [0, 1], is compact and Kleene’s Alternative is the statement that C\documentclass[12pt]{minimal} \usepackage{amsmath} \usepackage{wasysym} \usepackage{amsfonts} \usepackage{amssymb} \usepackage{amsbsy} \usepackage{mathrsfs} \usepackage{upgreek} \setlength{\oddsidemargin}{-69pt} \begin{document}$${\mathcal{C}}$$\end{document}, or, equivalently, [0, 1], is positively noncompact. The class of the compact closed-and-separable sets and also the class of the closed-and-separable sets that are positively noncompact are characterized in many different ways and a host of equivalents of both the Fan Theorem and Kleene’s Alternative is found. (shrink)

MartinoEnrico.* * Intuitionistic Proof Versus Classical Truth, The Role of Brouwer’s Creative Subject in Intuitionistic Mathematics. Logic, Methodology and the Unity of Science; 42. Springer, 2018. ISBN: 978-3-319-74356-1 ; 978-3-030-08971-9, 978-3-319-74357-8. Pp. xiii + 170.

We identify bar recursion on moduli of continuity as a fundamental notion of constructive mathematics. We show that continuous functions from the Baire space \ to the natural numbers \ which have moduli of continuity with bar recursors are exactly those functions induced by Brouwer operations. The connection between Brouwer operations and bar induction allows us to formulate several continuity principles on the Baire space stated in terms of bar recursion on continuous moduli which naturally characterise some variants of bar (...) induction. These principles state that a certain kind of continuous function from \ to \ admits a modulus of continuity with a bar recursor. The results for the Baire space are recast in the setting of the Cantor space \ using the notion of fan recursor, a bar recursor for binary trees. This yields characterisations of uniformly continuous functions on the Cantor space and fan theorem in terms of fan recursors. The results for the Cantor space hold over the extensional version of intuitionistic arithmetic in all finite types ), and those for the Baire space hold over \ extended with the type for Brouwer operations. Our work places Spector’s bar recursion in a proper context of Brouwer’s intuitionistic mathematics and clarifies the connection between bar recursion and bar induction. (shrink)

Straightforwardly and strictly intuitionistic inferences show that the Brouwer– Heyting–Kolmogorov interpretation, in the presence of a formulation of the recognition principle, entails the validity of the Law of Testability: that the form ¬ f V ¬¬ f is valid. Therefore, the BHK and recognition, as described here, are inconsistent with the axioms both of intuitionistic mathematics and of Markovian constructivism. This finding also implies that, if the BHK and recognition are suitably formulated, then Brouwer’s original weak counterexample reasoning was fallacious. (...) The results of the present article extend and refine those of McCarty, C.. Antirealism and Constructivism: Brouwer’s Weak Counterexamples. The Review of Symbolic Logic. First View. Cambridge University Press. (shrink)

The aim of this paper is to reconstruct Brouwer’s justification for the intuitionistic revision of logic and mathematics. It is attempted to show that pivotal premisses of his argument are supplied by his philosophy. To this end, the basic tenets of his philosophical doctrine are discussed: the concepts of mind, causal attention, intuition of two-ity and his repudiation of realism.The restriction of intuitionistically allowable objects to spreads and species is traced back to Brouwer’s concept of intuition that is a defining (...) feature of his notion of mind. On the other hand, it is argued that his objections to some laws of classical logic result from the rejection of the rule of double negation elimination, which in turn follows from both, the claim that rules of logic should preserve evidence for assertions rather than truth, and too restrictive a concept of evidence. (shrink)

Dirk van Dalen’s biography studies the fascinating life of the famous Dutch mathematician and philosopher Luitzen Egbertus Jan Brouwer. Brouwer belonged to a special class of genius; complex and often controversial and gifted with a deep intuition, he had an unparalleled access to the secrets and intricacies of mathematics. Most mathematicians remember L.E.J. Brouwer from his scientific breakthroughs in the young subject of topology and for the famous Brouwer fixed point theorem. Brouwer’s main interest, however, was in the foundation of (...) mathematics which led him to introduce, and then consolidate, constructive methods under the name ‘intuitionism’. This made him one of the main protagonists in the ‘foundation crisis’ of mathematics. As a confirmed internationalist, he also got entangled in the interbellum struggle for the ending of the boycott of German and Austrian scientists. This time during the twentieth century was turbulent; nationalist resentment and friction between formalism and intuitionism led to the Mathematische Annalen conflict. It was here that Brouwer played a pivotal role. The present biography is an updated revision of the earlier two volume biography in one single book. It appeals to mathematicians and anybody interested in the history of mathematics in the first half of the twentieth century. (shrink)

Is a mathematical theorem proved because provable, or provable because proved? If Brouwer’s intuitionism is accepted, we’re committed, it seems, to the latter, which is highly problematic. Or so I will argue. This and other consequences of Brouwer’s attempt to found mathematics on the intuition of a move of time have heretofore been insufficiently appreciated. Whereas the mathematical anomalies of intuitionism have received enormous attention, too little time, I’ll try to show, has been devoted to some of the (...) temporal anomalies that Brouwer has invited us to introduce into 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.

When Kleene extended his recursive realizability interpretation from intuitionistic arithmetic to analysis, he was forced to use more than recursive functions to interpret sequences and conditional constructions. In fact, he used what classically appears to be the full continuum. We describe here a generalization to higher type of Kleene's realizability, one case of which, -realizability, uses general recursive functions throughout, both to realize theorems and to interpret choice sequences. -realizability validates a version of the bar theorem and the usual continuity (...) principles, while also providing naturally, as Kleene's 1965 realizability does not, for versions of lawless sequence axioms, as well as of Church's Thesis. (shrink)

The Dutch mathematician and philosopher L.E.J. Brouwer is well known for his ground-breaking work in topology and his iconoclastic philosophy of mathematics, intuitionism. What is far less well known is that Brouwer mused on the philosophy of the natural sciences as well. Later in life he also taught courses in physics at the University of Amsterdam.

Dedicated to Dana Scott on his sixtieth birthday.It is common knowledge that for a short while Hermann Weyl joined Brouwer in his pursuit of a revision of mathematics according to intuitionistic principles. There is, however, little in the literature that sheds light on Weyl's role and in particular on Brouwer's reaction to Weyl's allegiance to the cause of intuitionism. This short episode certainly raises a number of questions: what made Weyl give up his own program, spelled out in (...) “Das Kontinuum”, how did Weyl come to be so well-informed about Brouwer's new intuitionism, in what respect did Weyl's intuitionism differ from Brouwer's intuitionism, what did Brouwer think of Weyl's views,…? To some of these questions at least partial answers can be put forward on the basis of some of the available correspondence and notes. The present paper will concentrate mostly on the historical issues of the intuitionistic episode in Weyl's career.Weyl entered the foundational controversy with a bang in 1920 with his sensational paper “On the new foundational crisis in mathematics”. He had already made a name for himself in the foundations of mathematics in 1918 with his monograph “The Continuum” [18]; this contained in addition to a technical logical-mathematical construction of the continuum, a fairly extensive discussion of the shortcomings of the traditional construction of the continuum on the basis of arbitrary—and hence also impredicative—Dedekind cuts. (shrink)

Two different generalizations of Brouwer–Zadeh posets (BZ posets) are introduced. The former (called pre-BZ poset) arises from topological spaces, whose standard power set orthocomplemented complete atomic lattice can be enriched by another complementation associating with any subset the set theoretical complement of its topological closure. This complementation satisfies only some properties of the algebraic version of an intuitionistic negation, and can be considered as, a generalized form of a Brouwer negation. The latter (called degenerate BZ poset) arises from the so-called (...) special effects on a Hilbert space. It is shown that the standard Brouwer negation for effect operators produces a degenerate BZ poset with respect to the order induced from the partial sum operation. (shrink)