Summary Foundations of Logic 2 (Modal logic)
                (c) 2001-06-25 Fabian M. Suchanek
          http://suchanek.name/texts/summaries/fol2.txt


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.

My e-mail address is f.m.suchanek@zweb.de, but the letter 'z' has to 
be removed from the address.


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 <V,W,R>, 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''')