Research On Basic Propositional Logic Of Weakly Connected Transfer Framework

Visser’s basic propositional logic (BPL) is smaller than intuitionistic logic (Int) and is complete with respect to the calss of transitive Kripke frames in semantics. A number of research achievements on BPL have been gained in1990s, but nearly all of them focus on proof theories. In particular, Yasuhito Suzuki and Hiroakita Ono provided the Hilbert-style axiomatization for BPL. In their system, modus ponens rule (MP) can be just applied to axioms yet not suitable for hypotheses. This means that there are some classes of Kripke frames which can not be characterized by simply extending BPL with extra formulae as axioms. In fact, it is difficult to construct an extension of BPL with the Hilbert-style axiomatization. However, it has been shown that the logic LB by adding the formula (p→q)∨((p→q)→p) to BPL is complete with respect to the class of weak transitive Kripke frames, while the logic LD by adding the Dummett formula (p→q)∨(q→p) to BPL is incomplete.Dummett’s1959paper showed that intermediate logic (LC) can be obtained by adding (p→q)∨(q→p) to intuitionistic logic. LC is an expansion of intuitionistic logic, and characterizes the class of linear Kripke frames. Moreover, LC is an expansion of Int with countable matrix characterizations. This paper focuses on the logic LB and mainly includes the following parts:Chapter1mainly introduces the relationship between intuitionistic logic and sub-intuitionistic logic, and clarifies the concept of sub-intuitionistic logic from the semantic level. It further shows that BPL is a sub-intuitionistic logic, and talks about the current research on BPL.Chapter2provides a brief introduction of intuitionistic logic, intermediate logic and basic propositional logic, as well as some basic concepts of these logics. This part lays the foundation for the following discussion.Chapter3discusses the logic LB. This is the main part of the paper. We prove the logic LC is complete with respect to the class of weaker connect frames by the canonical model method. We show that LD is a proper sub-logic of LB by comparing the logic LD with the logic LB, and further claim that LB has the finite model property, but does not have two constant properties and the disjunction property.Chapter4proves that LB can be embedded to modal logic K4.3by Godel’s translation.Chapter5involves some conclusions and open questions.