| This is a file in the archives of the Stanford Encyclopedia of Philosophy. |
|
how to cite |
Stanford Encyclopedia of Philosophy |
content revised
|
Philosophically, intuitionism differs from logicism by treating logic as a part of mathematics rather than as the foundation of mathematics; from finitism by allowing (constructive) reasoning about infinite collections; and from platonism by viewing mathematical objects as mental constructs with no independent ideal existence. Hilbert's formalist program, to justify classical mathematics by reducing it to a formal system whose consistency should be established by finitistic (hence constructive) means, was the most powerful contemporary rival to Brouwer's developing intuitionism. In his 1912 essay Intuitionism and Formalism Brouwer correctly predicted that any attempt to prove the consistency of complete induction on the natural numbers would lead to a vicious circle.
Brouwer rejected formalism per se but admitted the potential usefulness of formulating general logical principles expressing intuitionistically correct constructions, such as modus ponens. Formal systems for intuitionistic propositional and predicate logic were developed by Heyting [1930], Gentzen [1935] and Kleene [1952]. The Gödel-Gentzen negative translation interpreted classical predicate logic in its intuitionistic subsystem. In [1965] Kripke provided a semantics with respect to which intuitionistic predicate logic is correct and complete.
A),
but with the law of contradiction
(A 
(A B)).
Brouwer [1908] observed that LEM was abstracted from finite
situations, then extended without justification to statements about
infinite collections. For example, if x, y range over the natural
numbers 0, 1, 2, ... and B(x) abbreviates the property (there is a y
> x such that both y and y+2 are prime numbers), then we have no
general method for deciding whether B(x) is true or false for
arbitrary x, so
x(B(x)
B(x))
cannot be asserted in the present state of our knowledge. And if A
abbreviates the statement
xB(x), then
(A A)
cannot be asserted because neither A nor
(A) has yet been proved.
One may object that these examples depend on the fact that the Twin Primes Conjecture has not yet been settled. A number of Brouwer's original "counterexamples" depended on problems (such as Fermat's Last Theorem) which have since been solved. But to Brouwer the general LEM was equivalent to the a priori assumption that every mathematical problem has a solution -- an assumption he rejected, anticipating Gödel's incompleteness theorem by a quarter of a century.
, , ,
, 
.
This contrasts with the classical situation, where e.g.,
(A B) is equivalent to
(A & B),
and
xA(x) is equivalent to
xA(x).
From the B-H-K viewpoint, a sentence of the form
(A B)
asserts that either a proof of A, or a proof of B, has been
constructed; while
(A & B)
asserts that an algorithm has been constructed which would
effectively convert any pair of constructions proving
A and B
respectively, into a proof of a known contradiction.
Following is a Hilbert-style formalism, from Kleene [1952], for
intuitionistic first-order predicate logic. The language L
has predicate letters P, Q(.),... of all arities and individual
variables a,b,c,... (with or without subscripts 1,2,...), as well as
symbols &, , ,
, ,
for the logical connectives and quantifiers, and parentheses (, ).
We use A, B, C as metavariables for well-formed formulas and x,y,z as
metavariables for individual variables. Anticipating applications
(for example to intuitionistic arithmetic) we use s,t as
metavariables for terms; in the case of pure predicate logic,
terms are simply individual variables.
There are three rules of inference:
B), conclude B.
A(x)),
where x is a variable which does not occur free in C, conclude
(C xA(x)).
C),
where x is a variable which does not occur free in C, conclude
(xA(x) C).
(B A).
B)
((A (B C))
(A C)).
(B A & B).
A.
B.
A B.
A B.
C)
((B C)
(A B C)).
B)
((A B)
A).
A (A B).
xA(x) A(t).
xA(x).
Intuitionistic propositional logic is the subtheory which results
when the language is restricted to formulas built from proposition
letters P, Q, R,... using the propositional connectives &,
, and ,
and only the propositional postulates are used. Thus the last two
rules of inference and the last two axiom schemas are absent from the
propositional theory.
If, in the given list of axiom schemas for intuitionistic propositional or first-order predicate logic, the law of contradiction:
is replaced by the law of double negation:
(or,equivalently, by LEM), a formal system for classical propositional or first-order predicate logic results. Since the law of contradiction is a classical theorem, intuitionistic logic is contained in classical logic.
While the Hilbert-style system H is useful for metamathematical investigations of intuitionistic logic, its forced linearization of deductions and its preference for axioms over rules make it an awkward instrument for establishing derivability. A natural deduction system I for intuitionistic predicate logic (with identity) results from the deductive system D, presented in Section 3 of the entry on Classical Logic in this Encyclopedia, by replacing the classical rule (DNE) of double negation elimination by the intuitionistic negation elimination rule
The reader may also wish to consult Section 2 (on Language) of the same entry, which applies mutatis mutandum to the language L of H and I. The Deduction Theorem and its converse, stated in the next section, are the keys to the equivalence of H with (the identity-free part of) I,(INE) If F entails A and F entails
B) is provable. The converse
of this theorem holds simply by the first rule of inference.
The Gödel-Gentzen negative translation associates with each
formula A of the language L a formula g(A) with no
or ,
which is equivalent to A in classical predicate logic. We define
g(A) by induction on the logical form of A, as follows:
P,
if P is prime.
B) is
(g(A)
& g(B)).
B) is
(g(A) g(B)).
A) is g(A).
xA(x)) is
x g(A(x)).
xA(x)) is
xg(A(x)).
B)
were classically provable for some formula B, then
(g(B) & g(B))
(which is g(B & B)) would in turn be
provable intuitionistically. Gödel [1933] interpreted these
results as showing that intuitionistic logic is richer than
classical logic, because
Gödel [1932] observed that intuitionistic propositional logic
has the disjunction property: If
(A B)
is a theorem, then A is a theorem or B is a theorem. Gentzen [1935]
established the disjunction property for closed formulas of
intuitionistic predicate logic. From this
it follows that if intuitionistic logic is consistent, then
(P P)
is not a theorem if P is prime. Kleene [1945, 1952] proved that
intuitionistic first-order number theory also has the related (cf.,
Friedman [1975]) existence property: If
xA(x)
is a closed theorem, then for some closed term t, A(t) is a theorem.
Kleene, Friedman and Troelstra also proved existence properties for second-order
intuitionistic systems.
The disjunction and existence properties are special cases of a
general phenomenon peculiar to nonclassical theories. The
admissible rules of a theory are the rules under which the
theory is closed. In classical propositional logic, if (A is
provable) implies (B is provable), then (A B) is
provable; thus every classically admissible rule is classically
derivable. Intuitionistically the situation is more interesting.
Harrop [1960] observed that intuitionistic propositional logic is
closed under the rule
(A
(B C)) /
(A B)
(A C),
while the corresponding implication is not provable
intuitionistically. In [2001] Iemhoff succeeded in proving a
conjecture of de Jongh and Visser, which provides a recursively
enumerable basis for the admissible rules of intuitionistic
propositional logic; Visser [2002] has shown that these are also the
admissible propositional rules of intuitionistic arithmetic, and of
intuitionistic arithmetic extended by Markov's Principle (see the
article on Constructive Mathematics in this Encyclopedia).
A Kripke structure K consists of a partially ordered
set K of nodes and a domain function D assigning
to each node k in K an inhabited set D(k)
of constructive objects, such that if
k 
k
,
then
D(k)
D(k).
In addition K has a forcing relation determined as
follows.
For each node k let L(k) be the language
extending L by new constants for all the elements of
D(k). To each node k and each prime predicate
P(x) assign a (possibly empty) subset T(P,k) of
D(k) in such a way that if
k k
then
T(P,k)
T(P,k),
and similarly for predicates of more variables. Say that k
forces P(d) if and only if
d 
T(P,k).
Now define forcing for compound sentences of L(k) by
B) if k forces A or
k forces B.
B) if, for every
k 
k,
if k forces A then
k forces B.
A if for no
k k does
k force A.
xA(x) if for every
k k and every
d D(k),
k forces A(d).
xA(x) if for
some d D(k),
k forces A(d).
A.
k and
k forces A
then k forces A.
xP(x)
xP(x))
is intuitionistically unprovable, it is enough to consider a Kripke
structure with K = {k,
k}, k <
k,
D(k) =
D(k) = {0},
T(P,k) empty but
T(P,k) = {0}.
Troelstra's [1973], Beeson's [1985] and Troelstra and van Dalen's [1988] are comprehensive studies of intuitionistic and semi-intutionistic theories, using both constructive and classical methods. Troelstra's [1998] presents formulas-as-types and (Kleene and Aczel) slash interpretations for propositional and predicate logic, as well as abstract and concrete realizability interpretations for a multitude of intuitionistic theories. Veldman's [1990] treats descriptive set theory from a strictly intuitionistic viewpoint. Martin-Löf's intuitionistic theory of types [1984] provides a general framework within which intuitionistic reasoning continues to develop.
First published: September 1, 1999
Content last modified: December 20, 2002
Table of Contents