UNIVERSITY OF CALIFORNIA, LOS ANGELES
Oct 19, 1968
DEPARTMENT OF PHILOSOPHY
LOS ANGELES
,
CALIFORNIA
90024
Dear Professor Prior,
In
your Egocentric Logic [
No
Ø
s
Aug 68], you
appear
to wonder whether the
quant
nal
definition of
p has any quantifier-free consequences not derivable
from the quantifier-free axiom schemas Q1-Q9. It does not.
If
we take
w
W F
,
to be a model in the
now familiar
Kripke way (W
worlds,
w
0
W, if
P
is a sent. constant, F(
P
)
f
W) and give the natural definitions
of truth in
+
w
W F
,
with the special clause:
Q
M
is true in
+
w
W F
,
iff there is exactly one
w
N
0
W s.t.
M
is true
in
+
w
N
W F
,
then,
it can be shown that your Q1-Q4 (plus the usual
nt)
set. Since the definition of
se for th
e
propositional
quantifiers), any quant-
free con
sequence of that definition is also valid
and hence already derivable from Q1-Q4
The
co
y of normal forms (there may be an
eve
n
easier
argument some
other
way).
P
1
P
be distinct sentence letters. Then there
are
exactly 2
m
state-descriptions
of the form
0
1
P
1
v
...
v
0
m
P
m
where each
0
i
is either
a
blank (or
alternatively ¬¬) or the negation sign. Let
us call the state-descriptions: S
1
...
S
m
. A
reduced model-desc
ription
(in
P
1
...
m
ction of the form
'
v
"
1
S
1
v
...
v
"
2
m
S
2
m
v
$
1
S
1
v
...
v
$
2
m
S
2
m
where (i)
'
= S
j
for some 1
#
j
#
2
m
each
"
j
and each
$
j
is either a blank or the negation sign (for all 1
#
j
#
s
m
$
j
is
a
blank then so is
"
j
(for all 1
#
j
#
2
m
), and (iv)
"
j
is a blank
for the j (1
#
j
#
2
m
) such
that
'
= S
j
.
LEMMA
1:
If D
is a reduced model-description (in
P
1
...
P
m
),
then there is a
model
in
which D is true
and all other reduced model-descriptions
in
P
1
...
P
m
are false.
Proof:
+
0,S
j
,
or
+
1,S
,
for 1
#
j
#
2
m
+
0,S
,
0
"
j
+
1,S
,
0
"
j
$
j
w
=
+
0,
,
If
is a sentence letter, and
x
= 0 or
x
= 1, then
+
x
,S
,
0
F(
P
) iff S
j
/
P
*
[Editors note] Im uncertain of this word.
2
An easy induction completes the proof.
LEMMA
2:
If
M
is any quantifier-free formula, there exists a
formula
P
such that
[
P
is
a
of reduced model-descriptions
or
P
is
z
sentential contradiction)] and
P
is provably equivalent to
M
.
Proof:
p
ut
M
into a provably equivalent form in which no modal operator
(including
Q
) stands within the scope of another. That th
is
can be done in S5 is a
familiar
fac
se especially three principles:
(
Q
P
:
~
Q
P
) [this is used to
confine
across a
Q
],
[
Q
(
p
w
q
)
{(
qp
v
~
(
p
:
q
))
(
Qp
v
~
¬
q
)
(
Qq
:
~
¬
p
))}]
q
to be a conjunction by putting the
original operand
into
disjunctive normal form and then using
the
principle to distribute],
/
(
Q
(
~
p
v
r
)
:
(
~
p
v
Qr
)) [this is
used
to confine
Q
to the part of its operand (when a conjunction)
which
contains no modal operators]. To see how
to reduce the degree of an operator
consider
a formula Op
'
where Op is either
~
or
Q
, if Op is
~
we put
'
in conjunctive
normal
for
m and distribute, the disjuncts can be put in the form A
w
B where A is
modally
closed (every sent. let.
in
the scope of an operator) and B is modally open-free.
Using
the first of the three principles we
formula
)
is modally closed;
/
(
)
:
~
)
)
v
(¬
)
:
~
¬
)
). Thus
/
:
~
A) and hence
/
[
~
(A
w
B)
:
(A
w
~
B)]. This will give a formula provably equivalent to Op
'
and of lower
degree
(unless Op
'
already had
no overlay
*
). If Op is
Q
put
'
normal
form
and distribute by
principle two. Components of the form
v
B with A modally
closed
and B modal-free.
Again using the fact that
/
A
:
~
A and the third principle we
obtain
/
(
Q
(A
v
B)
:
v
Q
B) which gives s
formula of lower
(unless Op
'
had
no overlay). Here are sketches of the proofs for the second and third principles.
show
(
p
w
q
)
(
Qp
v
~
(
p
w
q
))
(
Qp
v
~
¬
q
)
(
Qq
v
~
¬
p
)
From left to right:
case 1: Ass
Qp
v
~
(
p
:
q
)/
(
p
:
p
w
q
Q
(
p
w
q
)
case 2: Ass
Qp
v
~
¬
q
)/
(
p
:
p
w
q
/
case 3: As in case 2
3
|
| From right to left:
Ass
Q
(
p
w
q
), the following cases are by Q2
|
|
case 1:
~
(
p
w
q
6
p
v
q
/
~
(
p
:
p
w
p
,
|
~
(
p
:
q
)
|
case 2:
~
(
p
w
q
6
p
v
q
)/(1)
(
p
6
¬
q
,
(
q
6
¬
p
)
|
(
p
w
q
)/
p
w
q
|
Subcase a:
p
|
|
show
Qp
By the Ass and Q2 we have 2 more cases
|
___
|
| case a
1
:
~
(
p
w
q
6
p
)/
(
p
w
q
:
p
|
2
:
~
(
p
w
q
6
¬
p
)/
¬
p
/¬
p
but this contradicts
|
|___
the hypothesis of the subcase
|
|
show
¬
q
e have 2 more cases
|
___
|
| case a
3
:
~
(
p
w
q
6
q
~
(
p
6
¬
p
)/¬
p
which contradicts
|
|
hyp. of the subcase
|
4
:
~
(
p
w
q
6
¬
q
)/
(
q
6
¬
q)
/
~
¬
q
|
|___
|___
Subcase b:
q
show
(
~
p
v
r
)
(
~
p
v
Qr
)
|
From right to left, Ass
Qr
,
p
/
~
((
p
v
r
)
r
Q
(
~
p
v
r
)
|
From left to right, Ass
Q
(
~
p
v
r
(
~
p
v
r
)/
p
/
~
((
p
v
r
)
r
)
|___
by the Ass and Q4
/
~
p
v
Qr
M
ably equivalent form
M
without overlay. Now
take
each subformula
of
M
er the form
or
Q
)
, put
)
into
standard
disjunctive
normal form (each disjunct a state-desc. in the sent. lets of
by
z
(if
)
is a sent. contradiction). Then distribute
in the usual
way and distribute
Q
by principle two. One iteration may be required since principle two produces
some
new formulas of the form
(I take
as
an abb. for ¬
~
¬, a little
/
p
:
p
may be
required
along the way). We now
have a formula
M
O
provably equivalent to
M
N
whose
atoms
are: the sent. lets of
M
,
S
j
(where S
j
is a
state desc. in the sent. lets of
M
),
Q
S
j
(S
as before),
z
,
Q
z
,
. Put
M
O
into a provably equivalent disjunctive normal
form
in
these atoms. If a disjunct of this complete formula contains
z
,
z
or
Q
z
, replace
the
disjunction
by
z
. Now
omit any disjunct, ¬
z
, ¬
z
, and ¬
Q
z
and re-arrange remaining
non-
z
disjuncts in the form of a reduced model-description. If either
condition (iii) or
(iv)
of a reduced model-description
is not satisfied by any disjunct, replace that disjunct
by
z
. If what remai
ns c
ontains a non-
z
disjunct, drop all
s, otherwise replace the
whole
formula with
z
. Each of the foregoing transformatio
ns is bas
ed on a provable
equivalence. The final formula is the
P
called for in Lemma 2.
**
[Edito
rs note] Kap
etter introduced the notion of satisfaction with respect to an
assignment, but it has to be that
f
tion
7
P, to
every
propositional variable.
f
P
P
then refers to
the
satisfaction of
M
by an assignment just like
f
except that
it assigns to P t
7
P.
4
LEMMA
3:
If
P
is a disjunction containing each of
the reduced
model-descriptions
P
is provable.
Proof:
is provably equivalent to the tautology
formed by
adding additional disjuncts
in
the same atoms. these added disjuncts will all have the
model-descriptions
but
will violate either (iii) or (iv) and thus be provably false.
THEOREM
:
If
P
is valid (and quantifier-free),
P
is provable.
Proof:
By
lemma
2,
P
is provably equivalent to a disjunction of red. model-descs,
which
by
lemma 1 and the validity of
P
must contain all red.
model-descs (in
the sent. lets. of
P
, and which is thus by lemma 3 provable.
[I have assumed, what is easy, that all theorems are valid.]
The
method of proof also, of course, yields decidability for
t.-free
formulas.
On
the last
few
pages, you claim that certain formulas (e.g. Q6) do not follow
from
what amounts to the definition of
Q
in what you call quantified S5. Since there
is
a complete [and decidable] axiomatization for this
5 with prop. quants]
(complete
in
the sense of yielding all [and only] those theorems that are
true in every
model: with the clause
P
M
is satisfied by the
assignment
f
+
w
W F
,
iff for
all
7
P
f
W,
M
is satisfied
by
f
7
P
P
in
+
w
W F
,
.
)
and
since the definition of
Q
does define
Q
in
that
Q
M
is true when exactly
the
conditions on p. 1 of this letter [p. 1 also of the transcription (Ed.)]), all valid
formulas
must be theorems. Since the formulas you claim underivable are clearly valid,
I
must conclude that
you have in mind a defective
axiomatization for quantified S5. My
own axiomatization is as follows:
1.
P[
M
6
Q
]
(
P
M
6
P
Q
]
2.
P
M
6
Q
where
Q
is the resu
lt of replacing all free
in
M
by
free occs of some formula
'
.
***
[editorial comment] The sentence in brackets in the text appears in red at the top of p. 7 of the ms.
5
3.
/
M
6
P
M
M
4.
M
where
is a tautology
5.
~
[
M
6
Q
]
(
~
M
6
~
Q
]
6.
~
M
6
M
7.
M
6
~
M
where
is modally closed
8.
P[P
v
Q(Q
6
~
(P
6
Q))
Rules: Modus Ponens, Universal Generalization, Modal Generalization
My
completeness proof g
ms and is thus quite awful. I hope
there is an easier proof.
Probably
the system that you
had in mind lacked
Axiom 8, Kripke also seems
top have missed it at the end of his March 59 J.S.L. article (so that the added
remark
on the last page is not strictly correct).
Possibly
what you meant at
bot. p. 206-top p. 207 was that there
is no formula
M
,
for whi
M
v
Q
M
, or even just
M
le. This is true and is most
easily shown by model-theoretic methods.
The
fac
. S5 is decidable (and this that there exists a complete
axiomatization)
[oops! Ive misjudged the length
of this letter
***
] follows from
the fact
that
quant.
S5 is
isomorphic to a subtheory of 2
nd
order monadic predicate logic, which
is
known
P
is a sent. constant (or var.) of quant. S5, let
P
N
be
a
uniquely
determined monadic predicate constant
(or var.). Now we define
a translation
of formulas of quant. S5 into those of 2
nd
ord. monadic logic.
Trans(
P
P
N
x
(
x
Trans(
M
v
Q
) = (Trans(
M
)
Trans (
Q
))
Trans(¬
) = ¬ Trans(
M
)
Trans(
P
M
P
N
Trans(
M
)
Trans(
~
M
x
Trans(
M
)
It is
easy to show that an assignment
(of props to sent. vars)
f
sats in quant S5
M
in
+
w
W F
,
iff fv{
+
x
w
,
} sats in 2
nd
gic
Trans(
M
+
,
. What is more difficult
for me was establishing that the
intrinsic
tization given above works.
Since your
Q
,
and
O
are interdefinable and the quantifier-free axioms you
give are
equivalent on the basis of the defs, what I have said for
Q
goes also for
W
and
O
.
6
ve resorted to Lewis (?).
I
am sorry
not to have had the
opportunity of meeting you when you were here,
my
colleagues were all most e
nthusi
astic about your visit. I hope you will come to
California again soon.
Sincerely
David Kaplan
PS Could you put me on your reprint list?
