| Abstract
|
:
|
Basic Propositional Logic, BPL, was invented by Albert Visser in 1981. He wanted to interpret implication as formal provability. To protect his system against the liar paradox, modus ponens is weakened. One decade later Wim Ruitenburg, considering philosophical criticisms of the intuitionistic interpretation of the logical connectives, reintroduced BPL and its first order extension, BQC. His new proof interpretation gives a system weaker than Intuitionistic Logic. Another motivation for Basic logic, through modal logic, comes from K. Dosen. He started an investigation of propositional logics weaker than Heyting's that can be embedded by modal translations into normal modal logics weaker than S4. He concentrated on the systems K and D. What he found, among other things, was Basic Propositional Logic. We investigate the proof theoretical aspects of Basic Logic and model theoretical aspect of Basic Propositional Logic. A new axiomatization for Basic logic, GBQC, in the style of Gentzen's sequent calculus is introduced. A cut-elimination theorem for GBQC is proven. Some applications of the cut-elimination are considered. Among these, we prove that Basic Logic has the Disjunction Property DP and the Explicit Definability Property EP. An embedding theorem of Intuitionistic Logic into Basic Logic is proven. This theorem enables us to give new proofs of DP and EP for Intuitionistic Logic. It also shows that Basic Logic is consistent if and only if Intuitionistic Logic is consistent. In the model theory of Basic Propositional Logic, BPC, we give a detailed proof of the completeness theorem for BPC with respect to Kripke models. An interpolation theorem for BPC is proven. By using our embedding theorem, an interpolation theorem for Intuitionistic Propositional Logic IPC is derived. We show that Basic Propositional Logic plus the principle of excluded third is the intersection of two maximal (consistent) intermediate logics, Classical Propositional Logic CPC and usdE\sb1 = BPC + {\ T}\to\bot.usd The inherent algebraic models (the term models) of Basic Propositional Logic theoris are called Basic algebras. We prove a modification of Stone Representation for Basic algebra and, among other things, that every Basic algebra can be embedded into a complete Heyting algebra.
|