A Constructive Completeness Proof
for Intuitionistic Propositional Calculus
Judith Underwood*
TR 90-1179
December 1990
Department of Computer Science
Cornell University
Ithaca, NY 14853-7501
*Supported by a National Science Foundation Graduate Fellowship.
A Constructive Completeness Proof for
Intuitionistic Propositional CJcul11s
Judith Underwood*
December 18, 1990
Abstract
This paper presents a constructive proof of completeness of Kripke
models for the intuitionistic propositional calculus. The computa-
tional content of the proof is a form of the tableau decision procedure.
If a formula is valid, the algorithm produces a proof of the formula
in the form of an inhabitant of the corresponding type; if not, it pro-
duces a Kripke model and a state in the model such that the formula
is not forced at that state in that model.
1 Introduction
Intuitionistic logic has long been known to have important connections with
computer science. The Curry-Howard isomorphism describes the strong
correspondence between propositional logic and typed lambda calculus --H
propositions are interpreted as types and proofs of propositions aTe lambda
terms of the corresponding type. This duality gives rise to type theories
which have many applications, such as formalizing proofs iii systems like
Nuprl [1].
A good introduction to intuitionistic logic is Nerode [5], which describes
the tableau algorithm in detail. Girard [4] discusses the Curry-Howard iso-
morphism. The proof is modelled after the completeness proof in Fitting
Supported by a National Science Foundation Graduate Fellowslii1?.
[3]. A constructive completeness proof for classical propositional logic ap-
pears in Constable and Howe [2], which also contains an introduction to
Nuprl.
Much work in constructive mathematics has been concerned with the
extraction of algorithms from proofs. The proof presented here was devel-
oped by the opposite approach; the constructive proof was inspired by the
tableau algorithm. One interesting result of this approach is the insight pro-
vided into the connection between Kripke models and intuitionistic proofs.
If the formula is unprovable, a model which does not force the formula is
created from the failed tableau proof; in a sense, they have the same "data
structure".
In addition, the description of tableau algoritlim which arises from the
proof is easy to understand, and in particular (and unlike other presen-
tations) it is very easy to see that the algoritlim terminates. The algo-
rithm has double exponential time complexity; the problem is known to be
Pspace-complete [6].
One purpose of this paper is to show that the completeness proof is
suitable for formalization in Nnprl; hence, definitions will be iii tlie notation
of type theory, and the propositional logic proof of the formula (if one
exists) will be constructed as an inhabitant of the type corresponding to
the proposition. The mathematical and logical equivalents should be clear.
2 Definitions
The first problem is to translate the mathematical definition of validity to
type theory. We choose the most general definition of Kripke model, and
modify only slightly the definition of forcing.
In mathematical terms, a Knpke model is a triple consisting of a set, a
transitive and reflexive relation on that set, and a monotone flinction from
the set to the set of atomic formulas. The set can be thought of as "states
of knowledge"; the order relation then describes increasing information, as
the set of atomic formulas associated with each state is considered to be
the aton?c formulas known to be true at that state.
Although Nuprl type theory has set types, it is simpler in this case to
consider the set of states of knowledge as a type itself. This is expressed
by giving it the type Ui, the lowest in a hierarchy of universe types, that
2
is, types whose members are types. See [1] for more information. The type
theoretic definition of Kripke model is then:
Kripke?model = T: U1
: trunsitive?efleriverelation(T, T)
#af : monotone?relation(T Atomic formulas)
Forcing in a particular Kripke model K = (T, 1?, af) is inductively de-
fined as a predicate forces(K, 5, a), where s ? T and a E Term. At the
same time (i.e. by mutual recursion), to avoid troublesome negations in
the definition of forcing, a predicate notforces(K, 5, a) is also defined.
forces(K,s,a) =
af(s,a)			(a e Atrn?)
forces(K, 5, P) A forces(K, 5, ?)			(a = ?A
forees(K, 5, P) v forces(K, 5, ?)			(a = Pv ?)
Vs'.sPs'
notforces(K, 5', P) v frn?ces(A) 5', ?)			(a = P
notforces(K,s,a) = ?af(s,a)			(a ? Atrn??)
notforces(K, 5, p) v notforces(K, 5, ?) (a = ?A
notforces(K, 5, ?) A notforces(K, 5, ?) (a = Pv ?)
?s'.sRs'A
forees(K, 51, ?) A notforees(K, 5', ?) (a P
Let Term be the type of propositional formulas. As in [21, the proof is
described in terms of sequents.
Sequent (Term list)#(Term list)
However, more information is required for the intuitionistic case; thus our
basic unit will be a system of sequents.
System = (Sequent list)
(The list type is a convenience; sequents should be thought of as pairs of
sets and a system of sequents should be considered a set of sequents.) A
given sequent will be written as a pair ? ST, 5F > The formulas in ST are
the ones which are tagged "true" at some node in the tableau algoritlim;
similarly the formulas in 5F are tagged "false". The sequents themselves
correspond to the nodes in the tableau algoritlim; they will also correspond
to the states in the Knpke model disproving validity, if one exists.
3
3 Statement of the Theorem
Although we are generally interested only in the validity of a single formula
y, or rather a given sequent < ?, ? >, the induction requires a statement
which is true for systems of sequents. We will prove tliat, for any system,
either there is a sequent in this system which is provable or there is a Knpke
model which, for all sequents < 5T, SF > in the system, forces the formulas
in 5T but not those in 5F This Kripke model will be referred to as a
countermodel for the system.
A sequent < 5T, 5F > is provable if there is an inhabitant of the type
corresponding to A 5T H ? 5F (To make the paper accessible to readers
without intimate knowledge of type theory, the notation for propositions
and types will be the same.)
If there is a countermodel, we also supply a function f fron? the system
to the model such that f(< 5T, 5F >) is the state iii the system whidi
forces the formulas in 5T but not those in 5F
The formal statement of the theorem is then
VS: System.
? ?T',?F' >E ?(A4 H VSF'))
v
(T, R, af) : Kripk??mode1.
?f: 5 H T
V < 5T,5F >? &(f(? ST,SF>) 8
c S?.forc?s(K, s, o?) A Va c S?.notforccs(A?, 8, a))))
Note that when the theorem is applied to a formula cp, 5 will contain
exactly one sequent, namely ? ?, cp >; thus we have either cp is provable or
there is a countermodel which does not force ?.
4
Proof of the Theorem
The proof is by induction on the number of formulas which can be added
to the system. Each step either adds a fon?nla to a sequent in 5 or adds
another sequent to 5. All formulas added will be snbforninlas of the for-
mulas already in 5, hence only finitely many can be added to a particular
4
sequent. A new sequent < ST, SF > is added only when 110 more formulas
can be added to sequents already in 5, and then only if there is no sequent
? ST, 5F' > in 5 with 5T C ST, and 5F -
C 5' so that any new sequent
will never develop into a sequent already present in 5. Also, the formulas
in < 5T, 5F > will be subformulas of the formulas already in 5, so only
finitely many new sequents can be added.
The proof proceeds by cases.
1.
2.
For any pair < 5T,5F >? 5, if ?A? E 5T and (0 ? 5T or ? 5T),
apply the inductive hypothesis to 5', where 5' is 5 with ? 5T, 5F >
replaced by <5T U f0,Pl,SF>.
If, for the system 5', it is the case that 0 A ? A (A 5T) H ? 5F, i.e.
we have an inhabitant f' --H Ax0x? .... of the corresponding
function type, we can produce an inhabitant f of A 5T V 5F Given
an element ? of type A5T, set f equal to fr(?1(ro?AP),7r2(x?ffiAP),a).
Then, since 0 A ? Ei 5T, f ? A 5T H ? 5F (If some other sequent in
5' is the one corresponding to the inhabited type, since it is also in 5
the theorem still holds.)
If we have a countermodel A = (T, R, af) for 5', and we have f
5, H T such that f(< 5T U f0, Pi, 5F >) = s for some 8 E T (so
that V? Ei 5T U to,Pi.force?(K,?,?)), then we trivially have V? C
S?.force?(K, 8, ?). Letting f(? 5T, 5F >) = 8, we then have that
(T, 1?, af) is a Knpke countermodel for 5
For any pair < 5T, 5F >C 5, if 0 A P ? 5F and (o ? 5F and ? ? 5F),
apply the inductive hypothesis to 5i and 52, where St is 5 with
? 5T,5F > replaced by ? ST,SFUf0i > and 52 is 5 wth ? 5T,5F ?
replaced by ? 5T, 5F U fpi>.
If, for S1 and S2, it is the case that A 5T V S? V 0 a?td A 5T
V 5F V ?, so we have functions fi and f2 from the product type (cor-
responding to) A 5T to the disjoint union types (corresponding to)
V 5F V 0 and V 5F V P. (?Vhile V 5F is really a disjoint union type
and should have its elements tagged to identify whidi disjunct they
inhabit, the details of the tagging will be omitted to avoid the extra
notation.) To produce a function f to V 5F giveil all element a of
type A5T, decide if fi(a) E V5F. If so, f(a) = fr(a). Otherwise,
5
if f2(a) E V 5F, f(a) f2(a). If neither case holds, we nuist have
f1(a) ? o and f2(a) ? p. Then set f(a) jj(a)#f2(a), an dement of
?A?. Since ?A? ? 5F, f has type A5T H V5F.
Otherwise, we have a countermodel K (T, 1?, af) for Si or 52 As-
sume without loss of generality that we have a countermodel for Si.
If we have f : Si H T such that f(? 5T, 5F U f?? >)			s for some
s Ei T (so that V? ? 5F U f&J.notforces(K,s,?)), then			we tnvially
haveV? ? 5?.notforces(K,s,?). Letting f(< 5T,5F >)			s, we then
have that (T, R, af) is a Knpke countermodd for 5.
3. For any pair <5T,5F >? 5, if?vPc 5T and (o V 5T and p V 5T),
apply the inductive hypothesis to Si and 52, where Si is 5 with
<5T,5F > replaced by ? STUfol,SF > and 52 is 5 wth ? 5T,5F>
replaced by ? 5T U ???, 5F>.
If we have inhabitants fi of ? A (A 5T) V 5F and f2 of /J A (A 5T) H
V 5F, we can produce an element of A 5T V 5F Since 0 V ? cor-
responds to a disjoint union type, its inhabitants are tagged so that
it is possible to decide whether a given dement of 0 V ? is in 0 or in
P. Given a of type A 5T, decide whether 7rj(a) (where is the index
of the element of A5T of type 0 V P) is il-I 0 or ?. If 7r(a) ? 0,
let f(a) f1(7ri(a), a); if 7?(a) E t3, let f(a) f2(??i(e), a). In algo-
rithmic terms, f could be written "if 7ri(a) E 0 then f1(7?j(q), a) else
Then f has type A5T H V5F.
Otherwise, we have a countermodel K (T, R, af) for 5i or 52. As-
sume without loss of generality that we have a countermodel for 5i.
If we have f : 5? H T such that f(? 5T U fo?, 5F >) s for son?
s E T (so that V? ? 5T U fo?.forces(A,s,?)), then we trivially have
? 5?.forces(K,s,?). Letting f(? 5T,5F >) ?, we then have
that (T, 1?, af) is a Knpke counterinodel for 5.
4. For any pair <5T,5F >? 5,ifoV(3? 5F and(o V5p or(3VS?),
apply the inductive hypothesis to 5'. where 5' is 5 with ? 5T, 5F >
replaced by < 5T, 5F U fo, (3?>.
If we have an inhabitant f' of A 5T			V 5F V 0 V (3, we can produce
an inhabitant f of A 5T H ? 5F Given a of type A 5T, decide if f'(a)
`In Nupri type theory, this would be written decidc(Tii(a); x.f1(x, a), x.f2(x, a)).
6
5.
6.
is in V 5F If so, let f(a) f'(a). Otherwise, f'(a) C 0 or f'(a) ?
If f'(a) ? a, let f(a) be f'(a), tagged so that it is an element of the
disjoint union avP. Similarly, if f'(a) ? ?, let f(a) be ft(a), tagged as
an element of ovP. Then, since aV? ? 5F, f has type A5T H V5F.
Otherwise, we have a countermodel K = (T, R, af) for 5'. If we have
f : 5' H T such that f(? 5T,5F U fa, PJ >) = s for some s ? T
(so that V? ? 5F U fa, P?.notforces(K,s,?)), then we trivially have
? 5?.notforces(K,s,?). Letting f(? 5T,5F>) = s, we then have
that (T, R, af) is a Knpke countermodd for 5
For any pair ? 5T, 5F >? 5, if ? H ? C 5T and (a ? 5F or ? 5T),
apply the inductive hypothesis to Si and 52, where Si is 5 with
<5T, 5F > replaced by < 5T, SFU fal > and 52 is 5 Mth < 5T, 5F>
replaced by ? 5T U ffl?, 5F>.
If, for Si and 52, it is the case that A5T V 5F V a and A5T A ?
V 5F, then we have a function fi from A 5T to V 5F V a and a function
f2 from ? A A 5T to V 5F To pmduce a function f from A 5T to
V5F, given an element a of type A5T, decide if fr(a) c V5F. If so,
f(a) = f1(a). Otherwise, f1(a) ? a. Now since a P E 5T, we can
set f(a) equal to j?(x??Pfi(a),a) (since wa?Pf?(a) has type P). Then
f is of type A5T H V5F.
Otherwise, we have a countermodd K = (T, 1?, af) for 5i or 52. If K
is a countermodelfor 5i, and f: 5i H Tsudi that f(? 5T,5FUfal >
= s for some s Ei T (so that V? E SFU fat.notfarccs(A)s,?)), then
we trivially have V? C 5?.notfo?ces(K,s,?). Lctting f(? 5T,5F >
= 3, we then have that (T, 1?, af) is a I?ripke countcrmodd for 5.
If we have a counten?odd for 52, and f : 52 T such that f(? 5TU
fPt,5F >) = sforsomes ? T(sothatV? F 5?UfJ?J.forces(A?s,?)),
then we trivially have V? E S?.forces(K,?,?). Letting f(? 5T,5F >
= 3, we then have that (T, 1?, af) is a I&npke countermodel for 5.
For any pair ? 5T,5F >E 5, if a H			E 5F and V ? 4', 5F' >?
S.(STU fal ? 5T'VQ ? 5F'), and none of the previous cases hold, apply
the inductive hypothesis to 5', where 5' is 5 U f? 5T U fa), f?? >t.
If, for 5', we have an inhabitant f' of (A 5T A a) f3, then the
function AyAST.AxQ.f(y, w) is in A5T			(a ?), so the appropriate
7
tagged version of this function is in A 5T H ? 5F
If we have a countermodel K = (T, R1af) for 5', then since 5 C 5', <
ST, SF >C 5, so f(< ST,SF >) = s for some 5 C T. This means we al-
readyknowthatV? c S?.forces(K,5,?)AV? C S?.notforces(K,5,
So, we need not change f for 5, except to remove < 5T U f?J, fP? >
from its domain. We then have that (T, R, af) is a Kripke counter-
model for 5.
7. If none of the above cases hold, we have reached the base case.
Note that because none of the above cases hold, we know that, for
every ? 5T,5F >C 5,
& A P C 5T H a C 5T and? C 5T
0V ? C 5T H Q C 5T or C 5T
H C 5T H a C 5F or ? C 5T
a A ? C 5F H a C 5F or ? C 5F
? V ? C 5F H a C 5F and? C 5F
H C5F H 3 ? ST',SF'> 5T ? 5T' anda C5F and? C5F
If there is an ? 5T, 5F >C 5 such that 3a C 5T A 5F, then A5T H
V 5F is inhabited by AxAST.(j, 7ri(r)), where i is the index of a in A 5T
and j is the tag for a in the disjoint union V 5F
Otherwise, V ? 5T, 5F >C S, 5T fl 5F = ?. Let T --H 5 and define 1?,
a relation on T#T, by
1?(<5T,SF>, <ST',SF'>)?STC4'
It is easy to see that 1? is transitive and reflexive. Define af, a relation
on T#Atornicformulas by
af(? 5T,5F >,a) ? a C 5T
Since af is monotone with respect to 1?, (T, 1?, af) Kr4?ke?rnode1.
Note that since 5T fl 5F = ?, a C 5F H maf(s, a).
8
Define f 5 H T to be the identity map from 5 to T. To complete
the theorem, we must show that
V <ST, SF >? 5.
f(< 5T, SF>) = 5 H
(Va ? S?.forces(K, s, a) A Va E S?.notfrn?ces(K, s, a)).
Since forces and notforces are defined by mutual induction on the
complexity of the formula, the proofs of (Va E S?.fm?ce?(K, s, a) A
Va E S?.notforces(K, 5, a)) must proceed similarly. For sin-iplidty,
however, they will be presented sequentially.
We first prove Va ? S?.forces(K, s, a), by induction on the complex-
ity of a.
(a) a is an atom. Then forces(K, s, a) = af(s, a), true when a Ei 5T
by definition of af
a = P A ?. We know P E 5T and ? C 5T, 50 by induc-
tion hypothesis frn?ces(K, s, ?) and fw?cc?(A?, s, ?). Therefore,
frn?ces(K, s, P A ?).
a = pv?. We know P Ei 5T or ? ? 5T, 50 by induction hypothesis
forces(K, 5, ?) or forces(K, s, ?). Therefore, fovces(A, s,
a = H ? We need that Vs'.sks' H notforces(K,s',P) v
forces(K, 5', ?). Now, for all < 5T'? ?F' > sud? that f(< 5T'? SF'>
= 5', we know sRs' ? 5T C 5T'? ?? P H ? 5T' We
also know, then, that ? C 5T' or P E 5r$, so forces(K,s',?)
or notforces(K, 5', P). Therefore, forces(K, S'? H
The proof for Va E S?.notfrn?ces(K, 5, c?) is simil??r.
(a) a is an atom. Since 5T fl 5F = ?, a ? 5T, 50 maf(s,a), i.e.
notforces(K, 5, a).
a = P A ?. We know p ? 5F or ? C 5F, 50 by induction
hypothesis notforces(K, 5, ?) or notforces(A?, 5, ?). Therefore,
notforces(K, 5, (3 A
9
a = ? V ?. We know p ? 5F and ? E 5F, so by induction
hypothesis notforces(K, s,P) and notforces(K, s, ?). Therefore,
notforces(K, s,? V ?).
CL = H
Since < 5T, 5F >Ei T and rule 6 above doesn't apply, we must
have a < ?`, 5F' >? T.ST U fP? C 5T' A ? E 5F' Lets' =
f(< 5T'' 5F' >) By induction hypothesis, forces(K, s', ?) and
notforces(K,s',?). Also, since 5T ? 5T U fal c 5T'? ???`
Therefore, 3s'.sRs' A forces(K, 8', ?) A notfrn?ces(K, s', ?).
5 Conclusion
Each system of sequents in the above proof corresponds to a branch of the
tableau. If all branches close (i.e. if there is a sequent iii each system
such that 5T fl 5F is nonempty), then the formula is provable; else, the
open branch becomes a Knpke model which does not force the formula.
Note that a state (sequent) is added to the I&'ripke model only when nec-
essary to provide a state which fails to force an implication; hence, the
modd produced is minimal. The model produced is finite, so the proof also
demonstrates the completeness of finite Knpke modds.
If the proof were added to the Nuprl system, the result would be a pro-
cedure for deciding the (intuitionistic) validity of a propositional formula.
llowever, from inside Nuprl, we do not yet know that a proposition cannot
have both a proof and a countermodel; we have not proved so'undmess of
I?ripke models. This leads to some interesting questions about ?vhat model
makes the most sense in type theory; ideally, the soundness and complete-
ness theorems would say something meaningful about the type thcory as
well as the logic. Sud? a result would provide deeper understanding of the
relationship between logic and type theory, and would give insight into the
use of type theory to describe its own semantics (i.e. reflection).
References
[lj R. L. Constable et al. Implementing Mathematics with the Nnprl F??of
Development System. Prentice-llall, 1 9SG.
10
[2] R. L. Constable and D. J. Howe. Implementing ?4etamathematics as
an Approach to Automatic Theorem Proving. In Formal Techniqnes zn
Art?flcial Intell?ence, R. Banerji, ed. North-Holland, 1990.
[3] ?4. Fitting. Intn?tiont'stic Log?c, Model Theory, and Forc"ng. North-
Holland, 1969.
[4] J. Y. Girard. Proofs and Types. Cambridge University Press, 1989.
[5] A. Nerode. Some Lectures on Intuitionistic Logic. In Logic and Compitter
Science, Springer-Verlag Lecture Notes in ?Iathematics 1429, 1990.
[6] R. Statman. Intuitionistic Propositional Logic is Polynoinial-space
Complete. Theoretical Computer Science 9, 67-72,1979.
11