Background
Heyting, Arend was born on May 9, 1898 in Amsterdam.
Heyting, Arend was born on May 9, 1898 in Amsterdam.
University of Amsterdam.
He was a student of Luitzen Egbertus January Brouwer at the University of Amsterdam, and did much to put intuitionistic logic on a footing where it could become part of mathematical logic. Heyting gave the first formal development of intuitionistic logic in order to codify Brouwer"s way of doing mathematics. The inclusion of Brouwer"s name in the Brouwer–Heyting–Kolmogorov interpretation is largely honorific, as Brouwer was opposed in principle to the formalisation of certain intuitionistic principles (and went as far as calling Heyting"s work a "sterile exercise").
Heyting was born in Amsterdam, Netherlands, and died in Lugano, Switzerland.
1. 160–173 Studies in Logic and the Foundations of Mathematics V. Noordhoff North.V., Groningen. Second revised edition
Heyting embraces an intuitionistic philosophy of mathematics. However, in several important respects his philosophy ditiers from that of L. E. J. Brouwer, the father of modern mathematical cmpricism. As regards foundations for mathematics Heyting rejects the naive intuitionism of Brouwer, acknowledging that certainty in human thinking is impossible and maybe a meaningless aim. Between 1930 and 1960, while continuing to subscribe to the doctrine of self-evidence, he became convinced that it had "proved not to be intuitively clear what is intuitively clear to mathematics’ and developed the view that intuitionists should accept a ‘descending scale of grades of evidence’, beginning with assertions such as "2+2=4' which are reports of direct mental constructions. Such a view faces formidable difficulties in connection with the idea of mental objects whose natures are transparent to us through inspection, difficulties which have been investigated in the later philosophy of Wittgenstein. It is doubtful whether any psychological and subjective doctrine can provide an epistemological justification for mathematics. Heyting was to move away from the radical subjectivism and anti-language stance of Brouwer with his attempt in 1930 at a symbolic formulation of the logical principles of intuitionist propositional logic, and in Intuitionism (1966) he provides an account of mathematics and logic which does not start from a philosophical foundation. However, the reader is warned that public and symbolic expression of the content is inadequate. One can only learn what intuitionist mathematics is by practising it, for the symbolic account can only be understood by repeating the mental processes recorded in it. However, Heyting is more sympathetic to the acitivity of expressing intuitionist mathematics symbolically than was Brouwer. He sees symbolization as a support for memory as well as for communication and as essential for understanding between mathematicians. So in Heyting's writing there is increasing acknowledgement of a necessary social dimension in an adequate account of mathematical activity. In his explanation of the foundations of mathematics Brouwer rejected the logicism of Russell and W'hitehead. that mathematics is based on logic, and claimed that logic is based on mathematics. This implies that the steps of a logical proof are intuitively clear mental acts according to intuitionism rather than symbolic applications of previously laid down and publicly available logical laws. While accepting this philosophical position Heyting nevertheless developed an intuitionistic logic for which he provided an interpretation. The calculus employs four primitive constants A, V, which are independent of each other, and lower-case Latin letters are used for propositional variables. The following eleven axioms are accepted: Rules of derivation are the same as in the classical propositional calculus. From these it is not possible to derive part of the principle of Double Negation, ——> a, nor is the Law of Excluded Middle a theorem of the system. Due to the restriction on Double Negation indirect proot is not available in intuitionistic logic. When extended to the calculus of predicates appropriate limitations are placed on quantifiers; the existential quantifier in, e.g., conveys more information than the use of the universal quantifier in a formula regarded as equivalent in classical predicate logic, namely, —>(.xr)—>/>(.v). The use of the former is only allowed when an object with the property P has actually been constructed while the use of the latter depends only on the condition that we deduce a contradiction from some particular supposition. The above calculus admits of various interpretations and in particular has been interpreted by Heyting as a calculus of intended constructions. So understood a theorem expresses the fact that one has succeeded in making a construction. This is expressed in the so-called Principle ot Positivity, which requires that every mathematical or logical theorem must express the result of a mathematical construction. For comparison. a classical theorem expresses the fact that a proposition is true. Accordingly Heyting contrasts intuitionist and classical logic as the logics of knowledge and truth respectively. He thereby, as indicated in our remarks on language, takes philosophy of mathematics to the heart ot an ongoing debate of general philosophical interest concerning the logical relationships between the concepts of truth and meaning.
Royal Netherlands Academy of Arts and Sciences.