Summary Foundations of Logic 2 (Modal logic)
(c) 2001-06-25 Fabian M. Suchanek
http://suchanek.name
This is a summary of the Modal Logic lecture held by
Prof. Wolfgang Lenzen in the WS 2000 at the University
of Osnabrueck.
By reading the following text, you accept that the author does not
accept any responsibility for the correctness or completeness of
this text. If you have any corrections or remarks, please
send me a mail. This is the only way to make the publication of this
summary useful for me, too.
Types of truth:
* ordinary truth (contingent facts)
* necessary truth (true in all possible worlds)
* logical truth (tautologies)
* analytic truth ("Bachelors are unmarried")
* laws of nature
Necessity: N(p) := p is necessarily true
N(p) = ~M(~p) = I(~p) = (p->q) & (~q->p)
It is always N(p) & N(q) <=> N(p & q)
Possibility: M(p) := ~N(~p)
M(p) = ~N(~p) = ~I(p)
It is always: M(p & q) -> M(p) & M(q), M(p | q) <=> M(p) | M(q)
Impossibility: I(p) := ~M(p)
I(p) = N(~p) = ~M(p) = (p->~p)
Contingency: C(p) := M(p) & M(~p)
Incompatability: IC(p,q) := I(p & q)
Modal operators according to Leibniz:
Necessity: p is true in all possible worlds
Contingent truth: True in our world, but not in every possible world
Possible truth: Not true in our world,but in at least 1 possible world
Types of Implication:
* material implication: p > q (boolean expression)
* logical implication: p -> q (necessary inference)
* strict implication: (p => q) := N(p > q)
reflexive, transitive, not symmetric
Types of Equivalence:
* material equivalence: p = q (boolean expression)
* strict equivalence: (p <=> q) := N(p = q)
reflexive, transitive, symmetric
Types of Proofs:
* syntactic proofs:
* Shifting: Convert the formula to a known one
* Constructive: Assemble the formula by rules
* Indirect: Assume that the formula is false, lead to contradiction
* Falsify: Find a counter-example
* semantic proofs:
* Constructive: Substitute the modalities by their meaning,
proove the resulting expression by propositional calculus
* Indirect: Assume that the formula is false, substitute the
modalities by their meaning and find a contradiction
* Falsify: Find a diagram of worlds as a counter-example
Rules:
MP: Modus ponens: p, p > q |- q
RN: Rule of necessitation: p |- N(p)
N1: N(a > b) > (N(a) > N(b))
N2: N(a) > a
N3: N(a) > N(N(a))
N4: ~N(a) > N(~N(a))
Models:
A model is a triple , where
* V is a Valuation function, evaluating a boolean expression
V(world, expression) maps to {true,false}
* W is a non-empty set of worlds
* R is a Relation function, returns accessability
R(world1,world2) = (world1 can access world 2)
Models:
1. K-Model
Properties of R: none
Additional rules: Propositional Calculus,
MP: p,p>q |- q
RN: p |- N(p)
N1: N(a > b) > (N(a) > N(b))
Modalities: Infinite
2. T-Model
Properties of R: reflexive
Additional rules: N2: N(p) > p
Modalities: Inifite
3. S4-Model
Properties of R: reflexive, transitive
Additional rules: N3: N(p) > N(N(p))
Modalities: N(p) -> N(M(N(p))) -> N(N(p)) -> M(N(M(p))) -> M(p)
\----------------bare-truth-------------------^
4. S5-Model
Properties of R. reflexive, transitive, symmetric
Additional rules: N4: M(p) > N(M(p))
Modalities: {M|N}M(p)=M(p) {M|N}N(p)=N(p)
Provability:
"|- a in X" means a is provable in model X
Adequacy of a model:
1. The model must be self-consistent, i.e.
if |- a in model X then a is semantically valid (true in every
possible world of every possible model with a relation function
R satisfying the conditions of model X)
2. The model must be complete
Proof of semantic validity of a model X:
1. Every axiom of X is valid in X
2. If a is valid in X, then also N(a) must be valid
(this is obvious)
3. Proofs of N(i) i=1..5, using the properties of R in X
Proof of semantic validity of the S5-model:
1. (numerous proofs)
2. (obvious)
3. Proof of all rules: (FMS version)
N1: N(a > b) > (N(a) > N(b))
<=> N(a > b) & N(a) > N(b)
<=> N( (a > b) & a) > N(b)
<=> N(a & b) > N(b)
<=> N(a) & N(b) > N(b) (obvious)
N2: N(a) > a
Assumption Ex V: Ex w: V(w,N2)=f
<=> V(w,N(a))=t & V(w,a)=f
<=> (All w': R(w,w') > V(w',a)=t) & V(w,a)=f
=> V(w,a)=t & V(w,a)=f
N3: N(a) > N(N(a))
Assumption Ex V: Ex w: V(w,N3)=f
<=> V(w,N(a))=t & V(w,N(N(a)))=f
<=> (All w': R(w,w') > V(w,a)=t)
& (Ex w'': R(w,w'') & V(w'',N(a))=f)
<=> (All w': R(w,w') > V(w,a)=t)
& (Ex w'': R(w,w'') & Ex w''': R(w'',w''') > V(w''',a)=f)
Contradictory, since R(w,w'') & R(w',w''') => R(w,w''')
N4: ~N(a) > N(~N(a))
Assumption: Ex V. Ex w: V(w, N4) = f
<=> V(w,~N(a))=t & V(w,N(~N(a)))=f
<=> (Ex w': R(w,w') & V(w',a)=f)
(Ex w'': R(w,w'') & V(w'',~N(a))=f)
<=> (Ex w': R(w,w') & V(w',a)=f)
(Ex w'': R(w,w'') & All w''': R(w'',w''') > V(w''',a)=t)
Contradictory, since R(w,w'') & R(w',w''') > R(w,w''')