Sahlqvist-theory-for-Hybrid-Logic.pdf
《Sahlqvist-theory-for-Hybrid-Logic.pdf》由会员分享,可在线阅读,更多相关《Sahlqvist-theory-for-Hybrid-Logic.pdf(6页珍藏版)》请在三一文库上搜索。
1、Sahlqvist theory for Hybrid Logic Opgedragen aan Dick de Jongh voor zijn 65ste verjaardag Balder ten Cate, Maarten Marx and Petrucio Viana In his work and life, Dick de Jongh often emphasized the importance of bring- ing together diff erent disciplines, of viewing problems from diff erent perspec- t
2、ives, and of gaining insight, understanding and joy by employing Irans offi cial government policy called dialogue among civilisations. All these aspects are combined in the work he did in the last phase of his career: the master of logic program at the ILLC. The dialogue between the world embodied
3、in the highly mixed group of foreign students and the ILLC has been enormously benefi cial for both sides. We do not exaggerate if we say that the lives of all three authors of this little work have been enormously enriched through this part of Dicks work. Thanks Dick. 1Introduction Hybrid logic com
4、es with a general completeness result: Every extension with pure axioms of the basic hybrid logic with name and bg rules is complete 2, 3. A pure axiom is a formula constructed from nominals only, thus not containing arbitrary proposition letters. Pure axioms correspond to fi rst order frame conditi
5、on and are quite expressive 2. For instance, i 3i defi nes the class of irrefl exive frames. We can compare this general result with Sahlqvists theorem for modal logic, a similar general completeness result. Several questions come to mind. Is every Sahlqvist axiom expressible as a pure axiom? No, th
6、e ChurchRosser axiom 32p 23p is a counterexample 5. On the other hand, in the presence of the tense modalities, the answer is yes 6. This gives us two new questions: 1. Is the extension of the basic hybrid logic with a set of Sahlqvist axioms always complete? That is, does Sahlqvists theorem go thro
7、ugh for hybrid logic? 2. Can we combine the two general completeness results? That is, is every extension of the basic hybrid logic with a set of Sahlqvist axioms and a set of pure axioms complete with respect to the class of frames defi ned by and together? This paper answers both questions. We sho
8、w that every extension of the basic hybrid logic with canonical modal axioms (and hence, Sahlqvist axioms) is complete even without the name and bg rules, and we give a Sahlqvist formula and a pure formula such that the basic hybrid logic extended with the axioms and is incomplete even in the presen
9、ce of the name and the bg rules. As a corollary, we solve an embarrassing open problem in hybrid logic: whether Beths de- fi nability property holds (cf. 4 for a discussion of this open problem and some partial results). Another corollary of our analysis is that name and bg are superfl uous not only
10、 for the basic hybrid system, but also for every Sahlqvist extension. This is a desirable result, since these rules 1 are non-orthodox in the sense that they involve syntactic side-conditions, much like the Gabbays irrefl exivity rule. The paper is organized as follows. This section briefl y recalls
11、 hybrid logic. Section 2 shows Sahlqvists theorem for hybrid logic. In Section 3 we derive interpolation and Beths property. Section 4 shows that a combination of Sahlqvist and pure axioms is not guaranteed to be complete. We conclude in Section 5. 2Hybrid logic What follows is a short textbook-styl
12、e presentation of hybrid logic, following 2. Hybrid logic is the result of extending the basic modal language with a second sort of atomic propositions called nominals, and with satisfaction operators. The nominals behave similar to ordinary proposition letters, except that their interpretation in m
13、odels is restricted to singleton sets. In other words, nominals act as names for worlds. Satisfaction operators allow one to express that a formula holds at the world named by nominal. For example, ip expresses that p holds at the world named by the nominal i. Formally, let prop be a countably infi
14、nite set of proposition letters and nom a countably infi nite set of nominals.1The formulas of the basic hybrid logic are given as follows. := p | i | | | | 3 | i where p prop and i nom. The truth defi nition for the nominals is the same as for the proposition letters: our models are of the form M =
15、 (F,V ), where F is a frame and V a valuation function for the proposition letters and nominals. The truth defi nition for the nominals is the same as for the proposition letters: M,w |= i iff w V (i). The only diff erence is in the admissible valuations: only valuation functions are allowed that as
16、sign to each nominal a singleton set. The interpretation of the satisfaction operators is as could be expected: M,w |= i iff M,v |= , where V (i) = v. Next, let us turn to axiomatizations for this language. Let be the set of axioms given by agree, back, introduction, ref, and self-dual, for all i,j
17、nom. agreejip ip back3ip ip introductioni p ip refii self-dualip ip. Let KH()be the smallest set of formulas containing all tautologies, axioms 2(p q) (2p 2q), i(p q) (ip iq) for i nom, and the axioms in , closed under modus ponens, uniform substitution of formulas for proposition letters and nomina
18、ls for nominals, generalization (If then 2), and -generalization (If then i). Given a set of hybrid formulas, the logic KH() is obtained by adding the formulas in to KH()as extra axioms, and closing under the given rules. Theorem 2.1 KH()is strongly sound and complete for the class of all frames. A
19、sketch of the proof of Theorem 2.1 can be found in 2. Theorem 2.1 also follows from our results in Section 3. A general completeness result holds for extensions of the basic logic with pure axioms, provided two extra derivation rules are added to the calculus. A pure axiom is an axiom that contains
20、no proposition letters, only nominals. nameIf i and i does not occur in , then bgIf i3j j where j 6= i and j does not occur in , then i2 1 The results discussed in this paper and their proofs also apply if nom is fi nite. 2 Several variants of these rules occur in literature, under names such as Cov
21、 5 and Name and Paste 2. It the above shape, the rules fi rst appear in 3. Let K+ H() be the logic obtained by adding these two inference rules to KH(). Given a set of hybrid formulas, the logic K+ H() is obtained by adding the formulas in to K + H() as extra axioms, and closing under all rules, inc
22、luding the two extra rules. Theorem 2.2 (3) Let be any set of pure formulas.Then K+ H() is strongly sound and complete for the frame class defi ned by . One question left open by Theorem 2.2 is when are the rules needed. While the proof of Theorem 2.2 is based on a Henkin model construction that cru
23、cially depends on the presence of the rules, this does not exclude the possibility of completeness without rules. Another question that remains is if every extension of K+ H() with Sahlqvist axioms is complete. Recall from the introduction that not every Sahlqvist axiom corresponds to a pure axiom.
24、3Sahlqvist completeness for hybrid logic Consider frames of the form F = hW,R,(Ri)inom,(Si)inomi, where each Riis a binary relation on W and each Siis a subset of W. Let us call such frames non-stanfard frames, to distinguish them from the ordinary frames. Let us say that such a non-standard frame i
- 配套讲稿:
如PPT文件的首页显示word图标,表示该PPT已包含配套word讲稿。双击word图标可打开word文档。
- 特殊限制:
部分文档作品中含有的国旗、国徽等图片,仅作为作品整体效果示例展示,禁止商用。设计者仅对作品中独创性部分享有著作权。
- 关 键 词:
- Sahlqvist theory for Hybrid Logic
链接地址:https://www.31doc.com/p-3793949.html