A NOTE ON IRREFLEXIVE~ ASYMMETRIC AND INTRANSITIVE KRIPKE MODELS
by
Henrik Sa.hlqvist Oslo
PREPRJNT SERIES - Ma.tema.tisk institutt, Universitetet i Oslo
It is well knovm that certain schemata of modal logic correspond to certain conditions on the relation of the Kripke models. E.g .. , one can prove that all instances of DA =>OOA are valid in a model structure if and only if the relation of the structure is transitive.
In [1], S.K. Thomason mentions the problem of whether there is a schema of modal logic that corresponds in this sense to the rela- tion being irreflexive. This problem is closely related to a re- sult announced by Lemmon ffiLd Scott in [2], namely, that there is no schema Z such that a formula A is provable in the minimal (semi-)normal modal logic K with Z as added axiom schema if and only if A is valid in all irreflexive model structures.
The proof was to be presented in later parts of [2]. They con- jectured that the same is true of asymmetry and anti-symmetry.
We shall present here a simple proof that no schema corresponds to any of these properties, nor to a certain generalization of the notion of intransitivity, or any property entailed by it.
The notation is mainly taken from [3]. VVnen U is a set, R a binary relation over U and V a function from propositional variables to subsets of U , :f{ = (~ ,RX) is called a model structure (world system, frame) and ?~
=
(U~,Ru,Vu> a model.When
u
1.e
=u
1c ,
R7.e
= R:rt ,ll
is said to be a model onJc .
For u E U-ze. ~~A
u is defined in the usual way and reads "A is true at u in
u
II •l=ti A means Vu E Uu. I=UA u
'
and reads "A is true inU,
II •If .)fii A for some u , then
U
is said to be a coun termodel for uA • 't=:J{A means
rtU
onJt
~ l=U.A ~ and reads "A is valid in:.R'
11 •vVhen Z is a schema,
F~Z
means: For all instances For typographical reasons we sometimes writeu->~
and u* f=*A for l=u7~A •
A of
z '
u j= A for
K is the system that has modus ponens and necessitation as rules and the axiom schema
in addition to axioms from some axiomatization of propositional logic with modus ponens as the only rule.
The main point of this paper is the following lemma:
LElVIJ):IA 1. If a formula B has a countermodel, then it has an asymmetric (and hence irreflexive and anti-symmetric) and intran- sitive countermodel.
Proof. Let
11=
(U,R,V) and be such that .¥u B •u
0
Construct a new countermodel U-'~~ = (u-x-,Rl(-,v-x-) as follows:
i)
u.,~ consists of all finite seq_uenc8su. E U for
]. 0 < i < n and
(Call them R-seq_uences.)
u.Ru. 1 ]. J.+
(u ,u1 , ••• ,u) where o n for 0 < i < n-1 •
ii) (u0 , ••• ,um)R*(u0 , ••• ,un) holds iff (u0 , ••• ,un) =
(u0 , . • .,um>*<un> , where -:f is the "clash" or concaten- ation operation of sequences.
iii) For atomic formulas A, (u0 , • • • ,un> E V*(A) iff un EV(A).
We shall prove that if (u0 , ••• , un) E U""c , then (u0 , ••• ,un> l=* A iff un l= A , or, when u' denotes the last element of
u'~ E U'~: u* 1=* A iff u 1 F= A , for all formulas A • The proof goes by induction:
at~ For atomic formulas A
u* I=* A <-> u* E v-x-(A) <-> u' E= V(A) <-> u' l= A • I) u ~~ ~* .., A <-> I u * I=* A <-> luI F A <-> u' l= I A •
" ) u -)(- 1=-)(- A " B <-> u * I=* A & u -X- I=* B ~-> u ' I= A & u ' I= B
<-> u' I= Af\B.
0) u* 11'- OA <-> V(u0 , ••• ,un) EU*(u*R-K-(u0 , ... ,un)-(u0 , ••• ,~)1=*A)
<-> \f(u0 , ••• ,un) EU'~((u0, ••• ,un)=u**(un> _, uni=A)
<-> \i'un E U(u'R un _. un i= A) <-> u' != OA • Hence we have
and intransitive.
7£.*
Af(u
>B.
0
And R* is asymmetric QED.
Instead of this induction we could have used the p-morphism theorem. Let
Define U Uo
ping from U* to
mean
ax
1 , ••• , xn_1 ~ xRx1 A x1 Rx2A ••• Axn_1 Ry • It is easy to check that the map- which takes u* into u' (the last ele- ment of u* ) is a p-morphism, reliable on every propositional letter. See (3].The model constructed in the above proof has the form of a tree, and, of course, is not just asymmetric and intransitive. It has all properties which can be expressed by a sentence of the form
for m
I
p ,or of the form (2) m
AxRu1 ".u1Ru2A ••• Au 1Ry _. /1. (z. =u.)),
m- O<i<m l l for 2 < m .
Let us call the property of satisfying (1)m~p , for, m
I
p ,m,p-intransitivity, and the property expressed by (2)m, for 2_::m~
m,m-intransitivi~.
Then we see that:
irreflexivity is 1,0-intransitivity;
asymmetry is 2,0-intransitivity;
intransitivity is 2,1-intransitivity.
If we restrict ourselves to connected model structures, the class of model structures obtained from arbitrary model structures by the construction in the above proof is determined up to isomor- phism by the L -sentence
w1 (.OJ
(3) A (1) A J\(2)
mfp m~p 2<m m
i.e~ , we have:
J4.J ( )
LEMMA 2. r. is connected i.e. ,
u.,.,c
is of the form Uu and sa tis-o
fies (3) as an ordinary relational structure for the first order language with one binary relation symbol ((UX,RJi;l=(3)) iff~
is isomorphic to a model structure obtained by the construdtion in the proof of Lemma 1.
Proof. If
Jr:
is isomorphic to a model structure obtained by the construction, then it certainly is connected and satisfies (3).If
J{
is connected and satisfies (3), then use the construction on.k
itself, starting with some u0 from which all points in the structure can be reached, and obtain 1{~~- Then .7{ ~ J{-r' is
For .J( l= (3) im- plies that if two ~-sequences, at least one of them of length
greater than 2 , have the same last element, they are equal. If two R~-sequences have the same last element and neither of them has length greater that 2 , then they are trivially equal, since all ~-sequences begin with u
0 and IU Rv u •
0 -'to 0
This means that we can state the full strength of the proof of Lemma 1 as:
LEMMA 3. If (*) is any sentence implied in L w1w by (3), then if a modal formula has a countermodel, it has a countermodel sa- tisfying
(*).
A class of model structures ~ is said to determine a modal logic S if for all formulas A 1-s A <-> V X(
J.C
E 1; ---t \=.1< A) • A proper~ty of model structures is said to determine a logic if the class of model structures having the property determines it.
THEOREM 1. If(*) is any sentence implied by (3), K is determined by the property of satisfying ( •'f) ("determined by ( *)").
Proof. We have 1-K A <:-> '\/ ]{. f:J(A • Hence, one way is immediate.
If ~KA , then A has a countermodel, and hence, by Lemma 3, a countermodel satisfying
(*).
COROLLARY. There is no schema Z such that K ~ KZ and KZ is determined by (*), for any (*) implied by (3). In particular we can take as (*) the sentence expressing irreflexivity, or asymme- try, anti-symmetry or intransitivity.
COROLLARY. Every class of model structures between the class of all ]{ and the class of
X
satisfying ( 3) determines the logic K.A schema Z is said to correspond to a property if ~~Z iff J{
has the property.
THEOREM 2. There is no schema Z corresponding to any property which can be expressed by a sentence
(*)
implied by(3),
except the trivial property of just being a model structure.Proof. Suppose there was such a schema Z • There exists a model not satisfying
(*).
It must be a countermodel for some instance of Z • Hence, by Lemma 3, this instance has a countermodel sa- tisfying(*),
which contradicts the assumption.We now admit more than one relation in the model structures and more than one necessity operator. The necessity operator be- longing to a relation R is denoted fB) , etc. Kn is the n-modal system (system with n necessity operators) where we have the K- axiom and necessitation for all operators. Below, ~ is supposed to range over model structures with the appropriate number of re- lations, ~< being one of them.
THEOREM
3.
For any sentence (*) implied by(3),
the property that R~ satisfies (*) determines Kn • For any (*) implied by(3),
except the trivial sentence, no schema in the language of Kn corresponds to the property that R~ satisfies(*).
Proof. We have to generalize our Lemma 3. Given a model
?.l
= ( U ,R, ••• , V) , let T be the union of the n relations ofU.
Let U* be the set of all (finite) T-sequences beginning with u0 •
For all relations
s
ofU
9 define byiff u* 2 = u**<u''> 1 2' and U ' 1 S u' 2 • For atomic A let u* E V*(A) iff u' E V(A) •
Then for all S of
1.-i
9 the inductive clauselli))
is proved as []) is proved in Lemm~ 1.Could we add an axiom schema to some system other than K , a system which is determined by some property, and get a new sys- tem which is determined by, for example, irreflexivity and the given property? Is there a schema corresponding to irreflexivity together with some other property to which a conjunct of the sche- rna corresponds?
We do not try to answer the general question but restrict ourselves to systems obtained by adding to K some of the axiom schemas G' m,n,p,q
In [2] there are given completeness results for all these systems, with respect to the properties expressed by
We may argue roughly as follows (deta~ of the argument is given
below)~
We have the system KG I m,n9p,q • (Or a system with several G1 - schemas added to K.) All theorems in the system are valid in all model structures satisfying (in the following we
omit the parameters m,n,p~q)~ hence in all model structures sa- tisfying g 1 and conjuncts of ( 3) which are consistent with g' • Conversely, given a non-theorem of the theory, it has a counter- model
U
satisfying g 1 • "Unravel"U
as in the proof ofLemma 1, getting
U* .
Take the closure of I) ~ 0* with respect to1'\J
g I o The new model uv behaves like (}0
U*
, and satisfies g1 and some of the conjuncts of(3).
The conju..n.cts of(3)
(or more gene- rally, the sentences implied by (3)) which are "saved" by thisconstruction, no matter what countermodel we started with, express properties which cannot be matched by any schemas added to the system.
Examples show that not all conjuncts of (3) which are consistent with g1 are saved. The difficult problem then is to determine what conjuncts of (3) are saved.
'I/} ·)I;
We have to be more precise about the phrase "the closure of (..{., with respect to g1 " ·
Let Uu = (Uu ,R ~ uu ) , l(u·:<-)
0 0 0
the (i+1)st element of u* , u' before, and u*lj
=
(u , ••• ,u. 1>
0 J-
be the length of u*
'
be the last element of u. l
u*
be as
If
U
satisfies g1 and u0 E U , thenm,n,p,q
U
u also satis-0
fies g' m,n,p,q • Unravel
1t
from u0 and getU* .
For all t that we can "find" by the existential quantifier in
0
· d f 11 ~ * E u* , 1·f
g ' g1 ven any u, v, w , an or a u" , v m,n,p,q
3:j~O: u*lj = v-'<-lj
and
l(u*)
=
m+n+j, l(v·x·)=
p+q+j , u1=
v'=
t0
then identify u* and v* and the trees above them (i.e. delete
v* and the tree over it from
U*
and substitute "arrows" point-"'-"
ing to v* with "arrows" pointing to u7E- )
.
We get ~u • Since u* and v* are copies in ,,uk
of the same point, t in
0
'
1_f,
the trees over u* and v~* in 11.,* are isomorphic and the valuation over the trees is the same. Hence, for all formulas A 9...,
if ( u0 , ••• 9 un) E
U ,
i. e. ,U , ?1./*
and are equivalent.""
We shall prove that
'lt
satisfies g I m,n,p,q o Let u *, v* , w* E U 9v* = u
* * <
vk 1-m ' • • • ' vk 1-1 )w* = u
* * <
wk 2-p , ••• , v11 c2-1 >so we have v Rm v and w RP w and
k 1-m-1 k 1-1 k 2-p-1 k 2-1 '
=
wk 2-P-1=
u' •Since is satisfied by
11
there is a t E U0
that and wk 2-1 R q t 0 • I.e., there exist in
x1 9 • • • 'xn-1 'Y 1 ' • • • 9 Y q-1 such that
such
u
v* -*
<
x1 9 • • • 9 xn_1 , t 0 ) E u* and wi<- -*<
y 1 , ••• , y q-1 , t 0>
E u* • But these two R1L- sequences must have been identified in the con-""
struction of
f/.t •
Hence there is a t* EU
such that v* Rnt*0 0
and
We may now get theorems of the following kind:
K + the schema G' m, 1,o,o
( 0
m0
A :::> A) is determined not only by the property expressed by g' m,1 but also by the property,o,o expressed by g' 1 '' A (1) , •
m, ,o,o o<m'<m m ,o
K + the schema G' (0 A :J Op A) o, 1 ,p,o
by the property expressed by g' o,1,p,o expressed by g' 1 1\ A (1) I •
o, ,p,o o<m' m ,o But these theorems are rather limited.
is determined not only but also by the property
More general cases are either difficult to analyse or are such that every conjunct of (3) is violated by construction from some countermodel.
If we knew enough about the different systems to be able to choose our countermodels suitably~ the matter might be considerably sim- plified.
REFERENCES
[1] S.K. Thomason: Semantic analysis of tense logic.
JSL, to appear.
[2] E.J. Lemmon and Dana Scott: Intensional Logic. Preliminary draft of initial chapters by E.J. Lemmon.
Mimeographed, Stanford University, July 1966.
[3] Krister Segerberg: An Essay in Classical Modal Logic.
Uppsala 1971.