基于广义谢弗竖的分析性模态公理系统

沿着安德森等人开创的方向，我们将分析性公理系统从经典逻辑推向模态逻辑，所定义的广义谢弗竖混合了模态词和广义析舍。在这篇论文中，我们给出常见的正规模态逻辑的分析性公理系统及其强完全性定理和插值定理，并讨论演绎关系的性质：单调性和切割性。

Generalized Sheffer-stroke Based Analytical Modal Axiomatic Systems

Our main objective is to propose analytic modal axiomatic systems, in which the proof of theorem is very easy. And so they are suitable to be the foundation of modal theorem prover. An axiomatic system is called analytic, if the premises and con- sequences of its inferential rules share propositional variables. Our results in modal logic follow the originate work of Anderson et al, which propose analytic axiomatic systems for classical logic. We first define an n-ary operator and give a new notation of modal formulas, which is convenient to express the axioms of such systems. The n-ary operator is actually a hybrid of generalized NAND and modality, which saves the connectives and parentheses. And so we name it generalized Sheffer stroke. The formula in new notation [A0…An-1; B0… Bm-1] is semantically equivalent to ┐A0 ∨… ∨ ┐An-1 ∨ ◇（┐B0 ∨… ∨ ┐Bm-1）. Based on the new notation, we firstly propose analytic modal axiomatic systems （AMAS） for some normal modal logics, such as K, D, T, S4, K4 and D4, by adding modal rules to analytic axiomatic system of propositional logic, not modal axioms. And so we could compare different modal logics in term of modal rules, not modal axioms. Secondly, we give the strong completeness theorems and interpolation theorems for such systems. Besides, we propose a new definition of derivation in term of AMAS. Although they have no Modus Ponens, the analytic axiomatic systems have common conditions on deducibility relation, such as reflexive, monotonic and cut, which shows that the new definition of derivation is reasonable. Finally, we propose a more general form of AMAS, namely component-wise axiomatic systems, which are fit for more modal logics, including modal logic of which frames are symmetric, such as S5： provide a component-wise mechanism similar to hyper-sequent to distinct possible worlds and retain information of them.