Modal Logic

From Wiki Notes @ WuJiewen.com, by Jiewen Wu

Jump to: navigation, search

Contents

Syntax

The basic modal logic is defined using a set of propositional letters \,\Phi, and a unary operator \,\Box. A well-formed formula is then given by the rule

\phi := p\mid\perp\mid\neg\phi\mid\phi\vee\phi\mid\Box\phi ,

where p ranges over elements of \,\Phi. A dual operator of \,\Box is \,\Diamond: \,\Diamond\phi\equiv\neg\Box\neg\phi.

Semantics

Modal logic can be interpreted using possible world semantics, at the level of frames and models.

A frame is a pair \,\mathfrak{F}=(W, R), where W is a non-empty set of worlds, and R is a binary relation on W, e.g., \,R\subseteq W\times W. A model is a pair \,\mathfrak{M}=(\mathfrak{F},V), where \,\mathfrak{F} is a frame for the logic and V is a function that assigns to each propositional letter p a subset of W, e.g., V is a map \,\Phi\to Powerset(W). V is to address our frames with contingent information. Only statements deserve the description logical if they are invariant under changes of contingent information. Hence we further define satisfiable and valid.

Satisfiable

A formula \,\phi is satisfiable at world w in \,\mathfrak{M}=(W, R, V) if the following holds. We only show some of the formulas.

  • \,\mathfrak{M},w\Vdash p iff w \,\in V(p).
  • \,\mathfrak{M},w\Vdash\Box\phi iff for all v \,\in W such that wRv (i.e. v is an R-successor of w, or w is related to v by the binary relation R), we have \,\mathfrak{M},w\Vdash\phi.
  • \,\mathfrak{M},w\Vdash\Diamond\phi iff for some v \,\in W such that wRv, we have \,\mathfrak{M},w\Vdash\phi.

Satisfaction is local, meaning that formulas are evaluated inside models, at some particular state/world w.

A formula is globally true in a model \,\mathfrak{M}, denoted as \,\mathfrak{M}\Vdash\phi if it is satisfied at all states/worlds in \,\mathfrak{M}.

Valid

A formula is valid in a frame \,\mathfrak{F} if it is true at every state in every model that can be build upon the frame, i.e., \,\mathfrak{F}\Vdash\phi. Note that this kind of validity is often called \,\mathfrak{F}-valid, and when a formula is valid on all frames, it is valid as the notion we are familiar with in propositional logic. Fro example, \,\Diamond(p\vee q)\to(\Diamond p\vee\Diamond q) is valid on all frames.

Proof Theory

System K

a Hilbert-style system K is built on boolean Hilbert System by adding an extra, the distribution, axiom K:

  • Axiom K: \,\Box (p\to q)\to(\Box p\to\Box q)

Since K is an axiom, it is the same as other three axioms such that all instances of K are tautologies, and can be used freely in proofs. For system K, we also have the duality mentioned before \,\Diamond p\equiv\neg\Box\neg p.

Modus ponens is still used in K, and we introduce another rule, the necessity rule or the generalization rule:

  • NEC: Given \,\phi, we can prove \,\Box\phi.


Important Notes

Modus ponens preserves validity, global truth and satisfiability. However, the NEC rule only preserves validity and global truth, it does NOT preserve satisfiability. When p is true in some state, we cannot conclude that p is true at all R-accessible states, i.e., \,p\to\Box p is not valid. We can only use NEC rule on all tautologies \,\phi.

K is sound because all its axioms are valid and all the rules of inference preserve validity. K is also complete: if a formula is valid, then it is K-provable.

Linear-time Temporal Logic

Temporal Logic

The basic temporal language is an extension to the basic modal logic. It is defined using two unary operators F and P. F\,\phi is interpreted as \,\phi will be true at some future time, while p\,\phi means \,\phi was true at some past time. Their duals are written as G and H respectively, meaning it is always going to be the case and it always has been the case.

Interesting assertions can be made about time in this logic. For instance, P\,\phi\to GP\,\phi means whatever has happened will always have happened, and F\,\phi\to FF\,\phi shows that we are thinking of time as dense: between any two instants there is always a third.

Retrieved from "http://www.wujiewen.com/wiki/Modal_Logic"
Personal tools