filtration
Let be a Kripke model for a modal logic . Let be a set of wff’s. Define a binary relation![]()
on :
Then is an equivalence relation![]()
on . Let be the set of equivalence classes
![]()
of on . It is easy to see that if is finite, so is . Next, let
Then is a well-defined function. We call a binary relation on a filtration of if
-
•
implies
-
•
implies that for any wff with , if , then .
The triple is called a filtration of the model .
Proposition 1.
(Filtration Lemma) Let be a set of wff’s closed under the formation of subformulas: any subformula of any formula
![]()
in is again in . Then
| Title | filtration |
|---|---|
| Canonical name | Filtration1 |
| Date of creation | 2013-03-22 19:35:39 |
| Last modified on | 2013-03-22 19:35:39 |
| Owner | CWoo (3771) |
| Last modified by | CWoo (3771) |
| Numerical id | 8 |
| Author | CWoo (3771) |
| Entry type | Definition |
| Classification | msc 03B45 |
| \@unrecurse |