Difference between revisions of "Modal Logic"
(→Syntax) |
(→Syntax) |
||
| Line 7: | Line 7: | ||
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>. | ||
| − | The basic temporal language is an extension to the basic modal logic. It is defined using | + | 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''. |
==Semantics== | ==Semantics== | ||
Revision as of 13:32, 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>.
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.
