Basic Propositional Calculus I
The system of modal logic \({\mathbf K}4\) can be considered as a generalization of both Lewis' \({\mathbf S}4\) and provability logic \({\mathbf G}\) [see \textit{C. Smoryński}, Self-reference and modal logic (1985; Zbl 0596.03001)]. On the other hand, the Heyting propositional calculus \({\mathbf H}\) presents a purely propositional counterpart of \({\mathbf S}4\). In this context, the propositional systems \({\mathbf B}{\mathbf P}{\mathbf C}\) (Basic Propositional Calculus) and \({\mathbf F}{\mathbf P}{\mathbf C}\) (Formal Propositional Calculus), satisfying the following informal `proportion' \({\mathbf H}:{\mathbf S}4={\mathbf F}{\mathbf P}{\mathbf C}:{\mathbf G}= {\mathbf B}{\mathbf P}{\mathbf C}:{\mathbf K}4\), occur quite naturally [see \textit{A. Visser}, ``A propositional logic with explicit fixed points, Stud. Logica 40, 155-175 (1981; Zbl 0469.03012)]. However, \({\mathbf B}{\mathbf P}{\mathbf C}\) remains an exotic system even to those concerned with nonclassical logics. This paper presents an overview of \({\mathbf B}{\mathbf P}{\mathbf C}\) including the corresponding axiomatization and a development of a Kripke-type semantics for \({\mathbf B}{\mathbf P}{\mathbf C}\). The main result is a completeness theorem for the class of transitive Kripke structures, followed by several interesting refinements. As byproducts, some results related to the systems \({\mathbf H}\), \({\mathbf F}{\mathbf P}{\mathbf C}\) and classical propositional calculus are obtained as well.
- A cut-free Gentzen formulation of basic propositional calculus
- A modal analog for Glivenko's theorem and its applications
- A modified subformula property for the modal logic KC4
- The modalized Heyting calculus: a conservative modal extension of the intuitionistic logic
- scientific article; zbMATH DE number 218532
- scientific article; zbMATH DE number 1778906
- All finitely axiomatizable subframe logics containing the provability logic CSM₀ are decidable
- scientific article; zbMATH DE number 3884136
- scientific article; zbMATH DE number 4070861
- scientific article; zbMATH DE number 94918
- Sequent calculi for Visser's propositional logics
- A closer look at some subintuitionistic logics
- \(l\)-hemi-implicative semilattices
- Latarres, lattices with an arrow
- A cut-free Gentzen formulation of basic propositional calculus
- Fuzzy sets and formal logics
- Proof complexity of substructural logics
- Representations of Sheffer stroke algebras and Visser algebras
- Valuations: bi, tri, and tetra
- Principal congruences in weak Heyting algebras
- Binary modal companions for subintuitionistic logics
- Implication via spacetime
- On PBZ*-lattices
- Quasi-subtractive varieties
- Correspondences between gentzen and hilbert systems
- ASSERTIONALLY EQUIVALENT QUASIVARIETIES
- Completions of Basic Algebras
- Frontal operators in weak Heyting algebras
- The de Jongh property for basic arithmetic
- Constructive embedding from extensions of logics of strict implication into modal logics
- Esakia duality and its extensions
- Basic predicate calculus
- The variety of modal weak Gödel algebras
- On self‐distributive weak Heyting algebras
- Interpolation Property on Visser's Formal Propositional Logic
- On the implicative-infimum subreducts of weak Heyting algebras
- A study on some classes of distributive lattices with a generalized implication
- Multipliers in weak Heyting algebras
- A semantical analysis of some subintuitionistic modal logics
- A constructive interpretation of the logical constants
- Algebraic semantics for weak subintuitionistic logic WF
- D-complete single axioms for the equivalential calculus with the rules d and r
- Open filters and congruence relations on self-distributive weak Heyting algebras
- On weak Lewis distributive lattices
- On a generalization of Heyting algebras. I
- Bounded distributive lattices with strict implication and weak difference
- On commutative weak Heyting algebras and some of its subreducts
- Amalgamation property for the class of basic algebras and some of its natural subclasses
This page was built for publication: Basic Propositional Calculus I
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q4210835)