期刊
ADVANCES IN PROOF THEORY
卷 28, 期 -, 页码 291-318出版社
BIRKHAUSER BOSTON
DOI: 10.1007/978-3-319-29198-7_8
关键词
Modal logic; Infinitary logic; Kripke semantics; Tait-style calculi; Cut-elimination
We investigate the (multiagent) infinitary version K-w1 of the propositional modal logic K, in which conjunctions and disjunctions over countably infinite sets of formulas are allowed. It is known that the natural infinitary extension LKw1 square (here presented as a Tait-style calculus, TKw1#) of the standard sequent calculus LKp square for K is incomplete with respect to Kripke semantics. It is also known that in order to axiomatize K-w1 one has to add to LKw1 square new initial sequents corresponding to the infinitary propositional counterpart BFw1 of the Barcan Formula. We introduce a generalization of standard Kripke semantics, and prove that K-w1(#) is sound and complete with respect to it. By the same proof strategy, we show that the stronger system TKw1, allowing countably infinite sequents, axiomatizes K-w1 although it provably does not admit cut-elimination.
作者
我是这篇论文的作者
点击您的名字以认领此论文并将其添加到您的个人资料中。
推荐
暂无数据