Errett Bishop's work in constructive mathematics is overwhelmingly regarded as a turning point for mathematics based on intuitionistic logic. It brought new life to this form of mathematics and prompted the development of new areas of research that witness today's depth and breadth of constructive mathematics. Surprisingly, notwithstanding the extensive mathematical progress since the publication in 1967 of Errett Bishop's Foundations of Constructive Analysis, there has been no corresponding advances in the philosophy of constructive mathematics Bishop style. The aim of (...) this paper is to foster the philosophical debate about this form of mathematics. I begin by considering key elements of philosophical remarks by Bishop, especially focusing on Bishop's assessment of Brouwer. I then compare these remarks with ``traditional'' philosophical arguments for intuitionistic logic and argue that the latter are in tension with Bishop's views. ``Traditional'' arguments for intuitionistic logic turn out to be also in conflict with significant recent developments in constructive mathematics. This rises pressing questions for the philosopher of mathematics, especially with regard to the possibility of offering alternative philosophical arguments for constructive mathematics. I conclude with the suggestion to look anew at Bishop's own remarks for inspiration. (shrink)

This volume of Metatheoria includes translations into Spanish of the three famous papers on the schools in foundations of mathematics, logicism, intuitionism and formalism, presented at the Königsberg’s Symposium on Foundations of Mathematics in September 1930 and finally published in the journal Erkenntnis in 1931. The three papers constituted a milestone in the Philosophy of Mathematics of the last century. In this introduction to the translations, the editors of the volume outline the historical context in which the original papers were (...) conceived and they include some details concerning their original publication. They also stress the decisive role played by the papers in the philosophy of mathematics in the last century. A summary of them is provided and the underlying ideas of the Vienna Circle on the nature of mathematics and the impact of Gödel theorems in the foundations programs are discussed. Moreover, they briefly introduce the original contributions to the volume that follow the translations. (shrink)

Proceeding of the work in trivalent logic developped under the direction of the professor Hugo Padilla Chacón at the 90's at the National Autonome University of México. Program in RLisp.

We present a new English translation of L.E.J. Brouwer's paper ‘De onbetrouwbaarheid der logische principes’ of 1908, together with a philosophical and historical introduction. In this paper Brouwer for the first time objected to the idea that the Principle of the Excluded Middle is valid. We discuss the circumstances under which the manuscript was submitted and accepted, Brouwer's ideas on the principle of the excluded middle, its consistency and partial validity, and his argument against the possibility of absolutely undecidable propositions. (...) We note that principled objections to the general excluded middle similar to Brouwer's had been advanced in print by Jules Molk two years before. Finally, we discuss the influence on George Griss' negationless mathematics. (shrink)

The birth, growth, stabilization and subsequent understanding of a new field of practical and theoretical enquiry is always a conceptual process including several typologies of events, phenomena an...

This paper discusses Michael Dummett’s attempt to base the use of intuitionistic logic in mathematics on a proof-conditional semantics. This project is shown to face significant obstacles resulting from the existence of variants of standard intuitionistic logic. In order to overcome these obstacles, Dummett and his followers must give an intuitionistically acceptable completeness proof for intuitionistic logic relative to the BHK interpretation of the logical constants, but there are reasons to doubt that such a proof is possible. The paper concludes (...) by proposing an alternative way of thinking about why one should use intuitionistic logic when doing mathematics. (shrink)

The concept of “necessity of thought” plays a central role in Dag Prawitz’s essay “Logical Consequence from a Constructivist Point of View” (Prawitz 2005). The theme is later developed in various articles devoted to the notion of valid inference (Prawitz, 2009, forthcoming a, forthcoming b). In section 1 I explain how the notion of necessity of thought emerges from Prawitz’s analysis of logical consequence. I try to expound Prawitz’s views concerning the necessity of thought in sections 2, 3 and 4. (...) In sections 5 and 6 I discuss some problems arising with regard to Prawitz’s views. (shrink)

The period from 1900 to 1935 was particularly fruitful and important for the development of logic and logical metatheory. This survey is organized along eight "itineraries" concentrating on historically and conceptually linked strands in this development. Itinerary I deals with the evolution of conceptions of axiomatics. Itinerary II centers on the logical work of Bertrand Russell. Itinerary III presents the development of set theory from Zermelo onward. Itinerary IV discusses the contributions of the algebra of logic tradition, in particular, Löwenheim (...) and Skolem. Itinerary V surveys the work in logic connected to the Hilbert school, and itinerary V deals specifically with consistency proofs and metamathematics, including the incompleteness theorems. Itinerary VII traces the development of intuitionistic and many-valued logics. Itinerary VIII surveys the development of semantical notions from the early work on axiomatics up to Tarski's work on truth. (shrink)

Intuitionism’s disagreement with classical logic is standardly based on its specific understanding of truth. But different intuitionists have actually explicated the notion of truth in fundamentally different ways. These are considered systematically and separately, and evaluated critically. It is argued that each account faces difficult problems. They all either have implausible consequences or are viciously circular.

The aim here is to investigate assertion and inference as notions of logic. Assertion will be explained in terms of its purpose, which is to give interlocutors the right to request the assertor to do a certain task. The assertion is correct if, and only if, the assertor knows how to do this task. Inference will be explained as an assertion equipped with what I shall call a justification profile, a strategy for making good on the assertion. The inference is (...) valid if, and only if, correctness is preserved from the premiss assertions to the conclusion assertion. Most of this is a spelling out of views on assertion and inference presented by Per Martin-Löf in lectures since 2015. (shrink)

At the beginning of the twentieth century, among the foundational schools of mathematics appeared ‘intuitionism’ by Dutchman L. E. J. Brouwer, who based arithmetic on the intuition of time and all mental constructions that could be made out of it. His pupil Arend Heyting was the first populariser of intuitionism, and he repeatedly emphasised that no philosophy was required to practise intuitionism so that such mathematics could be shared by anyone. Still, stimulated by invitations to humanistic conferences, he wrote a (...) series of notes, preserved in the State Archives, Haarlem, about solipsism. In them, he operated a series of theoretical reflections consisting of the stripping away of the patterns that are part of our consciousness and their subsequent progressive re-introduction, in order to understand the formation of our Self as distinct from the natural world and other humans. In 1996, following a stroke, neuroscientist Jill Bolte Taylor experienced the deprivation of certain abilities in her brain and their successive regaining. In her experience there are remarkable similarities with what Heyting had hypothesised about the formation of the self. The purpose of this article is to highlight them and point out how Heyting's theoretical construct was found to be embodied in the brain. (shrink)

Though the divide between reason-based and causal-explanatory approaches in psychiatry and psychopathology is old and deeply rooted, current trends involving multi-factorial explanatory models and evidence-based approaches to interpersonal psychotherapy, show that it has already been implicitly bridged. These trends require a philosophical reconsideration of how reasons can be causes. This paper contributes to that trajectory by arguing that Donald Davidson’s classic paradigm of 1963 is still a valid option.

What is the appropriate notion of truth for sentences whose meanings are understood in epistemic terms such as proof or ground for an assertion? It seems that the truth of such sentences has to be identified with the existence of proofs or grounds, and the main issue is whether this existence is to be understood in a temporal sense as meaning that we have actually found a proof or a ground, or if it could be taken in an abstract, tenseless (...) sense. Would the latter alternative amount to realism with respect to proofs or grounds in a way that would be contrary to the supposedly anti-realistic standpoint underlying the epistemic understanding of linguistic expressions? Before discussing this question, I shall consider reasons for construing linguistic meaning epistemically and relations between such reasons and reasons for taking an anti-realist point of view towards the discourse in question. (shrink)

Brouwer's criticism of mathematical proofs making essential use of the tertium non datur had a surprisingly late response in logical circles. Among the diverse reactions in the mid 1920s and early 1930s, it is possible to delimit a coherent body of opinions on these questions: (1) whether Brouwer's denial of the tertium non datur meant only the abandonment of this classical law or, beyond that, the affirmation of its negation; (2) whether one or both of these alternatives were logically inconsistent; (...) and (3) whether Brouwer's line of argument was forced to take resort to the very law it was designed to refute. The controversy centred around a series of articles by Marcel Barzin and Alfred Errera who fought against the intuitionistic critique, missed their victory because of conceptual confusions and fallacious reasoning, but emerged unconvinced from the debate in the late 1930s. The controversy is of interest to the historiography of formal logic since it stimulated the clarification not only of the concepts of formal validity, decidability, many-valued systems of logic and non-classical systems generally, but also of the distinction between object and meta-level, and between a formal system and its semantics. Most important, the debate, by putting pressure on the intuitionistic camp to make their ideas more precise, seems to have given the decisive motivation towards Heyting's answer to this demand by his axiomatization of intuitionistic logic in 1930. (shrink)

After the 1930s, the research into the foundations of mathematics changed.None of its main directions (logicism, formalism and intuitionism) had any longer the pretension to be the only true mathematics.Usually, the determining factor in the change is considered to be Gödel?s work, while Heyting?s role is neglected.In contrast, in this paper I first describe how Heyting directly suggested the abandonment of the big foundational questions and the putting forward of a new kind of foundational research consisting in the isolation of (...) formal, intuitive, logical and platonistic elements within classical mathematics.Furthermore, I describe how Heyting indirectly influenced the abandon?ment of the old directions of foundational research by making out some lists of degrees of evidence that exist within intuitionism. (shrink)

This paper is an attack on the Dummett-Prawitz view that the principle of bivalence has a crucial double significance, metaphysical and meaning theoretical. On the one hand it is said that holding bivalence valid is what characterizes a realistic view, i.e. a view in metaphysics, and on the other hand it is said that there are meaning theoretical arguments against its acceptability. I argue that these two aspects are incompatible. If the failure of validity of bivalence depends on properties of (...) linguistic meaning, then there are no metaphysical consequences to be drawn. The case for this view is straightforward as long as we are discussing a language different from our own. But it seems that the distinction between failure because of meaning and failure because of reality cannot be applied to our own language, simply because our own language is just what we use to represent reality. I argue that this impression is illusory. In order to draw a conclusion about reality, meaning must be connected with truth in a non-trivial way, and precisely this cannot be done in the language for which the meaning theory itself is correct. (shrink)

In the present paper I wish to regard constructivelogic as a self-contained system for the treatment ofepistemological issues; the explanations of theconstructivist logical notions are cast in anepistemological mold already from the outset. Thediscussion offered here intends to make explicit thisimplicit epistemic character of constructivism.Particular attention will be given to the intendedinterpretation laid down by Heyting. This interpretation, especially as refined in the type-theoretical work of Per Martin-Löf, puts thesystem on par with the early efforts of Frege andWhitehead-Russell. This quite (...) recent work, however,has proved valuable not only in the philosophy andfoundations of mathematics, but has also foundpractical application in computer science, where thelanguage of constructivism serves as an implementableprogramming language, and within the philosophy oflanguage.\footnote{Nordstr\"{o}m et al. give an overview of the work in computerscience, whereas Ranta provides an impressiveconstructivist alternative to Montague Grammar usingthe richer type structure of Martin-L\"{o}f in placeof the simple classical type theory of Church.} Mypresentation will be carried out through a contrastwith standard metamathematical work.\footnote{Troelstra and van Dalen give an encyclopedictreatment of the metamathematics of constructivism.}In the course of the development I have occasion tooffer some novel considerations on thenature of proof and inference. (shrink)

A comprehensive survey of Martin-Löf's constructive type theory, considerable parts of which have only been presented by Martin-Löf in lecture form or as part of conference talks. Sommaruga surveys the prehistory of type theory and its highly complex development through eight different stages from 1970 to 1995. He also provides a systematic presentation of the latest version of the theory, as offered by Martin-Löf at Leiden University in Fall 1993. This presentation gives a fuller and updated account of the system. (...) Earlier, brief presentations took no account of the issues related to the type-theoretical approach to logic and the foundations of mathematics, while here they are accorded an entire part of the book. Readership: Comprehensive accounts of the history and philosophy of constructive type theory and a considerable amount of related material. Readers need a solid background in standard logic and a first, basic acquaintance with type theory. (shrink)

Prawitz has recently developed a theory of epistemic grounding that differs in many respects from his earlier semantics of arguments and proofs. An innovative approach to inferences yields a new conception of the intertwinement of the notions of valid inference and proof. We aim at singling out three reasons that may have led Prawitz to the ground-theoretic turn, i.e.: a better order in the explanation of the relation between valid inferences and proofs; a notion of valid inference based on which (...) valid inferences and proofs are recognisable as such; a reconstruction of the deductive activity that makes inferences capable of yielding justification per se. These topics are discussed by Prawitz with reference to a very general and ancient question: why and how correct deduction has the epistemic power to compel us to accept its conclusions, provided its premises are justified? We conclude by remarking that, in spite of some improvements, the ground-theoretic approach shares with the previous one a problem of vacuous validity which, as Prawitz himself points out, blocks in both cases a satisfactory explanation of epistemic compulsion. (shrink)

The aim of this paper is to present a constructive solution to Frege's puzzle (largely limited to the mathematical context) based on type theory. Two ways in which an equality statement may be said to have cognitive significance are distinguished. One concerns the mode of presentation of the equality, the other its mode of proof. Frege's distinction between sense and reference, which emphasizes the former aspect, cannot adequately explain the cognitive significance of equality statements unless a clear identity criterion for (...) senses is provided. It is argued that providing a solution based on proofs is more satisfactory from the standpoint of constructive semantics. (shrink)

The work has two parts. The first part is about Peirce and his ideas about the continuum. There are considered the connection of his theory of continuity with his loic and his philosophy. In the second part Peirce's ideas are compared with models of todays logic and mathematics. There is considerd constructive mathematics, the logic of perception from Bell, Blau's Logic of reflection and a model of Myrvold. Then there is developed a new model.

Hilbert’s choice operators τ and ε, when added to intuitionistic logic, strengthen it. In the presence of certain extensionality axioms they produce classical logic, while in the presence of weaker decidability conditions for terms they produce various superintuitionistic intermediate logics. In this thesis, I argue that there are important philosophical lessons to be learned from these results. To make the case, I begin with a historical discussion situating the development of Hilbert’s operators in relation to his evolving program in the (...) foundations of mathematics and in relation to philosophical motivations leading to the development of intuitionistic logic. This sets the stage for a brief description of the relevant part of Dummett’s program to recast debates in metaphysics, and in particular disputes about realism and anti-realism, as closely intertwined with issues in philosophical logic, with the acceptance of classical logic for a domain reflecting a commitment to realism for that domain. Then I review extant results about what is provable and what is not when one adds epsilon to intuitionistic logic, largely due to Bell and DeVidi, and I give several new proofs of intermediate logics from intuitionistic logic+ε without identity. With all this in hand, I turn to a discussion of the philosophical significance of choice operators. Among the conclusions I defend are that these results provide a finer-grained basis for Dummett’s contention that commitment to classically valid but intuitionistically invalid principles reflect metaphysical commitments by showing those principles to be derivable from certain existence assumptions; that Dummett’s framework is improved by these results as they show that questions of realism and anti-realism are not an “all or nothing” matter, but that there are plausibly metaphysical stances between the poles of anti-realism and realism, because different sorts of ontological assumptions yield intermediate rather than classical logic; and that these intermediate positions between classical and intuitionistic logic link up in interesting ways with our intuitions about issues of objectivity and reality, and do so usefully by linking to questions around intriguing everyday concepts such as “is smart,” which I suggest involve a number of distinct dimensions which might themselves be objective, but because of their multivalent structure are themselves intermediate between being objective and not. Finally, I discuss the implications of these results for ongoing debates about the status of arbitrary and ideal objects in the foundations of logic, showing among other things that much of the discussion is flawed because it does not recognize the degree to which the claims being made depend on the presumption that one is working with a very strong logic. (shrink)

Dans ce texte, je pars de l’analyse intuitionniste de la vérité mathématique, « A est vrai si et seulement s’il existe une preuve de A » comme cas particulier de l’analyse de la vérité en termes de « vérifacteur », et je montre pourquoi Wittgenstein partageait celle-ci avec les intuitionnistes. Cependant, la notion de preuve à l’oeuvre dans cette analyse est, selon l’intuitionnisme, celle de la « preuve-comme-objet », et je montre par la suite, en interprétant son argument sur le (...) caractère « synoptique » des preuves, que Wittgenstein avait plutôt en tête une conception de la « preuve-comme-trace ».In this paper, I start with the intutionist analysis of mathematical truth, « A is true if and only if there exists a proof of A », as a particular case of the analysis of truth in terms of « truth-makers », and I show why Wittgenstein shared it with the intuitionists. However, the notion of proof at work in this analysis is, according to intuitionism, that of « proof-as-object », and I then show, with an interpretation of his argument on the « surveyability » of proofs, that, instead, Wittgenstein had in mind a notion of « proof-as-trace ». (shrink)

Gentzen's systems of natural deduction and sequent calculus were byproducts in his program of proving the consistency of arithmetic and analysis. It is suggested that the central component in his results on logical calculi was the use of a tree form for derivations. It allows the composition of derivations and the permutation of the order of application of rules, with a full control over the structure of derivations as a result. Recently found documents shed new light on the discovery of (...) these calculi. In particular, Gentzen set up five different forms of natural calculi and gave a detailed proof of normalization for intuitionistic natural deduction. An early handwritten manuscript of his thesis shows that a direct translation from natural deduction to the axiomatic logic of Hilbert and Ackermann was, in addition to the influence of Paul Hertz, the second component in the discovery of sequent calculus. A system intermediate between the sequent calculus LI and axiomatic logic, denoted LIG in unpublished sources, is implicit in Gentzen's published thesis of 1934—35. The calculus has half rules, half “groundsequents,” and does not allow full cut elimination. Nevertheless, a translation from LI to LIG in the published thesis gives a subformula property for a complete class of derivations in LIG. After the thesis, Gentzen continued to work on variants of sequent calculi for ten more years, in the hope to find a consistency proof for arithmetic within an intuitionistic calculus. (shrink)

Michael Dummett has interpreted and expounded upon intuitionism under the influence of Wittgensteinian views on language, meaning and cognition. I argue against the application of some of these views to intuitionism and point to shortcomings in Dummett's approach. The alternative I propose makes use of recent, post-Wittgensteinian views in the philosophy of mind, meaning and language. These views are associated with the claim that human cognition exhibits intentionality and with related ideas in philosophical psychology. Intuitionism holds that mathematical constructions are (...) mental processes or objects. Constructions are, in the first instance, forms of consciousness or possible experience of a particular type. As such, they must be understood in terms of the concept of intentionality. This view has a historical basis in the literature on intuitionism. In a famous 1931 lecture Heyting in fact identifies constructions with fulfilled or fulfillable mathematical intentions. I consider some of the consequences of this identification and contrast them with Dummett's views on intuitionism. (shrink)

It is by now well known that Gödel first advocated the philosophy of Leibniz and then, since 1959, that of Husserl. This raises three questions:1.How is this turn to Husserl to be interpreted? Is it a dismissal of the Leibnizian philosophy, or a different way to achieve similar goals?2.Why did Gödel turn specifically to the later Husserl's transcendental idealism?3.Is there any detectable influence from Husserl on Gödel's writings?Regarding the first question, Wang [96, p.165] reports that Gödel ‘[saw] in Husserl's work (...) a method of refining and consolidating Leibniz' monadology’. But what does this mean? In what for Gödel relevant sense is Husserl's work a refinement and consolidation of Leibniz' monadology?The second question is particularly pressing, given that Gödel was, by his own admission, a realist in mathematics since 1925. Wouldn't the uncompromising realism of the early Husserl's Logical investigations have been a more obvious choice for a Platonist like Gödel?The third question can only be approached when an answer to the second has been given, and we want to suggest that the answer to the first question follows from the answer to the second. We begin, therefore, with a closer look at the actual turn towards phenomenology.Some 30 years before his serious study of Husserl began, Gödel was well aware of the existence of phenomenology. Apart from its likely appearance in the philosophy courses that Gödel took, it reached him from various directions. (shrink)

In 1933 Godel introduced a calculus of provability (also known as modal logic S4) and left open the question of its exact intended semantics. In this paper we give a solution to this problem. We find the logic LP of propositions and proofs and show that Godel's provability calculus is nothing but the forgetful projection of LP. This also achieves Godel's objective of defining intuitionistic propositional logic Int via classical proofs and provides a Brouwer-Heyting-Kolmogorov style provability semantics for Int which (...) resisted formalization since the early 1930s. LP may be regarded as a unified underlying structure for intuitionistic, modal logics, typed combinatory logic and λ-calculus. (shrink)

This volume is dedicated to Prof. Dag Prawitz and his outstanding contributions to philosophical and mathematical logic. Prawitz's eminent contributions to structural proof theory, or general proof theory, as he calls it, and inference-based meaning theories have been extremely influential in the development of modern proof theory and anti-realistic semantics. In particular, Prawitz is the main author on natural deduction in addition to Gerhard Gentzen, who defined natural deduction in his PhD thesis published in 1934. The book opens with an (...) introductory paper that surveys Prawitz's numerous contributions to proof theory and proof-theoretic semantics and puts his work into a somewhat broader perspective, both historically and systematically. Chapters include either in-depth studies of certain aspects of Dag Prawitz's work or address open research problems that are concerned with core issues in structural proof theory and range from philosophical essays to papers of a mathematical nature. Investigations into the necessity of thought and the theory of grounds and computational justifications as well as an examination of Prawitz's conception of the validity of inferences in the light of three “dogmas of proof-theoretic semantics” are included. More formal papers deal with the constructive behaviour of fragments of classical logic and fragments of the modal logic S4 among other topics. In addition, there are chapters about inversion principles, normalization of proofs, and the notion of proof-theoretic harmony and other areas of a more mathematical persuasion. Dag Prawitz also writes a chapter in which he explains his current views on the epistemic dimension of proofs and addresses the question why some inferences succeed in conferring evidence on their conclusions when applied to premises for which one already possesses evidence. (shrink)

MICHAEL DUMMETT, Elements of intuitionism. With the assistance of Robert Minio. Oxford: Oxford University Press, 1977. xii + 466 pp. No price stated.

Truth-maker analyses construe truth as existence of proof, a well-known example being that offered by Wittgenstein in theTractatus. The paper subsumes the intuitionistic view of truth as existence of proof under the general truth-maker scheme. Two generic constraints on truth-maker analysis are noted and positioned with respect to the writings of Michael Dummett and theTractatus. Examination of the writings of Brouwer, Heyting and Weyl indicates the specific notions of truth-maker and existence that are at issue in the intuitionistic truth-maker analysis, (...) namely that of proof in the sense of proof-object (Brouwer, Heyting) and existence in the nonpropositional sense of a judgement abstract (Weyl). Furthermore, possible anticipations in the writings of Schlick and Pfänder are noted. (shrink)

Even though Husserl and Brouwer have never discussed each other's work, ideas from Husserl have been used to justify Brouwer's intuitionistic logic. I claim that a Husserlian reading of Brouwer can also serve to justify the existence of choice sequences as objects of pure mathematics. An outline of such a reading is given, and some objections are discussed.

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.

We may try to explain proofs as chains of valid inference, but the concept of validity needed in such an explanation cannot be the traditional one. For an inference to be legitimate in a proof it must have sufficient epistemic power, so that the proof really justifies its final conclusion. However, the epistemic concepts used to account for this power are in their turn usually explained in terms of the concept of proof. To get out of this circle we may (...) consider an idea within intuitionism about what it is to justify the assertion of a proposition. It depends on Heyting’s view of the meaning of a proposition, but does not presuppose the concept of inference or of proof as chains of inferences. I discuss this idea and what is required in order to use it for an adequate notion of valid inference. (shrink)

Recently discovered documents have shown how Gentzen had arrived at the final form of natural deduction, namely by trying out a great number of alternative formulations. What led him to natural deduction in the first place, other than the general idea of studying “mathematical inference as it appears in practice,” is not indicated anywhere in his publications or preserved manuscripts. It is suggested that formal work in axiomatic logic lies behind the birth of Gentzen’s natural deduction, rather than any single (...) decisive influence in the work of others. Various axiomatizations are explored in turn, from the classical axioms of Hilbert and Ackermann to the intuitionistic axiomatization of Heyting. (shrink)

Weyl's inclination toward constructivism in the foundations of mathematics runs through his entire career, starting with Das Kontinuum. Why was Weyl inclined toward constructivism? I argue that Weyl's general views on foundations were shaped by a type of transcendental idealism in which it is held that mathematical knowledge must be founded on intuition. Kant and Fichte had an impact on Weyl but HusserFs transcendental idealism was even more influential. I discuss Weyl's views on vicious circularity, existence claims, meaning, the continuum (...) and choice sequences, and the intuitive-symbolic distinction against the background of his transcendental idealism and general intuitionism. (shrink)

The notion of cognitive act is of importance for an epistemology that is apt for constructive type theory, and for epistemology in general. Instead of taking knowledge attributions as the primary use of the verb 'to know' that needs to be given an account of, and understanding a first-person knowledge claim as a special case of knowledge attribution, the account of knowledge that is given here understands first-person knowledge claims as the primary use of the verb 'to know'. This means (...) that a cognitive act is an act that counts as cognitive from a first-person point of view. The method of linguistic phenomenology is used to explain or elucidate our epistemic notions. One of the advantages of the theory is that an answer can be given to some of the problems in modern epistemology, such as the Gettier problem. (shrink)

This article provides an English translation of a historic discussion on the foundations of mathematics, during which Kurt GÖdel first announced his incompleteness theorem to the mathematical world. The text of the discussion is preceded by brief background remarks and commentary.