Difference between revisions of "Modal Logic"
m (→Extension Axioms) |
|||
(27 intermediate revisions by the same user not shown) | |||
Line 2: | Line 2: | ||
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 | 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\ | + | <math>\phi := p\mid\perp\mid\neg\phi\mid\phi\vee\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>. | 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== | + | ==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> if the following holds. We only show some of the formulas. | ||
+ | |||
+ | *<math>\,\mathfrak{M},w\Vdash p</math> iff w <math>\,\in</math> V(p). | ||
+ | *<math>\,\mathfrak{M},w\Vdash\Box\phi</math> iff for '''all''' v <math>\,\in</math> 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 <math>\,\mathfrak{M},w\Vdash\phi</math>. | ||
+ | *<math>\,\mathfrak{M},w\Vdash\Diamond\phi</math> iff for '''some''' v <math>\,\in</math> W such that wRv, we have <math>\,\mathfrak{M},w\Vdash\phi</math>. | ||
+ | |||
+ | Satisfaction is local, meaning that formulas are evaluated inside models, at some particular state/world w. | ||
+ | |||
+ | A formula is '''globally true''' in a model <math>\,\mathfrak{M}</math>, denoted as <math>\,\mathfrak{M}\Vdash\phi</math> if it is satisfied at all states/worlds in <math>\,\mathfrak{M}</math>. | ||
+ | |||
+ | ===Valid=== | ||
+ | A formula is valid in a frame <math>\,\mathfrak{F}</math> if it is true at every state in every model that can be build upon the frame, i.e., <math>\,\mathfrak{F}\Vdash\phi</math>. Note that this kind of validity is often called <math>\,\mathfrak{F}</math>-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, <math>\,\Diamond(p\vee q)\to(\Diamond p\vee\Diamond q)</math> 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: <math>\,\Box (p\to q)\to(\Box p\to\Box q)</math> | ||
+ | |||
+ | 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 <math>\,\Diamond p\equiv\neg\Box\neg p</math>. | ||
+ | |||
+ | Modus ponens is still used in K, and we introduce another rule, the necessity rule or the generalization rule: | ||
+ | |||
+ | * NEC: Given <math>\,\phi</math>, we can prove <math>\,\Box\phi</math>. | ||
+ | |||
+ | |||
+ | ====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., <math>\,p\to\Box p</math> is not valid. '''We can only use NEC rule on all tautologies <math>\,\phi</math>.''' | ||
+ | |||
+ | 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<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''. | 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. | 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. | ||
− | |||
− | |||
− | |||
− | |||
− |
Latest revision as of 22:31, 21 November 2009
Contents
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\vee\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>.
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> if the following holds. We only show some of the formulas.
- <math>\,\mathfrak{M},w\Vdash p</math> iff w <math>\,\in</math> V(p).
- <math>\,\mathfrak{M},w\Vdash\Box\phi</math> iff for all v <math>\,\in</math> 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 <math>\,\mathfrak{M},w\Vdash\phi</math>.
- <math>\,\mathfrak{M},w\Vdash\Diamond\phi</math> iff for some v <math>\,\in</math> W such that wRv, we have <math>\,\mathfrak{M},w\Vdash\phi</math>.
Satisfaction is local, meaning that formulas are evaluated inside models, at some particular state/world w.
A formula is globally true in a model <math>\,\mathfrak{M}</math>, denoted as <math>\,\mathfrak{M}\Vdash\phi</math> if it is satisfied at all states/worlds in <math>\,\mathfrak{M}</math>.
Valid
A formula is valid in a frame <math>\,\mathfrak{F}</math> if it is true at every state in every model that can be build upon the frame, i.e., <math>\,\mathfrak{F}\Vdash\phi</math>. Note that this kind of validity is often called <math>\,\mathfrak{F}</math>-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, <math>\,\Diamond(p\vee q)\to(\Diamond p\vee\Diamond q)</math> 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: <math>\,\Box (p\to q)\to(\Box p\to\Box q)</math>
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 <math>\,\Diamond p\equiv\neg\Box\neg p</math>.
Modus ponens is still used in K, and we introduce another rule, the necessity rule or the generalization rule:
- NEC: Given <math>\,\phi</math>, we can prove <math>\,\Box\phi</math>.
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., <math>\,p\to\Box p</math> is not valid. We can only use NEC rule on all tautologies <math>\,\phi</math>.
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<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.