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 correct and 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 2 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).
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:
- From A and (A B), conclude B.
- From (C A(x)),
where x is a variable which does not occur free in C, conclude
(C xA(x)).
- From (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
(one or two) 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. A derivation of a formula E from a collection
F of assumptions is any sequence of formulas, each of
which belongs to F or is an axiom or an immediate consequence,
by a rule of inference, of preceding formulas of the sequence, such
that E is the last formula of the sequence. If such a derivation
exists, we say E is derivable from F.
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:
A (A B).
is replaced by the law of double negation:
A A.
(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
(INE) If F entails A and F entails
A,
then F entails B.
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,
Like their classical extensions, intuitionistic propositional and
predicate logic satisfy the Deduction Theorem: If B is
derivable from A with all variables free in A held constant in the
deduction (that is, without using the second or third rule of
inference on any variable x occurring free in A, unless the
assumption A does not occur in the deduction before the inference in
question), then (A 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:
- 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
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).
Intuitionistic systems have inspired a variety of interpretations,
including Beth's tableaus, Rasiowa and Sikorski's topological models,
formulas-as-types, Kleene's recursive realizabilities, and the Kleene and
Aczel slashes. 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. Kleene's [1969] formalizes the theory
of partial recursive functionals, enabling precise formalizations
of the function-realizability interpretation used in [1965] and of
a related q-realizability interpretation which establishes a recursive
uniformization rule for intuitionistic analysis.
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.
- Beeson, M. J., Foundations of Constructive Mathematics,
Springer, Berlin (1985).
- 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).
- Iemhoff, R., "On the admissible rules of intuitionistic propositional
logic," Jour. Symb. Logic 66 (2001): 281-294.
- 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., Formalized Recursive Functionals and Formalized
Realizability, Memoirs of the American Mathematical Society 89 (1969).
- 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.
- Martin-Löf, P., Intuitionistic Type Theory,
Notes by Giovanni Sambin of a series of lectures given in Padua, June 1980,
Bibliopolis, Napoli (1984).
- Troelstra, A. S., Ed., Metamathematical Investigation of
Intuitionistic Arithmetic and Analysis, Lecture Notes in
Mathematics 344, Springer-Verlag, Berlin (1973). Corrections and
additions available from the editor.
- Troelstra, A. S., "Realizability," Chapter VI of S. R. Buss, ed.,
Handbook of Proof Theory, Elsevier, Amsterdam and New York
(1998): 407-473.
- Troelstra, A. S. and van Dalen, D., Constructivism in
Mathematics: An Introduction, in two volumes,
Amsterdam: North-Holland (1988).
- Veldman, W., "A survey of intuitionistic descriptive set theory,"
in P. P. Petkov, ed., Mathematical Logic, Proceedings of the
Heyting Conference, Plenum Press, New York and London (1990):
155-174.
- Visser, A., "Substitutions of Sigma^{0}_{1}
sentences: explorations between intuitionistic propositional logic
and intuitionistic arithmetic," Annals of Pure and Applied
Logic 114 (2002): 227-271.
[Please contact the author with suggestions.]
Brouwer, Luitzen Egbertus Jan |
finitism |
formalism |
logicism |
mathematics: constructive |
Platonism: in metaphysics |
logic: classical
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: December 20, 2002