Systems of Illative Combinatory Logic

PDF hosted at the Radboud Repository of the Radboud University
Nijmegen
The following full text is a publisher's version.
For additional information about this publication click this link.
http://hdl.handle.net/2066/17259
Please be advised that this information was generated on 2015-02-03 and may be subject to
change.
T u t J o u r n a l o r S ym bo lic L o g ic
Volume 5N, N u m b e r 3, Sept. 1993
SYSTEM S O F ILLATIVE C O M B IN A T O R Y L O G IC
C O M P L E T E FOR FIRST-O RD ER P R O P O S IT IO N A L
A ND PRED ICA TE C A LCU LU S
HENK
B A R EN D R E G T , M A R TIN
B U N D ER , A N D W IL
DEKKERS
A b s t r a c t . Illative c o m b i n a t o r y logic co n s is ts o f the t h e o r y o f c o m b i n a t o r s o r l a m b d a c a lc u lu s e x t e n d e d
by e x t r a c o n s t a n t s ( a n d c o r r e s p o n d i n g a x i o m s a n d rules) i n t e n d e d to c a p t u r e inference. T h e p a p e r c o n s i d e r s
systems o f illative c o m b i n a t o r y logic that a rc s o u n d for first-order p r o p o s i t i o n a l a n d p r e d i c a te calculus.
T h e i n t e r p r e t a t i o n fr o m o r d i n a r y logic in to the illative system s c a n be d o n e in two ways: following the
p r o p o s i lio n s-as-ly p es p a r a d i g m , in which d e r i v a t i o n s b e c o m e c o m b i n a t o r s or. in a m o r e direct w ay. in
which d e r i v a t i o n s a re not t r a n s l a t e d . Both t r a n s l a t i o n s a r e closely related in a c a n o n i c a l way. T h e tw o direct
t r a n s l a t i o n s turn o u t to be c o m p le t e . T h e p a p e r fulfills the p r o g r a m o f C h u r c h [1932], [1933] a n d C u r r y
[1930] to base logic o n a c o n s i s t e n t system o f / - t e r m s o r c o m b i n a t o r s . H i t h e r t o this p r o g r a m h a d failed
because system s o f I C L were e it h e r l o o w e a k (to p r o v id e a s o u n d i n t e r p r e t a t i o n ) o r l o o s t r o n g (s o m e tim e s
even inconsistent).
§1. Introduction. T h e t h e o r y of c o m b i n a t o r s ( C u r r y et al. [1958], [1 9 7 2 ]) a n d
the l a m b d a calculus ( C h u r c h [1941], B a r e n d r e g t [ 1 9 8 4 ] ) are theories t h a t success
fully analyze the n o t i o n of effective c o m p u t a b i l i t y . H o w e v e r, the original fo u n d ers
of these subjects, C u r r y a n d C h u r c h , also h a d a im e d to p r o v i d e a basic for logic
(and thereby m a th e m a tic s). F o r m a l systems in t e n d e d to achieve this are given in
C h u r c h [ 1932], [ 1933] a n d C u r r y [ 1930], [ 1931 ], [ 1932], [ 1933], [ 1934a], [11934b],
[1935]. U n f o r t u n a t e l y , it was s h o w n in Klecne a n d Rosser [ 1 9 3 5 ] t h a t these sys
tems are inconsistent. In C u r r y [1942c] the inconsistency of C u r r y [ 1 9 3 4 ] was
simplified. This d eriv a tio n , n o w k n o w n as “ C u r r y ’s p a r a d o x ”, is a k in to the Russell
p a r a d o x but requires no p r o p e r tie s of n eg atio n . It can be w ritten in only a few lines.
C u r r y a n d his school then s t a r t e d a p r o g r a m of defining several systems of
illative c o m b i n a t o r y logic (IC L ) of v ary in g stren g th , see C u r r y [1942 a]. T h e goal
was to “ find s t r o n g e r a n d s t r o n g e r systems which are co n s iste n t a n d w e a k e r a n d
w e a k e r systems which are in consistent but s t r o n g e n o u g h to interpret logic, h o p i n g
to end up with a co n s iste n t system in which logic can be i n t e r p r e t e d " ( q u o t a t i o n
from C u r r y a n d Feys [1958; §8S3, p. 276]).
F o l l o w i n g this m e t h o d o l o g y , B u n d e r [1969], [1973], [1 9 7 4 ] i n t r o d u c e d restric
tions on the rules of the illative c o n s t a n t s so t h a t first-order p r o p o s i t i o n a l a n d
Received May 5, 1992.
This research was su p p o rte d by the Australian Research Council G r a n t A 68930230.
< 1993. Association lor Symbolic Logic
0022-4812/93/5803-0001/ $03.00
«•
769
•
770
HENK BARENDREGT, MARTIN BUNDER. AND W I L DEKKERS
predicate calculus can be in te rp re ted in the resulting systems. B u n d e r [ 1 9 8 3 a ] also
allows m u c h of set theory. In all these systems the usual d e r i v a t i o n of C u r r y 's
p a r a d o x is blocked, but the consistency of these systems r e m a i n s an o p e n question.
T h a t the q u e s t i o n is not a c a d e m i c w as s h o w n in B u n d e r [ 1 9 7 6 ] a n d [ 1 9 8 3 a ] , where
related illative systems were p r o v e d to be inconsistent.
In the rest of this section we give a s h o r t i n t r o d u c t i o n to illative c o m b i n a t o r y
logic by s h o w i n g the early inconsistent system of C u r r y [1934]. In §2 we i n t r o d u c e
systems slightly w e a k e r t h a n the ones in B u n d e r [1973], [1974] but s t r o n g e n o u g h
to in te rp re t logic. We derive r o u g h l y the following s o u n d n e s s result
A K
A => [ ^ ] h r [-4].
where L represents p r o p o s i t i o n a l or p r e d ic a te logic a n d [ —] o n e of tw o possible
t r a n s l a t i o n s of each system into an IC L system C (there will then be 4 such C's).
O f the i n t e r p r e t a t i o n s one is the p r o p o s i t i o n s - a s - t y p e s i n t e r p r e t a t i o n d u e to C u r r y ,
H o w a r d , a n d de Bruijn; the o t h e r is a m o r e direct i n t e r p r e t a t i o n . Finally, in §2 we
sh o w th a t the tw o i n t e r p r e t a t i o n s are c a n o n ic a ll y related.
In {¡3 we derive c o m p l e te n e s s results for 2 of the 4 systems of ICL. These,
a g ain roughly, take the following form
[,-l] I—c [,4 ] => A I—L A.
This c o m p le te n e s s result implies the consistency of the I C L s involved.
Illative combinatory logic. N o w we will present a simple system . / of illative
c o m b i n a t o r y logic in o r d e r to explain the general idea. T h e system is s t r o n g e n o u g h
to represent the [ =>, Vj f r a g m e n t of first-order intuiitionistic p r e d ic a te calculus.
T h e in tu itio n b e h in d the system . / is as follows. T e r m s are type-free l a m b d a
terms extended by s om e extra constants. A term X is considered to have an assertive
value. A term X Z can be seen as a s t a t e m e n t say in g “ Z is of type X " o r “ Z g X "
or “ Z satisfies the p red icate A'". T h e term
c o r r e s p o n d s to the class {£ | X }.
T h e r e is a term E such th at the s t a t e m e n t ‘E X Y ’ is in t e rp r e t e d as “X
Y " or
“(V.v e X ) Y x ' \ U sin g this E one can define im p lic a tio n a n d q u a n ti fi c a tio n .
1.1. D
efinition.
T h e s y s t e m . / is d e f i n e d a s f o l l o w s .
(i) T, the set of terms o f i s given by the following a b s t r a c t g r a m m a r :
T = V IE | T T | / K T .
Here V is the syntactical c a t e g o r y of variables a n d E is a c o n s t a n t . We also write
T = /1(E),
since T is o b t a i n e d from the set A of type-free l a m b d a te r m s by a d d i n g the c o n
s ta n t E.
(ii) O n T the usual n o t i o n of /^ /-red u ctio n is given by the c o n t r a c t i o n rules
U x.M )N -
A/ [a* := /V],
/ X . M x -> M
if a* £ F V ( M ) .
Here F V ( M ) is the set of free variables of M. T h e resulting ( m o r e step) [h]-reduction
a n d /hj-convertihility relation are d e n o t e d by
a n d = . S y n tactic e q u a li ty is d e
n o te d by = .
SYSTEMS OF I LLATI VE C O M B I N A T O R Y L O G I C
771
(iii) A statement o f . / is j u s t an elem ent of T. A basis is a set of statem ents.
(iv) Let r be a basis, a n d let X be a s t a t e m e n t ; then X is derivable from T, n o t a
tion r b X , if r \- X can be p r o d u c e d by the n a t u r a l d e d u c t i o n system in T a b l e 1.
T
able
1
X e r => r \— X ,
r \ - x i x=Y=>r\-Y,
r b E X Y , r b x z =>
rb
yz,
r , x .x b Yx, X i F V ( r , X, y ) ^> r b e a t .
In the last rule x is s o m e variable. T h e system is based on /^/-conversion. Therefore,
this last rule co u ld be replaced by
r,x
^
b y, X t F V ( n
r b s(/x.x)(A x.y).
1.2. D e f i n i t i o n . F o r X , Y e T write
(i) X 3 y = 5 (KX)(Ky>,
(ii) V u e x . y = E X ( / w . y ) .
1.3. P r o p o s i t i o n . The following holds f o r the system J.
(i) r b X => y, r b x => r b y.
(ii) a b y ^ r b x ^ y .
(iii) ƒ" b Vi/ g X . Y , r \— X t => r \~ Y [ u := *].
(iv) r , x i / b y, h ^ FV(r,AT) => r b V n e i . y .
N o w it is possible to in te rp re t the {=>, V} f r a g m e n t of first-order intuitionistic
predicate logic into J . F o r ex am p le, a sentence like
Vx(Æx
3
Rx)
h o ld in g in a universe A is t r a n s l a t e d as the s t a t e m e n t
(Vx
g
A . R x => R x )
which is EA( Àx. E(K{Rx))(K(Rx))) a n d is p r o v a b l e in .ƒ.
U n f o r t u n a t e l y , the i n t e r p r e t a t i o n is not c o m p l e t e (i.e., if the t r a n s l a t i o n of a for
m u l a (p is p r o v a b l e in
then cp itself is p r o v a b l e in logic) because the system . / is
n o t consistent; every s t a t e m e n t X (i.e., every term) can be derived in . / (from the
e m p t y basis).
1.4. P r o p o s i t i o n ( C u r r y ’s p a ra d o x ). Let X be a statement o f J . Then \~X.
P r o o f . Let X be given. T a k e
y = ( / y . ( yy) id
X){Xy.(yy) id X ) .
T h e n Y = Y id X . Therefore, the following d e r i v a t i o n s h o w s th a t \~X.
Y b y;
y b y
ybX ,
3
X,
since Y = Y
by 1.3(i);
id X
;
772
H E N K BA REN D R E G T , M A R T I N B U N D E R , A N D W I L D E K K E R S
h
Y =5 X ,
b y 1. 3 (ii);
3
h- Y,
since y
hX ,
by 1.3(i).
x = y;
□
N o t e th at the d e r i v a t i o n of X is related to the p r o o f of the t h e o r e m of L ö b
[
1
9
5
5
]
-
In the next section the illative system . / will be f o r m u l a t e d m o r e carefully so
t h a t the system b e c o m e s co n s iste n t a n d in fact c o m p l e t e over o r d i n a r y logic.
§2. Sound interpretations of logics in ICL’s. In the i n t r o d u c t i o n we stated that
logic can be in te rp r e ted in tw o w ays in ICL's. In fact, this can be d o n e b o t h for the
p r o p o s i t i o n a l a n d p red icate calculus, so there will be four related illative systems.
T h e i n t e r p r e t a t i o n will be d o n e for the {=> ¡ (respectively { =>,V¡) f r a g m e n t of intuitionistic logic. This is the m o st essential p a r t of logic a n d the direct i n t e r p r e t a
tion ([ —] below) can be e x te n d e d to include the logical o p e r a t o r s —i, &, v, a n d 3.
In s e c o n d - o r d e r logic these o p e r a t o r s are definable from =>, V, so b o t h o u r i n t e r
p r e t a t i o n s can be e x te n d e d into s o u n d (and p r o b a b l y c o m p le te ) i n t e r p r e t a t i o n s of
s e c o n d - o r d e r logical calculi.
N o w we display the tw o logical calculi t h a t will be interpreted.
2.1.
D e f i n i t i o n . Let P R O P be the =d f r a g m e n t of intuitionistic p r o p o s i t i o n a l
losic d e t e r m i n e d as follows.
(i)
T h e set of f o r m u la s of P R O P , n o t a t i o n FPROP, is defined by the following
a b s t r a c t syntax:
FpRop =
^
F oP R
DO
r>PD 13 F
u uP R O P
H ere V is a set of p r o p o s i t i o n a l variables.
(ii)
Let r <= Fprop a n d cp e FPROP. T h e n T f - PROP cp is defined by the system of
n a t u r a l d e d u c t i o n in T a b l e 2.
T
able
2 PROP.
Let PR E D be the { =5, V } f r a g m e n t of first-order m a n y - s o r t e d
intuitionistic p red icate calculus of a given s i g n a t u r e s.
Below as an example, we will treat a version of PR E D with s the s i g n a t u r e of
the s tr u c tu r e
2 .2 . D
efinition.
< A , , A 2, f , g, P , a )
with
A,, A 2
f: A, -» A,
n o n e m p t y sets;
a u n a r y function:
SYSTEMS OF I LLATI VE C O M B I N A T O R Y L O G I C
g :
A
A,
A,
a b i n a r y function;
P Ç At
a
g
773
a u n a r y relation;
A,
a constant.
(All results also hold for a r b i t r a r y signatures.)
(i)
T h e set of term s of P R E D , n o t a t i o n TTPRED, is defined by the following a b
stract syntax:
^ pred — T\, T
TAl = V a ' a f T Al gTAlTA„
Ta , = V A=.
(ii)
T h e set of f o r m u la s of P R E D , n o t a t i o n FPRIiD, is defined by the following
a b s t r a c t syntax:
FP R E D
(iii) r I
pred
PTL
FP R E D
FP R E D V V A,FP R E D
(P iS a x i o m a t i s e d by the system of n a t u r a l d e d u c t i o n in T a b l e 3
T
able
3 PRED.
(pg r => r
(p\
r\-(p^> i¡/,r\-(p= > r\-i¡/;
r, (p i- i// => r i- (p =>\jj\
r h V.va,(/5, t e TAi => r h- (p\_xAi := f];
r h cp, x A> £ F V ( n => r h VxA,<p.
N o w the systems P R O P a n d P R E D will be i n t e rp r e t e d in I C L ’s. In o r d e r to
block the p r o o f of the C u r r y p a r a d o x , B u n d e r [1969], [1973], [ 1 9 7 4 ] modified the
system . / by restricting the E - i n t r o d u c t i o n rule a n d a d d i n g s o m e o t h e r a x i o m s a n d
a rule. T h e resulting system ./0 was s t r o n g e n o u g h to p ro v id e s o u n d i n t e r p r e t a t i o n s
of P R O P a n d P R E D , while the p r o o f of the C u r r y p a r a d o x was blocked. H o w ev er,
the p r o b l e m s of the c o m p l e te n e s s of the i n t e r p r e t a t i o n a n d even of the consistency
of y 0 r e m a i n e d open. ( T h e system ./0 will be described later.)
We will give modified versions of ./0 in which the logics can be e m b e d d e d in a
s o u n d way by tw o k in d s of e m b e d d i n g s . T h e first kind is ‘‘d i r e c t ”, a n d the second
kind is a c c o r d i n g to the “ p r o p o s i t i o n s - a s - t y p e s ” a n d “ p r o o f s - a s - t e r m s ” p a r a d i g m ,
see B a r e n d r e g t [1992; §5.1, §5.4]. As there are tw o logical systems, P R O P a n d
P R E D , there will be four systems of ICL. These systems are called ./P . . / E , .ƒ F,
a n d , / G respectively. T h e i r use for the tw o kin ds of i n t e r p r e t a t i o n is as follows.
Let [ y be the direct a n d [ ] 2 the p r o p o s i t i o n s - a s - t y p e s tr a n s la tio n . T h e n T a b l e 4
(see next page) sh o w s the systems of I C L th a t are used for the tw o t r a n s l a t i o n s of
P R O P and PRED .
774
HENK BARENDREGT, MARTIN BUNDER, AND W I L DEKKERS
T
4
able
H
1
[]2
PROP
yp
./f
PRED
.ƒ£
./G
For example
[ ] 2: P R E D -» . / G .
T h e four systems I C L will be described now, a n d m o r e o v e r , their relative
s t r e n g th s will be c o m p a r e d .
2.3.
D e f i n i t i o n . Let T = A(E, L) be the set of type-free l a m b d a te r m s e x te n d e d
by the e x tra c o n s t a n t s E a n d L.
(i) Define the following term s in T.
P EE Àxy.E(Kx)(Ky),
F = Lxyz.Zx(yoz),
G = Àxyz.Ex(Syz),
H = L K,
w here K =
M N = À x . M ( N x ), a n d S = ¿pqr.pr(qr).
W rite X ZD Y for P X Y.
(ii) Define the following four systems of illative c o m b i n a t o r y logic , / P , J E , . / F ,
a n d , / G . All four systems have as rules those given in T a b l e 5.
T
able
5
All s y s t e m s .
X e r => r H X\
r i- X, X =p y => r h y.
T h e four systems have the specific rules given in T a b l e s 6 - 9 .
T
able
6 ,/P .
pc
r h X
3
p¡
r j h
Y ,r\-H X
pH
r , x h h y, r b h x => r b h ( x => y ).
y, r \- x
T
able
=> r b y ;
=> r b x => y ;
7 ./£ .
r h zxy, r b x v
=> r b y v ;
r , X x h Y x , r h l x , a í F V ( r , x , y>
=> r b e x y -,
r , X x h H(yx), r b l x , a - < ¿ F v < r , x , y ) => r b h ( s a t ) .
775
SYSTEMS O F I LLATI VE C O M B I N A T O R Y L O G I C
T a b le 8 J F .
yz, r h xv
=> r
Fc
r
f¡
r , a a b Y ( Z x ), r h l a , a- $ F V ( r , a
fl
t a ' x h Ly, r h l a : , a $ f v ( P , a \ y )
b f a
T
able
9
y, z) => r
b
Y(Zvy
b fx
yz;
=> r b L(FAr y )
./G .
Gc
r h g A' y z , r \- x v
G¡
r , a: a b yv(ZA), r t- l a \ a ¿ F V ( r , x , y, z ) => r b g a y z ;
gl
r , at a h L( yv), r b l a \ a
=> r b y K ( Z K ) ;
F v i r , at, y>
r h u g x y ).
T o get a taste for w h a t will follow, we give s o m e e x a m p l e s of i n t e r p r e t a t i o n s of
ta u to lo g ie s in the ICL's.
2.4.
E x a m p l e s , (i) T h e f o r m u l a p => p of P R O P is tr a n s l a t e d as p =5 p in . / P .
T h e fact th a t p
p is indeed a wff of P R O P is expressed in .ƒ P as Hp h H ( / ) d p),
which s h o u l d be i n t e rp r e t e d as “ if p is a p r o p o s i t i o n , then so is p
p ”. So H func
tions as the class of p r o p o s i t i o n s . It was used in C u r r y [ 1 9 4 2 a ], B u n d e r [1969],
a n d o th e r s to block the d e r i v a t i o n of C u r r y ' s p a r a d o x . Aczel [1980] uses H as in
B u n d e r [1969] a n d in . / P .
T h e fact t h a t p z> p is derivable in P R O P is in te rp re ted in , / P as Hp b p id p.
This s h o u ld be in t e rp r e t e d as “ if p is a p r o p o s i t i o n , th en p =) p is d e r i v a b l e ”.
(ii) T h e s a m e f o r m u l a p 3 p is t r a n s l a t e d in . / F as F pp. T h e fact t h a t p => p is
a wiï of P R O P is expressed in .ƒ F by Lp I- L(Fpp) w hich s h o u l d be i n t e r p r e t e d as
“ if p is a type, then Fpp is a t y p e ”. T h e type Fpp is intuitively the function space type
p -> p. T h e fact t h a t p i p is d e r iv ab le in P R O P is in te rp re ted in .ƒ F by m a k i n g
the type Fpp “ i n h a b i t e d ” by the expression Ay.y (form ulas-as-types a n d terms-asd e r iv a t i o n s i n t e r p r e t a t i o n )
Lp h F ppUy. y).
(iii) Similarly, c o n s i d e r the f o r m u l a V a a ( P a ^ Pa) of P R E D . I n t e r p r e t e d in J E
this b e c o m e s
L.4 , F A H P b H ( E A ( À x . P x => Pa)).
T h e intuitive m e a n i n g of F.4HP is “ P is of type A -> H ”, t h a t is, P is a m a p from .4
into the p r o p o s i t i o n s and. hence, a p r e d ic a te on A. (In generalised type systems the
basis L . 4 , F 4 H P w o u ld be w ritten as the c o n t e x t A
P: A -► * p, see B a r e n d r e g t
[1992], especially the systems / P R E D a n d / P . ) T h e fact th at V a a ( P a =5 Pa) is d e
rivable in P R E D be c o m e s
L4,F.4HP h EA(/,x.Px
which is derivable in . / E .
(iv) T h e f o r m u l a V a a ( P a
3
3
Pa),
P a ) in P R E D t r a n s la t e d in , / G be c o m e s
L.4, F.4 LP b L(G.4( / a . P a 3 P a )),
776
H E N K B A R F N D REGT , M A R T I N MUNDI R, A N D W I L D E K K E R S
which s h o u ld be in te rp re ted as “ if A is a type a n d P is in A - * L. then G A( / . x. Px zdPx)
is a type". In the PTS la n g u a g e of / P this is
A : *, P: A -► * h ( \x : .4.P.v -> P.v) : *.
T h e fact th at V.vA(P.v 3 P.v) is a t a u t o l o g y is in t e rp r e t e d in
of the type G A (/.v. P.v 3 P.v).
.9'
G by the i n h a b i t a t i o n
L.4,F.4LP f- G A ( À x . P x => P.v)(/..vJ.y.y).
2.5. Notes, (i) ./0 /.s essentially J E plus the following :
I—L/l ■>,
bZIH,
and
t~LH
By the a x io m “ KLH ' one can interpret s e c o n d - o r d e r p r o p o s i t i o n a l a n d p red icate
logic. F o r example, by rule 5¡ o n e gets
\-EH(Àp.p -> p)
( = V/)
6 H.p -> p).
So one can q u a n tify o v e r p r o p o s iti o n s . By
o n e c a n derive p f- H p a n d even
p 1- H(Hp). Here one has a m i x t u r e of s t a t e m e n t s in the l a n g u a g e a n d in the m e t a
language. This gives p r o b l e m s in the s t u d y of c o m p l e t e n e s s a n d m a y b e it is better
to skip this a x i o m “ h Z l h T , as we have d o n e in the systems . / P, J E , . / F, a n d J G .
(ii) In the IC L 's not only t a u t o lo g ie s can be derived but also so-called syntactical
conditions. F o r example, in signature s one has f (a ) e TAi a n d P(f(a)) e FpRliD. These
translate as F A XA J \ A {a\~ A ^ f a ) a n d FA xA xf , A ^ i . F A ^ P h H (P( fa)), respectively.
T h e f o l l o w i n g l e m m a is u s e f u l f o r d e t e r m i n i n g t h e r e l a t i v e s t r e n g t h o f t h e f o u r
system s.
2.6. L e m m a . For all X , Y e T one has the following in A ( 5 ,
(i) F(KA)(K V) = K ( P X Y ),
L):
(ii) G X ( K V) = K ( Z X y ) ,
(iii) FA y = G A (K Y ).
P r o o f , (i) F(KA')(KV) = ;.r.5(KA')((KV) z) = / . z . E ( K X ) ( K Y ) = K ( P X Y ) , since
( K Y) z = À x . K Y ( z x ) = A.v.y = K Y.
(ii) G X ( K )') = á z . E X ( S ( K 3 Y )r) = À z . E X Y = K ( E X Y ) , since S ( K ° Y ) z =
/c.(K Y)c(zc) = Âc.Yc = y.
(iii) FA y = Â z . E X ( Y z) = A z .£ A (S (K > ')r) = G A ( K y ),
since
S(K Y ) z =
Àv.K Yv(zv) = Àv.Y(zv) = Y z.
□
2.7. P r o p o s i t i o n . The systems . / P . J E , J F. and J G are related as follows :
J F
*J G
J P
■» J E
where —* denotes nondecreasing strength , i.e., s
s 2 means that f o r all T. X
111
SYSTEMS OF I LLATI VE C O M B I N A T O R Y L O G I C
We will s h o w th a t if s, —►.s-2 in the d i a g r a m then every rule of s, can be
derived in .s2 .
(i) Case J P —►J E . T h e rules Pc, P¡, a n d PH follow from respectively E c, E t, a n d
5 h by the s u b s t i t u t i o n s of K.Y for X a n d KY' for Y.
(ii) C as e J P -> J F . T h e n Pc, P¡, a n d PH follow from Fc, F¡, a n d F, by the s u b
stitutions of K.V for X a n d KY' for Y a n d L e m m a 2.6(i).
(iii) C ase . / F - » , / G . N o w Fc, F¡, a n d FL follow from G c, G¡, a n d G L by the
s u b s t i t u t i o n of K Y for Y a n d L e m m a 2.6( iii ).
(iv) C as e J E - + J G . T h e n £ c, £¡, a n d E H follow from G c, G¡, a n d G L by the
s u b s t i t u t i o n of K Y for Y a n d L e m m a 2.6(ii).
□
N o w we will s h o w formally h o w the logics P R O P a n d P R E D can be in terp reted
in the illative systems. We start with P R O P .
2.8. D e f i n i t i o n . Let r be a closed term in /1(Z. L). T w o m a p s (for / = 1,2)
P roof.
m
a n d tw o m a p s
/ r : FpRop “ *■illative c o n te x t s
are defined by T a b l e 10. ( N o t e th a t these illative c o n t e x t s are effectively g r a m
matical c o n d i t i o n s on the variables ( p r o p o s i t i o n a l , individual) t h a t a p p e a r in a
proposition.)
T
able
10
<p
M l
r ; ( <p)
p
rp
H (rp)
<A => i
['AVr => LxVr
/;'(<//), /•,'(*>
¡ i Up )
M ;
rp
L(rp)
r i m r ;{-/.}
T h e r in the a b o v e definition a n d in 2.12 can be replaced by I (i.e., omitted). H o w
ever. in 2.15 we use it to derive a relation between the tw o in t e r p r e t a t io n s .
2.9. L e m m a . Let cp e IF,>RO,> and let
be the set o f (free) propositional
variables in (p. Then
(i) r 'r Up) = {H(rp,),...,H(rp„)J.
(ii) r ; U p ) = {L(rpj).....L(rp„)}.
(iii) H i/). Hi// \ - f P H (cp z d i//).
(iv) U p , Li// b>,, UF(pi/j).
(V) T'r (cp) h , P H [(/>];.
( v i) T ; ( ( p ) h > F L [</>];.
P r o o f , (i), (ii) follow by in d u c tio n on the length of (p.
(iii), (iv) follow by PH a n d Fl .
(v) follows by (i) a n d (iii).
(vi) follows by (ii) a n d (iv).
2 . 10. D e f i n i t i o n . Let A c FPROp-
(i) [A V r = I M ' r j t p e A}.
(ii) [¿I ] 2 = {[</>], .xv | (p e A) with x (p a fresh v a riab le ch o sen uniquely for cp.
□
77S
HENK BARENDREGT, MARTIN BUNDER, AND W IL DEKKERS
(iii) r r( A ) = ¡ / '(</» | </) G zl|,
(iv) r'r(A,ip) = r r( A i r r(q>).
If zl is a set of a s s u m p t i o n s in a d e d u c t i o n in P R O P o r P R E D , then [zl]' is the
set of t r a n s la t e d a s s u m p t i o n s . N o t e th a t [</?]“ in a sense represents a class. Each
[</)],.yv then represents the c o n d i t i o n th a t [(/)]; is in h ab ited , c o r r e s p o n d i n g to the
fact th a t (p is a s s u m e d to be true. T h e T'r(A) are g r a m m a t i c a l c o n d i t i o n s required
for the variables of A.
In the p r o o f of the following p r o p o s i t i o n there is an u n e x p e c te d difficulty in
s h o w i n g the s o u n d n e s s of m o d u s ponens. T h e difficulty can be a v o i d e d by a trick,
which however, d oes not w o r k for P R E D as we will sec a n d explain.
2.11. P r o p o s i t i o n ( s o u n d n e s s of the i n t e r p r e t a t i o n s for P R O P ) . Let A u {cp\ <=
Fp r o p ■ Then one has the following for all closed r.
(l) A \~ prop (P ^ M r * ^
h/P
•
(ii) A I—prop <P => 3 Aƒ g A [ [ z l ] 2, T;( A, (p) \-JY [</?]2 A7/ ] .
P r o o f , (i) By in d u c t io n on the d e r i v a t i o n of A I—Pr Qp (p in P R O P .
If cp g A , then the result holds by the first rule for b in / / P .
If A I- (p is a direct c o n s e q u e n c e of A b \¡j => cp a n d A b i// then the i n d u c t i o n
h y p o th e s is ( IH ) implies (leaving out the super- a n d subscripts)
[ J ] , /'(zi, i/y 3 (p) b [i//] 3 [ip],
[zl], T(A, i//) I- [i//].
Therefore, by rule Pc o n e has [ J ] , T(A, ip). / (*//) I- [</>]. If { q x____q } is the
set of p r o p o s i t i o n a l variables o c c u r r i n g in i// but n ot in (p or A a n d p is a p r o p o s i
tional variable o c c u r r i n g in </), then we have
[/I], T(A, cp), H(rq , )........H ( r q j b [</>],
where H (rp) g T(A,cp). S u b s t i t u t i n g p for each of q {, ___ qm, we o b t a i n
[.J], /
If A b cp is A b \p
one has
3
(Zl,
cp) b [(/)].
/ a n d is a direct c o n s e q u e n c e of zl,i// b /, then by the IH
By L e m m a 2.9(v)
/(i//) b H 1 l/y].
Hence, we have [zl], T(A ), T(i//), / ' ( / ) b [i//
3
/ ] . So by the definition of T
[zl], T(A ). / ’(<// 3 / ) b [l// 3 / ] .
(ii) S a m e as for (i) except t h a t for every p e A u {(p\ in the d e r i v a t i o n [p]¡. will
have a t t a c h e d a variable x p a n d every c o m p o u n d p r o p o s i t i o n a c o m p o u n d term.
F o r example, if (p e A , then [zl ] 2 b [<p] 2.\(p a n d in the m o d u s p o n e n s case if
[zl],/'(zl,i/y 3 (/)) b,,. (F[i//][(/?])M
and
[zl], /'(zl, i/y) b
[i//] /V,
SYSTEMS OF I LLATI VE C O M B I N A T O R Y L O G I C
779
[zJ],r(zl,!//,i// =) ip) b > F (>](A///V).
□
then
(i) A S(E, L) is A(E, L) e x te n d e d by the e x t r a c o n s t a n t s A A 2,
P , f , g , a as so ciated with the s i g n a t u r e s of the m a n y - s o r t e d s t r u c t u r e of o u r e x a m
ple. Because we are going to in t e rp re t e m a n y - s o r t e d predicate logic with sorts
A j , A 2, it is useful to have a m o n g the free variables of the / - c a l c u l u s infinite sets
ŸÏ , Ÿ2, with y : = { x h y ^ z h . . . }. x , y , z d e n o t e a r b i t r a r y variables.
(ii) Let r be a closed term in A S(E, L). T w o m a p s (for / = 1 , 2 )
2.12.
D efin itio n ,
[ ] r • FpRED • Ls(—, L)
and a m ap
FpRi D
are defined by T a b l e s
11
illative c o n te x t s
a n d 12.
T
1
able
11
ru )
wi
X
.A;
AjXj
XJ
a
a
fs
0
m
r(s)
i
r<s), /(o
gSt
T
<p
Pi
=>X
V.xA'i//
able
12
Mr'
[</>];
r(P[i]r‘)
r(P[í]r2)
[*A!lr = Cx3r'
F[<A]r2M;
^i(/A', • Mr) G/I,(A.v, • [i//];)
¡'Up)
no
/(•A), /!*)
r(iA) —{-4,-v,}
(iii)
= ( L A l , L A 2 , F A l A 1ƒ, FA 1{FA2 A I )g, F A , H (r oP), A , a>,
r r2s = <L,4,, LA 2 , F A l A i f , FA , ( F A , A ¡ )g, F A , L ( r . P ) , A . a ) ,
and
= Ï r.su \ ^ 2x i } where x 2 e i 2
___ •
s o m e variable.
« i
T h e definitions Í ' s. a n d r r‘ s of c o u r s e refer to o u r e x a m p l e of a m a n y - s o r t e d
p red icate calculus with s ig n a t u r e s.
It is essential to a d d A 2x 2 to r irs (and if required, similarly, for o t h e r sorts) to
avoid the p r o b l e m of possibly e m p t y d o m a i n s . It w o u ld be n a t u r a l that
I- P R E D (P
I r.s» [ ^ ] r > ^ ( ¿ 1 , <p) H > r [ < / > ] / .
780
Hl N k B A R E N D R E G T , M A R T I N B U N D E R . A N D W I L D E K K E R S
H o w e v e r , this is not true. T h e similar p r o b l e m for PT S's (sec B a r e n d r e g t [ 1 9 9 2 ] )
was first n o te d by E. B a r e n d s e n [1989]. T h e p o in t is th at in o r d i n a r y (minimal,
intuitionistic, or classical) logic it is always a s s u m e d th at the universes A , , A 2, . . . of
the s t r u c t u r e are s u p p o s e d to be n o n e m p t y . F o r exam ple,
(V.ya (R\- - Q)) -> (V.vAP.v) -> 0
is p r o v a b l e in P R E D , but only
logic one also allows s t r u c t u r e s
atised by P e r c m a n s [1949] a n d
p r o b l e m tu rn s up in the case of
valid in s t r u c t u r e s with A ^ 0 . In so-called free
with e m p t y d o m a i n s . T h is logic has been a x i o m M o s t o w s k i [1951]. W h a t is u n e x p e c te d is t h a t the
m o d u s p o n e n s (cf. the p r o o f of P r o p o s i t i o n 2.14).
2.13. Lemma. Let (p g pr i-d ■
I f t g TAj, then in .(/ Z or .ƒ G one has T(/), r'rs 1- Aj\_t~\lr .
(ii)
r rl s ,r(cp)
i <fr h[</>],!.
(iii) r l J ' ( < p ) \ - ' fC L[cPy ; .
(i) By in d u c tio n on the length of /, using the s t a t e m e n t s A l a1FAl A lJ\
a n d FA{(F A 2A {)g in F rl s .
(ii) If (p = Pt where 1 g TAi, then by / ' r‘v I— F.4,H(r P), (i), a n d / (</?) = F{t)
we have r lr s , F(cp) \~f I H(/*(P [ r ] )) as required. T h e r e m a i n i n g cases are as in
L e m m a 2.9(v).
(iii) As in (ii) a n d L e m m a 2.9(vi).
2.14. P r o p o s i t i o n (s o u n d n e s s of the i n t e r p r e t a t i o n s for P R E D ) . Let A u { ( p } <=
FPRtD; then the following hold for all closed r.
P roof,
□
(i) .1 t- PRED (P ^ ^ r.'v ’
]r ’
(p )
[ (p ] r •
(ii) A l-,,REiD (p => r r2' +, [ z l ] r2, r(A,(p) \ - , c [(/)]2 A/ for some M.
P r o o f , (i) T h e i n d u c t i o n on the p r o o f of A I—preo (P is as m
p r o o f of
P r o p o s i t i o n 2.11 (i ). W h e n , in the case of m o d u s p o n en s, te rm s A lx l for v a r i
ables .v, g FV(i p) — FV((/?) need to be r e m o v e d from the left of the b we replace x ,
by a. If te rm s A 2x¡ for x ¡ e FV(i p) — F V((/)), we replace x¡ by x 2 a n d n o te that
a 2 .v2 g n :; .
(ii)
T h e in d u c t io n on the p r o o f of A t-,>RHD (P is as *n l ^e p r o o f of P r o p o s i
tion 2.11 (ii) with G [i//](/..\\[(/)]) instead of F[i p~\\_(p\. Variables m a y need to be
replaced as in (i).
2.15. P r o p o s i t i o n (the relation between the tw o interpretations), (i) For ip g
one Inis K [(/>],! = [</)]¿ r .
(ii) For ip e FPR|.d one has K[</i]r‘ = [<p]¿ r .
P r o o f , (i) By i n d u c t i o n on the length of (p.
F |> r o i >
K [ p ] ' = K</■ƒ?) = [ p ] ¿ r ,
K[<p => i/o,! = K([<p]r' 3 [./,],') = F|K[<p]r')(KW
rl ).
by L e m m a 2.6(i), so by the IH
K |>
=> <PVr =
F ( [< /> ]£ , r ) ( | > ] ^
r) =
[ (P => < A ]k r •
(ii) By i n d u c t i o n on the length of cp as in (i) b ut also using L e m m a 2.6(ii).
□
§3. Completeness of two of the interpretations. In this section we derive c o m
pleteness for the i n t e r p r e t a t i o n s [ ]*: P R O P - + y P a n d [ ] ' : P R E D - > . / £ . W e c o n -
SYSTEMS OF I LLATI VE C O M B I N A T O R Y L O G I C
781
j e c t u r e c o m p l e t e n e s s for the i n t e r p r e t a t i o n s [ ] 2: P R O P -> . / F a n d [ ] 2: P R E D ->
. / G . but we have not been able to prove it .1
We start with the p r o o f of the c o m p l e t e n e s s for / / Z relative to P R E D . This
occupies s u b s e c tio n s 3.1-3.11. T h e p r o o f for . / P relative to P R O P in 3 . 1 2 - 3 . 1 4
p roceeds in a similar way but is m u c h easier.
Completeness for / / Z relative to P R E D . We will s h o w
V r [ r r;s , [ z i ] r , r(zi, (p) h y z [i/>]r ] =>
11
r»Ri£D
Here the s i g n a t u r e s a n d the c o n t e x t r r‘;v+ are as in 2.2 a n d 2.12; again the result
can easily be generalised to o t h e r signatures.
It is sufficient to s h o w
h /S
M
r
=> A
h p R l i D </>
for a special r. We c h o o s e r = I, i.e., we o m i t r a n d we prove
/Y
i [ip]1 => b{>RliD(p ,
>r(A,(p)
a
where the definitions of r s!,+ a n d [ —] ‘ are o b t a i n e d from 2.12 by every w h ere
o m i t t i n g r.
T h e p r o o f goes in tw o steps. First we define a grammar in o r d e r to an a ly z e the
terms M such t h a t rs1,+, [ z l ] 1, T(zl, cp) \-^z M. T h e n the c o m p l e te n e s s is s h o w n by
m e a n s of this analysis. In s te a d of
we shall m o stly write K
3.1.
R e m a r k . T h a t it is not o b v i o u s t h a t c o m p l e t e n e s s holds is because not only
t r a n s l a t i o n s of t a u t o lo g ie s can be derived in the I C L ’s, but also syntactical s t a t e
ments. Let F = r y , [ A ] l,r(A,(p). T h e n we can derive in . / Z s e q u e n ts of the form
r h [<p],
where [(/?] is (the t r a n s l a t i o n of) a logical formula, but also
r h H(Pi),
where H (Pt) c o r r e s p o n d s to the syntactical s t a t e m e n t Pt e FPKIiD in the m e t a
language. In
r
b LA¡
LA¡ c o r r e s p o n d s to the fact th at A¡ is one of the sets in the s i g n a t u r e s. Even a
m i x t u r e is possible
Hp
b /) 3 Hp.
U sing the g r a m m a r it will be s h o w n t h a t such mixed s t a t e m e n t s d o n ot interfere
with the logic. T h e t r a n s l a t i o n s of logical f o r m u la s will form a class & ( p r o p o s itio n s )
in o u r g r a m m a r a n d the o t h e r s t a t e m e n t s a class # ( g r a m m a t i c a l conditions).
1After the paper had been sent to the jo u r n a l we succeeded in proving completeness for [ ] 2: P R O P
J F , but completeness for [ ] 2: P R E D -*■ . / G is still open.
782
H E N K B A R E N D R E G T , MA R T I N B U N D E R , A N D W I L D E K K E R S
3.2. D
( c r a m m a r for derivable s t a t e m e n t s in . / £ )
efinition
•
h
i
—
.7 2 *
a
/y, = y
.? = P.î\ Z
= L.4
A
.4,^
)
5 (K .y })(K ^),
Z M .U a ,///') £ ( K / / ) ( K : ^ ) L ( K ^ ) ,
/J : = ! M 3 N e /J ; N ~/h] iW J »
—
// = [ M | 3 N g / / | N
M
1
A/J,
= {A/1 3/V g # 1/V =„ A / },
C = . ' / kj ?j .
3.3. R e m a r k s , (i) All ele m e n ts of 0 are in /i//-normal form if we read K M as
/V.A7. So all elem ents of (! have a (unique) /i/7- n o r m a l form.
(ii)
a n d ^ d o not e x h a u s t the possible t h e o r e m s of J Z , e.g.,
H(H/?) h H(Hp z> p), Hp, H(Hp) \~ H(p => Hp).
C with n o r m a l form /V, a n d let 1/ be a variable. T h e n we
write // £i¡t) FV(A/) for it $ FV(/V).
N o w in 3 . 5 - 3 . 1 0 we state s o m e technical results t h a t are needed in the c o m p l e t e
ness proof. T h e m a i n p r o p o s i t i o n is 3.10, sla t in g th at only te rm s in C c a n be derived
from r ] ,+; this gives the required analysis.
3.5. L e m m a , (i) Let '// = . '7X, J 2, /A
or C. Then
3.4. N
o tatio n.
Let A/
g
VVG 1f \ t¡ G
, X¡ G 1¡ =: \v[.\'i := / ], .v2 := N ] g ^ •
(ii) Let H = / T ^ . f or (!. Then
W G 1! \ t¡ G e^, X, G 1/ =5
\v[ a 1 : = / j , a 2 : = i 2 ] G ^ •
(i) B y a simple induction.
(ii) F r o m (i) a n d
P roof,
A/,
= fhj
A7/?, Aí,
= a,,
!<>i
A/-> => A/, [.y :=
/V,]
□
M 2 [ v := /V,]
3.6. L e m m a . Let c X { - ■X n = Vn
lh M f o r some A/ g C and some constant c. Then
/i g {1,2} and M = cY, • • • Yn with Y¡ = fhj X¡.
P r o o f . By C h u r c h - R o s s e r a n d the fact that all ele m e n ts of (! are in ßtj - n o r m a l
form.
□
3.7. L e m m a , (i) P s1,+ c r/J.
(ii) # n # = 0 .
(iii) ÿ n J* = 0 .
P r o o f , (i) F.4 , !./ = ^ .4 j (/ .a , . / ! , ( / a j )) g # b e c a u s e /I { ( ƒ a t ) g
Moreover,
F.4 j(Fv42 A , )c) =
Z A ,(/.a , . Z A 2( á x 2. A
,( cjx t a2))) e
Finally, F.4,HP = 5 . 4 , ( / . a , . H ( P a , )) G # b ecause H(P.v,) g &
(ii) By an easy induction.
(iii) F r o m (ii) by C h u r c h - R o s s e r a n d the fact t h a t the ele m e n ts of (9 =
in /^//-normal form.
u
are
□
783
SYSTEMS OE I LLATI VE C O M B I N A T O R Y L O G I C
3.8. L e m m a , (i) [ — ] 1 : P R E D —►zls(.E,L) induces bijections
étm
[ —] 1 : FPRHI) -h►.JA
I f (/) G F PRHD, i hen [ ( /? ] ' G / A and F(cp) c : '//.
(iii) I f A c: FPRIiD and ip G FPRED, then P s1,+ u [zl ] 1 u / ' ( zl,
(ii)
) cz
<T.
P r o o f , (i) a n d (ii) b y e a s y i n d u c t i o n s .
(iii) from (ii) a n d 3.7(i).
3.9. L e m m a . I f cp e FPRI:D, a A|
M
P roof.
□
g
V a ', /Ai
g
TAi, a,
then
g
1[-v,- := [/aJ'] = [>[.va* := U,]]1.
By an easy in d u c tio n .
□
3.10. P r o p o s i t i o n .
r t- a/, r a c => m g c .
P roof.
(*)
We use i n d u c t i o n lo a d i n g a n d s h o w
r b- A/, r c ( P & u t lh] F V ( D => A/ g ( ' & 1/
FV(A/)
by i n d u c t i o n on the d e r i v a t i o n of / I— A7. We only c o n s i d e r the three Z-rules; the
o t h e r two rules are easy.
Case E c. / ’ I— A/ /.s F h Y F as a direct consequence o f I h E X Y , I' I— X K
By the 1H one has 5 A Y g C7, u <£/jr, F V ( Z A V ) & A’ F g C, t/
F V (Ar K). We d is
tinguish tw o cases a c c o r d i n g to the form of 5 A' Y, using L e m m a 3.6.
Subcase ^ c.(a). A = .4,, V = /.x¡.0 with 0 e (1. N o w A ¡ V e C & u $lh) ¥ \ ( A i V).
So V = t¡ where /, g
a n d u $ F V ( / (). Hence, by L e m m a 3.5(i)
A/ = ( / a i. O ) t i = 0 [ a , := /,]
g
C
and
u i f „ FV(0[.\-, := f,]),
u $ F V ( / a , . 0 ) u FV(/,).
Subcase 5 c(b). A = Kp, Y = KO, with p g ¿A, 0 e C. N o w Y V = Ö. where
u FV(O).
Case E x. r h- A/ is F h E X Y as direct consequence o f I' h LA\ I\ X x h- Ya
with X $ FV(T, A, Y ).
By the IH on e has LA' g (! a n d u $ fht FV(LA). We distinguish tw o cases a c c o r d
ing to the form of A.
Subcase 5¡(a). .V = A,. N o w a is a n y variable, so we m a y a s s u m e th at a g i¡\
u =É a. T h e n A a g C a n d u £ F V M . a ) ; hence, by the IH o n e has
because
Ya
g C
and
u i fU] FV( Y a ).
Let Ya = 0 g C . T h e n M = E A ^ á x . O ) , where u $ftl¡ F V ( / a . O ) .
Subcase 5¡(b). A' = K p. T h e n I \ p h Y a . O n e has a ^ FV(T, p), u $pn FV(T, p)
because i/ $lhj FV(LA'). So by the IH o n e has
Ya = 0 g ( ' ,
w here a £ FV(O), u ÿ FV(O).
Hence, Y = KO a n d M = £(Kp)(KO), where z/ ÿ FV(pO).
784
I I F NK B A R E N D R E G T , M A R T I N B U N D E R , A N D W I L D E K K E R S
Case Z H. F h M is r b* H(-EA'Y’) as a direct consequence o f I' b LA',
r , X x h H( YX )
with X $ FV(T, A\ Y).
T h e p r o o f is similar to the p r o o f for case E t. We n o w get H ( Y x ) e C ; hence,
Y x e i? a n d
M = H(EA¡(/.x¡.p))
with u $ F V(/.x¡.p) in case E H(a),
M = H ( E ( K p {)(Kp2))
with u $ F V ( p , p 2) in case 3 H(b).
□
3 . 1 1. P r o p o s i t i o n (com pleteness for J E relative to P R E D ) .
r s1-+, [ d ] l ,r(d,</>) i- j E í (p V => ^ ^ pred ^P"
F si,+ c=
by L e m m a 3.7(i) a n d r(A,cp) a 7/ by L e m m a 3.8(ii). Hence, it
is sufficient to prove
P roof.
(**)
ro ^iA V
M , Ty a
3?, M
=
[ i / ? ] 1 = > zl I- p r e d
(P-
W rite r =
, [ ^ ] 1• T h e n T c: ¿P; hence, M e C by P r o p o s i t i o n 3.10. T h e p r o o f of
(**) goes by induction.
Case 1. r h M because M e T.
M = [(/?]' g J by L e m m a 3.8(i), so as .Jf c 7/> a n d
n 7j = 0 , M e [ z l ] 1. As
the elem ents of [zl ] 1 are in nf as are those of J® o n e has [cp~\[ e [zl ] 1 a n d by
L e m m a 3.8(i) ip e zl. Hence, zl l - m .D (p.
Case 2. F I— M is a direct consequence o f f h N and M = N.
N o w Ai = M = [</)]' a n d by the IH for N o n e has A 1~,>R,.D (p.
Case £ c. F h M is F h Y V as a direct consequence of F
E X Y . i h XV.
As E X Y e 0 by P r o p o s i t i o n 3.10, w'e need c o n s i d e r only 4 cases.
Subcase 5 c(a). X = A h Y = a x ¿.p. N o w F h A¡V e C by P r o p o s i t i o n 3.10. T h e r e
fore. V = t¡ = \_t\ ] 1. Since p e /A we can write p = [_i//]1 bv 3.8(i ). Therefore, [(/)]’ =
Y V = û x , p ) [ t Aiy = [i//]l [.Y(- := [ / a , ] 1] = [<//[.ya - := tAJ ] ' . So
M
'
^ [ i / / [ - y Ai : =
/Ai] ] ‘ .
Hence, (p = i//[aa ' := tAJ . E X Y = EA¡(Áx¡.p) = [Va:a 't//] 1. By the IH o n e has
A I- pred V a a,i//. S o zl 1—PRED i//[aa ' := fAi] = cp.
Subcase £ e(b). X = K p n V = K p2 . T h e n [f/>]1 = A/ = YK = p 2 e
a n d by
3.8(i), we can write p { = [</>!]1. Therefore, E X Y = 5 ( K p , ) ( K p 2) = \_(pi => rp]1. By
the IH o n e has
A
pred
I-
{P\
—5 (/^-
Also. A'K = p i = [(/j,]1, so by the IH one has
•
1 ' pred
(P i
•
Therefore, it follows by m o d u s p o n e n s th at
A
I-
pred
(P-
Subcase Z c(c). X = A h Y = Áx¡.q. Since F h A , V e C\ one has V e
There
fore, M = Y V = q [ x ¡ : = K] e rS. So A/ ^ [</>]' for all cp by L e m m a 3.7(iii).
785
SYSTEMS OF I LI. ATI VE C O M B I N A T O R Y L O G I C
Contradiction.
Subcase 5 c(d). X = K/?, Y = Kq. N o w M = Y V = cy, so M ^ [cp] 1 for all (p.
Contradiction.
Case 5¡. r \- M is I h- E X Y as a direct consequence o f /' h L X , r , X x h- Yx
with X ÿ F V ( r . X, V).
As .EX y = [(/)]1 e ^ we need c o n s i d e r only 2 cases.
Subcase 5¡(a). X = A h Y = Áx¡.p. Let p = [ i//] 1. T h e n M = [ V a a,i//] *. N o w x is
a n y variable, so we m a y a s s u m e a* g Y¡. T h e n X x = A , a g
As r , X a h Y x o n e has T, X a I- [ i / / ] So zl I pred & by the IH. N o w a does not
o c c u r in T, so
1 ^ PRED Va Aií//.
Subcase ^¡(b). X = K p 1? Y' = K p2 . Let pj = [<Pi]\ p 2 = [ ^ 2 ]1* T h e n M =
L(Pi 3 ^ z ] 1- N o w r , X a h y.v is r , p , h p 2. So by the IH o n e has z l , ^ l~pRbD (/?2 .
Hence,
^ ^ PRED ^1 —> ^2*
£H. r h y\/ is r h H(ZXy)
r, Xa h H( Ya) vvif/i a £ FV( T,X, y ).
Case
as
a direct
consequence
of
f h LX,
T h is case is n o t a p p lic a b le because M $ 0*.
□
Completeness for ,/ P relative to PROP. T h e p r o o f of this c o m p l e te n e s s follows
the s a m e p a t t e r n as the p r o o f of the c o m p l e t e n e s s for / / E relative to PRED, b ut it
is easier. As in t h a t p r o o f it is sufficient to t a k e r = I, i.e., we o m it r.
3.12. D e f i n i t i o n ( g r a m m a r for d e riv ab le s t a t e m e n t s for ,/P).
= 1 ' I 0> ID
<8 =
W 9 \ & z>
(9 = 9 \ P .
ÿ , a n d & are then defined as in Definition 3.2.
3.13. P r o p o s i t i o n .
r h , P M, r c <9 => M
g
0.
By i n d u c t i o n on the d e r i v a t i o n of T h /P M. T h e v a r io u s cases c o r r e
s p o n d to the tw o initial cases a n d cases ITc(b), £¡(b), a n d 5 H(b) of the p r o o f of
P r o p o s i t i o n 3.10.
□
3.14. P r o p o s i t i o n (com pleteness f o r J P relative to P R O P ) .
P roof.
[zl ] l , r l(A, cp) \—fp
[(/?]1 => zl
I- prop (P-
T h is consists of the initial cases a n d cases ^ c(b), £ c(d), ^¡(b) of the
p r o o f of P r o p o s i t i o n 3.11 a n d the E H case with K p , for A' a n d K p 2 for Y'. As be
fore [ —] l is 1-1 a n d
= 0 a n d if X g (9 then T'(A') c= <$.
□
P roof.
§4. Remarks and open problems.
4.1.
R e m a r k s , (i) T h e systems ,/P , J E , ,/F , a n d J G are based on /i//conversion. It is possible to w o r k with v a r i a n t s of these systems based on /ic o n v e r s io n only. C h a n g e the rules for J E as in T a b l e 13 (see next page) a n d similarly
786
HENK BARENDREGT, MARTIN BUNDER, AND W I L DEKKERS
for . / P , . / F , a n d J G . T h e n in the p r o o f of the c o m p l e t e n e s s for J E relative to
P R E D only m i n o r c h a n g e s need to be m a d e , like replacing A¡, X , X x , a n d ßt] by
ÀXi.AiXi, À x . X , X , a n d ß , respectively.
T a b le
13 ,/5 .
X e r
r h A';
r h a\ X =p y
r h £(/x.x)(/x.y), r h (/a.atjk
r, X h y, r h l ( X x . x ) , x t fv(d
r b y;
r h (/a. y )K;
r h 5(/A.A:)(/A.y);
r, Ar h h y, r b l U x . x i a ¿ f v ( D => r h h ( ^ ( à a .X ) ( â a . y »
Similar c h a n g e s s h o u l d be m a d e in the p r o o f of the c o m p l e t e n e s s for , / P rela
tive to P R O P . T h e r e a d e r is invited to verify all details.
(ii) T h e a d d i t i o n a l primitive L a d d e d to A( E) was n ot strictly necessary. We
could have used the definition L = W E a n d simplified o u r g r a m m a r for derivable
s t a t e m e n t s in J E in Definition 3.2 in the following way:
& = P&\ \ Z A i{ÁXi. & ) \ Z ( K & ) ( K # ) ,
=
A & lZ A ^ x ^ lZ íK # )^ ).
N o t e t h a t n o w L(K,^) = Z ( K ^ ) ( K . ^ ) , so L(K.^) shifts from ({/ to & \ Similarly for
, / P , H can be defined as WP as was d o n e in C u r r y [1 942a].
(iii) In the w o r k of Seldin a n d o t h e r s L is defined as FEH, w h e re E is a u n i v e r
sal class. U n d e r this definition H/> a n d L(Kp) are interderivable, but o u r p r o o f of
P r o p o s i t i o n 3.10 fails.
(iv) T h e title of the p a p e r refers to c o m b i n a t o r y logic, but the systems used are
based on l a m b d a calculus t h r o u g h o u t . T h e illative systems c o u ld have been based
on c o m b i n a t o r y logic using an a p p r o p r i a t e b r a c k e t a b s t r a c t i o n a lg o r it h m .
(v) F o r historical a n d o t h e r r e m a r k s c o n c e r n i n g the c o m b i n a t o r s 5, P, F, a n d
G, see H indley a n d Seldin [1986; C h a p t e r 17 for Z a n d P, C h a p t e r 13 a n d C h a p
ter 15 for F, a n d C h a p t e r 16 §§C, D for G].
4.2. Open problems. T h e following is a list of o p e n p roblem s.
(i) Is the i n t e r p r e t a t i o n [ ] 2: P R O P -»• J F c o m p l e t e ? Is the i n t e r p r e t a t i o n
[ ] 2: P R E D —►J G c o m p l e t e ?
(ii) Is J F a c o n s e rv ativ e extension of J P a n d J G a c o n s e r v a t iv e extension
of J Z ?
(iii) A d d i n g as a x i o m LH to J Z one c a n in te rp re t s e c o n d - o r d e r p r o p o s i t i o n a l
a n d predicate logic. Is this i n t e r p r e t a t i o n c o m p l e t e ?
(iv) Is the extension J 0 of J Z in 2.5 c o m p l e t e ? Are similar e x te n s io n s of J F
and J G complete?
4.3. R e m a r k . T h e system J 0 is consistent. T h is can be seen in the following
way. Let
<§ = r I L A¡ I LH I Z\ H I Z A \ X y / f j ) \ E H ( X y . 9 ) \ S ( K&) ( K&) \ A { 8 \ H #,
# = { M \ l N e 9 \ N =PnM}.
SYSTEMS OF I LLATI VE C O M B I N A T O R Y L O G I C
787
T h e n one can prov e
r h Al f c ^ = > M e «
So if I—A//, then A/ has a n o r m a l form. Hence, the system is consistent, because
Q = (à x . x x )(à x . x x ) c a n n o t be derived. This weak consistency result was pro v ed
by a similar m e t h o d in B u n d e r [1983b].
REFERENCES
P. A c z e l [1980], Frege structures and the notions o f proposition, truth unii set, The Kleene sym posium
(J. Barwise, H. J. Keisler, and K. K unen, editors), N o rlh -H o lla n d , A m sterdam , pp. 31 59.
H. P. B a r e n d r e g t [1984], The lumhila calculus, its sy n ta x and semantics. Studies in Logic and the
F o u n d a tio n s of M athem atics, N o rth -H o lla n d , Amsterdam.
----------[1992], Lam bda calculi with types, H andbook o f logic in com puter science, Vol. //(S . Ahramski,
D. M. G a b b a y , and T. S. E. M a ib a u m , editors), Oxford University Press, L o n d o n and New York.
E. B a r e n d s e n [ 1989 J, Representation o f logic, data types and recursive fu n ctio ns in typed lambda cal
culi, M asters Thesis, D e p a r tm e n t of C o m p u te r Science, C atholic University, Nijmegen.
M. W. B u n d e r [1969], S et theory based on com binatory logic. Ph.D. thesis. D e p a rtm e n t of M a t h e
matics, University of Amsterdam.
----------[1973], .4 deduction theorem fo r restricted generality, N otre Dame Journal o f Formal Logic,
vol. 14, pp. 341-346.
----------[1974], Propositional and predicate calculus based on combinatory logic, N otre D ame Journal
o f Formal Logic, vol. 15, pp. 2 5 - 3 2 .
----------[1976], The inconsistency o f F *,, this J o u r n a l , vol. 41, pp. 4 6 7 -4 6 8 .
----------[1983], Predicate calculus o f arbitrarily high finite order, Archiv f ü r M a th L ogik und Grund
lagenforschung, vol. 23, pp. 1—10.
---------- [1983a], A one axiom set theory based on higher order predicate calculus, Archiv f ü r M a th
L ogik und Grundlagenforschung, vol. 23, pp. 9 9 -1 0 7 .
----------[1983b], A weak absolute consistency p ro o f fo r some systems o f illative combinatory logic, this
J o u r n a l , vol. 48, pp. 771-776.
A . C h u r c h [1932, 33], A set o f postulates fo r the foundation o f logic. Annals o f M athem atics (2),
vol. 33. pp. 3 4 6 - 3 6 6 an d vol. 34, pp. 8 3 9 -8 6 4 .
----------[1941], The calculi o f lambda conversion, Princeton University Press, Princeton.
H. B. C u r r y [1930], Grundlagen der kombinatorischen Logik, Am erican Journal o f M athem atics,
vol. 52, pp. 5 0 9 -5 3 6 ; pp. 7 8 9 -8 3 4 . (In au g u ral dissertation)
---------- [1931], The universal quantifier in combinatory logic. Annals o f M athem atics, vol. 32,
pp. 154-180.
----------[ 1932], Som e additions to the theory o f combinators, Am erican Journal o f M athem atics, vol. 54,
pp. 551-558.
----------[1933], Apparent variables fro m the standpoint o f combinatory logic. Annals o f M athem atics,
vol. 34, pp. 381-404.
----------[1934a], Functionality in combinatory logic, Proceedings o f the N ational A cadem y o f Sciences
o f the United S ta tes o f America, vol. 20, pp. 5 8 4 -5 9 0 .
----------[1934b], Some properties o f equality and implication in combinatory logic, Annals o f M a th e
matics, vol. 35. pp. 8 4 9 -8 5 0 .
----------[1935], Foundations o f the theory o f abstract sets fro m the standpoint o f combinatory logic,
Bulletin o f the Am erican M a th em a tica l Society, vol. 40, p. 654. (Abstract).
----------[1936], First properties o f functionality in combinatory logic, Tôhoku M a th em a tica l Journal,
vol. 41, pp. 371-401.
----------[1942a], Some advances in the com binatory theory o f quantification. Proceedings o f the N a
tional A ca dem y o f Sciences o f the United S ta tes o f America, vol. 28, pp. 56 4-569 .
----------[1942b], The com binatory foundations o f mathematical logic, this J o u r n a l , vol. 7, pp. 4 9 - 6 4 .
----------[1942c], The inconsistency o f certain fo rm a l logics, this J o u r n a l , vol. 7, pp. 1 15-117.
IL B. C u r r y and R. F e y s [1958], C om binatory logic, Vol. 1. N o rth -H o lla n d , Amsterdam.
788
HENK BARENDREGT, MARTIN BUNDER, AND W IL DEKKERS
H. B. C u r r y , J. R. H i n d l e y and J. P. S k l d i n [1972], C om binatory logic, Vol. 2, N o rth -H o lla n d ,
Am sterdam .
J. R. H i n d l e y and J. P.
S eldin
[1986], Introduction to combinators and X-calculus, C a m b rid g e U n i
versity Press, L o n d o n and New York.
S. K l e e n e and J . B. R o s s e r [1935]. The inconsistency o f certain form al logics, Annals o f M a th em a tics
(2), vol. 36, pp. 6 3 0 -6 3 6 .
M . L ö h [1955], A solution o f a problem o f Hen kin, this J o u r n a l , vol. 20, pp. 115-118.
A. M o s t o w s k i [ 1951 ]. On the rules o f proof in the pure functional calculus o f first order, this J o u r n a l ,
vol. 16, pp. 107-111.
W. P e r e m a n s [ 1949], Een opmerking over intuitionistische logica. Report Z W - 16, C W I, K ruislaan 413,
1098 SJ Am sterdam .
FACULTY OF MATHEMATICS AND COMPUTER SCIENCE
CA TH O LIC UNIVERSITY
NIJMEGEN, THE NETHERLANDS
E-mail: henk(fl cs.kun.nl
E-mail: [email protected]
FACULTY OF INFORMATICS, DEPARTMENT OF MATHEMATICS
UNIVERSITY OF W O L L O N G O N G
NSW AUSTRALIA
E-mail: M a rlin . Bunderfr/ info-gw.uow.edu.au
Sorting: T he first address is Professor B arendregt’s and Professor D e k k e rs’s; the second address is
Professor Bunder's.

Download Report