36:
7915:
8083:
Possible world semantics is a broader term encompassing various approaches, including Kripke semantics. It generally refers to the idea of analyzing modal statements by considering alternative possible worlds where different propositions are true or false. While Kripke semantics is a specific type of
8009:, developed a translation of sentential modal logic into classical predicate logic that, if he had combined it with the usual model theory for the latter, would have produced a model theory equivalent to Kripke models for the former. But his approach was resolutely syntactic and anti-model-theoretic.
7861:
The main defect of Kripke semantics is the existence of Kripke incomplete logics, and logics which are complete but not compact. It can be remedied by equipping Kripke frames with extra structure which restricts the set of possible valuations, using ideas from algebraic semantics. This gives rise to
7998:
and Tarski established the representability of
Boolean algebras with operators in terms of frames. If the two ideas had been put together, the result would have been precisely frame models, which is to say Kripke models, years before Kripke. But no one (not even Tarski) saw the connection at the
8084:
possible world semantics, there are other ways to model possible worlds and their relationships. Kripke semantics is a specific form of possible world semantics that employs relational structures to represent the relationships between possible worlds and propositions in modal logic.
8026:
gave a semantics in his papers introducing epistemic logic that is a simple variation of Kripke's semantics, equivalent to the characterisation of valuations by means of maximal consistent sets. He doesn't give inference rules for epistemic logic, and so cannot give a completeness
1153:, are valid in every Kripke model). However, the converse does not hold in general: while most of the modal systems studied are complete of classes of frames described by simple conditions, Kripke incomplete normal modal logics do exist. A natural example of such a system is
7986:
for the modalities of necessity and possibility by means of giving the valuation function a parameter that ranges over
Leibnizian possible worlds. Bayart develops this idea further, but neither gave recursive definitions of satisfaction in the style introduced by
7499:
7888:
Blackburn et al. (2001) point out that because a relational structure is simply a set together with a collection of relations on that set, it is unsurprising that relational structures are to be found just about everywhere. As an example from
3623:
2865:
8033:
had many of the key ideas contained in Kripke's work, but he did not regard them as significant, because he had no completeness proof, and so did not publish until after Kripke's papers had created a sensation in the logic
8015:
gave a rather more complex approach to the interpretation of modal logic, but one that contains many of the key ideas of Kripke's approach. He first noted the relationship between conditions on accessibility relations and
4127:
The axioms T, 4, D, B, 5, H, G (and thus any combination of them) are canonical. GL and Grz are not canonical, because they are not compact. The axiom M by itself is not canonical (Goldblatt, 1991), but the combined logic
1945:
4618:
2685:
4495:
4414:
7620:
7193:
6735:
7268:
5295:
2614:
2047:
1578:
2406:
3419:
3257:
3039:
2536:
1759:
2780:
2729:
3077:
6931:
6529:
4678:
2187:
3124:
5583:
2345:
2459:
305:
8232:
7559:
7129:
6682:
3806:
1004:
897:
434:
7994:
developed an approach to modeling modal logics that is still influential in modern research, namely the algebraic approach, in which
Boolean algebras with operators are used as models.
4293:
2304:
5327:
4710:
4120:
A union of canonical sets of formulas is itself canonical. It follows from the preceding discussion that any logic axiomatized by a canonical set of formulas is Kripke complete, and
6267:
6134:
2942:
7362:
7068:
5656:
1986:
1871:
1621:
6772:
6566:
2980:
2257:
2225:
2085:
6889:
6487:
1269:
966:
466:
353:
6841:
5712:
4549:
4351:
5831:
7901:. Blackburn et al. thus claim because of this connection that modal languages are ideally suited in providing "internal, local perspective on relational structures." (p. xii)
6426:. That is, the 'local' aspect of existence for sections of a sheaf was a kind of logic of the 'possible'. Though this development was the work of a number of people, the name
5950:
4862:
4623:
Carlson models are easier to visualize and to work with than usual polymodal Kripke models; there are, however, Kripke complete polymodal logics which are
Carlson incomplete.
4948:
3326:
2134:
7697:
5034:
3387:
2108:
1419:
1298:
681:
598:
538:
7346:
6084:
5141:
3389:, which means that for every possible world in the model, there is always at least one possible world accessible from it (which could be itself). This implicit implication
7726:
3922:
2900:
1797:
1229:
6326:
6167:
3364:
3204:
624:
564:
7847:
7821:
7752:
7313:
7032:
6801:
6376:
6217:
6046:
6011:
5901:
5866:
5782:
5747:
5510:
5112:
5086:
5000:
4974:
4914:
4888:
4820:
4794:
3976:
3147:
1445:
1378:
1324:
923:
785:
707:
650:
239:
8040:
presented a semantics of intuitionistic logic based on trees, which closely resembles Kripke semantics, except for using a more cumbersome definition of satisfaction.
6293:
5976:
5060:
4768:
4734:
3873:
3842:
1830:
1481:
1024:
829:
755:
486:
4002:
3948:
3181:
263:
219:
199:
179:
4202:
There are various methods for establishing FMP for a given logic. Refinements and extensions of the canonical model construction often work, using tools such as
3893:
727:
3541:
8160:
modal formulae can be meaningfully 'understood'. Thus: whereas the notion of 'has a model' in classical non-modal logic refers to some individual formula
4144:
2787:
1134:). It is vital to know which modal logics are sound and complete with respect to a class of Kripke frames, and to determine also which class that is.
8012:
8462:
The Search for
Certainty : A Philosophical Account of Foundations of Mathematics: A Philosophical Account of Foundations of Mathematics
1631:
The following table lists common modal axioms together with their corresponding classes. The naming of the axioms often varies; Here, axiom
131:
and other non-classical systems. The development of Kripke semantics was a breakthrough in the theory of non-classical logics, because the
7078:
The key property which follows from this definition is that bisimulations (hence also p-morphisms) of models preserve the satisfaction of
1881:
4554:
4231:
modal algebra can be transformed into a Kripke frame. As an example, Robert Bull proved using this method that every normal extension of
2620:
3433:
The following table lists several common normal modal systems. Frame conditions for some of the systems were simplified: the logics are
4223:
In some cases, we can use FMP to prove Kripke completeness of a logic: every normal modal logic is complete with respect to a class of
17:
8152:
a specific 'something' that makes a specific modal formula true; in Kripke semantics a 'model' must rather be understood as a larger
4430:
4356:
1494:
than to prove its completeness, thus correspondence serves as a guide to completeness proofs. Correspondence is also used to show
7202:
5236:
4249:
Kripke semantics has a straightforward generalization to logics with more than one modality. A Kripke frame for a language with
2557:
1996:
1536:
135:
of such logics was almost non-existent before Kripke (algebraic semantics existed, but were considered 'syntax in disguise').
8568:
8511:
8421:
8395:
8371:
8345:
8317:
8296:
8273:
2355:
242:
8649:
3392:
3211:
1644:
8724:
8687:
2990:
2482:
1705:
4169:
This is a powerful criterion: for example, all axioms listed above as canonical are (equivalent to) Sahlqvist formulas.
2747:
2696:
8589:
8442:
3050:
8631:
7962:
7936:
4645:
2144:
79:
57:
7944:
7572:
7145:
6687:
3084:
50:
5518:
2315:
2417:
272:
7526:
7096:
6649:
4635:
follows the same principles as the semantics of modal logic, but it uses a different definition of satisfaction.
3773:
971:
864:
401:
4252:
2267:
8540:
8470:
7940:
7505:
but many applications need the reflexive and/or transitive closure of this relation, or similar modifications.
3422:
1154:
1126:
7494:{\displaystyle \langle w_{0},w_{1},\dots ,w_{n}\rangle \;R'\;\langle w_{0},w_{1},\dots ,w_{n},w_{n+1}\rangle }
1121:
8706:
5300:
4683:
3721:
6224:
6091:
2907:
8767:
8757:
8065:
7890:
6894:
6492:
5588:
1956:
1841:
1591:
2953:
2230:
2198:
2058:
8752:
8701:
6862:
6460:
1242:
939:
439:
326:
5670:
4518:
4320:
8125:
from the notion of 'model' in classical non-modal logics: In classical logics we say that some formula
6419:
5789:
4183:(FMP) if it is complete with respect to a class of finite frames. An application of this notion is the
4047:
The main application of canonical models are completeness proofs. Properties of the canonical model of
5908:
4835:
7894:
6740:
6534:
4921:
3275:
3150:
2113:
8020:-style axioms for modal logic. Kanger failed, however, to give a completeness proof for his system;
7853:
As in the case of unravelling, the definition of the accessibility relation on the quotient varies.
7673:
5007:
3369:
2090:
1395:
1274:
657:
571:
514:
8696:
7925:
7318:
6806:
6054:
5120:
4165:
there is an algorithm that computes the corresponding frame condition to a given
Sahlqvist formula.
44:
8606:
7929:
7879:
7702:
7037:
3898:
2876:
1773:
1205:
6298:
6139:
5209:
Intuitionistic logic is sound and complete with respect to its Kripke semantics, and it has the
4195:
which has FMP is decidable, provided it is decidable whether a given finite frame is a model of
3346:
3186:
603:
543:
8525:
7826:
7800:
7731:
7292:
7011:
6780:
6418:, it was realised around 1965 that Kripke semantics was intimately related to the treatment of
6331:
6172:
6016:
5981:
5871:
5836:
5752:
5717:
5480:
5091:
5065:
4979:
4953:
4893:
4867:
4799:
4773:
3955:
3717:
3129:
1424:
1357:
1303:
902:
764:
686:
629:
388:
224:
154:
61:
8615:
8359:
8762:
8747:
8196:
6272:
5955:
5210:
5039:
4747:
4719:
4179:
3850:
3827:
1807:
1466:
1009:
841:
814:
732:
471:
266:
8498:
8284:
3981:
3927:
3163:
846:. The satisfaction relation is uniquely determined by its value on propositional variables.
8742:
8715:
8331:
4632:
4184:
3512:
1092:
248:
204:
184:
128:
164:
8:
8190:
8050:
7639:
preserves the accessibility relation, and (in both directions) satisfaction of variables
7086:
4121:
1990:
112:
3618:{\displaystyle \forall w\,\exists u\,(w\,R\,u\land \forall v\,(u\,R\,v\Rightarrow u=v))}
8410:
8060:
8055:
3878:
2734:
2349:
2261:
1801:
1236:
1146:
712:
158:
8491:
8627:
8585:
8564:
8550:
8536:
8507:
8466:
8438:
8417:
8391:
8367:
8341:
8313:
8292:
8269:
8037:
5226:
4420:
4188:
4159:
4148:
3643:
3333:
7995:
8521:
8487:
8259:
8030:
7898:
7875:
4244:
4214:
4140:
3504:
2984:
1664:
8678:
8431:
Gasquet, Olivier; Herzig, Andreas; Said, Bilal; Schwarzentruber, François (2013).
8164:
that logic, the notion of 'has a model' in modal logic refers to the logic itself
4220:
Most of the modal systems used in practice (including all listed above) have FMP.
8719:
8682:
8653:
8579:
8558:
8460:
8432:
8385:
8381:
8335:
8307:
8263:
8023:
4211:
4025:
3680:
2860:{\displaystyle w\,R\,u\land w\,R\,v\Rightarrow \exists x\,(u\,R\,x\land v\,R\,x)}
2138:
1648:
364:
8662:
8099:
1580:
generates an incomplete logic, as it corresponds to the same class of frames as
8405:
8355:
8006:
7883:
6997:
4419:
A simplified semantics, discovered by Tim
Carlson, is often used for polymodal
3525:
1875:
1680:
104:
120:
8736:
8666:
8554:
8327:
7991:
7979:
7863:
5192:
4224:
3667:
1656:
1195:
is Kripke complete if and only if it is complete of its corresponding class.
1117:
150:
8366:. Handbook of Philosophical Logic. Vol. 3. Springer. pp. 225–339.
8002:
7771:
6852:
6446:
6442:, there are methods for constructing a new Kripke model from other models.
6439:
6423:
6415:
4827:
4199:. In particular, every finitely axiomatizable logic with FMP is decidable.
3653:
3635:
3329:
2470:
1584:(viz. transitive and converse well-founded frames), but does not prove the
132:
8506:. Handbook of the History of Logic. Vol. 7. Elsevier. pp. 1–98.
7975:
Similar work that predated Kripke's revolutionary semantic breakthroughs:
8291:. Handbook of Philosophical Logic. Vol. 2. Springer. pp. 1–88.
6996:
A bisimulation of models is additionally required to preserve forcing of
4143:
whether a given axiom is canonical. We know a nice sufficient condition:
1676:
1636:
1512:
are normal modal logics that correspond to the same class of frames, but
144:
124:
116:
8581:
Multiagent
Systems: Algorithmic, Game-Theoretic, and Logical Foundations
8600:
8017:
7630:
6457:, but the latter term is rarely used). A p-morphism of Kripke frames
3269:
1070:
108:
8148:. In the Kripke semantics of modal logic, by contrast, a 'model' is
8132:
a 'model' if there exists some 'interpretation' of the variables of
7914:
4314:. The definition of a satisfaction relation is modified as follows:
1940:{\displaystyle w\,R\,u\Rightarrow \exists v\,(w\,R\,v\land v\,R\,u)}
307:("possibly A" is defined as equivalent to "not necessarily not A").
8560:
Sheaves in
Geometry and Logic: A First Introduction to Topos Theory
4713:
4613:{\displaystyle \forall u\in D_{i}\,(w\;R\;u\Rightarrow u\Vdash A).}
4055:
with respect to the class of all Kripke frames. This argument does
3497:
3437:
with respect to the frame classes given in the table, but they may
2680:{\displaystyle w\,R\,u\land w\,R\,v\Rightarrow u\,R\,v\lor v\,R\,u}
1490:
It is often much easier to characterize the corresponding class of
7982:
seems to have been the first to have the idea that one can give a
4295:
as the set of its necessity operators consists of a non-empty set
3735:
if no contradiction can be derived from it using the theorems of
8526:"A Kripke-Joyal Semantics for Noncommutative Logic in Quantales"
8430:
8105:
3712:) can be constructed that refutes precisely the non-theorems of
8663:"4.4 Constructive Propositional Logic — Kripke Semantics"
8535:. Vol. 6. London: College Publications. pp. 209–225.
8243:
Quasi-historical
Interlude: the Road from Vienna to Los Angeles
3720:
as models. Canonical Kripke models play a role similar to the
1057:) be the class of all frames which validate every formula from
4490:{\displaystyle \langle W,R,\{D_{i}\}_{i\in I},\Vdash \rangle }
4409:{\displaystyle \forall u\,(w\;R_{i}\;u\Rightarrow u\Vdash A).}
8434:
Kripke's Worlds: An Introduction to Modal Logics via Tableaux
8087:
8602:
The proof theory and semantics of intuitionistic modal logic
8168:(i.e.: the entire system of its axioms and deduction rules).
4158:
the class of frames corresponding to a Sahlqvist formula is
1149:(in particular, theorems of the minimal normal modal logic,
5348:, and the following compatibility conditions hold whenever
7263:{\displaystyle s=\langle w_{0},w_{1},\dots ,w_{n}\rangle }
5290:{\displaystyle \langle W,\leq ,\{M_{w}\}_{w\in W}\rangle }
7519:
be a set of formulas closed under taking subformulas. An
4067:
of the canonical model satisfies the frame conditions of
2609:{\displaystyle \Box (\Box A\to B)\lor \Box (\Box B\to A)}
149:
The language of propositional modal logic consists of a
8531:. In Governatori, G.; Hodkinson, I.; Venema, Y. (eds.).
8205:, p. 20, 2.2 The semantics of intuitionistic logic.
2042:{\displaystyle w\,R\,v\wedge v\,R\,u\Rightarrow w\,R\,u}
1573:{\displaystyle \Box (A\leftrightarrow \Box A)\to \Box A}
8257:
4210:. As another possibility, completeness proofs based on
2401:{\displaystyle w\,R\,u\land w\,R\,v\Rightarrow u\,R\,v}
1033:
of frames or models, if it is valid in every member of
3716:, by an adaptation of the standard technique of using
1350:, and define satisfaction of a propositional variable
1116:
Semantics is useful for investigating a logic (i.e. a
8220:
7829:
7803:
7734:
7705:
7676:
7575:
7529:
7365:
7321:
7295:
7205:
7148:
7099:
7040:
7014:
6897:
6865:
6809:
6783:
6743:
6690:
6652:
6537:
6495:
6463:
6334:
6301:
6275:
6227:
6175:
6142:
6094:
6057:
6019:
5984:
5958:
5911:
5874:
5839:
5792:
5755:
5720:
5673:
5591:
5521:
5483:
5303:
5239:
5123:
5094:
5068:
5042:
5010:
4982:
4956:
4924:
4896:
4870:
4838:
4802:
4776:
4750:
4722:
4686:
4648:
4557:
4521:
4433:
4359:
4323:
4255:
3984:
3958:
3930:
3901:
3881:
3853:
3830:
3776:
3544:
3423:
existential quantifier on the range of quantification
3395:
3372:
3349:
3278:
3214:
3189:
3166:
3132:
3087:
3053:
2993:
2956:
2910:
2879:
2790:
2750:
2699:
2623:
2560:
2485:
2420:
2358:
2318:
2270:
2233:
2201:
2147:
2116:
2093:
2061:
1999:
1959:
1884:
1844:
1810:
1776:
1708:
1594:
1539:
1487:
corresponds to the class of reflexive Kripke frames.
1469:
1427:
1398:
1360:
1306:
1277:
1245:
1208:
1012:
974:
942:
905:
867:
817:
767:
735:
715:
689:
660:
632:
606:
574:
546:
517:
474:
442:
404:
329:
275:
251:
227:
207:
187:
167:
115:
systems created in the late 1950s and early 1960s by
8305:
8171:
6937:, which satisfies the following “zig-zag” property:
4626:
4063:, because there is no guarantee that the underlying
3414:{\displaystyle \Diamond A\rightarrow \Diamond \top }
3252:{\displaystyle \forall w\,\forall u\,\neg (w\,R\,u)}
8492:"Mathematical Modal Logic: a View of its Evolution"
5216:
3034:{\displaystyle w\,R\,u\land w\,R\,v\Rightarrow u=v}
2531:{\displaystyle \Box (\Box (A\to \Box A)\to A)\to A}
1754:{\displaystyle \Box (A\to B)\to (\Box A\to \Box B)}
1124:relation reflects its syntactical counterpart, the
8577:
8409:
8121:of 'model' in the Kripke semantics of modal logic
8093:
7841:
7815:
7746:
7720:
7691:
7614:
7553:
7493:
7340:
7307:
7262:
7187:
7123:
7062:
7026:
6925:
6883:
6835:
6795:
6766:
6729:
6676:
6560:
6523:
6481:
6370:
6320:
6287:
6261:
6211:
6161:
6128:
6078:
6040:
6005:
5970:
5944:
5895:
5860:
5825:
5776:
5741:
5706:
5650:
5577:
5504:
5321:
5289:
5135:
5106:
5080:
5054:
5028:
4994:
4968:
4942:
4908:
4882:
4856:
4814:
4788:
4762:
4728:
4704:
4672:
4612:
4543:
4489:
4408:
4345:
4287:
3996:
3970:
3942:
3916:
3887:
3867:
3836:
3800:
3617:
3413:
3381:
3358:
3320:
3251:
3198:
3175:
3141:
3118:
3071:
3033:
2974:
2936:
2894:
2859:
2775:{\displaystyle \Diamond \Box A\to \Box \Diamond A}
2774:
2724:{\displaystyle \Box \Diamond A\to \Diamond \Box A}
2723:
2679:
2608:
2530:
2453:
2400:
2339:
2298:
2251:
2219:
2181:
2128:
2102:
2079:
2041:
1980:
1939:
1865:
1824:
1791:
1753:
1615:
1572:
1475:
1439:
1413:
1372:
1318:
1292:
1263:
1223:
1111:
1045:) to be the set of all formulas that are valid in
1018:
998:
960:
917:
891:
823:
779:
749:
721:
701:
675:
644:
618:
592:
558:
532:
480:
460:
428:
347:
299:
257:
233:
213:
193:
173:
8500:Logic and the Modalities in the Twentieth Century
4147:identified a broad class of formulas (now called
4108:, the underlying frame of the canonical model of
8734:
8549:
7869:
3072:{\displaystyle \Diamond A\leftrightarrow \Box A}
27:Formal semantics for non-classical logic systems
8326:
7352:. The definition of the accessibility relation
4673:{\displaystyle \langle W,\leq ,\Vdash \rangle }
2182:{\displaystyle \forall w\,\exists v\,(w\,R\,v)}
8622:. In Zamuner, Edoardo; Levy, David K. (eds.).
8412:Intuitionistic Logic, Model Theory and Forcing
8362:. In Gabbay, Dov M.; Guenthner, Franz (eds.).
7615:{\displaystyle \langle W',R',\Vdash '\rangle }
7188:{\displaystyle \langle W',R',\Vdash '\rangle }
6730:{\displaystyle \langle W',R',\Vdash '\rangle }
4512:for each modality. Satisfaction is defined as
3119:{\displaystyle \forall w\,\exists !u\,w\,R\,u}
1626:
1533:is Kripke incomplete. For example, the schema
8616:"The architecture of meaning: Wittgenstein's
8282:
7511:is a useful construction which uses to prove
5578:{\displaystyle w\Vdash P(t_{1},\dots ,t_{n})}
4044:has a counterexample in the canonical model.
2340:{\displaystyle \Diamond A\to \Box \Diamond A}
1338:. On the other hand, a frame which validates
7762:preserves satisfaction of all formulas from
7609:
7576:
7548:
7530:
7488:
7424:
7411:
7366:
7257:
7212:
7182:
7149:
7118:
7100:
7082:formulas, not only propositional variables.
6920:
6898:
6878:
6866:
6724:
6691:
6671:
6653:
6575:preserves the accessibility relation, i.e.,
6518:
6496:
6476:
6464:
5316:
5304:
5284:
5269:
5255:
5240:
4699:
4687:
4667:
4649:
4484:
4463:
4449:
4434:
4282:
4256:
4040:, in particular every formula unprovable in
3795:
3777:
2454:{\displaystyle \Box (\Box A\to A)\to \Box A}
1258:
1246:
993:
975:
955:
943:
886:
868:
455:
443:
423:
405:
342:
330:
300:{\displaystyle \Diamond A:=\neg \Box \neg A}
8713:
8660:
8584:. Cambridge University Press. p. 397.
8241:, See the last two paragraphs in Section 3
8215:
8140:true; this specific interpretation is then
7943:. Unsourced material may be challenged and
7554:{\displaystyle \langle W,R,\Vdash \rangle }
7124:{\displaystyle \langle W,R,\Vdash \rangle }
6737:is a p-morphism of their underlying frames
6677:{\displaystyle \langle W,R,\Vdash \rangle }
4191:that a recursively axiomatized modal logic
3801:{\displaystyle \langle W,R,\Vdash \rangle }
999:{\displaystyle \langle W,R,\Vdash \rangle }
892:{\displaystyle \langle W,R,\Vdash \rangle }
429:{\displaystyle \langle W,R,\Vdash \rangle }
138:
8578:Shoham, Yoav; Leyton-Brown, Kevin (2008).
8520:
8486:
8226:
8214:See a slightly different formalization in
7904:
7856:
7512:
7423:
7414:
6414:As part of the independent development of
5155:, could be defined as an abbreviation for
4588:
4584:
4384:
4373:
4288:{\displaystyle \{\Box _{i}\mid \,i\in I\}}
3861:
3857:
3421:is similar to the implicit implication by
2299:{\displaystyle w\,R\,v\Rightarrow v\,R\,w}
743:
739:
8497:. In Gabbay, Dov M.; Woods, John (eds.).
8458:
8354:
8287:. In Gabbay, D.M.; Guenthner, F. (eds.).
8177:
7963:Learn how and when to remove this message
6409:
6243:
6110:
4577:
4366:
4272:
3593:
3589:
3582:
3569:
3565:
3558:
3551:
3242:
3238:
3228:
3221:
3112:
3108:
3104:
3094:
3015:
3011:
3001:
2997:
2918:
2914:
2850:
2846:
2836:
2832:
2825:
2812:
2808:
2798:
2794:
2673:
2669:
2659:
2655:
2645:
2641:
2631:
2627:
2394:
2390:
2380:
2376:
2366:
2362:
2292:
2288:
2278:
2274:
2172:
2168:
2161:
2154:
2035:
2031:
2021:
2017:
2007:
2003:
1930:
1926:
1916:
1912:
1905:
1892:
1888:
1818:
1814:
1183:is the largest class of frames such that
80:Learn how and when to remove this message
8465:. Oxford University Press. p. 256.
8283:Bull, Robert A.; Segerberg, K. (2012) .
4217:usually produce finite models directly.
4207:
4203:
4172:
1064:A modal logic (i.e., a set of formulas)
43:This article includes a list of general
8626:. London: Routledge. pp. 211–244.
8613:
8598:
8404:
8380:
8306:Chagrov, A.; Zakharyaschev, M. (1997).
8238:
8202:
7085:We can transform a Kripke model into a
5322:{\displaystyle \langle W,\leq \rangle }
4705:{\displaystyle \langle W,\leq \rangle }
4093:is valid in every frame that satisfies
3428:
14:
8735:
8714:Moschovakis, Joan (16 December 2022).
8676:
6433:
6262:{\displaystyle w\Vdash (\forall x\,A)}
6129:{\displaystyle w\Vdash (\exists x\,A)}
5477:, we define the satisfaction relation
2937:{\displaystyle w\,R\,v\Rightarrow w=v}
492:and modal formulas, such that for all
6926:{\displaystyle \langle W',R'\rangle }
6524:{\displaystyle \langle W',R'\rangle }
5651:{\displaystyle P(t_{1},\dots ,t_{n})}
4497:with a single accessibility relation
3724:construction in algebraic semantics.
1981:{\displaystyle \Box A\to \Box \Box A}
1866:{\displaystyle \Box \Box A\to \Box A}
1616:{\displaystyle \Box A\to \Box \Box A}
7941:adding citations to reliable sources
7908:
7356:varies; in the simplest case we put
5377:realizations of function symbols in
4736:satisfies the following conditions:
4238:
2975:{\displaystyle \Diamond A\to \Box A}
2252:{\displaystyle \Diamond \Box A\to A}
2220:{\displaystyle A\to \Box \Diamond A}
2080:{\displaystyle \Box A\to \Diamond A}
310:
221:("necessarily"). The modal operator
29:
8725:Stanford Encyclopedia of Philosophy
8688:Stanford Encyclopedia of Philosophy
8673:N.B: Constructive = intuitionistic.
8647:
7766:. In typical applications, we take
7199:is the set of all finite sequences
6884:{\displaystyle \langle W,R\rangle }
6482:{\displaystyle \langle W,R\rangle }
5329:is an intuitionistic Kripke frame,
4032:-consistent set is contained in an
3755:-consistent set that has no proper
3699:
1264:{\displaystyle \langle W,R\rangle }
961:{\displaystyle \langle W,R\rangle }
461:{\displaystyle \langle W,R\rangle }
348:{\displaystyle \langle W,R\rangle }
24:
8668:Introduction to Mathematical Logic
8005:, building on unpublished work of
6851:P-morphisms are a special kind of
6430:is often used in this connection.
6237:
6104:
6064:
5707:{\displaystyle w\Vdash (A\land B)}
5130:
4558:
4544:{\displaystyle w\Vdash \Box _{i}A}
4360:
4346:{\displaystyle w\Vdash \Box _{i}A}
4051:immediately imply completeness of
4008:The canonical model is a model of
3693:transitive, serial, and Euclidean
3576:
3552:
3545:
3408:
3376:
3229:
3222:
3215:
3193:
3133:
3095:
3088:
2819:
2155:
2148:
2123:
2117:
2097:
1899:
1074:with respect to a class of frames
524:
291:
285:
241:("possibly") is (classically) the
188:
49:it lacks sufficient corresponding
25:
8779:
8677:Garson, James (23 January 2023).
8641:
8624:Wittgenstein's Enduring Arguments
8390:(2nd ed.). Clarendon Press.
8337:A New Introduction to Modal Logic
7070:, for any propositional variable
6843:, for any propositional variable
5826:{\displaystyle w\Vdash (A\lor B)}
4627:Semantics of intuitionistic logic
4235:has FMP, and is Kripke complete.
4155:a Sahlqvist formula is canonical,
3875:if and only if for every formula
8607:Edinburgh Research Archive (ERA)
7913:
6394:) is the evaluation which gives
5945:{\displaystyle w\Vdash (A\to B)}
5217:Intuitionistic first-order logic
4857:{\displaystyle w\Vdash A\land B}
34:
8364:Alternatives to Classical Logic
6767:{\displaystyle f\colon W\to W'}
6561:{\displaystyle f\colon W\to W'}
6449:in Kripke semantics are called
6136:if and only if there exists an
4943:{\displaystyle w\Vdash A\lor B}
4299:equipped with binary relations
4074:We say that a formula or a set
3321:{\displaystyle \Box \to \Box B}
2129:{\displaystyle \neg \Box \bot }
1519:does not prove all theorems of
1112:Correspondence and completeness
488:is a relation between nodes of
359:is a (possibly empty) set, and
269:in terms of necessity like so:
8437:. Springer. pp. XV, 198.
8268:. Cambridge University Press.
8208:
8183:
8111:
8094:Shoham & Leyton-Brown 2008
8077:
7692:{\displaystyle u\Vdash \Box A}
6935:B ⊆ W × W’
6819:
6813:
6753:
6646:A p-morphism of Kripke models
6547:
6365:
6362:
6356:
6350:
6344:
6256:
6250:
6247:
6234:
6206:
6203:
6197:
6191:
6185:
6123:
6117:
6114:
6101:
6073:
6067:
6035:
6029:
6000:
5994:
5939:
5933:
5930:
5924:
5918:
5890:
5884:
5855:
5849:
5820:
5814:
5811:
5799:
5771:
5765:
5736:
5730:
5701:
5695:
5692:
5680:
5645:
5642:
5636:
5614:
5608:
5595:
5572:
5566:
5563:
5531:
5499:
5493:
5029:{\displaystyle w\Vdash A\to B}
5020:
4604:
4592:
4578:
4400:
4388:
4367:
3612:
3609:
3597:
3583:
3559:
3402:
3382:{\displaystyle \Diamond \top }
3328:, which logically establishes
3309:
3306:
3297:
3291:
3285:
3282:
3246:
3232:
3060:
3019:
2963:
2922:
2883:
2854:
2826:
2816:
2760:
2709:
2649:
2603:
2597:
2588:
2579:
2573:
2564:
2522:
2519:
2513:
2510:
2501:
2495:
2489:
2442:
2439:
2433:
2424:
2384:
2325:
2282:
2243:
2205:
2176:
2162:
2103:{\displaystyle \Diamond \top }
2068:
2025:
1966:
1934:
1906:
1896:
1854:
1783:
1748:
1739:
1730:
1727:
1724:
1718:
1712:
1601:
1561:
1558:
1549:
1543:
1414:{\displaystyle w\Vdash \Box p}
1293:{\displaystyle w\Vdash \Box A}
1215:
1053:is a set of formulas, let Mod(
676:{\displaystyle w\Vdash \Box A}
593:{\displaystyle w\Vdash A\to B}
584:
533:{\displaystyle w\Vdash \neg A}
168:
13:
1:
8289:Extensions of Classical Logic
8251:
7870:Computer science applications
7348:for a propositional variable
7341:{\displaystyle w_{n}\Vdash p}
6836:{\displaystyle f(w)\Vdash 'p}
6079:{\displaystyle w\Vdash \bot }
5367:is included in the domain of
5136:{\displaystyle w\Vdash \bot }
4744:is a propositional variable,
3708:, a Kripke model (called the
3441:to a larger class of frames.
123:. It was first conceived for
7891:theoretical computer science
6402:, and otherwise agrees with
5470:of variables by elements of
5229:language. A Kripke model of
3704:For any normal modal logic,
1006:for all possible choices of
157:, a set of truth-functional
7:
8702:Encyclopedia of Mathematics
8044:
7770:as the projection onto the
7721:{\displaystyle \Box A\in X}
7063:{\displaystyle w'\Vdash 'p}
4640:intuitionistic Kripke model
4100:for any normal modal logic
4082:with respect to a property
3917:{\displaystyle \Box A\in X}
2895:{\displaystyle A\to \Box A}
1792:{\displaystyle \Box A\to A}
1627:Common modal axiom schemata
1224:{\displaystyle \Box A\to A}
1155:Japaridze's polymodal logic
10:
8784:
8661:Detlovs, V.; Podnieks, K.
8459:Giaquinto, Marcus (2002).
7895:labeled transition systems
7873:
6420:existential quantification
6321:{\displaystyle a\in M_{u}}
6162:{\displaystyle a\in M_{w}}
4242:
4187:question: it follows from
3359:{\displaystyle \Diamond A}
3199:{\displaystyle \Box \bot }
2543:reflexive and transitive,
1763:holds true for any frames
619:{\displaystyle w\nVdash A}
559:{\displaystyle w\nVdash A}
201:), and the modal operator
142:
103:, and often confused with
7842:{\displaystyle v\Vdash A}
7816:{\displaystyle u\Vdash A}
7747:{\displaystyle v\Vdash A}
7308:{\displaystyle s\Vdash p}
7027:{\displaystyle w\Vdash p}
6796:{\displaystyle w\Vdash p}
6371:{\displaystyle u\Vdash A}
6269:if and only if for every
6212:{\displaystyle w\Vdash A}
6041:{\displaystyle u\Vdash B}
6006:{\displaystyle u\Vdash A}
5896:{\displaystyle w\Vdash B}
5861:{\displaystyle w\Vdash A}
5777:{\displaystyle w\Vdash B}
5742:{\displaystyle w\Vdash A}
5505:{\displaystyle w\Vdash A}
5340:-structure for each node
5107:{\displaystyle u\Vdash B}
5081:{\displaystyle u\Vdash A}
4995:{\displaystyle w\Vdash B}
4969:{\displaystyle w\Vdash A}
4909:{\displaystyle w\Vdash B}
4883:{\displaystyle w\Vdash A}
4815:{\displaystyle u\Vdash p}
4789:{\displaystyle w\Vdash p}
4020:contains all theorems of
3971:{\displaystyle X\Vdash A}
3722:Lindenbaum–Tarski algebra
3336:in every possible world.
3151:uniqueness quantification
3142:{\displaystyle \exists !}
1498:of modal logics: suppose
1440:{\displaystyle w\Vdash p}
1373:{\displaystyle u\Vdash p}
1342:has to be reflexive: fix
1319:{\displaystyle w\Vdash A}
918:{\displaystyle w\Vdash A}
780:{\displaystyle w\Vdash A}
702:{\displaystyle u\Vdash A}
645:{\displaystyle w\Vdash B}
234:{\displaystyle \Diamond }
8614:Stokhof, Martin (2008).
8387:Elements of Intuitionism
8136:which makes the formula
8071:
7984:possible world semantics
3741:maximal L-consistent set
1463:using the definition of
139:Semantics of modal logic
105:possible world semantics
8671:. University of Latvia.
8533:Advances in Modal Logic
7905:History and terminology
7880:state transition system
7857:General frame semantics
7789:if and only if for all
7523:-filtration of a model
6288:{\displaystyle u\geq w}
5971:{\displaystyle u\geq w}
5952:if and only if for all
5055:{\displaystyle u\geq w}
5036:if and only if for all
4763:{\displaystyle w\leq u}
4729:{\displaystyle \Vdash }
3868:{\displaystyle X\;R\;Y}
3837:{\displaystyle \Vdash }
3718:maximal consistent sets
1825:{\displaystyle w\,R\,w}
1476:{\displaystyle \Vdash }
1019:{\displaystyle \Vdash }
824:{\displaystyle \Vdash }
750:{\displaystyle w\;R\;u}
481:{\displaystyle \Vdash }
468:is a Kripke frame, and
155:propositional variables
127:, and later adapted to
64:more precise citations.
8716:"Intuitionistic Logic"
8599:Simpson, Alex (1994).
8382:Dummett, Michael A. E.
8360:"Intuitionistic Logic"
8262:; Venema, Yde (2002).
7843:
7817:
7748:
7722:
7693:
7616:
7555:
7495:
7342:
7309:
7264:
7189:
7125:
7064:
7028:
6927:
6885:
6837:
6797:
6768:
6731:
6678:
6562:
6525:
6483:
6428:Kripke–Joyal semantics
6410:Kripke–Joyal semantics
6372:
6322:
6289:
6263:
6213:
6163:
6130:
6080:
6042:
6007:
5972:
5946:
5897:
5862:
5827:
5778:
5743:
5708:
5652:
5579:
5506:
5323:
5291:
5137:
5108:
5082:
5056:
5030:
4996:
4970:
4944:
4910:
4884:
4858:
4816:
4790:
4764:
4730:
4706:
4674:
4614:
4545:
4491:
4410:
4347:
4289:
3998:
3997:{\displaystyle A\in X}
3972:
3944:
3943:{\displaystyle A\in Y}
3918:
3889:
3869:
3838:
3802:
3759:-consistent superset.
3739:, and Modus Ponens. A
3619:
3415:
3383:
3360:
3322:
3253:
3200:
3177:
3176:{\displaystyle \Box A}
3143:
3120:
3073:
3035:
2976:
2938:
2896:
2861:
2776:
2725:
2681:
2610:
2532:
2455:
2402:
2341:
2300:
2253:
2221:
2183:
2130:
2104:
2081:
2043:
1982:
1941:
1867:
1826:
1793:
1755:
1681:symbolic logic systems
1617:
1574:
1477:
1441:
1415:
1374:
1320:
1294:
1265:
1225:
1141:of Kripke frames, Thm(
1020:
1000:
962:
919:
893:
825:
781:
751:
723:
703:
677:
646:
620:
594:
560:
534:
482:
462:
430:
389:accessibility relation
349:
301:
259:
235:
215:
195:
175:
151:countably infinite set
18:Kripke–Joyal semantics
8620:and formal semantics"
8154:universe of discourse
8066:Muddy Children Puzzle
7844:
7818:
7749:
7723:
7694:
7617:
7556:
7515:for many logics. Let
7496:
7343:
7310:
7265:
7190:
7126:
7065:
7029:
6928:
6886:
6838:
6798:
6769:
6732:
6679:
6563:
6526:
6484:
6373:
6323:
6290:
6264:
6214:
6164:
6131:
6081:
6043:
6008:
5973:
5947:
5898:
5863:
5828:
5779:
5744:
5709:
5653:
5580:
5507:
5391:agree on elements of
5324:
5292:
5211:finite model property
5138:
5109:
5083:
5057:
5031:
4997:
4971:
4945:
4911:
4885:
4859:
4817:
4791:
4765:
4731:
4707:
4675:
4631:Kripke semantics for
4615:
4546:
4492:
4411:
4348:
4290:
4180:finite model property
4173:Finite model property
4086:of Kripke frames, if
3999:
3973:
3945:
3919:
3890:
3870:
3839:
3803:
3727:A set of formulas is
3620:
3416:
3384:
3361:
3323:
3254:
3201:
3178:
3144:
3121:
3074:
3036:
2977:
2939:
2897:
2862:
2777:
2726:
2682:
2611:
2533:
2456:
2403:
2342:
2301:
2254:
2222:
2184:
2131:
2105:
2082:
2044:
1983:
1942:
1868:
1827:
1794:
1756:
1618:
1575:
1478:
1442:
1416:
1375:
1321:
1295:
1266:
1226:
1167:to a class of frames
1160:A normal modal logic
1127:syntactic consequence
1021:
1001:
963:
920:
894:
833:satisfaction relation
826:
782:
752:
724:
704:
678:
647:
621:
595:
561:
535:
483:
463:
431:
350:
302:
260:
258:{\displaystyle \Box }
236:
216:
214:{\displaystyle \Box }
196:
194:{\displaystyle \neg }
176:
7990:J.C.C. McKinsey and
7937:improve this section
7827:
7801:
7732:
7703:
7674:
7573:
7527:
7363:
7319:
7293:
7203:
7146:
7142:, we define a model
7097:
7038:
7012:
6895:
6863:
6807:
6781:
6741:
6688:
6650:
6535:
6493:
6461:
6453:(which is short for
6332:
6299:
6273:
6225:
6173:
6140:
6092:
6055:
6017:
5982:
5956:
5909:
5872:
5837:
5790:
5753:
5718:
5671:
5589:
5519:
5481:
5466:Given an evaluation
5301:
5237:
5121:
5092:
5066:
5040:
5008:
4980:
4954:
4922:
4894:
4868:
4836:
4800:
4774:
4748:
4720:
4684:
4646:
4633:intuitionistic logic
4555:
4519:
4431:
4357:
4321:
4253:
3982:
3956:
3928:
3899:
3879:
3851:
3828:
3820:, and the relations
3774:
3654:strict partial order
3542:
3513:equivalence relation
3457:
3429:Common modal systems
3393:
3370:
3347:
3339:Note that for axiom
3276:
3212:
3187:
3164:
3130:
3085:
3051:
2991:
2954:
2908:
2877:
2788:
2748:
2697:
2621:
2558:
2483:
2418:
2356:
2316:
2268:
2231:
2199:
2145:
2114:
2091:
2059:
1997:
1957:
1882:
1842:
1808:
1774:
1706:
1592:
1537:
1467:
1425:
1396:
1358:
1304:
1275:
1243:
1206:
1198:Consider the schema
1122:semantic consequence
1010:
972:
968:, if it is valid in
940:
903:
865:
815:
765:
733:
713:
687:
658:
630:
604:
572:
544:
515:
472:
440:
402:
327:
273:
249:
225:
205:
185:
174:{\displaystyle \to }
165:
129:intuitionistic logic
97:relational semantics
8768:Non-classical logic
8758:Philosophical logic
8312:. Clarendon Press.
8285:"Basic Modal Logic"
8191:Andrzej Grzegorczyk
8106:Gasquet et al. 2013
8051:Alexandrov topology
6434:Model constructions
5455:, then it holds in
4059:work for arbitrary
3366:implicitly implies
1675:are named based on
1643:is named after the
1179:). In other words,
500:and modal formulas
113:non-classical logic
8753:Mathematical logic
8551:Mac Lane, Saunders
8216:Moschovakis (2022)
8061:Two-dimensionalism
8056:Normal modal logic
7839:
7813:
7778:over the relation
7744:
7718:
7689:
7612:
7551:
7491:
7338:
7305:
7260:
7185:
7121:
7060:
7024:
6974:u’ R’ v’
6963:u’ R’ v’
6923:
6881:
6833:
6793:
6774:, which satisfies
6764:
6727:
6674:
6558:
6521:
6479:
6455:pseudo-epimorphism
6368:
6318:
6285:
6259:
6209:
6159:
6126:
6076:
6038:
6003:
5968:
5942:
5893:
5858:
5823:
5774:
5739:
5704:
5648:
5575:
5502:
5319:
5287:
5133:
5104:
5078:
5052:
5026:
4992:
4966:
4940:
4906:
4880:
4854:
4812:
4786:
4760:
4726:
4716:Kripke frame, and
4702:
4670:
4610:
4541:
4487:
4421:provability logics
4406:
4343:
4285:
4149:Sahlqvist formulas
4139:In general, it is
3994:
3968:
3940:
3914:
3885:
3865:
3834:
3812:is the set of all
3798:
3770:is a Kripke model
3615:
3435:sound and complete
3411:
3379:
3356:
3318:
3249:
3196:
3173:
3139:
3116:
3069:
3031:
2972:
2934:
2892:
2857:
2772:
2721:
2677:
2606:
2528:
2451:
2398:
2337:
2296:
2249:
2217:
2179:
2126:
2100:
2077:
2039:
1978:
1937:
1863:
1822:
1789:
1751:
1613:
1570:
1473:
1437:
1411:
1370:
1316:
1290:
1261:
1221:
1191:. It follows that
1147:normal modal logic
1049:. Conversely, if
1016:
996:
958:
915:
889:
821:
777:
747:
719:
699:
673:
642:
616:
590:
556:
530:
478:
458:
426:
345:
297:
255:
231:
211:
191:
171:
8648:Burgess, John P.
8570:978-1-4612-0927-0
8522:Goldblatt, Robert
8513:978-0-08-046303-2
8488:Goldblatt, Robert
8423:978-0-444-53418-7
8416:. North-Holland.
8397:978-0-19-850524-2
8373:978-94-009-5203-4
8347:978-1-134-80028-5
8319:978-0-19-853779-3
8298:978-94-009-6259-0
8275:978-1-316-10195-7
8108:, pp. 14–16.
8038:Evert Willem Beth
7973:
7972:
7965:
7899:program execution
7131:and a fixed node
5336:is a (classical)
5159:→ ⊥. If for all
4239:Multimodal logics
3888:{\displaystyle A}
3751:for short) is an
3697:
3696:
3663:Grz or T, 4, Grz
3334:rule of inference
3262:
3261:
2547:−Id well-founded
1175: = Mod(
1118:derivation system
1104: ⊇ Thm(
1082: ⊆ Thm(
722:{\displaystyle u}
311:Basic definitions
161:(in this article
90:
89:
82:
16:(Redirected from
8775:
8729:
8720:Zalta, Edward N.
8710:
8692:
8683:Zalta, Edward N.
8672:
8657:
8652:. Archived from
8637:
8610:
8595:
8574:
8546:
8530:
8517:
8505:
8496:
8483:
8481:
8479:
8455:
8453:
8451:
8427:
8415:
8401:
8377:
8351:
8323:
8302:
8279:
8246:
8236:
8230:
8224:
8218:
8212:
8206:
8200:
8194:
8187:
8181:
8175:
8169:
8115:
8109:
8103:
8097:
8091:
8085:
8081:
8031:Richard Montague
7968:
7961:
7957:
7954:
7948:
7917:
7909:
7876:Kripke structure
7848:
7846:
7845:
7840:
7822:
7820:
7819:
7814:
7758:It follows that
7753:
7751:
7750:
7745:
7727:
7725:
7724:
7719:
7698:
7696:
7695:
7690:
7621:
7619:
7618:
7613:
7608:
7597:
7586:
7560:
7558:
7557:
7552:
7500:
7498:
7497:
7492:
7487:
7486:
7468:
7467:
7449:
7448:
7436:
7435:
7422:
7410:
7409:
7391:
7390:
7378:
7377:
7347:
7345:
7344:
7339:
7331:
7330:
7314:
7312:
7311:
7306:
7285: <
7269:
7267:
7266:
7261:
7256:
7255:
7237:
7236:
7224:
7223:
7194:
7192:
7191:
7186:
7181:
7170:
7159:
7130:
7128:
7127:
7122:
7093:. Given a model
7069:
7067:
7066:
7061:
7056:
7048:
7033:
7031:
7030:
7025:
7006:w B w’
6986:v B v’
6970:u B u’
6959:v B v’
6943:u B u’
6932:
6930:
6929:
6924:
6919:
6908:
6890:
6888:
6887:
6882:
6855:. In general, a
6842:
6840:
6839:
6834:
6829:
6802:
6800:
6799:
6794:
6773:
6771:
6770:
6765:
6763:
6736:
6734:
6733:
6728:
6723:
6712:
6701:
6683:
6681:
6680:
6675:
6567:
6565:
6564:
6559:
6557:
6530:
6528:
6527:
6522:
6517:
6506:
6488:
6486:
6485:
6480:
6438:As in classical
6377:
6375:
6374:
6369:
6327:
6325:
6324:
6319:
6317:
6316:
6294:
6292:
6291:
6286:
6268:
6266:
6265:
6260:
6218:
6216:
6215:
6210:
6168:
6166:
6165:
6160:
6158:
6157:
6135:
6133:
6132:
6127:
6085:
6083:
6082:
6077:
6047:
6045:
6044:
6039:
6012:
6010:
6009:
6004:
5977:
5975:
5974:
5969:
5951:
5949:
5948:
5943:
5902:
5900:
5899:
5894:
5867:
5865:
5864:
5859:
5832:
5830:
5829:
5824:
5783:
5781:
5780:
5775:
5748:
5746:
5745:
5740:
5713:
5711:
5710:
5705:
5657:
5655:
5654:
5649:
5635:
5634:
5607:
5606:
5584:
5582:
5581:
5576:
5562:
5561:
5543:
5542:
5511:
5509:
5508:
5503:
5328:
5326:
5325:
5320:
5296:
5294:
5293:
5288:
5283:
5282:
5267:
5266:
5147:The negation of
5142:
5140:
5139:
5134:
5113:
5111:
5110:
5105:
5087:
5085:
5084:
5079:
5061:
5059:
5058:
5053:
5035:
5033:
5032:
5027:
5001:
4999:
4998:
4993:
4975:
4973:
4972:
4967:
4949:
4947:
4946:
4941:
4915:
4913:
4912:
4907:
4889:
4887:
4886:
4881:
4863:
4861:
4860:
4855:
4821:
4819:
4818:
4813:
4795:
4793:
4792:
4787:
4769:
4767:
4766:
4761:
4735:
4733:
4732:
4727:
4711:
4709:
4708:
4703:
4679:
4677:
4676:
4671:
4619:
4617:
4616:
4611:
4576:
4575:
4550:
4548:
4547:
4542:
4537:
4536:
4496:
4494:
4493:
4488:
4477:
4476:
4461:
4460:
4415:
4413:
4412:
4407:
4383:
4382:
4352:
4350:
4349:
4344:
4339:
4338:
4294:
4292:
4291:
4286:
4268:
4267:
4245:Multimodal logic
4177:A logic has the
4145:Henrik Sahlqvist
4136:) is canonical.
4003:
4001:
4000:
3995:
3977:
3975:
3974:
3969:
3949:
3947:
3946:
3941:
3923:
3921:
3920:
3915:
3894:
3892:
3891:
3886:
3874:
3872:
3871:
3866:
3844:are as follows:
3843:
3841:
3840:
3835:
3807:
3805:
3804:
3799:
3700:Canonical models
3624:
3622:
3621:
3616:
3509:T, 5 or D, B, 4
3453:Frame condition
3444:
3443:
3420:
3418:
3417:
3412:
3388:
3386:
3385:
3380:
3365:
3363:
3362:
3357:
3327:
3325:
3324:
3319:
3258:
3256:
3255:
3250:
3205:
3203:
3202:
3197:
3182:
3180:
3179:
3174:
3148:
3146:
3145:
3140:
3125:
3123:
3122:
3117:
3078:
3076:
3075:
3070:
3040:
3038:
3037:
3032:
2985:partial function
2981:
2979:
2978:
2973:
2943:
2941:
2940:
2935:
2901:
2899:
2898:
2893:
2866:
2864:
2863:
2858:
2781:
2779:
2778:
2773:
2730:
2728:
2727:
2722:
2686:
2684:
2683:
2678:
2615:
2613:
2612:
2607:
2537:
2535:
2534:
2529:
2460:
2458:
2457:
2452:
2407:
2405:
2404:
2399:
2346:
2344:
2343:
2338:
2305:
2303:
2302:
2297:
2258:
2256:
2255:
2250:
2226:
2224:
2223:
2218:
2188:
2186:
2185:
2180:
2135:
2133:
2132:
2127:
2109:
2107:
2106:
2101:
2086:
2084:
2083:
2078:
2048:
2046:
2045:
2040:
1987:
1985:
1984:
1979:
1946:
1944:
1943:
1938:
1872:
1870:
1869:
1864:
1831:
1829:
1828:
1823:
1798:
1796:
1795:
1790:
1760:
1758:
1757:
1752:
1695:Frame condition
1686:
1685:
1679:'s numbering of
1665:L. E. J. Brouwer
1622:
1620:
1619:
1614:
1579:
1577:
1576:
1571:
1482:
1480:
1479:
1474:
1446:
1444:
1443:
1438:
1420:
1418:
1417:
1412:
1379:
1377:
1376:
1371:
1325:
1323:
1322:
1317:
1299:
1297:
1296:
1291:
1270:
1268:
1267:
1262:
1235:is valid in any
1230:
1228:
1227:
1222:
1025:
1023:
1022:
1017:
1005:
1003:
1002:
997:
967:
965:
964:
959:
924:
922:
921:
916:
898:
896:
895:
890:
830:
828:
827:
822:
811:”. The relation
799:is satisfied in
786:
784:
783:
778:
756:
754:
753:
748:
728:
726:
725:
720:
708:
706:
705:
700:
682:
680:
679:
674:
651:
649:
648:
643:
625:
623:
622:
617:
599:
597:
596:
591:
565:
563:
562:
557:
539:
537:
536:
531:
487:
485:
484:
479:
467:
465:
464:
459:
435:
433:
432:
427:
387:is known as the
354:
352:
351:
346:
306:
304:
303:
298:
264:
262:
261:
256:
240:
238:
237:
232:
220:
218:
217:
212:
200:
198:
197:
192:
180:
178:
177:
172:
93:Kripke semantics
85:
78:
74:
71:
65:
60:this article by
51:inline citations
38:
37:
30:
21:
8783:
8782:
8778:
8777:
8776:
8774:
8773:
8772:
8733:
8732:
8697:"Kripke models"
8695:
8650:"Kripke Models"
8644:
8634:
8592:
8571:
8543:
8528:
8514:
8503:
8494:
8477:
8475:
8473:
8449:
8447:
8445:
8424:
8406:Fitting, Melvin
8398:
8374:
8356:Van Dalen, Dirk
8348:
8328:Cresswell, M.J.
8320:
8299:
8276:
8258:Blackburn, P.;
8254:
8249:
8237:
8233:
8227:Goldblatt 2006b
8225:
8221:
8213:
8209:
8201:
8197:
8188:
8184:
8176:
8172:
8116:
8112:
8104:
8100:
8092:
8088:
8082:
8078:
8074:
8047:
8024:Jaakko Hintikka
7969:
7958:
7952:
7949:
7934:
7918:
7907:
7886:
7874:Main articles:
7872:
7859:
7828:
7825:
7824:
7823:if and only if
7802:
7799:
7798:
7786:
7733:
7730:
7729:
7704:
7701:
7700:
7675:
7672:
7671:
7601:
7590:
7579:
7574:
7571:
7570:
7528:
7525:
7524:
7476:
7472:
7463:
7459:
7444:
7440:
7431:
7427:
7415:
7405:
7401:
7386:
7382:
7373:
7369:
7364:
7361:
7360:
7326:
7322:
7320:
7317:
7316:
7315:if and only if
7294:
7291:
7290:
7279:
7275:
7251:
7247:
7232:
7228:
7219:
7215:
7204:
7201:
7200:
7174:
7163:
7152:
7147:
7144:
7143:
7137:
7098:
7095:
7094:
7049:
7041:
7039:
7036:
7035:
7034:if and only if
7013:
7010:
7009:
6998:atomic formulas
6990:u R v
6976:, there exists
6949:, there exists
6947:u R v
6912:
6901:
6896:
6893:
6892:
6864:
6861:
6860:
6859:between frames
6822:
6808:
6805:
6804:
6803:if and only if
6782:
6779:
6778:
6756:
6742:
6739:
6738:
6716:
6705:
6694:
6689:
6686:
6685:
6651:
6648:
6647:
6628:u R v
6577:u R v
6550:
6536:
6533:
6532:
6510:
6499:
6494:
6491:
6490:
6462:
6459:
6458:
6436:
6412:
6333:
6330:
6329:
6312:
6308:
6300:
6297:
6296:
6274:
6271:
6270:
6226:
6223:
6222:
6174:
6171:
6170:
6153:
6149:
6141:
6138:
6137:
6093:
6090:
6089:
6056:
6053:
6052:
6018:
6015:
6014:
5983:
5980:
5979:
5957:
5954:
5953:
5910:
5907:
5906:
5873:
5870:
5869:
5838:
5835:
5834:
5833:if and only if
5791:
5788:
5787:
5754:
5751:
5750:
5719:
5716:
5715:
5714:if and only if
5672:
5669:
5668:
5663:
5630:
5626:
5602:
5598:
5590:
5587:
5586:
5585:if and only if
5557:
5553:
5538:
5534:
5520:
5517:
5516:
5482:
5479:
5478:
5475:
5460:
5453:
5446:
5440:
5428:
5421:
5415:
5405:-ary predicate
5396:
5389:
5382:
5372:
5365:
5334:
5302:
5299:
5298:
5272:
5268:
5262:
5258:
5238:
5235:
5234:
5219:
5201:
5187:
5177:
5122:
5119:
5118:
5093:
5090:
5089:
5067:
5064:
5063:
5041:
5038:
5037:
5009:
5006:
5005:
4981:
4978:
4977:
4955:
4952:
4951:
4950:if and only if
4923:
4920:
4919:
4895:
4892:
4891:
4869:
4866:
4865:
4864:if and only if
4837:
4834:
4833:
4826:condition (cf.
4801:
4798:
4797:
4775:
4772:
4771:
4749:
4746:
4745:
4721:
4718:
4717:
4685:
4682:
4681:
4647:
4644:
4643:
4629:
4571:
4567:
4556:
4553:
4552:
4551:if and only if
4532:
4528:
4520:
4517:
4516:
4506:
4466:
4462:
4456:
4452:
4432:
4429:
4428:
4427:is a structure
4378:
4374:
4358:
4355:
4354:
4353:if and only if
4334:
4330:
4322:
4319:
4318:
4304:
4263:
4259:
4254:
4251:
4250:
4247:
4241:
4215:sequent calculi
4175:
4132:(in fact, even
4078:of formulas is
3983:
3980:
3979:
3978:if and only if
3957:
3954:
3953:
3929:
3926:
3925:
3900:
3897:
3896:
3880:
3877:
3876:
3852:
3849:
3848:
3829:
3826:
3825:
3775:
3772:
3771:
3764:canonical model
3710:canonical model
3702:
3543:
3540:
3539:
3431:
3394:
3391:
3390:
3371:
3368:
3367:
3348:
3345:
3344:
3277:
3274:
3273:
3213:
3210:
3209:
3188:
3185:
3184:
3165:
3162:
3161:
3131:
3128:
3127:
3086:
3083:
3082:
3052:
3049:
3048:
2992:
2989:
2988:
2955:
2952:
2951:
2909:
2906:
2905:
2878:
2875:
2874:
2789:
2786:
2785:
2749:
2746:
2745:
2733:(a complicated
2698:
2695:
2694:
2622:
2619:
2618:
2559:
2556:
2555:
2484:
2481:
2480:
2419:
2416:
2415:
2357:
2354:
2353:
2317:
2314:
2313:
2269:
2266:
2265:
2232:
2229:
2228:
2200:
2197:
2196:
2146:
2143:
2142:
2115:
2112:
2111:
2092:
2089:
2088:
2060:
2057:
2056:
1998:
1995:
1994:
1958:
1955:
1954:
1883:
1880:
1879:
1843:
1840:
1839:
1809:
1806:
1805:
1775:
1772:
1771:
1707:
1704:
1703:
1663:is named after
1655:is named after
1649:epistemic logic
1635:is named after
1629:
1593:
1590:
1589:
1538:
1535:
1534:
1532:
1525:
1518:
1511:
1504:
1468:
1465:
1464:
1426:
1423:
1422:
1397:
1394:
1393:
1380:if and only if
1359:
1356:
1355:
1305:
1302:
1301:
1276:
1273:
1272:
1244:
1241:
1240:
1207:
1204:
1203:
1114:
1011:
1008:
1007:
973:
970:
969:
941:
938:
937:
904:
901:
900:
866:
863:
862:
816:
813:
812:
766:
763:
762:
734:
731:
730:
714:
711:
710:
688:
685:
684:
683:if and only if
659:
656:
655:
631:
628:
627:
605:
602:
601:
600:if and only if
573:
570:
569:
545:
542:
541:
540:if and only if
516:
513:
512:
473:
470:
469:
441:
438:
437:
403:
400:
399:
365:binary relation
328:
325:
324:
313:
274:
271:
270:
250:
247:
246:
226:
223:
222:
206:
203:
202:
186:
183:
182:
166:
163:
162:
147:
141:
101:frame semantics
95:(also known as
86:
75:
69:
66:
56:Please help to
55:
39:
35:
28:
23:
22:
15:
12:
11:
5:
8781:
8771:
8770:
8765:
8760:
8755:
8750:
8745:
8731:
8730:
8711:
8693:
8674:
8658:
8656:on 2004-10-20.
8643:
8642:External links
8640:
8639:
8638:
8632:
8611:
8596:
8591:978-0521899437
8590:
8575:
8569:
8555:Moerdijk, Ieke
8547:
8541:
8518:
8512:
8484:
8471:
8456:
8444:978-3764385033
8443:
8428:
8422:
8402:
8396:
8378:
8372:
8352:
8346:
8324:
8318:
8303:
8297:
8280:
8274:
8253:
8250:
8248:
8247:
8231:
8219:
8207:
8195:
8182:
8178:Giaquinto 2002
8170:
8117:Note that the
8110:
8098:
8086:
8075:
8073:
8070:
8069:
8068:
8063:
8058:
8053:
8046:
8043:
8042:
8041:
8035:
8028:
8021:
8010:
8007:C. A. Meredith
8000:
7996:Bjarni Jónsson
7988:
7971:
7970:
7921:
7919:
7912:
7906:
7903:
7897:, which model
7884:model checking
7871:
7868:
7858:
7855:
7851:
7850:
7838:
7835:
7832:
7812:
7809:
7806:
7784:
7756:
7755:
7743:
7740:
7737:
7717:
7714:
7711:
7708:
7688:
7685:
7682:
7679:
7648:
7634:
7611:
7607:
7604:
7600:
7596:
7593:
7589:
7585:
7582:
7578:
7550:
7547:
7544:
7541:
7538:
7535:
7532:
7503:
7502:
7490:
7485:
7482:
7479:
7475:
7471:
7466:
7462:
7458:
7455:
7452:
7447:
7443:
7439:
7434:
7430:
7426:
7421:
7418:
7413:
7408:
7404:
7400:
7397:
7394:
7389:
7385:
7381:
7376:
7372:
7368:
7337:
7334:
7329:
7325:
7304:
7301:
7298:
7277:
7276: R w
7273:
7259:
7254:
7250:
7246:
7243:
7240:
7235:
7231:
7227:
7222:
7218:
7214:
7211:
7208:
7184:
7180:
7177:
7173:
7169:
7166:
7162:
7158:
7155:
7151:
7135:
7120:
7117:
7114:
7111:
7108:
7105:
7102:
7076:
7075:
7059:
7055:
7052:
7047:
7044:
7023:
7020:
7017:
6994:
6993:
6966:
6933:is a relation
6922:
6918:
6915:
6911:
6907:
6904:
6900:
6880:
6877:
6874:
6871:
6868:
6849:
6848:
6832:
6828:
6825:
6821:
6818:
6815:
6812:
6792:
6789:
6786:
6762:
6759:
6755:
6752:
6749:
6746:
6726:
6722:
6719:
6715:
6711:
6708:
6704:
6700:
6697:
6693:
6673:
6670:
6667:
6664:
6661:
6658:
6655:
6644:
6643:
6638:) =
6618:’, there is a
6600:
6556:
6553:
6549:
6546:
6543:
6540:
6520:
6516:
6513:
6509:
6505:
6502:
6498:
6478:
6475:
6472:
6469:
6466:
6435:
6432:
6411:
6408:
6380:
6379:
6367:
6364:
6361:
6358:
6355:
6352:
6349:
6346:
6343:
6340:
6337:
6315:
6311:
6307:
6304:
6284:
6281:
6278:
6258:
6255:
6252:
6249:
6246:
6242:
6239:
6236:
6233:
6230:
6220:
6208:
6205:
6202:
6199:
6196:
6193:
6190:
6187:
6184:
6181:
6178:
6156:
6152:
6148:
6145:
6125:
6122:
6119:
6116:
6113:
6109:
6106:
6103:
6100:
6097:
6087:
6075:
6072:
6069:
6066:
6063:
6060:
6049:
6037:
6034:
6031:
6028:
6025:
6022:
6002:
5999:
5996:
5993:
5990:
5987:
5967:
5964:
5961:
5941:
5938:
5935:
5932:
5929:
5926:
5923:
5920:
5917:
5914:
5904:
5892:
5889:
5886:
5883:
5880:
5877:
5857:
5854:
5851:
5848:
5845:
5842:
5822:
5819:
5816:
5813:
5810:
5807:
5804:
5801:
5798:
5795:
5785:
5773:
5770:
5767:
5764:
5761:
5758:
5738:
5735:
5732:
5729:
5726:
5723:
5703:
5700:
5697:
5694:
5691:
5688:
5685:
5682:
5679:
5676:
5666:
5661:
5647:
5644:
5641:
5638:
5633:
5629:
5625:
5622:
5619:
5616:
5613:
5610:
5605:
5601:
5597:
5594:
5574:
5571:
5568:
5565:
5560:
5556:
5552:
5549:
5546:
5541:
5537:
5533:
5530:
5527:
5524:
5501:
5498:
5495:
5492:
5489:
5486:
5473:
5464:
5463:
5458:
5451:
5444:
5438:
5426:
5419:
5413:
5399:
5394:
5387:
5380:
5375:
5370:
5363:
5360:the domain of
5332:
5318:
5315:
5312:
5309:
5306:
5286:
5281:
5278:
5275:
5271:
5265:
5261:
5257:
5254:
5251:
5248:
5245:
5242:
5218:
5215:
5199:
5193:vacuously true
5185:
5175:
5145:
5144:
5132:
5129:
5126:
5115:
5103:
5100:
5097:
5077:
5074:
5071:
5051:
5048:
5045:
5025:
5022:
5019:
5016:
5013:
5003:
4991:
4988:
4985:
4965:
4962:
4959:
4939:
4936:
4933:
4930:
4927:
4917:
4905:
4902:
4899:
4879:
4876:
4873:
4853:
4850:
4847:
4844:
4841:
4831:
4811:
4808:
4805:
4785:
4782:
4779:
4759:
4756:
4753:
4725:
4701:
4698:
4695:
4692:
4689:
4669:
4666:
4663:
4660:
4657:
4654:
4651:
4628:
4625:
4621:
4620:
4609:
4606:
4603:
4600:
4597:
4594:
4591:
4587:
4583:
4580:
4574:
4570:
4566:
4563:
4560:
4540:
4535:
4531:
4527:
4524:
4504:
4501:, and subsets
4486:
4483:
4480:
4475:
4472:
4469:
4465:
4459:
4455:
4451:
4448:
4445:
4442:
4439:
4436:
4417:
4416:
4405:
4402:
4399:
4396:
4393:
4390:
4387:
4381:
4377:
4372:
4369:
4365:
4362:
4342:
4337:
4333:
4329:
4326:
4302:
4284:
4281:
4278:
4275:
4271:
4266:
4262:
4258:
4240:
4237:
4225:modal algebras
4189:Post's theorem
4174:
4171:
4167:
4166:
4163:
4156:
4118:
4117:
4104:that contains
4098:
4006:
4005:
3993:
3990:
3987:
3967:
3964:
3961:
3951:
3939:
3936:
3933:
3913:
3910:
3907:
3904:
3884:
3864:
3860:
3856:
3833:
3797:
3794:
3791:
3788:
3785:
3782:
3779:
3701:
3698:
3695:
3694:
3691:
3688:
3684:
3683:
3678:
3675:
3671:
3670:
3664:
3661:
3657:
3656:
3650:
3647:
3640:
3639:
3633:
3630:
3626:
3625:
3614:
3611:
3608:
3605:
3602:
3599:
3596:
3592:
3588:
3585:
3581:
3578:
3575:
3572:
3568:
3564:
3561:
3557:
3554:
3550:
3547:
3536:
3533:
3529:
3528:
3526:total preorder
3523:
3520:
3516:
3515:
3510:
3507:
3501:
3500:
3495:
3492:
3488:
3487:
3484:
3481:
3477:
3476:
3473:
3470:
3466:
3465:
3462:
3459:
3455:
3454:
3451:
3448:
3430:
3427:
3410:
3407:
3404:
3401:
3398:
3378:
3375:
3355:
3352:
3317:
3314:
3311:
3308:
3305:
3302:
3299:
3296:
3293:
3290:
3287:
3284:
3281:
3260:
3259:
3248:
3245:
3241:
3237:
3234:
3231:
3227:
3224:
3220:
3217:
3206:
3195:
3192:
3172:
3169:
3159:
3155:
3154:
3138:
3135:
3115:
3111:
3107:
3103:
3100:
3097:
3093:
3090:
3079:
3068:
3065:
3062:
3059:
3056:
3046:
3042:
3041:
3030:
3027:
3024:
3021:
3018:
3014:
3010:
3007:
3004:
3000:
2996:
2982:
2971:
2968:
2965:
2962:
2959:
2949:
2945:
2944:
2933:
2930:
2927:
2924:
2921:
2917:
2913:
2902:
2891:
2888:
2885:
2882:
2872:
2868:
2867:
2856:
2853:
2849:
2845:
2842:
2839:
2835:
2831:
2828:
2824:
2821:
2818:
2815:
2811:
2807:
2804:
2801:
2797:
2793:
2782:
2771:
2768:
2765:
2762:
2759:
2756:
2753:
2743:
2739:
2738:
2731:
2720:
2717:
2714:
2711:
2708:
2705:
2702:
2692:
2688:
2687:
2676:
2672:
2668:
2665:
2662:
2658:
2654:
2651:
2648:
2644:
2640:
2637:
2634:
2630:
2626:
2616:
2605:
2602:
2599:
2596:
2593:
2590:
2587:
2584:
2581:
2578:
2575:
2572:
2569:
2566:
2563:
2553:
2549:
2548:
2538:
2527:
2524:
2521:
2518:
2515:
2512:
2509:
2506:
2503:
2500:
2497:
2494:
2491:
2488:
2478:
2474:
2473:
2461:
2450:
2447:
2444:
2441:
2438:
2435:
2432:
2429:
2426:
2423:
2413:
2409:
2408:
2397:
2393:
2389:
2386:
2383:
2379:
2375:
2372:
2369:
2365:
2361:
2347:
2336:
2333:
2330:
2327:
2324:
2321:
2311:
2307:
2306:
2295:
2291:
2287:
2284:
2281:
2277:
2273:
2259:
2248:
2245:
2242:
2239:
2236:
2216:
2213:
2210:
2207:
2204:
2194:
2190:
2189:
2178:
2175:
2171:
2167:
2164:
2160:
2157:
2153:
2150:
2136:
2125:
2122:
2119:
2099:
2096:
2076:
2073:
2070:
2067:
2064:
2054:
2050:
2049:
2038:
2034:
2030:
2027:
2024:
2020:
2016:
2013:
2010:
2006:
2002:
1988:
1977:
1974:
1971:
1968:
1965:
1962:
1952:
1948:
1947:
1936:
1933:
1929:
1925:
1922:
1919:
1915:
1911:
1908:
1904:
1901:
1898:
1895:
1891:
1887:
1873:
1862:
1859:
1856:
1853:
1850:
1847:
1837:
1833:
1832:
1821:
1817:
1813:
1799:
1788:
1785:
1782:
1779:
1769:
1765:
1764:
1761:
1750:
1747:
1744:
1741:
1738:
1735:
1732:
1729:
1726:
1723:
1720:
1717:
1714:
1711:
1701:
1697:
1696:
1693:
1690:
1628:
1625:
1612:
1609:
1606:
1603:
1600:
1597:
1569:
1566:
1563:
1560:
1557:
1554:
1551:
1548:
1545:
1542:
1530:
1523:
1516:
1509:
1502:
1496:incompleteness
1472:
1451:, which means
1436:
1433:
1430:
1410:
1407:
1404:
1401:
1369:
1366:
1363:
1315:
1312:
1309:
1289:
1286:
1283:
1280:
1260:
1257:
1254:
1251:
1248:
1220:
1217:
1214:
1211:
1137:For any class
1120:) only if the
1113:
1110:
1041:We define Thm(
1039:
1038:
1027:
1015:
995:
992:
989:
986:
983:
980:
977:
957:
954:
951:
948:
945:
934:
914:
911:
908:
888:
885:
882:
879:
876:
873:
870:
831:is called the
820:
776:
773:
770:
759:
758:
746:
742:
738:
718:
698:
695:
692:
672:
669:
666:
663:
653:
641:
638:
635:
615:
612:
609:
589:
586:
583:
580:
577:
567:
555:
552:
549:
529:
526:
523:
520:
477:
457:
454:
451:
448:
445:
425:
422:
419:
416:
413:
410:
407:
371:. Elements of
344:
341:
338:
335:
332:
312:
309:
296:
293:
290:
287:
284:
281:
278:
267:may be defined
254:
230:
210:
190:
170:
143:Main article:
140:
137:
107:) is a formal
88:
87:
42:
40:
33:
26:
9:
6:
4:
3:
2:
8780:
8769:
8766:
8764:
8761:
8759:
8756:
8754:
8751:
8749:
8746:
8744:
8741:
8740:
8738:
8727:
8726:
8721:
8717:
8712:
8708:
8704:
8703:
8698:
8694:
8690:
8689:
8684:
8680:
8679:"Modal Logic"
8675:
8670:
8669:
8664:
8659:
8655:
8651:
8646:
8645:
8635:
8633:9781134107070
8629:
8625:
8621:
8619:
8612:
8608:
8604:
8603:
8597:
8593:
8587:
8583:
8582:
8576:
8572:
8566:
8562:
8561:
8556:
8552:
8548:
8544:
8538:
8534:
8527:
8523:
8519:
8515:
8509:
8502:
8501:
8493:
8489:
8485:
8474:
8468:
8464:
8463:
8457:
8446:
8440:
8436:
8435:
8429:
8425:
8419:
8414:
8413:
8407:
8403:
8399:
8393:
8389:
8388:
8383:
8379:
8375:
8369:
8365:
8361:
8357:
8353:
8349:
8343:
8340:. Routledge.
8339:
8338:
8333:
8329:
8325:
8321:
8315:
8311:
8310:
8304:
8300:
8294:
8290:
8286:
8281:
8277:
8271:
8267:
8266:
8261:
8256:
8255:
8244:
8240:
8235:
8228:
8223:
8217:
8211:
8204:
8199:
8192:
8186:
8179:
8174:
8167:
8163:
8159:
8156:within which
8155:
8151:
8147:
8143:
8139:
8135:
8131:
8128:
8124:
8120:
8114:
8107:
8102:
8095:
8090:
8080:
8076:
8067:
8064:
8062:
8059:
8057:
8054:
8052:
8049:
8048:
8039:
8036:
8032:
8029:
8025:
8022:
8019:
8014:
8011:
8008:
8004:
8001:
7997:
7993:
7992:Alfred Tarski
7989:
7985:
7981:
7980:Rudolf Carnap
7978:
7977:
7976:
7967:
7964:
7956:
7946:
7942:
7938:
7932:
7931:
7927:
7922:This section
7920:
7916:
7911:
7910:
7902:
7900:
7896:
7892:
7885:
7881:
7877:
7867:
7865:
7864:general frame
7854:
7836:
7833:
7830:
7810:
7807:
7804:
7796:
7793: ∈
7792:
7788:
7781:
7780:
7779:
7777:
7773:
7769:
7765:
7761:
7741:
7738:
7735:
7715:
7712:
7709:
7706:
7686:
7683:
7680:
7677:
7669:
7665:
7661:
7657:
7653:
7649:
7646:
7643: ∈
7642:
7638:
7635:
7632:
7628:
7625:
7624:
7623:
7605:
7602:
7598:
7594:
7591:
7587:
7583:
7580:
7568:
7564:
7561:is a mapping
7545:
7542:
7539:
7536:
7533:
7522:
7518:
7514:
7510:
7506:
7483:
7480:
7477:
7473:
7469:
7464:
7460:
7456:
7453:
7450:
7445:
7441:
7437:
7432:
7428:
7419:
7416:
7406:
7402:
7398:
7395:
7392:
7387:
7383:
7379:
7374:
7370:
7359:
7358:
7357:
7355:
7351:
7335:
7332:
7327:
7323:
7302:
7299:
7296:
7288:
7284:
7280:
7252:
7248:
7244:
7241:
7238:
7233:
7229:
7225:
7220:
7216:
7209:
7206:
7198:
7178:
7175:
7171:
7167:
7164:
7160:
7156:
7153:
7141:
7138: ∈
7134:
7115:
7112:
7109:
7106:
7103:
7092:
7088:
7083:
7081:
7073:
7057:
7053:
7050:
7045:
7042:
7021:
7018:
7015:
7007:
7003:
7002:
7001:
6999:
6991:
6987:
6983:
6980: ∈
6979:
6975:
6971:
6967:
6964:
6960:
6956:
6953: ∈
6952:
6948:
6944:
6940:
6939:
6938:
6936:
6916:
6913:
6909:
6905:
6902:
6875:
6872:
6869:
6858:
6854:
6853:bisimulations
6846:
6830:
6826:
6823:
6816:
6810:
6790:
6787:
6784:
6777:
6776:
6775:
6760:
6757:
6750:
6747:
6744:
6720:
6717:
6713:
6709:
6706:
6702:
6698:
6695:
6668:
6665:
6662:
6659:
6656:
6641:
6637:
6633:
6629:
6625:
6622: ∈
6621:
6617:
6613:
6609:
6605:
6601:
6598:
6594:
6590:
6586:
6582:
6578:
6574:
6571:
6570:
6569:
6554:
6551:
6544:
6541:
6538:
6531:is a mapping
6514:
6511:
6507:
6503:
6500:
6473:
6470:
6467:
6456:
6452:
6448:
6447:homomorphisms
6443:
6441:
6431:
6429:
6425:
6421:
6417:
6407:
6405:
6401:
6397:
6393:
6389:
6385:
6359:
6353:
6347:
6341:
6338:
6335:
6313:
6309:
6305:
6302:
6282:
6279:
6276:
6253:
6244:
6240:
6231:
6228:
6221:
6200:
6194:
6188:
6182:
6179:
6176:
6154:
6150:
6146:
6143:
6120:
6111:
6107:
6098:
6095:
6088:
6070:
6061:
6058:
6050:
6032:
6026:
6023:
6020:
5997:
5991:
5988:
5985:
5965:
5962:
5959:
5936:
5927:
5921:
5915:
5912:
5905:
5887:
5881:
5878:
5875:
5852:
5846:
5843:
5840:
5817:
5808:
5805:
5802:
5796:
5793:
5786:
5768:
5762:
5759:
5756:
5733:
5727:
5724:
5721:
5698:
5689:
5686:
5683:
5677:
5674:
5667:
5664:
5639:
5631:
5627:
5623:
5620:
5617:
5611:
5603:
5599:
5592:
5569:
5558:
5554:
5550:
5547:
5544:
5539:
5535:
5528:
5525:
5522:
5515:
5514:
5513:
5496:
5490:
5487:
5484:
5476:
5469:
5461:
5454:
5447:
5437:
5433:
5429:
5423: ∈
5422:
5412:
5409:and elements
5408:
5404:
5400:
5397:
5390:
5383:
5376:
5373:
5366:
5359:
5358:
5357:
5355:
5352: ≤
5351:
5347:
5344: ∈
5343:
5339:
5335:
5313:
5310:
5307:
5279:
5276:
5273:
5263:
5259:
5252:
5249:
5246:
5243:
5232:
5228:
5224:
5214:
5212:
5207:
5205:
5198:
5194:
5190:
5184:
5180:
5174:
5170:
5166:
5162:
5158:
5154:
5150:
5127:
5124:
5116:
5101:
5098:
5095:
5075:
5072:
5069:
5049:
5046:
5043:
5023:
5017:
5014:
5011:
5004:
4989:
4986:
4983:
4963:
4960:
4957:
4937:
4934:
4931:
4928:
4925:
4918:
4903:
4900:
4897:
4877:
4874:
4871:
4851:
4848:
4845:
4842:
4839:
4832:
4829:
4825:
4809:
4806:
4803:
4783:
4780:
4777:
4757:
4754:
4751:
4743:
4739:
4738:
4737:
4723:
4715:
4696:
4693:
4690:
4664:
4661:
4658:
4655:
4652:
4641:
4636:
4634:
4624:
4607:
4601:
4598:
4595:
4589:
4585:
4581:
4572:
4568:
4564:
4561:
4538:
4533:
4529:
4525:
4522:
4515:
4514:
4513:
4511:
4508: ⊆
4507:
4500:
4481:
4478:
4473:
4470:
4467:
4457:
4453:
4446:
4443:
4440:
4437:
4426:
4425:Carlson model
4422:
4403:
4397:
4394:
4391:
4385:
4379:
4375:
4370:
4363:
4340:
4335:
4331:
4327:
4324:
4317:
4316:
4315:
4313:
4310: ∈
4309:
4305:
4298:
4279:
4276:
4273:
4269:
4264:
4260:
4246:
4236:
4234:
4230:
4226:
4221:
4218:
4216:
4213:
4209:
4205:
4200:
4198:
4194:
4190:
4186:
4182:
4181:
4170:
4164:
4161:
4157:
4154:
4153:
4152:
4150:
4146:
4142:
4137:
4135:
4131:
4125:
4123:
4115:
4111:
4107:
4103:
4099:
4096:
4092:
4089:
4088:
4087:
4085:
4081:
4077:
4072:
4070:
4066:
4062:
4058:
4054:
4050:
4045:
4043:
4039:
4035:
4031:
4027:
4023:
4019:
4015:
4011:
3991:
3988:
3985:
3965:
3962:
3959:
3952:
3937:
3934:
3931:
3911:
3908:
3905:
3902:
3882:
3862:
3858:
3854:
3847:
3846:
3845:
3831:
3823:
3819:
3815:
3811:
3792:
3789:
3786:
3783:
3780:
3769:
3765:
3760:
3758:
3754:
3750:
3746:
3742:
3738:
3734:
3730:
3725:
3723:
3719:
3715:
3711:
3707:
3692:
3689:
3686:
3685:
3682:
3679:
3676:
3673:
3672:
3669:
3668:partial order
3665:
3662:
3659:
3658:
3655:
3651:
3648:
3645:
3642:
3641:
3637:
3634:
3631:
3628:
3627:
3606:
3603:
3600:
3594:
3590:
3586:
3579:
3573:
3570:
3566:
3562:
3555:
3548:
3537:
3534:
3531:
3530:
3527:
3524:
3521:
3518:
3517:
3514:
3511:
3508:
3506:
3503:
3502:
3499:
3496:
3493:
3490:
3489:
3485:
3482:
3479:
3478:
3474:
3471:
3468:
3467:
3463:
3460:
3456:
3452:
3449:
3446:
3445:
3442:
3440:
3436:
3426:
3424:
3405:
3399:
3396:
3373:
3353:
3350:
3342:
3337:
3335:
3331:
3315:
3312:
3303:
3300:
3294:
3288:
3279:
3271:
3267:
3243:
3239:
3235:
3225:
3218:
3207:
3190:
3170:
3167:
3160:
3157:
3156:
3152:
3136:
3113:
3109:
3105:
3101:
3098:
3091:
3080:
3066:
3063:
3057:
3054:
3047:
3044:
3043:
3028:
3025:
3022:
3016:
3012:
3008:
3005:
3002:
2998:
2994:
2986:
2983:
2969:
2966:
2960:
2957:
2950:
2947:
2946:
2931:
2928:
2925:
2919:
2915:
2911:
2903:
2889:
2886:
2880:
2873:
2870:
2869:
2851:
2847:
2843:
2840:
2837:
2833:
2829:
2822:
2813:
2809:
2805:
2802:
2799:
2795:
2791:
2783:
2769:
2766:
2763:
2757:
2754:
2751:
2744:
2741:
2740:
2736:
2732:
2718:
2715:
2712:
2706:
2703:
2700:
2693:
2690:
2689:
2674:
2670:
2666:
2663:
2660:
2656:
2652:
2646:
2642:
2638:
2635:
2632:
2628:
2624:
2617:
2600:
2594:
2591:
2585:
2582:
2576:
2570:
2567:
2561:
2554:
2551:
2550:
2546:
2542:
2539:
2525:
2516:
2507:
2504:
2498:
2492:
2486:
2479:
2476:
2475:
2472:
2469:
2465:
2462:
2448:
2445:
2436:
2430:
2427:
2421:
2414:
2411:
2410:
2395:
2391:
2387:
2381:
2377:
2373:
2370:
2367:
2363:
2359:
2351:
2348:
2334:
2331:
2328:
2322:
2319:
2312:
2309:
2308:
2293:
2289:
2285:
2279:
2275:
2271:
2263:
2260:
2246:
2240:
2237:
2234:
2214:
2211:
2208:
2202:
2195:
2192:
2191:
2173:
2169:
2165:
2158:
2151:
2140:
2137:
2120:
2094:
2074:
2071:
2065:
2062:
2055:
2052:
2051:
2036:
2032:
2028:
2022:
2018:
2014:
2011:
2008:
2004:
2000:
1992:
1989:
1975:
1972:
1969:
1963:
1960:
1953:
1950:
1949:
1931:
1927:
1923:
1920:
1917:
1913:
1909:
1902:
1893:
1889:
1885:
1877:
1874:
1860:
1857:
1851:
1848:
1845:
1838:
1835:
1834:
1819:
1815:
1811:
1803:
1800:
1786:
1780:
1777:
1770:
1767:
1766:
1762:
1745:
1742:
1736:
1733:
1721:
1715:
1709:
1702:
1699:
1698:
1694:
1691:
1688:
1687:
1684:
1682:
1678:
1674:
1670:
1667:; and axioms
1666:
1662:
1658:
1657:deontic logic
1654:
1650:
1646:
1642:
1638:
1634:
1624:
1610:
1607:
1604:
1598:
1595:
1587:
1583:
1567:
1564:
1555:
1552:
1546:
1540:
1529:
1522:
1515:
1508:
1505: ⊆
1501:
1497:
1493:
1488:
1486:
1470:
1462:
1458:
1454:
1450:
1434:
1431:
1428:
1408:
1405:
1402:
1399:
1391:
1387:
1383:
1367:
1364:
1361:
1353:
1349:
1346: ∈
1345:
1341:
1337:
1333:
1329:
1313:
1310:
1307:
1287:
1284:
1281:
1278:
1255:
1252:
1249:
1238:
1234:
1218:
1212:
1209:
1201:
1196:
1194:
1190:
1187:is sound wrt
1186:
1182:
1178:
1174:
1170:
1166:
1163:
1158:
1156:
1152:
1148:
1144:
1140:
1135:
1133:
1129:
1128:
1123:
1119:
1109:
1107:
1103:
1099:
1095:
1094:
1089:
1085:
1081:
1077:
1073:
1072:
1067:
1062:
1060:
1056:
1052:
1048:
1044:
1036:
1032:
1028:
1013:
990:
987:
984:
981:
978:
952:
949:
946:
935:
932:
929: ∈
928:
912:
909:
906:
883:
880:
877:
874:
871:
860:
859:
858:
856:
852:
847:
845:
843:
838:
834:
818:
810:
806:
802:
798:
794:
790:
774:
771:
768:
744:
740:
736:
716:
696:
693:
690:
670:
667:
664:
661:
654:
639:
636:
633:
613:
610:
607:
587:
581:
578:
575:
568:
553:
550:
547:
527:
521:
518:
511:
510:
509:
507:
503:
499:
496: ∈
495:
491:
475:
452:
449:
446:
420:
417:
414:
411:
408:
397:
392:
390:
386:
382:
378:
374:
370:
366:
362:
358:
339:
336:
333:
322:
318:
308:
294:
288:
282:
279:
276:
268:
252:
244:
228:
208:
160:
156:
152:
146:
136:
134:
130:
126:
122:
118:
114:
110:
106:
102:
98:
94:
84:
81:
73:
63:
59:
53:
52:
46:
41:
32:
31:
19:
8763:Sheaf theory
8748:Model theory
8723:
8700:
8686:
8667:
8654:the original
8623:
8617:
8601:
8580:
8563:. Springer.
8559:
8532:
8499:
8476:. Retrieved
8461:
8448:. Retrieved
8433:
8411:
8386:
8363:
8336:
8332:Hughes, G.E.
8308:
8288:
8264:
8260:de Rijke, M.
8242:
8239:Stokhof 2008
8234:
8222:
8210:
8203:Simpson 1994
8198:
8185:
8173:
8165:
8161:
8157:
8153:
8149:
8145:
8141:
8137:
8133:
8129:
8126:
8122:
8118:
8113:
8101:
8089:
8079:
8003:Arthur Prior
7983:
7974:
7959:
7953:October 2009
7950:
7935:Please help
7923:
7893:, they give
7887:
7860:
7852:
7794:
7790:
7782:
7775:
7767:
7763:
7759:
7757:
7667:
7663:
7659:
7655:
7651:
7644:
7640:
7636:
7626:
7566:
7562:
7520:
7516:
7508:
7507:
7504:
7353:
7349:
7286:
7282:
7271:
7196:
7139:
7132:
7090:
7084:
7079:
7077:
7071:
7005:
6995:
6989:
6985:
6981:
6977:
6973:
6969:
6962:
6958:
6954:
6950:
6946:
6942:
6934:
6857:bisimulation
6856:
6850:
6844:
6645:
6639:
6635:
6631:
6627:
6623:
6619:
6615:
6611:
6607:
6603:
6596:
6592:
6588:
6584:
6580:
6576:
6572:
6454:
6450:
6445:The natural
6444:
6440:model theory
6437:
6427:
6424:topos theory
6416:sheaf theory
6413:
6403:
6399:
6395:
6391:
6387:
6383:
6381:
5659:
5471:
5467:
5465:
5456:
5449:
5442:
5435:
5431:
5424:
5417:
5410:
5406:
5402:
5392:
5385:
5378:
5368:
5361:
5353:
5349:
5345:
5341:
5337:
5330:
5233:is a triple
5230:
5222:
5220:
5208:
5203:
5196:
5188:
5182:
5178:
5172:
5168:
5164:
5160:
5156:
5152:
5148:
5146:
4828:monotonicity
4823:
4741:
4642:is a triple
4639:
4637:
4630:
4622:
4509:
4502:
4498:
4424:
4418:
4311:
4307:
4300:
4296:
4248:
4232:
4228:
4222:
4219:
4201:
4196:
4192:
4185:decidability
4178:
4176:
4168:
4151:) such that
4138:
4133:
4129:
4126:
4119:
4113:
4109:
4105:
4101:
4094:
4090:
4083:
4079:
4075:
4073:
4068:
4064:
4060:
4056:
4052:
4048:
4046:
4041:
4037:
4033:
4029:
4026:Zorn's lemma
4021:
4017:
4013:
4009:
4007:
3821:
3817:
3813:
3809:
3767:
3763:
3761:
3756:
3752:
3748:
3744:
3740:
3736:
3732:
3728:
3726:
3713:
3709:
3705:
3703:
3649:GL or 4, GL
3438:
3434:
3432:
3340:
3338:
3330:modus ponens
3268:can also be
3265:
3263:
2784:convergent:
2735:second-order
2544:
2540:
2471:well-founded
2467:
2466:transitive,
2463:
1672:
1668:
1660:
1652:
1640:
1632:
1630:
1585:
1581:
1527:
1520:
1513:
1506:
1499:
1495:
1491:
1489:
1484:
1460:
1456:
1452:
1448:
1389:
1385:
1381:
1354:as follows:
1351:
1347:
1343:
1339:
1335:
1331:
1327:
1232:
1199:
1197:
1192:
1188:
1184:
1180:
1176:
1172:
1168:
1164:
1161:
1159:
1150:
1142:
1138:
1136:
1132:derivability
1131:
1125:
1115:
1105:
1101:
1097:
1091:
1087:
1083:
1079:
1075:
1069:
1065:
1063:
1058:
1054:
1050:
1046:
1042:
1040:
1034:
1030:
930:
926:
854:
850:
848:
840:
836:
832:
808:
804:
800:
796:
792:
788:
760:
505:
501:
497:
493:
489:
398:is a triple
396:Kripke model
395:
393:
384:
380:
376:
372:
368:
360:
356:
320:
317:Kripke frame
316:
314:
148:
133:model theory
125:modal logics
100:
96:
92:
91:
76:
67:
48:
8743:Modal logic
8478:24 December
8450:24 December
8309:Modal Logic
8265:Modal Logic
8013:Stig Kanger
7866:semantics.
7569:to a model
7091:unravelling
6451:p-morphisms
5448:) holds in
5227:first-order
4824:persistency
4208:unravelling
4160:first-order
4141:undecidable
4012:, as every
3660:Grz, S4Grz
3486:transitive
3464:all frames
1677:C. I. Lewis
1645:truth axiom
1637:Saul Kripke
1588:-tautology
1165:corresponds
375:are called
321:modal frame
159:connectives
145:Modal logic
121:André Joyal
117:Saul Kripke
62:introducing
8737:Categories
8605:(Thesis).
8542:1904987206
8472:019875244X
8252:References
8166:as a whole
8142:a model of
8034:community;
7631:surjection
7622:such that
7509:Filtration
7270:such that
6984:such that
6957:such that
6626:such that
6568:such that
6398:the value
6295:and every
6169:such that
5163:such that
4714:preordered
4243:See also:
4204:filtration
4162:definable,
4112:satisfies
3733:consistent
3538:preorder,
3475:reflexive
3439:correspond
3081:function:
2904:discrete:
2737:property)
1991:transitive
1130:relation (
849:A formula
837:evaluation
791:satisfies
729:such that
323:is a pair
70:April 2013
45:references
8707:EMS Press
8618:Tractatus
8557:(2012) .
8524:(2006b).
8490:(2006a).
8358:(2013) .
8334:(2012) .
8146:formula F
7924:does not
7834:⊩
7808:⊩
7739:⊩
7713:∈
7707:◻
7684:◻
7681:⊩
7610:⟩
7603:⊩
7577:⟨
7549:⟩
7546:⊩
7531:⟨
7489:⟩
7454:…
7425:⟨
7412:⟩
7396:…
7367:⟨
7333:⊩
7300:⊩
7258:⟩
7242:…
7213:⟨
7183:⟩
7176:⊩
7150:⟨
7119:⟩
7116:⊩
7101:⟨
7051:⊩
7019:⊩
6921:⟩
6899:⟨
6879:⟩
6867:⟨
6824:⊩
6788:⊩
6754:→
6748::
6725:⟩
6718:⊩
6692:⟨
6672:⟩
6669:⊩
6654:⟨
6602:whenever
6548:→
6542::
6519:⟩
6497:⟨
6477:⟩
6465:⟨
6357:→
6339:⊩
6306:∈
6280:≥
6238:∀
6232:⊩
6198:→
6180:⊩
6147:∈
6105:∃
6099:⊩
6065:⊥
6062:⊩
6024:⊩
5989:⊩
5963:≥
5925:→
5916:⊩
5879:⊩
5844:⊩
5806:∨
5797:⊩
5760:⊩
5725:⊩
5687:∧
5678:⊩
5658:holds in
5621:…
5548:…
5526:⊩
5488:⊩
5401:for each
5317:⟩
5314:≤
5305:⟨
5285:⟩
5277:∈
5250:≤
5241:⟨
5131:⊥
5128:⊩
5099:⊩
5073:⊩
5047:≥
5021:→
5015:⊩
4987:⊩
4961:⊩
4935:∨
4929:⊩
4901:⊩
4875:⊩
4849:∧
4843:⊩
4807:⊩
4781:⊩
4755:≤
4724:⊩
4700:⟩
4697:≤
4688:⟨
4668:⟩
4665:⊩
4659:≤
4650:⟨
4599:⊩
4593:⇒
4565:∈
4559:∀
4530:◻
4526:⊩
4485:⟩
4482:⊩
4471:∈
4435:⟨
4395:⊩
4389:⇒
4361:∀
4332:◻
4328:⊩
4306:for each
4277:∈
4270:∣
4261:◻
4080:canonical
3989:∈
3963:⊩
3935:∈
3909:∈
3903:◻
3832:⊩
3796:⟩
3793:⊩
3778:⟨
3638:preorder
3598:⇒
3577:∀
3574:∧
3553:∃
3546:∀
3409:⊤
3406:◊
3403:→
3397:◊
3377:⊤
3374:◊
3351:◊
3313:◻
3310:→
3301:∧
3292:→
3280:◻
3270:rewritten
3230:¬
3223:∀
3216:∀
3194:⊥
3191:◻
3168:◻
3134:∃
3096:∃
3089:∀
3064:◻
3061:↔
3055:◊
3020:⇒
3006:∧
2967:◻
2964:→
2958:◊
2923:⇒
2887:◻
2884:→
2841:∧
2820:∃
2817:⇒
2803:∧
2767:◊
2764:◻
2761:→
2755:◻
2752:◊
2716:◻
2713:◊
2710:→
2704:◊
2701:◻
2664:∨
2650:⇒
2636:∧
2598:→
2592:◻
2586:◻
2583:∨
2574:→
2568:◻
2562:◻
2523:→
2514:→
2505:◻
2502:→
2493:◻
2487:◻
2446:◻
2443:→
2434:→
2428:◻
2422:◻
2385:⇒
2371:∧
2350:Euclidean
2332:◊
2329:◻
2326:→
2320:◊
2283:⇒
2264: :
2262:symmetric
2244:→
2238:◻
2235:◊
2212:◊
2209:◻
2206:→
2156:∃
2149:∀
2124:⊥
2121:◻
2118:¬
2098:⊤
2095:◊
2072:◊
2069:→
2063:◻
2026:⇒
2012:∧
1973:◻
1970:◻
1967:→
1961:◻
1921:∧
1900:∃
1897:⇒
1858:◻
1855:→
1849:◻
1846:◻
1802:reflexive
1784:→
1778:◻
1743:◻
1740:→
1734:◻
1728:→
1719:→
1710:◻
1608:◻
1605:◻
1602:→
1596:◻
1565:◻
1562:→
1553:◻
1550:↔
1541:◻
1471:⊩
1432:⊩
1406:◻
1403:⊩
1365:⊩
1311:⊩
1285:◻
1282:⊩
1259:⟩
1247:⟨
1237:reflexive
1216:→
1210:◻
1014:⊩
994:⟩
991:⊩
976:⟨
956:⟩
944:⟨
910:⊩
887:⟩
884:⊩
869:⟨
819:⊩
772:⊩
694:⊩
668:◻
665:⊩
637:⊩
611:⊮
585:→
579:⊩
551:⊮
525:¬
522:⊩
476:⊩
456:⟩
444:⟨
424:⟩
421:⊩
406:⟨
343:⟩
331:⟨
292:¬
289:◻
286:¬
277:◊
253:◻
229:◊
209:◻
189:¬
169:→
109:semantics
8408:(1969).
8384:(2000).
8045:See also
7783:u ≡
7772:quotient
7699:, where
7606:′
7595:′
7584:′
7420:′
7281:for all
7195:, where
7179:′
7168:′
7157:′
7054:′
7046:′
6917:′
6906:′
6827:′
6761:′
6721:′
6710:′
6699:′
6579:implies
6555:′
6515:′
6504:′
6013:implies
5297:, where
5088:implies
4680:, where
4227:, and a
4212:cut-free
3808:, where
3690:D, 4, 5
3636:directed
3632:T, 4, G
3535:T, 4, M
3522:T, 4, H
3498:preorder
1659:; axiom
1651:; axiom
1639:; axiom
1202: :
1093:complete
1029:a class
936:a frame
925:for all
861:a model
844:relation
761:We read
709:for all
436:, where
355:, where
8722:(ed.).
8709:, 2001
8685:(ed.).
8123:differs
7987:Tarski;
7945:removed
7930:sources
7787: v
7728:, then
7658:)
7008:, then
6610:)
6587:)
5191:→ ⊥ is
5181:, then
4796:, then
4122:compact
4028:, each
3666:finite
3652:finite
3208:empty:
3149:is the
1526:. Then
1421:, thus
1392:. Then
1300:, then
1145:) is a
842:forcing
807:forces
803:”, or “
58:improve
8630:
8588:
8567:
8539:
8510:
8469:
8441:
8420:
8394:
8370:
8344:
8316:
8295:
8272:
8189:After
8162:within
8119:notion
8027:proof;
7882:, and
7670:) and
7662:
7289:, and
7089:using
6614:
6591:
5171:, not
4770:, and
4229:finite
3681:serial
3646:, K4W
3450:Axioms
3264:Axiom
2139:serial
1459:
1455:
1388:
1384:
1334:
1330:
1326:since
1239:frame
383:, and
381:worlds
47:, but
8718:. In
8681:. In
8529:(PDF)
8504:(PDF)
8495:(PDF)
8072:Notes
8018:Lewis
7999:time.
7629:is a
7565:from
6382:Here
5441:,...,
5430:: if
5416:,...,
5225:be a
5195:, so
4712:is a
4065:frame
4024:. By
3924:then
3895:, if
3629:S4.2
3532:S4.1
3519:S4.3
3494:T, 4
3332:as a
1876:dense
1692:Axiom
1271:: if
1171:, if
1078:, if
1071:sound
899:, if
855:valid
839:, or
377:nodes
363:is a
8628:ISBN
8586:ISBN
8565:ISBN
8537:ISBN
8508:ISBN
8480:2014
8467:ISBN
8452:2014
8439:ISBN
8418:ISBN
8392:ISBN
8368:ISBN
8342:ISBN
8314:ISBN
8293:ISBN
8270:ISBN
8144:the
7928:any
7926:cite
7862:the
7087:tree
6988:and
6972:and
6961:and
6945:and
6891:and
6684:and
6630:and
6489:and
6422:in
6051:not
5749:and
5384:and
5221:Let
5117:not
4890:and
4423:. A
4233:S4.3
4134:K4.1
4130:S4.1
3824:and
3762:The
3743:(an
3687:D45
3447:Name
2477:Grz
1689:Name
1671:and
1096:wrt
857:in:
795:”, “
787:as “
504:and
265:and
243:dual
181:and
119:and
111:for
8158:any
8150:not
8130:has
7939:by
7774:of
7650:if
7513:FMP
7278:i+1
7080:all
7004:if
6968:if
6941:if
5868:or
5151:, ¬
4976:or
4830:)),
4740:if
4638:An
4206:or
4057:not
4038:MCS
4018:MCS
3818:MCS
3766:of
3749:MCS
3491:S4
3480:K4
3272:as
3183:or
2987::
2412:GL
2227:or
2110:or
2087:or
1647:in
1447:by
1108:).
1100:if
1090:is
1086:).
1068:is
853:is
626:or
379:or
367:on
319:or
245:of
153:of
99:or
8739::
8705:,
8699:,
8665:.
8553:;
8330:;
8245:..
7878:,
7797:,
7660:R’
7354:R’
7197:W’
7000::
6955:W’
6951:v’
6642:’.
6612:R’
6599:),
6589:R’
6406:.
6328:,
5978:,
5512::
5356::
5213:.
5206:.
5167:≤
5062:,
4124:.
4071:.
3677:D
3674:D
3644:GL
3505:S5
3483:4
3472:T
3469:T
3461:—
3458:K
3425:.
3343:,
3158:-
3153:)
3045:-
2948:-
2871:-
2742:G
2691:M
2552:H
2352::
2310:5
2193:B
2141::
2053:D
1993::
1951:4
1878::
1836:-
1804::
1768:T
1700:K
1683:.
1623:.
1586:GL
1582:GL
1483:.
1231:.
1157:.
1061:.
835:,
508::
394:A
391:.
315:A
283::=
8728:.
8691:.
8636:.
8609:.
8594:.
8573:.
8545:.
8516:.
8482:.
8454:.
8426:.
8400:.
8376:.
8350:.
8322:.
8301:.
8278:.
8229:.
8193:.
8180:.
8138:F
8134:F
8127:F
8096:.
7966:)
7960:(
7955:)
7951:(
7947:.
7933:.
7849:.
7837:A
7831:v
7811:A
7805:u
7795:X
7791:A
7785:X
7776:W
7768:f
7764:X
7760:f
7754:.
7742:A
7736:v
7716:X
7710:A
7687:A
7678:u
7668:v
7666:(
7664:f
7656:u
7654:(
7652:f
7647:,
7645:X
7641:p
7637:f
7633:,
7627:f
7599:,
7592:R
7588:,
7581:W
7567:W
7563:f
7543:,
7540:R
7537:,
7534:W
7521:X
7517:X
7501:,
7484:1
7481:+
7478:n
7474:w
7470:,
7465:n
7461:w
7457:,
7451:,
7446:1
7442:w
7438:,
7433:0
7429:w
7417:R
7407:n
7403:w
7399:,
7393:,
7388:1
7384:w
7380:,
7375:0
7371:w
7350:p
7336:p
7328:n
7324:w
7303:p
7297:s
7287:n
7283:i
7274:i
7272:w
7253:n
7249:w
7245:,
7239:,
7234:1
7230:w
7226:,
7221:0
7217:w
7210:=
7207:s
7172:,
7165:R
7161:,
7154:W
7140:W
7136:0
7133:w
7113:,
7110:R
7107:,
7104:W
7074:.
7072:p
7058:p
7043:w
7022:p
7016:w
6992:.
6982:W
6978:v
6965:,
6914:R
6910:,
6903:W
6876:R
6873:,
6870:W
6847:.
6845:p
6831:p
6820:)
6817:w
6814:(
6811:f
6791:p
6785:w
6758:W
6751:W
6745:f
6714:,
6707:R
6703:,
6696:W
6666:,
6663:R
6660:,
6657:W
6640:v
6636:v
6634:(
6632:f
6624:W
6620:v
6616:v
6608:u
6606:(
6604:f
6597:v
6595:(
6593:f
6585:u
6583:(
6581:f
6573:f
6552:W
6545:W
6539:f
6512:R
6508:,
6501:W
6474:R
6471:,
6468:W
6404:e
6400:a
6396:x
6392:a
6390:→
6388:x
6386:(
6384:e
6378:.
6366:]
6363:)
6360:a
6354:x
6351:(
6348:e
6345:[
6342:A
6336:u
6314:u
6310:M
6303:a
6283:w
6277:u
6257:]
6254:e
6251:[
6248:)
6245:A
6241:x
6235:(
6229:w
6219:,
6207:]
6204:)
6201:a
6195:x
6192:(
6189:e
6186:[
6183:A
6177:w
6155:w
6151:M
6144:a
6124:]
6121:e
6118:[
6115:)
6112:A
6108:x
6102:(
6096:w
6086:,
6074:]
6071:e
6068:[
6059:w
6048:,
6036:]
6033:e
6030:[
6027:B
6021:u
6001:]
5998:e
5995:[
5992:A
5986:u
5966:w
5960:u
5940:]
5937:e
5934:[
5931:)
5928:B
5922:A
5919:(
5913:w
5903:,
5891:]
5888:e
5885:[
5882:B
5876:w
5856:]
5853:e
5850:[
5847:A
5841:w
5821:]
5818:e
5815:[
5812:)
5809:B
5803:A
5800:(
5794:w
5784:,
5772:]
5769:e
5766:[
5763:B
5757:w
5737:]
5734:e
5731:[
5728:A
5722:w
5702:]
5699:e
5696:[
5693:)
5690:B
5684:A
5681:(
5675:w
5665:,
5662:w
5660:M
5646:)
5643:]
5640:e
5637:[
5632:n
5628:t
5624:,
5618:,
5615:]
5612:e
5609:[
5604:1
5600:t
5596:(
5593:P
5573:]
5570:e
5567:[
5564:)
5559:n
5555:t
5551:,
5545:,
5540:1
5536:t
5532:(
5529:P
5523:w
5500:]
5497:e
5494:[
5491:A
5485:w
5474:w
5472:M
5468:e
5462:.
5459:v
5457:M
5452:u
5450:M
5445:n
5443:a
5439:1
5436:a
5434:(
5432:P
5427:u
5425:M
5420:n
5418:a
5414:1
5411:a
5407:P
5403:n
5398:,
5395:u
5393:M
5388:v
5386:M
5381:u
5379:M
5374:,
5371:v
5369:M
5364:u
5362:M
5354:v
5350:u
5346:W
5342:w
5338:L
5333:w
5331:M
5311:,
5308:W
5280:W
5274:w
5270:}
5264:w
5260:M
5256:{
5253:,
5247:,
5244:W
5231:L
5223:L
5204:A
5202:¬
5200:⊩
5197:w
5189:A
5186:⊩
5183:w
5179:A
5176:⊩
5173:u
5169:u
5165:w
5161:u
5157:A
5153:A
5149:A
5143:.
5125:w
5114:,
5102:B
5096:u
5076:A
5070:u
5050:w
5044:u
5024:B
5018:A
5012:w
5002:,
4990:B
4984:w
4964:A
4958:w
4938:B
4932:A
4926:w
4916:,
4904:B
4898:w
4878:A
4872:w
4852:B
4846:A
4840:w
4822:(
4810:p
4804:u
4784:p
4778:w
4758:u
4752:w
4742:p
4694:,
4691:W
4662:,
4656:,
4653:W
4608:.
4605:)
4602:A
4596:u
4590:u
4586:R
4582:w
4579:(
4573:i
4569:D
4562:u
4539:A
4534:i
4523:w
4510:W
4505:i
4503:D
4499:R
4479:,
4474:I
4468:i
4464:}
4458:i
4454:D
4450:{
4447:,
4444:R
4441:,
4438:W
4404:.
4401:)
4398:A
4392:u
4386:u
4380:i
4376:R
4371:w
4368:(
4364:u
4341:A
4336:i
4325:w
4312:I
4308:i
4303:i
4301:R
4297:W
4283:}
4280:I
4274:i
4265:i
4257:{
4197:L
4193:L
4116:.
4114:P
4110:L
4106:X
4102:L
4097:,
4095:P
4091:X
4084:P
4076:X
4069:L
4061:L
4053:K
4049:K
4042:L
4036:-
4034:L
4030:L
4022:L
4016:-
4014:L
4010:L
4004:.
3992:X
3986:A
3966:A
3960:X
3950:,
3938:Y
3932:A
3912:X
3906:A
3883:A
3863:Y
3859:R
3855:X
3822:R
3816:-
3814:L
3810:W
3790:,
3787:R
3784:,
3781:W
3768:L
3757:L
3753:L
3747:-
3745:L
3737:L
3731:-
3729:L
3714:L
3706:L
3613:)
3610:)
3607:v
3604:=
3601:u
3595:v
3591:R
3587:u
3584:(
3580:v
3571:u
3567:R
3563:w
3560:(
3556:u
3549:w
3400:A
3354:A
3341:D
3316:B
3307:]
3304:A
3298:)
3295:B
3289:A
3286:(
3283:[
3266:K
3247:)
3244:u
3240:R
3236:w
3233:(
3226:u
3219:w
3171:A
3137:!
3126:(
3114:u
3110:R
3106:w
3102:u
3099:!
3092:w
3067:A
3058:A
3029:v
3026:=
3023:u
3017:v
3013:R
3009:w
3003:u
2999:R
2995:w
2970:A
2961:A
2932:v
2929:=
2926:w
2920:v
2916:R
2912:w
2890:A
2881:A
2855:)
2852:x
2848:R
2844:v
2838:x
2834:R
2830:u
2827:(
2823:x
2814:v
2810:R
2806:w
2800:u
2796:R
2792:w
2770:A
2758:A
2719:A
2707:A
2675:u
2671:R
2667:v
2661:v
2657:R
2653:u
2647:v
2643:R
2639:w
2633:u
2629:R
2625:w
2604:)
2601:A
2595:B
2589:(
2580:)
2577:B
2571:A
2565:(
2545:R
2541:R
2526:A
2520:)
2517:A
2511:)
2508:A
2499:A
2496:(
2490:(
2468:R
2464:R
2449:A
2440:)
2437:A
2431:A
2425:(
2396:v
2392:R
2388:u
2382:v
2378:R
2374:w
2368:u
2364:R
2360:w
2335:A
2323:A
2294:w
2290:R
2286:v
2280:v
2276:R
2272:w
2247:A
2241:A
2215:A
2203:A
2177:)
2174:v
2170:R
2166:w
2163:(
2159:v
2152:w
2075:A
2066:A
2037:u
2033:R
2029:w
2023:u
2019:R
2015:v
2009:v
2005:R
2001:w
1976:A
1964:A
1935:)
1932:u
1928:R
1924:v
1918:v
1914:R
1910:w
1907:(
1903:v
1894:u
1890:R
1886:w
1861:A
1852:A
1820:w
1816:R
1812:w
1787:A
1781:A
1749:)
1746:B
1737:A
1731:(
1725:)
1722:B
1716:A
1713:(
1673:5
1669:4
1661:B
1653:D
1641:T
1633:K
1611:A
1599:A
1568:A
1559:)
1556:A
1547:A
1544:(
1531:1
1528:L
1524:2
1521:L
1517:1
1514:L
1510:2
1507:L
1503:1
1500:L
1492:L
1485:T
1461:w
1457:R
1453:w
1449:T
1435:p
1429:w
1409:p
1400:w
1390:u
1386:R
1382:w
1368:p
1362:u
1352:p
1348:W
1344:w
1340:T
1336:w
1332:R
1328:w
1314:A
1308:w
1288:A
1279:w
1256:R
1253:,
1250:W
1233:T
1219:A
1213:A
1200:T
1193:L
1189:C
1185:L
1181:C
1177:L
1173:C
1169:C
1162:L
1151:K
1143:C
1139:C
1106:C
1102:L
1098:C
1088:L
1084:C
1080:L
1076:C
1066:L
1059:X
1055:X
1051:X
1047:C
1043:C
1037:.
1035:C
1031:C
1026:,
988:,
985:R
982:,
979:W
953:R
950:,
947:W
933:,
931:W
927:w
913:A
907:w
881:,
878:R
875:,
872:W
851:A
809:A
805:w
801:w
797:A
793:A
789:w
775:A
769:w
757:.
745:u
741:R
737:w
717:u
697:A
691:u
671:A
662:w
652:,
640:B
634:w
614:A
608:w
588:B
582:A
576:w
566:,
554:A
548:w
528:A
519:w
506:B
502:A
498:W
494:w
490:W
453:R
450:,
447:W
418:,
415:R
412:,
409:W
385:R
373:W
369:W
361:R
357:W
340:R
337:,
334:W
295:A
280:A
83:)
77:(
72:)
68:(
54:.
20:)
Text is available under the Creative Commons Attribution-ShareAlike License. Additional terms may apply.