INTUITIONISM AND INTUITIONISTIC LOGIC

Logic, in the modern preponderantly mathematical sense, deals with concepts like truth and consequence. The main task of logic is to discover the properties of these concepts. Ever since Aristotle it had been assumed that there is one ultimate logic for the case of descriptive statements, which lent logic a sort of immutable, eternal appearance. Only in the beginning of the twentieth century were certain principles of traditional logic submitted to a critical revision. It was L. E. J. Brouwer, who, in a radical constructive framework of mathematics, discovered that traditional logic could not be upheld in its full extent.

This entry sketches the basic ideas of Brouwer's constructivism, which goes by the name of intuitionism, and then discusses the fundamental principles. Next, an exposition of the familiar notions, such as proof system, semantics, and the like, is provided. In particular, this entry will show how the Brouwerian mathematical universe takes a special place in terms of its logical properties.

Intuitionistic Truth

For all practical purposes it suffices to consider in mathematical logic only a few logical constants, or connectives. The traditional conjunction (and, ∧), disjunction (or, ∨, and not, ¬), and implication (if …, then … , →) will do for propositional logic. By adding the two quantifiers, the universal quantifier (for all, ∀) and the existential quantifier (there is, ∃), one gets the required connectives for predicate logic. The notion of intuitionistic truth is laid down for composite statements by an inductive procedure. Hence, one has to start by explaining the truth of the basic statements, the so-called atomic ones.

In intuitionism the objects and relations of mathematics are mental creations of the individual, called subject here. And logic has its domain of action in the self-constructed universe. The fundamental construction is that of the natural numbers. The move of time causes the subject to experience a sensation, which is succeeded by another sensation, while the first one is stored in memory. Brouwer called this the ur-intuition. Through a process of abstraction (identification of experienced two-ities), the empty two-ity, that is, the number 2 is obtained. A process of iteration then yields the natural numbers, and reflection on the process yields the principle of complete induction. Now, one can establish simple identities like 2 + 3 = 5. This is done by a construction of the following kind: (1) construct 2, (2) construct 3, (3) construct the sum of 2 and 3, (4) construct 5, (5) carry out the comparison construction for the outcome of (3) and (4). The success of (5) tells one that "2 + 3 = 5." The basic statements are thus verified, or proved, by constructions. One can denote "the construction a proves φ" by "a :φ." It is easy to see how a conjunction is proved; one has a proof of φ∧ψ if one has a proof of φ and a proof of ψ. So the proof of φ∧ψ is an ordered pair (a, b ), such that a :φ and b :ψ.

The disjunction is slightly more problematic; φ∨ψ is a statement that contains two possibilities φ and ψ, and at least one of these is to be the case. Constructively, one wants therefore to select one of the two and provide a proof for it. We put this as (a, b ):φ∨ψ if a = 0 and b :φ, or a = 1 and b :ψ. So a distinguishes between φ and ψ and b is the required proof. The classical notion of disjunction (the word classical is used here for "nonintuitionistic") is more liberal, something like "it is φ or ψ but I don't know which." This notion is not constructively acceptable. The implication is by far the most interesting; p is a proof of φ→ψ means that p is an operation that carries proofs into proofs such that for a proof a of φ, p (a ) is a proof of ψ. In symbols: p : φ → ψ ⇔ for any a a :φ ⇒ p (a):ψ. This notion is in fact the natural interpretation of implication. The interpretation of negation has also to be rendered constructively, that is, we have to explain what a :¬φ means, a mere "not" will not do. Brouwer's solution was: ¬φ is true if φ can be reduced to a contradiction (absurdity); in terms of constructions: p :¬φ if for any proof a :φ, p (a ):┴, where ┴ stands for a contradiction. That is, ┴ is a statement that has no proof. As a consequence, φ cannot have a proof. In Brouwer's conception the paradigm of a contradiction is 0 = 1.

For the quantifiers, one has the following proof clauses, where one considers some fixed domains D of objects d :
a :∀x φ(x ) if for each d ∈ D a (d ):φ(d ).
(a, b ):∃x φ(x ) if b :φ(a ).

The constructive character of existence is thus made explicit in the sense that the proof contains a witness a and a proof of φ(a ).

The above proof interpretation defines truth as "having a proof," where a proof is a construction of an open-ended, unspecified nature. Hence, there is no preferred class of constructions specified—one recognizes a construction when one sees one. The precise form was published by Arend Heyting in 1934, and a similar interpretation was provided by Kolmogorov in his "problem-interpretation" (1932). In an informal manner the proof interpretation was conceived and used by Brouwer. He demonstrated the use of the interpretation, for example, in his proof of the historically first theorem of intuitionistic logic: ¬φ ↔ ¬¬¬φ. On the proof interpretation the principle of the excluded middle (PEM), φ∨¬φ, is not always provable (i.e., true). For it would demand that one can give for each proposition φ in advance either a proof of φ, or a construction that reduces any proof of φ into a proof of ⟂. This is not a matter of abstract logic, but a matter of a general superalgorithm that decides any φ, a so-called omniscience principle. Hence, on the proof interpretation, PEM is equivalent to Hilbert's dogma, which states that all mathematical problems are solvable (1900). However, on the same interpretation, there are no absolutely unsolvable problems, for if φ∨¬φ has no proof, φ cannot have a proof, and this is equivalent to "¬φ has a proof." So in this respect, David Hilbert was right, "there is no ignorabimus."

Formal Systems

The first formalization of (a fragment of) intuitionistic logic was presented by Kolmogorov (1925), and Heyting followed in 1930 with a full system. Both used Hilbert-type formalizations. The axioms were chosen in such a way that the classical system is obtained by adding just one extra axiom (schema): the principle of the excluded middle. The following is an axiom system:

There are three derivation rules:
From φ and φ→ψ derive ψ, in symbols φ, φ→ψ / ψ (modus ponens); σ→φ(x ) / σ→∀x φ(x ); φ(x )→σ / ∃x φ(x )→σ.

An alternative formalization was presented by Gerhard Gentzen (1909–1945); his system of natural deduction differed from the Hilbert-type formalization in having no axioms and only rules. The rules are particularly perspicuous, in the sense that they tell one how to introduce a connective and how to eliminate it. In other words, what one has to assume to conclude a composite statement, and what are the consequences of a composite statement. For example, from φ and ψ infer φ∧ψ; from φ∧ψ infer φ and likewise ψ. In Gentzen's notation:

Thus, the rules appear in the form of introduction rules and elimination rules. Some rules are purely local in the sense that they only concern the immediate premises and the consequence, and some are more complicated in that they concern the whole history of the derivation. The remaining rules can be found in the literature.

The Gentzen rules can be viewed as a means of providing the meaning of the connectives. This was the underlying idea of Per Martin-Löf's (1984) type theory, and it also played a role in Michael A. E. Dummett's (2000) meaning theory.

A question of immediate interest concerns the relation between intuitionistic and classical logic. The first is a subsystem of the second, that is, every intuitionistic theorem is a classical one. There is also a natural way of interpreting classical logic in intuitionistic logic. Kolmogorov (1925), Kurt Gödel (1934) and Gentzen (1934) translated classical logic so that derivability was preserved. If one denotes classical derivability by ├_c and intuitionistic derivability by ├, then Γ ├_c φ ⇔ Γ^o ├φ^o where φ^o is the translation of φ. One can see here the Gödel translation:

The translation clearly indicates from an intuitionistic point of view a weakening of the meaning of the connectives. The translation also works for concrete theories, for example, arithmetic. Let PA be the standard formalization of Peano's arithmetic, and HA the same for Heyting's arithmetic, where PA = HA + PEM. Now PA ⊦_c A ⇔ HA ⊦ A^o. This immediately shows that PA and HA are equally consistent. Historically, this came as a surprise. HA was supposed to be more consistent on the ground of its constructive nature. Translations, such as Gödel's, can also be carried out for certain higher order systems.

Gödel (1934) also observed that the extra strength of intuitionistic logic (from a constructive point of view) had an implicit modal character. He translated propositional logic into a modal logic, where □φ had the heuristic meaning "I know φ" or "I have established φ." The translation is given by:

Intuitionistic logic thus translates into modal logic, and derivability is preserved in the sense that ⊦ φ ⇒ S4 ⊦ φψ)^m. Gödel's idea was recently adopted and vigorously extended by Artemov (2002), who combined the proof interpretation and the modal interpretation for arithmetic and extensions.

There are many classically derivable propositions that are not derivable in intuitionistic logic, the best known being PEM and the double negation principle ¬¬φ→φ. The latter obviously follows from the first, but conversely the schema ¬¬φ→φ implies the schema φ∨¬φ (Bernays). One simply applies the double negation principle to φ∨¬φ (and uses some intuitionistic logic).

It is convenient to remember the following rule: ∃ and ∨ are strong connectives. So, as to be expected, for example, ¬(φ∧ψ)→(¬φ∨¬ψ), (φ→ψ)→(¬φ∨ψ), ¬∀x φ(x )→∃x ¬φ(x ), ∀x (φ∨ψ(x ))→(φ∨∀x ψ(x )) are not derivable.

In an obvious way intuitionistic logic is weaker than classical logic, that is to say, as a subsystem. However, it is stronger on the ground of certain metalogical properties. For example, if ├φ∨ψ, then ├φ or ├ψ (disjunction property). This testifies to the strength of the disjunction in intuitionistic logic. Similarly, one has ├∃x φ(x ) ⇒ ├φ(c ) for a constant c (in a language without function symbols) (existence property).

Semantics

Where classical logic basically has one natural semantics, the truth table semantics of true, false, intuitionistic logic has many semantics, each with its specific features. The intended intuitionistic semantics is the proof interpretation, but for model theoretic applications it is rather too open ended. There are semantic interpretations of intuitionistic logic that have the flexibility one needs for uncovering logical properties. There are roughly two classes of semantics: those based on (classical) set theory and those of an algorithmic nature. The set-theoretical ones will be considered first.

the topological interpretation (tarski)

In classical logic one can interpret propositional logic by means of Venn diagrams (or rather interpret monadic logic), that is, one assigns subsets of a set to propositions and interprets ∧, ∨, ¬ as ∩, ∪, ^c. The topological interpretation refines this by considering open sets in a topological space and reinterpreting ¬ by the interior of the complement (where the interior of a set is the largest open subset of that set). More precisely, given a topological space X and a domain D, assign an open set [[φ] in X to each atom φ (and ∅ to ┴) then

Under this interpretation one obtains completeness:
⊦φ ⇔ [[φ] = X for all topological spaces X.

Brouwer's theorem, ¬¬¬φ→¬φ, is topologically explained by the fact that the interior of the interior is the interior (also "the closure of the closure if the closure"). One can easily see that φ∨¬φ and ¬¬φ→φ are not valid, and hence not derivable: consider the real line R and put φ = R−{0}, then [[¬φ] = ∅ and [[¬¬φ] = R.

heyting valued interpretations (tarski and mckinsey)

Classical propositional logic, from an algebraic point of view, is a Boolean algebra if one identifies provably equivalent propositions. A similar fact holds for intuitionistic logic, only the algebra fails to be Boolean, for in general φ ↔ ¬¬φ is not valid. The algebras for intuitionistic logic are called Heyting algebras. Since Heyting (and Boolean) algebras have a partial ordering (given by [[φ] ≤ [[ψ] ⇒ ⊦φ→ψ) with suitable properties, they turn out to be lattices. The algebraic and lattice theoretic approach are closely related. Jaskowski (1936), in his pioneering work, constructed certain lattices that in a specific sense capture intuitionistic propositional logic. The applications of Heyting algebras and Heyting valued models can be found in Peter T. Johnstone's book, Stone Spaces (1982).

beth and kripke models

Where the previous interpretations are more technical than foundational in character, Beth and Saul Kripke formulated in the 1950s and 1960s interpretations that intended to do justice to Brouwer's philosophical motivations, in particular his conception of mathematics, and thus logic, as a creation of the subject. Beth introduced his models in 1956 and Kripke in 1963. Kripke showed how the two interpretations are in a precise sense equivalent. The underlying idea is to take the notions "the subject knows (or 'has established') φ at time t " seriously. So Beth and Kripke consider stages of research (or knowledge) in time for the subject. These states are partially ordered, as the subject has at each stage a number of options of how to pursue his or her research further. The subject is assumed to have perfect memory, so what is known at a certain stage is preserved in future stages. The subject directly becomes aware of and establishes basic facts, so at each stage k a number of atomic statements are accepted; one can denote "φ is known at stage k " by k ‖− φ, and we can say "φ is forced at stage k." The interpretation for composite statements is defined inductively. Some decisions are made on the spot, for example, φ ∧ ψ is forced at k if both φ and ψ are forced at k ; some, however, involve the future. The paradigmatic case is the implication: φ → ψ may be accepted as correct although no information is available about the correctness of φ and ψ. Here is a Brouwerian example: Let φ stand for "there are 100 consecutive zeros in the decimal expansion of π," and ψ for "there are 99 such decimals." Obviously φ → ψ is correct, even for an intuitionist. So what does k ‖− φ→ψ mean? The natural solution is: If at a future stage k ′ one has k ′ ‖− φ, then k ′ ‖− ψ. In fact, this is the natural interpretation of implication, which is only obscured by the truth table definition.

The universal quantifier also involves the future. The subject not only establishes atomic facts but also constructs objects of the domain. So at a later stage, in general, more objects will be available (exist) than at an earlier one. So the universal quantifier has also to take future elements into account; one can denote the domain at stage k by D (k ). One can now give Kripke's definition of ‖−:
k ‖− φ∧ψ ⇔ k ‖− φ and k ‖−ψ; k ‖− φ∨ψ ⇔ k ‖− φ or k ‖− ψ; k ‖− φ → ψ ⇔ ∀ k ′≥k (k ′ ‖−φ ⇒ k ′ ‖−ψ); k ‖−∃x φ(x )⇔∃d ∈D (k )(k ‖−φ(d )); k ‖− ∀x φ(x )⇔∀ k ′≥k ∀d ∈D (k ′)( k ′ ‖− φ(d )).

Furthermore ┴ is never forced. So for negation one has k ‖−¬φ ⇔ ∀ k ′≥k not k ′ ‖−φ. This semantics is sound, and even complete for intuitionistic logic. A particular partially ordered set with prescribed forcing for atoms, and a given domain assignment D (k ) for all k, is called a Kripke model. It is a simple exercise to construct countermodels for nonderivable statements. For example, the model with two stages, k _o and k ₁, such that k_o < k₁ and k_o forces no atoms, and
k ₁ ‖− φ, has the property that not k _o ‖−φ∨¬φ.

The completeness theorem (Kripke 1963) states that
┴φ ⇔ for all Kripke models K and all stages k ∈ K k ‖− φ.

For propositional intuitionistic logic it even suffices to consider only finite Kripke models. In that case the so-called finite model property holds: if not├ φ, then there is a finite Kripke model that refutes φ.

Kripke models have been extensively used in metalogical research. Unfortunately, the proofs of the completeness theorem use a classical metatheory and are based on PEM. Hence, not all the applications of Kripke semantics are intuitionistically correct. W. Veldman (1976) generalized the notion of the Kripke model, so that the use of PEM can be avoided.

Beth models are similar to Kripke models, be it that the clauses rely strongly on the future. For example, φv ψ is forced at stage k if any (infinite) sequence of future stages k ≤ k _o ≤ k ₁ ≤ … eventually leads to a stage in which φ or ψ is forced.

Beth models are less flexible than Kripke models, but they have their advantages for metalogical applications and for modeling second-order theories.

algorithmic interpretations

In 1945 Stephen Cole Kleene introduced an algorithmic interpretation of intuitionistic arithmetic called realizability. One may think of the constructions in the proof interpretation as partial recursive functions, so that the proof evidence can be given as the index n of such a function. We can say that "n realizes φ" (n r φ). For closed atoms the correctness can immediately be verified, so one defines n r t ₁ = t ₂ if t ₁ = t ₂ is true. The interesting case is, again, the implication: n r φ→σ if ∀m (m r φ ⇒{n }m r σ), where {n }m is assumed to converge. The class of all realizable sentences is a theory that extends HA ; it is axiomatized by some natural axioms. The interesting and surprising fact is that Church's thesis, CT₀ ∀x ∃y φ(x,y ) → ∃e ∀x φ(x {e }x ), is realized. Church's thesis claims that all algorithms (on natural numbers) are recursive functions. Hence, in this extended arithmetic (which is inconsistent with PA) all functions are given by Turing machines.

Gödel introduced an interpretation of arithmetic by means of (effective) functionals of higher types, the so-called Dialectica interpretation (1958). Another such interpretation was introduced by Georg Kreisel (b. 1923): modified realizability. For a survey of the previously discussed text and more, see the bibliography.

Second-Order Systems

On Brouwer's view, there are two basic kind of objects, given by the first and second act of intuitionism. The first act gives one the discrete objects, and the second infinite sequences. These sequences, say of natural numbers, need not be given by a law; they are chosen more or less arbitrarily by the subject, hence the name choice sequences. The codification takes place in second-order logic with variables for natural numbers x, y, z, … and variables for infinite sequences of natural numbers, α, β, γ, … (see Troelstra and Dalen 1988). There are a number of systems treating this intuitionistic analysis. Besides the obvious axioms they usually contain an axiom of countable choice, ∀x ∃y φ(x,y ) → ∃α∀x φ(x, α(x )), and continuity axioms of various strengths. The motivation for the continuity principle that comes to mind first runs as follows: suppose one has a function F from choice sequences to natural numbers; since the output has to be computed in a finite time, only a finite part of the input choice function α can be used. Hence F is a continuous function from Baire space to N. This argument is an oversimplification (see Atten and Dalen 2002). A formulation of the (weak) principle of continuity, WC, runs as follows: ∀α∃x φ(α,x ) → ∀α∃xy ∀β [α(0)=β(0)∧ … ∧ α(y −1) = β(y −1) → φ(β,x )]. For functions F one gets the ∀∃! prefix.

This continuity principle evidently fails for the following φ(α,x ): [∀z (α(z )=0∧x =0) ∨∃z (α(z )>0∧x =1)]. Hence, intuitionistic systems with continuity principles are inconsistent with PEM. Furthermore, Brouwer introduced a certain principle of transfinite induction, the principle of bar induction, which lends the system a considerable proof theoretic strength (enough to prove consistency of HA and PA ). A corollary is the so-called fan theorem, which basically says that the intuitionistic Cantor space is compact. A consequence of the fan theorem is the following: "every real function on a closed interval is uniformly continuous" (Brouwer 1975–1976); Brouwer also showed that the continuum is indecomposable, that is, R cannot be split into two nonempty parts.

In the 1920s Brouwer started to exploit the idealized choice activity of the subject. This was formalized and further analyzed by Kreisel, Kripke, and John Myhill in the 1960s. Kreisel laid down axioms for the theory of the creating subject in a kind of modal formulation. Let □_n φ stand for "the subject knows (has evidence for) φ at time n." The axioms are □_n φ→□_n+m φ; □_n φ ∨ ¬□_n φ; ∃x □_x φ↔φ.

Kripke simplified the theory by condensing the total action of the creating subject in one schema, ∃α(φ↔∃(α(x ) ≠ 0)), Kripke's schema (KS). This schema allowed a formal reconstruction of Brouwer's later results. A recent application of KS showed that, for example, the set of irrationals is indecomposable.

Of course, there is also a second-order arithmetic with set variables, HAS. In general, sets are less palpable then functions. In constructive mathematics one cannot reduce sets to characteristic functions, since only decidable sets have characteristic functions.

Metamathematical Aspects

There are striking similarities between function spaces and logic, which were first observed by Haskell Curry (1900–1982), who indicated the relation between certain combinators and propositional axioms. In the Curry-Howard isomorphism, this is extended to full logic. The present typed lambda calculus is based on these ideas. Henk Barendregt (b. 1947) systematized the various logical- and typed λ-calculus systems and arranged them in Barendregt's cube. Martin-Löf had already in the early 1970s introduced type systems that treat in a uniform way intuitionistic logic and higher-order type systems. These systems yield a most perspicuous presentation of mathematics in a constructive setting and also allow a thorough proof theoretical analysis. It may be remarked that in Martin-Löf's systems (suitable forms of) the axiom of choice became provable, thus confirming the strength of a constructive approach to mathematics. The type theoretic approach to mathematics has born fruit in computer science; there are, for example, implementations of type theory that allow automatic theorem proving. Nicolaas Govert de Bruijn (b. 1918) was the first to develop modern type systems in his AUTOMATH system.

The various semantics that were introduced over the years have found a generalized formulation in category theory. There is a special class of categories, called toposes, that in a most flexible way yields the existing older semantics. A topos can be viewed as a higher-order intuitionistic universe. Hyland (1982) introduced the effective topos, in which Church's thesis holds. Thus nowadays there are many models of all kinds of constructive universes around that allow metamathematical analysis. In particular, there are generalizations of the topological interpretation, the so-called sheaf interpretations, that perfectly model intuitionistic analysis and topology.

One particular line of research by McCarthy shows that in a universe with Church's thesis, intuitionistic truth (for predicate logic) is not arithmetical (hence, the logic is incomplete), and moreover that HA has up to isomorphism, only the standard models. This extends earlier work by Kreisel and refines insights into incompleteness of intuitionistic logic.

A great deal of metamathematical research deals with basic principles, such as transfinite inductions, axioms of choice, and continuity principles. Some of these principles are far from neutral with respect to logic, for example, the full axiom of choice implies PEM.

See also Brouwer, Luitzen Egbertus Jan; Logic, Non-Classical; Mathematics, Foundations of.

Bibliography

Atten, Mark van. On Brouwer. Belmont, CA: Wadsworth, 2004.

Atten, Mark van, and Dirk van Dalen. "Arguments for the Continuity Principle." Bulletin of Symbolic Logic 8 (3) (2002): 329–347.

Brouwer, L. E. J. Collected Works. Vol. 2, edited by A. Heyting. Amsterdam, Netherlands: North-Holland, 1975.

Buss, Samuel R. Handbook of Proof Theory. New York: Elsevier, 1998.

Dalen, Dirk van. "From Brouwerian Counter Examples to the Creating Subject." Studia Logica 62 (2) (1999): 305–314.

Dalen, Dirk van. "Intuitionistic Logic." In Handbook of Philosophical Logic. Vol. 5. 2nd ed., edited by D. M. Gabbay and F. Guenthner, 1–114. Dordrecht, Netherlands: Kluwer Academic, 2002.

Dalen, Dirk van. Logic and Structure. 4th ed. Berlin. Springer-Verlag, 2004.

Dalen, Dirk van. Mystic, Geometer, and Intuitionist: The Life of L. E. J. Brouwer. Vols. 1 and 2. New York: Oxford University Press, 1999, 2005.

Dalen, Dirk van, and M. van Atten. "Intuitionism." In A Companion to Philosophical Logic, edited by Dale Jacquette, 513–530. Malden, MA: Blackwell, 2002.

Dragalin, A. G. Mathematical Intuitionism: Introduction to Proof Theory. Providence, RI: American Mathematical Society, 1988.

Dummett, Michael A. E. Elements of Intuitionism. 2nd ed. New York: Oxford University Press, 2000.

Heyting, A. Mathematische Grundlagenforschung: Intuitionismus, Beweistheorie Berlin: J. Springer, 1934.

Johnstone, Peter T. Stone Spaces. New York: Cambridge University Press, 1982.

Mancosu, Paolo. From Brouwer to Hilbert: The Debate on the Foundations of Mathematics in the 1920s. New York: Oxford University Press, 1998.

Martin-Löf, Per. Intuitionistic Type Theory. Naples, Italy: Bibliopolis, 1984.

Mints, Grigori. A Short Introduction to Intuitionistic Logic. New York: Kluwer Academic, 2000.

Rasiowa, Helena. The Mathematics of Metamathematics. Warsaw, Poland: Pánstowe Wydawnictwo Naukowe, 1963.

Troelstra, A. S., and D. van Dalen. Constructivism in Mathematics: An Introduction. 2 vols. Amsterdam, Netherlands: North-Holland, 1988.

Troelstra, A. S., and H. Schwichtenberg. Basic Proof Theory. New York: Cambridge University Press, 1996.

Van Heijenoort, Jean. From Frege to Gödel: A Source Book in Mathematical Logic, 1879–1931. Cambridge, MA: Harvard University Press, 1967.

Dirk van Dalen (2005)