Difference between revisions of "Modal Logic"
| Line 16: | Line 16: | ||
A frame is a pair <math>\,\mathfrak{F}=(W, R)</math>, where W is a non-empty set of worlds, and R is a binary relation on W, e.g., <math>\,R\subseteq W\times W</math>. A model is a pair <math>\,\mathfrak{M}={\mathfrak{F},V}</math>, where <math>\,\mathfrak{F}</math> 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 <math>\,\Phi\to Powerset(W)</math>. 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''. | A frame is a pair <math>\,\mathfrak{F}=(W, R)</math>, where W is a non-empty set of worlds, and R is a binary relation on W, e.g., <math>\,R\subseteq W\times W</math>. A model is a pair <math>\,\mathfrak{M}={\mathfrak{F},V}</math>, where <math>\,\mathfrak{F}</math> 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 <math>\,\Phi\to Powerset(W)</math>. 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 <math>\,\phi</math> is satisfiable at world w in <math>\,\mathfrak{M}=(W, R, V)</math> as follows. | A formula <math>\,\phi</math> is satisfiable at world w in <math>\,\mathfrak{M}=(W, R, V)</math> as follows. | ||
Revision as of 13:52, 5 November 2009
Syntax
The basic modal logic is defined using a set of propositional letters <math>\,\Phi</math>, and a unary operator <math>\,\Box</math>. A well-formed formula is then given by the rule
<math>\phi := p\mid\perp\mid\neg\phi\mid\phi\wedge\phi\mid\Box\phi</math> ,
where p ranges over elements of <math>\,\Phi</math>. A dual operator of <math>\,\Box</math> is <math>\,\Diamond</math>: <math>\,\Diamond\phi\equiv\neg\Box\neg\phi</math>.
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<math>\,\phi</math> is interpreted as <math>\,\phi</math> will be true at some future time, while p<math>\,\phi</math> means <math>\,\phi</math> 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, <math>P\,\phi\to GP\,\phi</math> means whatever has happened will always have happened, and <math>F\,\phi\to FF\,\phi</math> shows that we are thinking of time as dense: between any two instants there is always a third.
Semantics
Modal logic can be interpreted using possible world semantics, at the level of frames and models.
A frame is a pair <math>\,\mathfrak{F}=(W, R)</math>, where W is a non-empty set of worlds, and R is a binary relation on W, e.g., <math>\,R\subseteq W\times W</math>. A model is a pair <math>\,\mathfrak{M}={\mathfrak{F},V}</math>, where <math>\,\mathfrak{F}</math> 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 <math>\,\Phi\to Powerset(W)</math>. 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 <math>\,\phi</math> is satisfiable at world w in <math>\,\mathfrak{M}=(W, R, V)</math> as follows.
