Stanford Encyclopedia of Philosophy
A |
B |
C |
D |
E |
F |
G |
H |
I |
J |
K |
L |
M |
N |
O |
P |
Q |
R |
S |
T |
U |
V |
W |
X |
Y |
Z
Intuitionistic Logic
Intuitionistic logic encompasses the principles of logical reasoning
which were used by L. E. J. Brouwer in developing
his intuitionistic mathematics, beginning in [1907]. Because these
principles also underly Russian recursive analysis and the
constructive analysis of E. Bishop and his followers, intuitionistic
logic may be considered the logical basis of constructive
mathematics.
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 complete.
Intuitionistic logic can be succinctly described as classical logic
without the Aristotelian law of excluded middle LEM
(A 
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.
The Brouwer-Heyting-Kolmogorov explication of intuitionistic truth,
outlined in Section 1 ("The Basis of Constructive Mathematics") of
the article on Constructive Mathematics in this Encyclopedia, results
in the constructive independence of the logical operations &,
, ,
, 
.
This contrasts with the classical situation, where e.g.,
(A B) is equivalent to
(A & B),
and
xA(x) is equivalent to
xA(x).
Intuitionistically, 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, individual
variables, and symbols for the logical operations. We use A, B, C as
metavariables for well-formed formulas. There are three rules of
inference:
- From A and (A B), conclude B.
- From C and (C A(x)),
where x is a variable which does not occur free in C, conclude
(C xA(x)).
- From C and (A(x) C),
where x is a variable which does not occur free in C, conclude
(xA(x) C).
The axioms are all formulas of the following forms, where in the
last two schemas the subformula A(t) is the result of substituting an
occurrence of the term t for every free occurrence of x in A(x), and
no variable free in t becomes bound in A(t) as a result of the
substitution.
- A (B A).
- (A B)
((A (B C))
(A C)).
- A (B A & B).
- A & B A.
- A & B B.
- A A B.
- B A B.
- (A C)
((B C)
(A B C)).
- (A B)
((A B)
A).
- A (A B).
- xA(x) A(t).
- A(t) xA(x).
A proof is any sequence of formulas, each of which is an
axiom or an immediate consequence, by a rule of inference, of
preceding formulas of the sequence. Any proof is said to
prove its last formula, which is called a theorem or
provable formula of first-order intuitionistic predicate
logic.
If, in the given list of axiom schemas, the law of contradiction:
A (A B).
is replaced by the law of double negation:
A A.
(or, equivalently, by LEM), a formal system for classical
first-order predicate logic results. Since the law of contradiction
is a classical theorem, intuitionistic logic is contained in
classical logic.
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:
- g(P) is P,
if P is prime.
- g(A & B) is (g(A) & g(B)).
- g(A B) is
(g(A)
& g(B)).
- g(A B) is
(g(A) g(B)).
- g(A) is g(A).
- g(xA(x)) is
x g(A(x)).
- g(xA(x)) is
xg(A(x)).
For each formula A, g(A) is provable intuitionistically if
and only if A is provable classically. In particular, if
(B & 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
- intuitionistic logic distinguishes formulas which are
classically equivalent, and
- intuitionistic logic is equiconsistent with classical logic.
Gödel extended the negative translation to number theory, but
attempts to apply it to intuitionistic analysis failed because the
negative translation of the countable axiom of choice has no
intuitionistic justification.
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 follows e.g., that
(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 and Friedman also proved existence properties for second-order
intuitionistic systems.
Intuitionistic systems have inspired a variety of interpretations,
including Beth's tableaus, Rasiowa and Sikorski's topological models,
and Kleene's recursive realizabilities. Kripke's [1965]
possible-world semantics, with respect to which intuitionistic
predicate logic is complete and consistent, most resembles classical
model theory.
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
- k forces (A & B) if k forces A and
k forces B.
- k forces (A B) if k forces A or
k forces B.
- k forces (A B) if, for every
k'
k,
if k' forces A then k' forces B.
- k forces A if for no
k' k does k' force A.
- k forces xA(x) if for every
k' k and every
d D(k'),
k' forces A(d).
- k forces xA(x) if for
some d D(k),
k forces A(d).
Any such forcing relation is consistent and monotone:
- for no sentence A and no k does k force both
A and A.
- if k k' and k forces A
then k' forces A.
Kripke's Soundness and Completeness Theorems establish that a
sentence of L is provable in intuitionistic predicate logic if
and only if it is forced by every node of every Kripke structure.
Thus to show that
(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}.
While intuitionistic arithmetic is a proper part of classical
arithmetic, the intuitionistic attitude toward mathematical objects
results in a theory of real numbers diverging from the classical.
For readers wishing to pursue this subject farther, the third edition
[1971] of Heyting's classic [1956] is an authentic and accessible
introduction to intuitionistic philosophy, logic and mathematical
practice. Kleene and Vesley's [1965] provides a careful axiomatic
treatment of, and a constructive consistency proof for,
intuitionistic analysis. Troelstra and van Dalen's comprehensive
[1988] brings the story nearly up to date.
- Brouwer, L. E. J., "On the Foundations of Mathematics,"
Thesis, Amsterdam (1907); English translation in A. Heyting, Ed.
L. E. J. Brouwer: Collected Works 1: Philosophy and
Foundations of Mathematics, Amsterdam: North
Holland / New York: American Elsevier (1975): 11-101.
- Brouwer, L. E. J., "The Unreliability of the Logical Principles,"
(1908); English translation in Heyting, Ed., Op.Cit.: 107-111.
- Brouwer, L. E. J., "Intuitionism and Formalism," Amsterdam:
(1912); English translation by A. Dresden in
Bull. Amer. Math. Soc. 20 (1913): 81-96, reprinted in
Heyting, Ed., Op.Cit.: 123-138.
- Friedman, H., "The disjunction property implies the numerical
existence property," Proc. Nat. Acad. Sci. 72
(1975): 2877-2878.
- Gentzen, G., "Untersuchungen über das logische Schliessen,"
Math. Zeitschrift 39 (1934-5): 176-210, 405-431.
- Gödel, K., "Zum intuitionistischen Aussagenkalkül,"
Anzeiger der Akademie der Wissenschaftischen in Wien
69 (1932): 65-66.
- Gödel, K., "Zur intuitionistischen Arithmetik und
Zahlentheorie," Ergebnisse eines mathematischen Kolloquiums
4 (1933): 34-38.
- Heyting, A., "Die formalen Regeln der intuitionistischen Logik,"
in three parts, Sitzungsber. preuss. Akad. Wiss.
(1930): 42-71, 158-169.
- Heyting, A., Intuitionism: An Introduction, Amsterdam:
North-Holland (1956). Third Revised Edition (1971).
- Kleene, S. C., "On the interpretation of intuitionistic number
theory," Jour. Symb. Logic 10 (1945): 109-124.
- Kleene, S. C., Introduction to Metamathematics, Princeton:
Van Nostrand (1952).
- Kleene, S. C. and Vesley, R. E., The Foundations of
Intuitionistic Mathematics, Especially in Relation to Recursive
Functions, Amsterdam: North-Holland (1965).
- Kripke, S. A., "Semantical analysis of intuitionistic logic," in
J. Crossley and M. A. E. Dummett, eds., Formal Systems and Recursive
Functions Amsterdam: North-Holland (1965): 92-130.
- Troelstra, A. S. and van Dalen, D., Constructivism in
Mathematics: An Introduction, in two volumes,
Amsterdam: North-Holland (1988).
constructive mathematics |
Brouwer, L. E. J. | logicism | finitism | platonism | formalism
Copyright © 1999 by
Joan R. Moschovakis
joan@math.ucla.edu
A |
B |
C |
D |
E |
F |
G |
H |
I |
J |
K |
L |
M |
N |
O |
P |
Q |
R |
S |
T |
U |
V |
W |
X |
Y |
Z
Table of Contents
First published: September 1, 1999
Content last modified: September 1, 1999