Part 2 overview

Welcome to Part 2!
We will cover: 7. Logics, soundness, completeness. Canonical model for K . 8. Soundness and completeness for more frame classes. 9. Finite model property, via ltrations. Decidability. 10. Modal -calculus. Thanks to Nick Bezhanishvili and Clemens Kupke (who taught part 2 in 2009 and 2010) for major contributions to the slides, exercises, and solutions.

115

7. Logics, soundness, completeness

Recall (denition 9) the notion of validity of a modal formula A in a class C of frames: A is valid in C if A is true at every world of every model whose frame is in C . Each class C of frames gives a logic: Log(C ) = {A : A is a modal L-formula valid in C}. Log(C ) (the logic of C ) comprises the laws of chemistry of C . We want a more concrete characterisation of Log(C ):

C comes straight from the application, so is too close to it. C is probably too big/abstract (to automate etc). We want the underlying rules controlling the form of Log(C ). We want to reason about formulas directly.

Reasoning via standard translation is possible especially with modern rst-order theorem provers but clumsy, unnatural, and doesnt take advantage of modal nature of formulas.
116

Hilbert systems
We will use Hilbert systems to capture the logics of classes of frames. A Hilbert system consists of 1. axioms 2. rules of inference. The axioms are given truths. They should be valid in some given class C of frames. The inference rules allow us to derive new truths from old. If the formulas above the line in a rule are already derived, the rule allows us to derive the formula underneath the line. (See next slide.) Rules should be chosen so as not to lead us from truth into falsehood. Formulas derived from C -valid formulas should also be valid in C . Hilbert systems are simple, powerful, exible, and in common use. (But not suited for practical reasoning.)
117

The Hilbert system K

The most basic Hilbert system for modal logic is called K . Note: K depends on L (our set of propositional atoms). Pick any two distinct p, q L. K -axioms All propositional tautologies (valid propositional formulas). Eg., p q p, (p q ) ((q r) (p r)), etc. Normality: (p q ) (p q ), for p, q as above. K -rules (if youve got the top, you can derive the bottom). Here, A, B are any formulas and p L is any atom. A, A B modus ponens (MP): B Universal generalisation (UG): A (also called Necessitation) A A Substitution (Sub): A(B/p) A(B/p) is the formula got by replacing all occurrences of the atom p in A by B . Eg. (p p q )(q/p) = q q q .

118

Proofs in a Hilbert system

Denition 50
Let H be a Hilbert system. We write H A, and say that A is a theorem of H , if there are formulas A1 , . . . , An such that

An = A each Ai (1 i n) is either

an axiom of H or is obtained from some of A1 , . . . , Ai1 by a rule of H .

The sequence A1 , . . . , An is called a proof of A (in H ), or a derivation of A (in H ), of length n.

119

Example of a proof
Example 51
Let A, B be any modal formulas. Then K (A B ) A. For, 1. p q p 2. A B A axiom (tautology) Sub(1) UG(2) axiom (normality) Sub(4) MP(3,5)

4. (p q ) (p q ) 6. (A B ) A

3. (A B A)

5. (A B A) ((A B ) A) is a proof of (A B ) A in K , of length 6.

In practice we often omit lines 1 and 4, and justify lines 2 and 5 by instance of tautology, instance of normality.

120

Useful properties of K
Lemma 52 (essentially MP)
Let A, B be formulas. If K A and K A B then K B .

Proof.
Suppose that X1 , . . . , Xn1 , A is a proof of A (in K ), and Y1 , . . . , Ym1 , A B is a proof of A B . Then by MP, X1 , . . . , Xn1 , A, Y1 , . . . , Ym1 , A B, B is a proof of B . We will use this later, justied by MP.

Exercise 53

So as far as K is concerned, we can write (A B C ) without worrying whether we mean ((A B ) C ) or (A (B C )), etc.

If A B is an instance of a tautology, show that K A B .

Exercise 54 (important)
Show that K A B (A B ) for any formulas A, B .
121

Logic generated by a Hilbert system

In this course, all Hilbert systems will have at least the axioms of K (they can have more axioms than K even innitely many more) exactly the inference rules of K : that is, MP, UG, and Sub.

Denition 55
1. The logic generated by a Hilbert system H is the set of all theorems of H : {A : A a modal formula, H A}. We denote this set by Thm(H ), or simply by H . 2. A modal logic is a set of the form Thm(H ), for some Hilbert system H . (Strictly, it is called a normal modal logic.) The denition is entirely syntactic. Aim: nd classes C of frames and Hilbert systems H such that Log(C ) = Thm(H ). Then we get a syntactic handle on validity. Many people nd this very impressive.
122

Soundness and completeness for K

We begin with the simplest case:

H = K , the basic Hilbert system.

C is the class of all frames. So Log(C ) is the set of all valid formulas.

We are going to show that Log(C ) = Thm(K ) that is, the logic of the class of all frames is just K . And here it is:

Theorem 56
A formula is a theorem of K i it is valid.

is called soundness. Proofs are sound: they do not prove false things. is called completeness. The proof system can prove all valid formulas.
123

Soundness of K
Soundness is easy. Its really just an exercise!

Proposition 57 (soundness for K )

Any theorem of K is valid. Proof. We prove a bit more. Let F = (W, R) be any frame. Claim 1. Any axiom of K is valid in F . Proof of claim. All propositional tautologies are plainly valid in F . Proposition 8 showed that (p q ) (p q ) is valid in any frame. So all K -axioms are valid in F . Claim
124

Proof of soundness ctd.

Claim 2. The rules of K preserve validity over F . Proof of claim. Suppose that A and A B are valid in F . Let p be any atom and C any formula. We show that B , A, and A(C/p) are valid in F . So let M = (W, R, h) be any model on F . Let t W be arbitrary. As A and A B are valid in F , we have M, t | = A and M, t |= A B . So plainly, M, t |= B . If u W and R(t, u), then M, u | = A (as A is valid in F ). But u was arbitrary, so M, t |= A. Let N = (W, R, g ), where g (p) = {w W : M, w |= C } g ( q ) = h( q ) for each atom q = p. We made p true in N just where C is true in M. So (exercise) M, w |= A(C/p) i N , w |= A for all w W . But A is valid in F . So N , t |= A. Hence M, t |= A(C/p). Claim
125

Proof of soundness ctd.

An easy induction on the length of a proof now shows that every K -theorem is valid in F . Try it yourself; details in theorem 75 later.

Completeness is harder. . .

126

Why is completeness harder?

We want to prove that if a given formula A0 is valid then K A0 . How? Two possible ways: 1. Assume A0 is valid. Show K A0 by constructing a proof of A0 in K . (How?!) 2. Assume K A0 . Show A0 is not valid, by constructing a model in which A0 is true at some world. Either way, we have to construct something. This is always tricky. It turns out that (2) is viable. (Easier to build innite things!) But what will the model be made of? What will its worlds be? Answer: syntactic objects namely, sets of formulas! But rst we try to give the idea, by having a look at a model.

127

Descriptions of worlds in a model

Let M = (W, R, h) be any model. For each t W , let t be the set of all formulas true at t in M: t = {A : M, t |= A}. t is a full description of t in modal logic. ( delta.) We try to represent t by this set t . (It doesnt matter what t actually is, after all.) So we form a new set of worlds: W d = {t : t W }. This W d is the set of all full descriptions of worlds in M. It is made of sets of formulas: syntactic! u d

128

Can we make a sensible model on W d ?

one suggested by the original model M, but made without peeking at M?

First, try to dene an assignment hd into W d . Let p be an atom. The description t of some t knows whether p is true at t: M, t |= p p t .
d

t Here, we know M, t |= p and M, t |= q , because p, q t . So why not let hd (p) = { W d : p }, for each atom p L. Then p is true at i its in !
129

Accessibility relation on W d ?
In M, we know that if R(t, u) and M, t |= A then M, u |= A. That is, if R(t, u) and A t then A u .
d A B A B

So R(t, u) leaves traces in t , u ! So why not try: for , W d ( gamma), let Rd (, ) i for every A, if A then A . This all makes sense, thinking of the as full descriptions of worlds. Anyway, we have dened a model Md = (W d , Rd , hd ).
130

Md is well-behaved
Lemma 58 Proof.

It turns out that the full descriptions making up Md describe themselves in Md (so (Md )d = Md ): For every formula A and W d , we have Md , |= A i A . An easy induction, using that for all , W d and formulas A, B : 2. A i A / 1.

3. A and B i A B

4. if A and Rd (, ) then A

5. if A / then there is with Rd (, ) and A / . These properties are easily seen to be true, if you remember that every W d is of the form t for some t W . See lemma 70 for a similar proof done in full.
131

The real story

This is all very well, but we needed a model M to start with. Were given only that K A0 , and we need to make a model satisfying A0 .

Still, this Md gives us a clue: why not build a model MK (say) whose worlds are sets of formulas!

Dene hd , Rd as above. Establish the 5 properties in lemma 58 (dry but necessary). Then we can prove MK , |= A i A , for all A and all sets included in MK . Show A0 is contained in some set in MK .

Then A0 will be true at ! We will have our model. But which sets of formulas do we include in MK , for this to work? Answer: maximal consistent sets of formulas.
132

Consistency preliminaries
Let (Gamma) be a set of formulas (maybe innite!). The following denitions are good for any Hilbert system H .

Denition 59
If A is a formula, we write H A if there are formulas B1 , . . . , Bn (for some n) such that H B1 . . . Bn A. Possibly, n = 0. So if H A then H A for any . Idea: H A says that A follows (is provable) from formulas in . These formulas need not be valid.

Example 60
{p, p q } K q , because (p (p q )) q is a propositional tautology, so K (p (p q )) q . Of course, p, p q are not valid!
133

Consistency
Denition 61 (consistency)
is said to be H -consistent if H . is said to be consistent (with no H stated) if it is K -consistent.

Exercise 62
Show that a set of modal formulas is H -consistent i H (A1 . . . An ) whenever A1 , . . . , An . This may be a nicer characterisation of consistency.

Example 63

{A, B, (A B )} is (K -)inconsistent, because (p q (p q )) is a tautology, so by (Sub), K (A B (A B )).

{p, q, r} is consistent, because otherwise, K (p q r), so by proposition 57, (p q r) is valid which it isnt.
134

Maximal consistent sets

Denition 64
A set of formulas is said to be maximal H -consistent (an H -MCS) if it is H -consistent but no larger set is H -consistent. A maximal consistent set (MCS) is a maximal K -consistent set. A clue to why MCSs are interesting is the following:

Exercise 65
Let M = (W, R, h) be any Kripke model. Let t W . Show that t = {A : M, t |= A} is a maximal consistent set. This suggests we should choose maximal consistent sets to put in our model.
135

So our full description model Md was made of MCSs!

Canonical model
Denition 66 (Canonical model for K )
1. Let WK = {all maximal (K -)consistent sets}. 2. For , WK , dene RK (, ) if for every formula A, if A then A . 3. For each atom p L, dene hK (p) = { WK : p }.

Let MK be the Kripke model (WK , RK , hK ). We call MK the canonical model for K . We call FK = (WK , RK ) the canonical frame for K . In the following, we show that the canonical model works. It gets a bit technical. But essentially we are establishing that 1. the ve properties of lemma 58 hold 2. A0 is a member of some MCS Look out for these points as we go along.
136

Extending a consistent set

Useful lemma

Lemma 67
If is consistent and A is a formula, then at least one of {A}, {A} is also consistent.

Proof.
Otherwise, there are B1 , . . . , Bn , C1 , . . . , Cm with K A B1 . . . Bn and K A C1 . . . Cm .
B, say C, say

Now K (A B ) [(A C ) (B C )] we can derive it from a tautology by Sub.

But K A C as well. MP now gives K B C . This means that is inconsistent contradiction.

As K A B , MP gives K (A C ) (B C ).

137

Which formulas does a MCS have in it?

Lemma 68 (handy test)
If is a MCS, then for any formula A we have K A i A .

Proof.
If A then as K A A, we obviously have K A. Conversely, suppose K A. So K B1 . . . Bn A, for some B1 , . . . , Bn . Claim. {A} is inconsistent. Proof of claim. We have B1 , . . . , Bn , A {A}. Now the following is an instance of a tautology, so a theorem of K : ( B 1 . . . B n A) ( B 1 . . . B n A ) . By MP, K B1 . . . Bn A . Claim By lemma 67, {A} must be consistent. And {A} . But is maximal consistent. So {A} = . So A .

138

Some properties of MCSs

Lemma 69
Let be a MCS and A, B, B1 , . . . , Bn be formulas (for some n 1). Then: 2. A i A / . 1. A, B i A B .

3. If B1 , . . . , Bn then (B1 . . . Bn ) as well. Proof. 1. If A B , then as K (A B A), we have K A. By lemma 68, A . Similarly, B . If A, B then as K A B (A B ) (!), we have K A B , so by lemma 68, A B . 2. Suppose A, A . Now K A A . So K . That is, is inconsistent. So at most one of A, A is in .
139

Lemma ctd.
By lemma 67, {A} or {A} is consistent. By maximality, = {A} or = {A}. So A or A . Weve shown that exactly one of A, A is in . This is equivalent to what is required.

3. We show B1 , . . . , Bn (B1 . . . Bn ) , by induction on n. The case n = 1 is trivial. Let n 2. Inductively assume the statement for n 1. We prove it for n. So assume that B1 , . . . , Bn . By exercise 54, K B1 B2 (B1 B2 ). So K (B1 B2 ). By lemma 68, (B1 B2 ) . By inductive hypothesis, (B1 . . . Bn ) .

140

Truth lemma for canonical model

Lemma 70 (truth lemma)
For every formula A and every MCS WK , we have: MK , |= A i A . Proof. By induction on A. For , we have MK , | = and (exercise) . If A is an atom p, then MK , | = p i hK (p) i p . Inductively, assume the lemma for A, B . Then: MK , | = A i MK , |= A, i A / (by the inductive hypothesis), i A (by lemma 69(2), as is maximal consistent). MK , | = (A B ) i MK , |= A and MK , |= B , i A and B (by the inductive hypothesis), i A B (by lemma 69(1)).
141

Truth lemma: the case A

Now the big case: A. Inductively assume the lemma for A. Suppose A . Take any WK with RK (, ). By denition of RK , we have A . So (by inductive hypothesis) MK , |= A. As was arbitrary, by semantics of we get MK , |= A.

Conversely, assume A / . We want to nd a MCS containing A and with RK (, ). That is, should contain 0 = {A} {B : B }.

142

Truth lemma: the case A ctd.

Claim. 0 = {A} {B : B } is consistent. Proof of claim. Assume not. So there are B1 , . . . , Bn such that K A B1 . . . Bn . Now K (A i Bi ) ( i Bi A) (instance of taut). By MP, we get K B1 . . . Bn A. Crucially: by UG, we then get K (B1 . . . Bn A). Using normality and MP we get K (B1 . . . Bn ) A.

Now B1 , . . . , Bn . By lemma 69(3), (B1 . . . Bn ) . So K A. By lemma 68, A . Contradiction. Claim By proposition 71 (next slide), there is a MCS with 0 . For every B , we have B B 0 . So RK (, ). Also, A 0 . By lemma 69(2), A / . So by the induction hypothesis, MK , |= A. It follows by semantics of that MK |= A, as required.
143

Lindenbaums lemma
Proposition 71 (Lindenbaum)
Any consistent set 0 extends to (is contained in) a MCS. Proof. Enumerate all modal formulas, as A0 , A1 , . . .. We dene a chain 0 1 of consistent sets. 0 is given, and is consistent. Inductively, dene n {An }, if this is consistent, n+1 = n , otherwise. Each n is consistent. Let = n n . Then: is consistent too (for a proof of from would be a proof from some n ). is maximal consistent. For, let A be a formula with A / . We know A = An for some n. By construction, n {A} is inconsistent (else n+1 = n {A} ). So {A} is inconsistent. So no set bigger than is consistent. And contains 0 .
144

Completeness is proved
Were done now! Relax.

Proposition 72 (completeness for K )

Any valid formula is a theorem of K .

Proof.
Suppose that A0 is not a theorem of K . Claim. {A0 } is consistent. Proof of claim. If not, then by exercise 62, K A0 . But K A0 A0 (instance of tautology). By MP, K A0 , contradicting our assumption. Claim Extend {A0 } to a MCS (proposition 71). By the truth lemma (lemma 70), MK , |= A for every A . But A0 . So MK , |= A0 . We found a model (MK ) satisfying A0 . So A0 is not valid.

Propositions 57 and 72 prove theorem 56.

145

Origin of canonical model

photos: Dana Scott, David Makinson

The canonical model construction was introduced (independently) by Lemmon & Scott (1966), Makinson (1966), Cresswell (1967), and Sch utte (1968). It remains important today.

146