Sequent-systems and groupoid models. I
Sequent-systems and groupoid models. I
复制标题
序列系统和群群模型。
DOI：
10.1007/bf00671566
复制
发表时间：
1988
期刊：
影响因子：
0.7
通讯作者：
K. Dosen
中科院分区：
文献类型：
--
作者：
K. Dosen
本文的目的是把比Heyting弱的一类命题逻辑的证明论和模型论联系起来。这个家庭包括系统类似的Lambek演算的句法类别，系统的相关逻辑，系统有关toBCK代数，最后，约翰森和海廷的逻辑。首先，给出了这些逻辑的序列系统，并证明了割消结果。在这些序列系统中，逻辑运算的规则永远不会改变：所有的变化都是在结构规则中进行的。接下来，休伯特式的配方给出这些逻辑，代数完备性结果证明相对于剩余格序广群。最后，模型结构相关的相关模型结构（厄克特，罚款，Eurquley，迈耶和Maksimova）给出了我们的逻辑。这些模型结构是基于群胚平行于序列系统。本文为蕴涵弱于Heyting的逻辑公理的对应理论奠定了基础，这种对应理论类似于正规模态逻辑的模态公理的对应理论。本文的第一部分包括前两节，分别讨论序列系统和Hubert公式。第二部分将在下一期杂志上发表，包含第三部分，讨论群胚模型。
The purpose of this paper is to connect the proof theory and the model theory of a family of propositional logics weaker than Heyting's. This family includes systems analogous to the Lambek calculus of syntactic categories, systems of relevant logic, systems related toBCK algebras, and, finally, Johansson's and Heyting's logic. First, sequent-systems are given for these logics, and cut-elimination results are proved. In these sequent-systems the rules for the logical operations are never changed: all changes are made in the structural rules. Next, Hubert-style formulations are given for these logics, and algebraic completeness results are demonstrated with respect to residuated lattice-ordered groupoids. Finally, model structures related to relevant model structures (of Urquhart, Fine, Routley, Meyer, and Maksimova) are given for our logics. These model structures are based on groupoids parallel to the sequent-systems. This paper lays the ground for a kind of correspondence theory for axioms of logics with implication weaker than Heyting's, a correspondence theory analogous to the correspondence theory for modal axioms of normal modal logics.The first part of the paper, which follows, contains the first two sections, which deal with sequent-systems and Hubert-formulations. The second part, due to appear in the next issue of this journal, will contain the third section, which deals with groupoid models.