Search

The classical interpretation of mathematical statements can be seen as comprising two separate but related aspects: a domain and a truth-schema. L. E. J. Brouwer’s intuitionistic project lays the groundwork for an alternative conception of the objects in this domain, as well as an accompanying intuitionistic truth-schema. Drawing on the work of Arend Heyting and Michael Dummett, I present two objections to classical mathematical semantics, with the aim of creating an opening for an alternative interpretation. With this accomplished, I then make the case for intuitionism as a suitable candidate to fill this void.

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 (i.e., which part is equiconsistent with $\textbf {PRA}$ or consistent provably in $\textbf {PRA}$ ) 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: (i) fan theorem for decidable fans but arbitrary bars; (ii) continuity principle and the axiom of choice both for arbitrary formulae; and (iii) $\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 (except the choice along functions); but that limited principle of omniscience LPO makes the situation completely classical.

We continue the investigation of the first paper where we studied logics with various negations including empirical negation and co-negation. We established how such logics can be treated uniformly with R. Sylvan's CCω as the basis. In this paper we use this result to obtain cut-free labelled sequent calculi for the logics.

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 ...

This paper sketches a way of supplementing classical mathematics with a motivation for a Brouwerian theory of free choice sequences. The idea is that time is unending, i.e. that one can never come to an end of it, but also indeterminate, so that in a branching time model only one branch represents the ‘actual’ one. The branching can be random or subject to various restrictions imposed by the creating subject. The fact that the underlying mathematics is classical makes such perhaps delicate issues as the fan theorem no longer problematic. On this model, only intuitionistic logic applies to the Brouwerian free choice sequences, and there it applies not because of any skepticism about classical mathematics, but because there is no ‘end of time’ from the standpoint of which everything about the sequences can be decided.

Powerful yet effective induction principles play an important role in computing, being a paramount component of programming languages, automated reasoning, and program verification systems. The Bar Induction (BI) principle is a fundamental concept of intuitionism, which is equivalent to the standard principle of transfinite induction. In this work, we investigate the compatibility of several variants of BI with Constructive Type Theory (CTT), a dependent type theory in the spirit of Martin-Löf’s extensional theory. We first show that CTT is compatible with a BI principle for sequences of numbers. Then, we establish the compatibility of CTT with a more general BI principle for sequences of name-free closed terms. The formalization of the latter principle within the theory involved enriching CTT’s term syntax with a limit constructor and showing that consistency is preserved. Furthermore, we provide novel insights regarding BI, such as the non-truncated version of BI on monotone bars being intuitionistically false. These enhancements are carried out formally using the Nuprl proof assistant that implements CTT and the formalization of CTT within the Coq proof assistant presented in previous works.

We consider some advanced topics in logic including fuzzy logic, temporal logic, intuitionist logic, undefined values in logic, logic and AI and theorem provers. Fuzzy logic is an extension of classical logic that acts as a mathematical model for vagueness. Temporal logic is concerned with the expression of properties that have time dependencies. Brouwer and others developed intuitionist logic as the logical foundation for intuitionism, which was a controversial theory of the foundations of mathematics based on a rejection of the law of the excluded middle and an insistence on constructive existence. We discuss several approaches that have been applied to dealing with undefined values that arise with partial functions including the logic of partial functions; Dijkstra’s approach with his cand and cor operators; and Parnas’s approach which preserves a classical two-valued logic.

Gentzen’s approach by transfinite induction and that of intuitionist Heyting arithmetic to completeness and the self-foundation of mathematics are compared and opposed to the Gödel incompleteness results as to Peano arithmetic. Quantum mechanics involves infinity by Hilbert space, but it is finitist as any experimental science. The absence of hidden variables in it interpretable as its completeness should resurrect Hilbert’s finitism at the cost of relevant modification of the latter already hinted by intuitionism and Gentzen’s approaches for completeness. This paper investigates both conditions and philosophical background necessary for that modification. The main conclusion is that the concept of infinity as underlying contemporary mathematics cannot be reduced to a single Peano arithmetic, but to at least two ones independent of each other. Intuitionism, quantum mechanics, and Gentzen’s approaches to completeness an even Hilbert’s finitism can be unified from that viewpoint. Mathematics may found itself by a way of finitism complemented by choice. The concept of information as the quantity of choices underlies that viewpoint. Quantum mechanics interpretable in terms of information and quantum information is inseparable from mathematics and its foundation.

Aristotle made the first steps to the establishment of the mathematical logic by giving ideas for the concepts “sentence” and “predicate”; the fundamental logical functions as conjunction, disjunction and negation, the logical quantifiers, modal operators, and many others. He was the first who justified the need for axioms and presented the first examples of such. For 23 centuries one of his proposed axioms—the Law of Excluded Middle (LEM)—has been among the main tools for proving mathematical assertions.

Nenhum aspecto da matemática foi tão analisado “à luz da teoria piagetiana” quanto o número. Os resultados encontrados por Piaget e Szeminska e publicados no livro A gênese do número na criança geraram, também, inúmeras publicações acerca das suas possíveis implicações pedagógicas. Para os pesquisadores, o número é elaborado a partir da síntese operatória da seriação e da classificação, estabelecendo um tertium entre as definições de número propostas por duas das principais correntes do pensamento matemático: o logicismo e o intuicionismo. Neste artigo expõe-se o debate entre intuicionismo e logicismo sobre o número e a posição epistemológica de Piaget que levou a uma nova concepção de compreender a gênese do número na criança. Palavras-chave: definição piagetiana de número; logicismo; intuicionismo. Abstract Perhaps no aspect in Mathematics has been so thoroughly analyzed than the concept of number from Piaget’s point of view. Results by Piaget and Szeminska in their book “The Child’s Conception of Number” brought forth several publications on possible pedagogical implications on the issue. For researchers, the number concept is worked out from the operational synthesis of serializing and classification, while establishing a tertium between the definitions of number, which have been proposed by two of the main mathematical thoughts, namely logics and intuitionalism. In this article the debate between intuitionalism and logics on the number and Piaget’s epistemological stance that led to a new concept on the genesis of number in the child is provided. Keywords: Piaget’s definition of number; logics; intuitionism.

The translation into English of Aleksandr Yakovlevich Khinchin's (1894–1959) 1926 paper entitled ‘Ideas of intuitionism and the struggle for a subject matter in contemporary mathematics’ is made available for the first time. Here, Khinchin presented the famous foundational debate between L.E.J. Brouwer and David Hilbert of the 1920s in terms of a search for a mathematics with content. His main aim seems to have been to make intuitionism ideologically acceptable to his audience at the Communist Academy by means of the claim that insofar as Brouwer's intuitionism had a clear ‘subject matter’ and Hilbert's new program was a concession to intuitionism, the alleged victory of intuitionism not only implied the defeat of ‘empty’ formalism, but also showed the compatibility and affinity of Marxism with the newest developments in modern mathematics. This introduction provides a tentative exploration of the issue of what was tactical (or due to ideological pressure) and what was real scientific interest (or due to ignorance) (or what was both) in Khinchin's 1926 paper in the form of a detailed commentary, especially, on the tactical side of his presentation of the positions of Brouwer and Hilbert.

As Weyl was interested in infinitesimal analysis and for some years embraced Brouwer's intuitionism, which he continued to see as an ideal even after he had convinced himself that it is a practical necessity for science to go beyond intuitionistic mathematics, this note presents some remarks on infinitesimals from a Brouwerian perspective. After an introduction and a look at Robinson's and Nelson's approaches to classical nonstandard analysis, three desiderata for an intuitionistic construction of infinitesimals are extracted from Brouwer's writings. These cannot be met, but in explicitly Brouwerian settings what might in different ways be called approximations to infinitesimals have been developed by early Brouwer, Vesley, and Reeb. I conclude that perhaps Reeb's approach, with its Brouwerian motivation for accepting Nelson's classical formalism, would have suited Weyl best.

Our very eloquent charge from Jan van Mill was to “draw a line to Brouwer from descriptive set theory, but this proved elusive: in fact there are few references to Brouwer, in Lusin (1928) [36] and Lusin (1930), none of them substantial; and even though Brouwer refers to Borel, Lebesgue and Hadamard in his early papers, it does not appear that he was influenced by their work in any substantive way. 1 We have not found any references by him to more developed work in descriptive set theory, after the critical Lebesgue (1905). So instead of looking for historical connections or direct influences (in either direction), we decided to identify and analyze some basic themes, problems and results which are common to these two fields; and, as it turns out, the most significant connections are between intuitionistic analysis and effective descriptive set theory, hence the title. ⇒ We will outline our approach and (limited) aims in Section 1 , marking with an arrow (like this one) those paragraphs which point to specific parts of the article. Suffice it to say here that our main aim is to identify a few, basic results of descriptive set theory which can be formulated and justified using principles that are both intuitionistically and classically acceptable; that we will concentrate on the mathematics of the matter rather than on history or philosophy; and that we will use standard, classical terminology and notation. This is an elementary, mostly expository paper, broadly aimed at students of logic and set theory who also know the basic facts about recursive functions but need not know a lot about either intuitionism or descriptive set theory. The only (possibly) new result is Theorem 6.1 , which justifies simple definitions and proofs by induction in Kleene’s Basic System of intuitionistic analysis, and is then used in Theorem 7.1 , Theorem 7.2 to give in the same system a rigorous definition of the Borel sets and prove that they are analytic; the formulation and proof of this last result is one example where methods from effective descriptive set theory are used in an essential way.

The paper resolves the great debate of the 20th century between the three philosophies of mathematics-logicism, intuitionism and formalism—founded by Bertrand Russell and A. N. Whitehead, L. E. J. Brouwer and David Hilbert, respectively. The issue: which one provides firm foundations for mathematics? None of them won the debate. We make a critique of each, consolidate their contributions, rectify their weakness and add our own to resolve the debate. The resolution forms the new foundations of mathematics. Then we apply the new foundations to assess the status of Hilbert’s 23 problems most of which in foundations and find out which ones have been solved, which ones have flawed solutions that we rectify and which ones are open problems. Problem 6 of Hilbert’s problems—Can physics be axiomatized?—is answered yes in E. E. Escultura, Nonlinear Analysis, A-Series: 69(2008), which provides the solution, namely, the grand unified theory (GUT). We also point to the resolution of the 379-year-old Fermat’s conjecture (popularly known as Fermat’s last theorem) in E. E. Escultura, Exact Solutions of Fermat’s Equations (Definitive Resolution of Fermat’s Last Theorem), Nonlinear Studies, 5(2), (1998). Likewise, the proof of the 274-year-old Goldbach’s conjecture is in E. E. Escultura, The New Mathematics and Physics, Applied Mathematics and Computation, 138(1), 2003.

The paper examines Andre 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 influence 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.

Intuitionistic logic has developed as a result of certain philosophical views on the foundation of mathematics, known as intuitionism. Intuitionism was originated by L. E. J. Brouwer in 1908. The first Hilbert style formalization of the intuitionistic logic, formulated as a proof system, is due to A. Heyting (1930). In this chapter we present a Hilbert style proof system I that is equivalent to the Heyting’s original formalization and discuss the relationship between intuitionistic and classical logic.

Brouwer’s intuitionism is based on quite different philosophical ideas about the nature of mathematical objects than classical mathematics. This intuitionistic point of view results in a different use of language and in a corresponding different intuitionistic logic which is far more subtle than the classical use of language and corresponding classical logic. Nevertheless an intuitionistic deduction system and a notion of intuitionistic deducibility was developed by A. Heyting and it is amazing to see that a small change in the logical axioms, replacing the logical axiom ГГA → A by ГA → (A → B), may have such far reaching consequences. Since finding (intuitionistic) formal deductions may be difficult, an intuitionistic tableaux based formal deduction system is presented in which the construction of intuitionistic deductions is rather straightforward. The semantics of intuitionistic logic and the notion of (intuitionistic) valid consequence are given in terms of (intuitionistic) Kripke models and it is shown that the three notions of intuitionistic valid consequence, intuitionistic deducibility and intuitionistic tableau-deducibility are equivalent. Intuitionistic sets are either finite constructions or otherwise, they are (subsets of) construction projects. Spreads are a particular kind of construction project, inducing specific principles which typically do not hold for other sets.

Revising classical logic—to deal with the paradoxes of self-reference, or vague propositions, for the purposes of scientific theory or of metaphysical anti-realism—requires the revision of probability theory. This chapter reviews the connection between classical logic and classical probability, clarifies nonclassical logic, giving simple examples, explores modifications of probability theory, using formal analogies to the classical setting, and provides two foundational justifications for these ‘nonclassical probabilities’. There follows an examination of extensions of the nonclassical framework: to conditionalization and decision theory in particular, before a final review of open questions and alternative approaches, and an evaluation of current progress.

By the end of the 19th century, mathematics had become very intensively developed. Mathematical logic became an independent discipline, and in the 1880s Cantor published his work on set theory. All this led to questions about the consistency of mathematical theories and decidability theorems. Therefore, for the second time in the history of mathematics, there emerged a crisis of the basis of mathematics.There were a few ideas for overcoming the crisis. In this paper, there will be described three trends in the philosophy of mathematics in the late 19th and early 20th centuries: logicism (Frege), intuitionism (Brouwer) and formalism (Hilbert). These three trends were described from the philosophical point of view and in the context of the crisis. Moreover, for each of them there will be present the most important methodological assumptions, and I will briefly describe attempts to achieve them. This will describe the problem in such a way that allows for the grasping of important differences and similarities between logicism, intuitionism and formalism and better understand their causes.

In 1932 Kolmogorov created a calculus of problems. This calculus became known to Deleuze through a 1945 paper by Paulette Destouches-Février. In it, he ultimately recognised a deepening of mathematical intuitionism. However, from the beginning, he proceeded to show its limits through a return to the Leibnizian project of Calculemus taken in its metaphysical stance. In the carrying out of this project, which is illustrated through a paradigm borrowed from Spinoza, the formal parallelism between problems, Leibnizian themes and Peircean rhemes provides the key idea. By relying on this parallelism and by spreading the dialectic defined by Lautman with its ‘logical drama’ onto a Platonic perspective, we will attempt to obtain Deleuze's full calculus of problems. In investigating how the same Idea may be in mathematics and in philosophy, we will proceed to show how this calculus of problems qualifies not only as a paradigm of the Idea but also as the apex of transdiciplinarity.2

An extension of intuitionism to empirical discourse, a project most seriously taken up by Dummett and Tennant, requires an empirical negation whose strength lies somewhere between classical negation (‘It is unwarranted that. . . ’) and intuitionistic negation (‘It is refutable that. . . ’). I put forward one plausible candidate that compares favorably to some others that have been propounded in the literature. A tableau calculus is presented and shown to be strongly complete.

Emmy Noether’s many articles around the time that Felix Klein and David Hilbert were arranging her invitation to Gottingen include a short but brilliant note on invariants of finite groups highlighting her creativity and perspicacity in algebra. Contrary to the idea that Noether abandoned Paul Gordan’s style of mathematics for Hilbert’s, this note shows her combining them in a way she continued throughout her mature abstract algebra.

In this paper investigates how natural deduction rules define connective meaning by presenting a new method for reading semantical conditions from rules called natural semantics. Natural semantics explains why the natural deduction rules are profoundly intuitionistic. Rules for conjunction, implication, disjunction and equivalence all express intuitionistic rather than classical truth conditions. Furthermore, standard rules for negation violate essential conservation requirements for having a natural semantics. The standard rules simply do not assign a meaning to the negation sign. Intuitionistic negation fares much better. Not only do the intuitionistic rules have a natural semantics, that semantics amounts to familiar intuitionistic truth conditions. We will make use of these results to argue that intuitionistic connectives, rather than standard ones have a better claim to being the truly logical connectives.

This papers extends the Nuprl proof assistant (a system representative of the class of extensional type theories a la Martin-Lof) with named exceptions and handlers, as well as a nominal fresh operator. Using these new features, we prove a version of Brouwer's Continuity Principle for numbers. We also provide a simpler proof of a weaker version of this principle that only uses diverging terms. We prove these two principles in Nuprl's meta-theory using our formalization of Nuprl in Coq and show how we can reflect these meta-theoretical results in the Nuprl theory as derivation rules. We also show that these additions preserve Nuprl's key meta-theoretical properties, in particular consistency and the congruence of Howe's computational equivalence relation. Using continuity and the fan theorem we prove important results of Intuitionistic Mathematics: Brouwer's continuity theorem and bar induction on monotone bars.

The formal system of intuitionistic epistemic logic IEL was proposed by S. Artemov and T. Protopopescu. It provides the formal foundation for the study of knowledge from an intuitionistic point of view based on Brouwer-Hayting-Kolmogorov semantics of intuitionism. We construct a cut-free sequent calculus for IEL and establish that polynomial space is sufficient for the proof search in it. We prove that IEL is PSPACE-complete.

One’s first impression is that Brouwer’s Continuity Theorem of intuitionistic analysis, that every total, real-valued function of a real variable is continuous, stands in straightforward contradiction to a simple theorem of conventional real analysis, that there are discontinuous, real-valued func­tions. Here we argue that, despite philosophical views to the contrary, first impressions are not misleading; the Brouwer Theorem, together with its proof, presents mathematicians and philosophers of mathematics with an antimony, one that can only be resolved by a close, foundational study of the structure of the intuitive continuum.

Godel regarded the Dialectica interpretation as giving constructive content to intuitionism, which otherwise failed to meet reasonable conditions of constructivity. He founded his theory of primitive recursive functions, in which the interpretation is given, on the concept of computable function of finite type. I will 1) criticize this foundation, 2) propose a quite different one, and 3) note that essentially the latter foundation also underlies the Curry-Howard type theory and hence Heyting’s intuitionistic conception of logic. Thus the Dialectica interpretation (in so far as its aim was to give constructive content to intuitionism) is superfluous. In the set of notes [1938a] for an informal lecture, Godel refers to a hierarchy of constructive or finitary systems, the lowest level of which he called finitary number theory and is, in fact, primitive recursive arithmetic (PRA). He mentions three constructive extensions of this system: the intuitionism of Brouwer and Heyting (the “modal-logical route”), concerning which he is quite critical, the use of transfinite induction, inspired by Gentzen’s consistency proof for PA, and the use of functions of finite or even transfinite type over the type N of natural numbers. The latter extension seems to be mentioned here for the first time in connection with constructive extensions of finitary number theory. He ranks it the most satisfactory of these extensions ∗Versions of this paper were presented at a joint workshop on Hilbert at CarnegieMellon University and the University of Pittsburgh in June 1998, at a workshop on foundations of mathematics at UCLA in May 2005 and at the IMLA ’05 workshop [Intuitionistic Modal Logic and Applications, of course] in Chicago. I received helpful comments on all of these occasions. As for the history of the idea of a hierarchy of types, I know only of these examples: The hierarchy of transfinite types in which the natural numbers constitute the lowest type

We discuss the foundations of constructive mathematics, including recursive mathematics and intuitionism, in relation to classical mathematics. There are connections with the foundations of physics, due to the way in which the different branches of mathematics reflect reality. Many different axioms and their interrelationship are discussed. We show that there is a fundamental problem in BISH (Bishop’s school of constructive mathematics) with regard to its current definition of ‘continuous function’. This problem is closely related to the definition in BISH of ‘locally compact’. Possible approaches to this problem are discussed. Topology seems to be a key to understanding many issues. We offer several new simplifying axioms, which can form bridges between the various branches of constructive mathematics and classical mathematics (‘reuniting the antipodes’). We give a simplification of basic intuitionistic theory, especially with regard to so-called ‘bar induction’. We then plead for a limited number of axiomatic systems, which differentiate between the various branches of mathematics. Finally, in the appendix we offer BISH an elegant topological definition of ‘locally compact’, which unlike the current definition is equivalent to the usual classical and/or intuitionistic definition in classical and intuitionistic mathematics, respectively.

Intuitionistic mathematics was created by Brouwer on the basis of constructive reasoning, where the existence of a proof was the criterion for truth. Kolmogorov and Godel proposed interpreting intuitionistic logic on the basis of classical notions of a problem's solution and of provability. In 1933 Godel made the first substantial step toward the building of such an interpretation. Despite much progress in the understanding of intuitionism, this task was not complete before the author's 1995 paper. This survey will cover the results of the past decade obtained within this framework.

This paper discusses the problem of availability of constructive metamathematics for constructive theories. Since intuitionism is usually considered as the most important kind of constructivism, we have the following question: Is it possible to give intuitionistically acceptable proofs of metamathematical theorems? This issue is illustrated by the completeness theorem for intuitionistic predicate logic and the consistency of arithmetic. The conclusion is that hitherto collected evidence justifies the claim that the universal intuitionistic metamathematics is very problematic.

We describe in some detail how to build an infinite computing machine within a continuous Newtonian universe. The relevance of our construction to the Church

In a seriesof papers beginning in 1944, the Dutch mathematician and philosopherGeorge Francois Cornelis Griss proposed that constructivemathematics should be developedwithout the use of the intuitionistic negation1 and,moreover, without any use of a nullpredicate.In the present work, we give formalized versions of intuitionisticarithmetic, analysis,and higher-order arithmetic in the spirit ofGriss' ``negationless intuitionistic mathematics''and then consider their relation to thecurrent formalizations of thesetheories.

In a series of papers beginning in 1944, the Dutch mathematician and philosopher George Francois Cornelis Griss proposed that constructive mathematics should be developed without the use of the intuitionistic negation 1 and, moreover, without any use of a null predicate. In the present work, we give formalized versions of intuitionistic arithmetic, analysis, and higher-order arithmetic in the spirit of Griss' negationless intuitionistic mathematics and then consider their relation to the current formalizations of these theories.

We show that various fragments of the intuitionistic/constructive theory of the reals are decidable.

In the course of a recent paper on modal' extensions of the intuitionist propositional calculus, [1], I made some suggestions as to the relationships between the system MIPC, the intuitionist predicate calculus, and the question of producing a genuine intuitionist concept of modality. This paper may be regarded as a clarification of those rather inaccurate ideas in the light of Kripke's outstanding analysis of the intuitionist predicate calculus, [2]. (I use Kripke's notation and terminology here without explanation — this work is intended to be read in conjunction with [2].) In particular, I shall adapt his interpretation of his modelling to give an account of MIPC in terms of differing mathematical intuitions.

In the standard textbooks Hilbert’s philosophy of mathematics is commonly labelled formalism and under this title distinguished from Brouwer’s intuitionism, on the one hand, and Russell’s logicism, on the other hand. However, as Hintikka (1997a) rightly remarks, this popular name is very misleading.

In the first section we mention the main philosophical approaches in the standard classification: platonism, intuitionism, logicism and formalism. In the second section, we discuss consistency statements, reflection principles and theories obtained by transfinite iterations of these principles. Furthermore, we present some results of the program of using large cardinals to cope with incompleteness in set theory. In the final section, we present the concept of physical natural numbers and attempt to give an alternative formalization of this concept.

In the late 1960s, Dana Scott first showed how the Stone-Tarski topological interpretation of Heyting's calculus could be extended to model intuitionistic analysis; in particular Brouwer's continuity principle. In the early '80s we and others outlined a general treatment of non-constructive objects, using sheaf models--constructions from topos theory--to model not only Brouwer's non-classical conclusions, but also his creation of "new mathematical entities". These categorical models are intimately related to, but more general than Scott's topological model. The primary goal of this paper is to consider the question of iterated extensions. Can we derive new insights by repeating the second act? In Continuous Truth I, presented at Logic Colloquium '82 in Florence, we showed that general principles of continuity, local choice and local compactness hold in the gros topos of sheaves over the category of separable locales equipped with the open cover topology. We touched on the question of iteration. Here we develop a more general analysis of iterated categorical extensions, that leads to a reflection schema for statements of predicative analysis. We also take the opportunity to revisit some aspects of both Continuous Truth I and Formal Spaces Fourman & Grayson 1982, and correct two long-standing errors therein.

This paper gives a survey of David Hilbert's (1862–1943) changing attitudes towards logic. The logical theory of the Gottingen mathematician is presented as intimately linked to his studies on the foundation of mathematics. Hilbert developed his logical theory in three stages: (1) in his early axiomatic programme until 1903 Hilbert proposed to use the traditional theory of logical inferences to prove the consistency of his set of axioms for arithmetic. (2) After the publication of the logical and set-theoretical paradoxes by Gottlob Frege and Bertrand Russell it was due to Hilbert and his closest collaborator Ernst Zermelo that mathematical logic became one of the topics taught in courses for Gottingen mathematics students. The axiomatization of logic and set-theory became part of the axiomatic programme, and they tried to create their own consistent logical calculi as tools for proving consistency of axiomatic systems. (3) In his struggle with intuitionism, represented by L. E. J. Brouwer and his advocate Hermann Weyl, Hilbert, assisted by Paul Bemays, created the distinction between proper mathematics and meta-mathematics, the latter using only finite means. He considerably revised the logical calculus of thePrincipia Mathematica of Alfred North Whitehead and Bertrand Russell by introducing the e-axiom which should serve for avoiding infinite operations in logic.

We review four sources that presented CBT in an intuitionist context, from which certain modes of reasoning, applied in the proofs of CBT, are expelled: A counterexample by Brouwer from his 1912 inauguration address, a theorem by Myhill his from 1955 paper, counterexamples by Dirk van Dalen from his 1968 paper and a theorem by Troelstra from his 1969 monograph.

Godel’s incompleteness theorems had a dramatic impact on Hilbert’s foundational program. That is common lore. For some, e.g. von Neumann and Herbrand, they undermined the finitist consistency program; for others, e.g. Godel and Bernays, they left room for a fruitful development of proof theory. This paper aims for a nuanced and deepened understanding of how Godel’s results effected a transformation of proof theory between 1930 and 1934. The starting-point of this transformative period is Godel’s announcement of a restricted unprovability result in September of 1930; its end-point is the completion of Gentzen’s first consistency proof for elementary number theory in late 1934. Hilbert, surprisingly, is the initial link between starting-point and end-point. He addressed Godelian issues in two strikingly different papers, (1931a) and (1931b), without mentioning Godel. In (1931a) he takes on the challenge of the restricted unprovability result; in (1931b) he responds to the second incompleteness theorem concerning the unprovability of consistency for a system S in S. He does so by bringing in semantic considerations and by pursuing novel, but also highly problematic directions: he argues for the contentual correctness of a constructive (for him, finitist) theory that includes intuitionist number theory. Gentzen followed the new directions in late 1931, addressed methodological issues and metamathematical problems in ingenious ways, while building on ideas and techniques that had been introduced in proof theory. Most distinctive is Gentzen’s struggle with contentual correctness and its relation to consistency. That is reflected in a sequence of notes Gentzen wrote between late-1931 and late-1934, but it is also central in his classical paper (1936). The immediate lessons seem to be: (i) there is real continuity between Hilbert’s proof theory and Gentzen’s work, and (ii) there is deepened concern for interpreting intuitionist arithmetic (and thus understanding classical arithmetic) from a more strictly constructive perspective. Ironically, the latter concern deeply influenced Godel’s functional interpretation of intuitionist arithmetic.

Constructive mathematics, mathematics in which the existence of an object means that that we can actually construct this object, started as a heavily restricted version ofmathematics, a version in which many commonly used mathematical techniques (like the Law of Excluded Middle) were forbidden to maintain constructivity. Eventually, it turned out that not only constructive mathematics is not a weakened version of the classical one - as it was originally perceived - but that, vice versa, classical mathematics can be viewed as a particular (thus, weaker) case of the constructive one. Crucial results in this direction were obtained by M. Gelfond in the 1970s. In this paper, we mention the history of these results, and show how these results affected constructive mathematics, how they led to new algorithms, and how they affected the current activity in logic programming-related research.

Problems are defined as abstract procedures. An explication of procedures as used in Transparent Intensional Logic (TIL) and called constructions is presented and the subclass of constructions called concepts is defined. Concepts as closed constructions modulo α- and η-conversion can be associated with meaningful expressions of a natural or professional language in harmony with Church’s conception. Thus every meaningful expression expresses a concept. Since every problem can be unambiguously determined by a concept we can state that every problem is a concept and every concept can be viewed as a problem.Kolmogorov’s idea of a connection between problems and Heyting’s calculus is examined and the non-classical features of the latter are shown to be compatible with realistic logic using partial functions.

It is evident that fuzzy logic should be studied from various scientific points of departure, however, fuzzy logic appears different depending on this viewpoint: from the standpoint of a philosopher or applied computer scientist fuzzy logic is a contrast to binary logic and crispness, while a mathematician examines fuzzy logic from a pure mathematical angle: what are the mathematical principles and algebraic structures behind fuzzy logic? Thus, for a mathematician there is nothing really fuzzy in fuzzy logic, indeed, it is an exact logic of inexact concepts and phenomena. An analogy can be found in probability theory: it is not relevant to ask what the probability is that Central Limit Theorem holds; this is a matter of exact proof, not a probability. Intuitionist mathematics is a branch of mathematical research where a theorem is accepted only if it can be proved on the basis of intuitionist logic: to prove, for example, that α holds it is not enough to show that ¬α leads to contradiction. In this sense intuitionist logic is a challenger for Boolean logic. In contrast, in mathematical fuzzy logic that has been developed as a formal system e.g. in [5], [11] and [17], the meta logic is Boolean logic. To our knowledge there is no approach to fuzzy logic where the situation would be different. The point of view in this reviewing paper is that of mathematicians’.

The idea of belief revision is strictly connected with such notions as revision and contraction given by two sets of postulates formulated by Alchourron, Gardenfors and Makinson in (Theoria, 48: 14–17, 1982; Journal of Symbolic Logic, 50: 510–530, 1985; Philosophical Essays Dedicated to Lennard Aqvist on His Fiftieth Birthday, pp. 88–101, 1982). In the paper expansion, contraction and revision are defined probably in the most orthodox way, i.e. by Tarski’s consequence operation (e.g. Compt. Rend. Seances Soc. Sci. Lett. Varsovie, cl.III, 23, 22–29) and Tarski-like elimination operation (see Łukowski, P., Logic and Logical Philosophy, 10: 59–78, 2002). In our approach nonmonotonicity appears as a final result of alternate using of two steps of our reasoning: “step forward” and “step backward”. Step forward extends the set of our beliefs and it is used when some new belief appears. Step backward reduces the set of our beliefs and it is used when we reject some previously accepted belief. A decision of adding or rejecting of some sentences is arbitrary and depends on our wish only. Thus, this decision cannot be logical and logic cannot justify it. In our approach logic is a tool for faultless and precise realization of extension or reduction of the set of our beliefs. But why some sentences should be added or refused depends on extralogical reasons. Such understood nonmonotonicity can be considered also on logics other than classical. A reconstruction of a given logic in its deductive-reductive form is here the basis of nonmonotonicity. It means that nonmonotonic reasoning can be formalized on the base of every logic for which its deductive-reductive form can be reconstructed. Firstly our approach is tested on the ground of the classical logic. Next it is confronted with the intuitionism represented by the Heyting-Brouwer logic. Procedures of contraction and revision are verified by using of the AGM postulates. We limit our considerations to first six conditions for contraction and revision, because of the well known relation between contraction satisfying first four conditions together with the sixth one and revision defined by this contraction and consequence operation. Satisfaction of almost every postulate is for us a good sign that our approach is reasonable. The only exception we make for the fifth postulate and for Harper identity. Analyzing the reasoning alternately extending and contracting the set of beliefs it is difficult to accept the postulate that adding previously rejected sentence we obtain again the same set of beliefs as before the contraction. This problem is deeper considered in the paper. The original AGM settles the relations between contraction and revision with, the well known Levi and Harper identities. In all cases of our approach, revision is defined on the basis of contraction which with respect to revision is prime.