Study On The Natural Deduction System Of Dual Basic Propositional Logic

Dual-intuitionistic logic is called DJ for short. Generally believed that it is got through, replacing the intuitionistic implication operator (→) by its dual operator (-) on the basis of intuitionistic propositional logic. These researches about DJ can be divided into two different aspects. In semantic terms, Rauszer added dual operator to intuitionistic propositional logic to get BH logic (also called BiInt), achieving the algebra and Kripke semantics; and Goodman studied dual intuitionistic logic on algebraical semantics. In the syntax,the sequence calculus(LDJ) of dual intuitionistic logic were given by Rauszer, Urbas, Czemark, Goodman et al. Gore studied the display calculus of dual intuitionistic logic. Luca Tranchini gave the natural deduction system(NDJ) of dual intuitionistic logic.In 1980, Visser first proposed the natural deduction system of basic proposition logic(BPL). He provided the Kripke semantic and proved the completeness and soundness theorem under the transitive frame. After that, it had been studied by some scholars from Hilbert-style axiomatic systems, Gentzen-type sequence calculus, algebra semantics and so on.Basic proposition logic is sublogic of intuitionistic logic. But there is no more study about the natural deduction system of dual basic propositional logic. So to explore it this paper is structured as follows:The first part is a literature review.We can get the clue of this paper by reviewing the history and listing related research.The second part describes the natural deduction system NDJ of dual intuitionistic propositional logic. This chapter is divided into three parts, including intuitionistic logic, dual intuitionistic logic DJ, the natural deduction system NDJ of dual intuitionistic logic.The third part describes the natural deduction system of basic propositional logic BPL. In this chapter, we will introduce BPL separately from the language, semantics, natural deduction systems, logical properties, philosophical significance and other important conclusions.The fourth part describes the natural deduction system of dual basic propositional logic DBPL. This chapter gives language, semantics, natural deduction system, and proves that the system is soundness in DBPL.The fifth part is the conclusion and summary. This chapter is to summarize the paper and look into the future.