We present a new proof of the embedding of the classical modal logic S4 into the logic of Boolean Bunched Implications (BBI). While the original proof is semantical, this proof is entirely syntactical. It proceeds via Hilbert-style calculi, and is built by analogy with a recently discovered proof by Godel of the embedding of intuitionistic propositional logic into S4. We present the first full proofs of deduction theorems for BBI, which are used to show that the embedding is preserved by reasoning with assumptions, including where those assumptions are organised into bunches. Unlike the existing proof, our proof is stable under arbitrary axiomatic extensions of S4, and applies to all known axiomatic extensions of BBI in the literature. We observe how this embedding is related to semantical properties of both logics. Moreover, the proof extends gracefully to language extensions of BBI, as we show with hybrid BBI, classical BI, and sub-classical BBI.
New proofs of weak normalization for intuitionistic and classical propositional logics (with the full set of operators -- falsum, implication, conjunction and disjunction) are presented and a deterministic algorithm for weak normalization is presented.
This paper gives a survey of propositional modal logic in an intuitionistic setting. Mainly intended for readers already familiar with classical modal logic, we discuss why there are two prominent families of such logics, intuitionistic modal logics (IMLs) and constructive modal logics (CMLs), what motivates their stud...
We study infinitary intuitionistic logic by employing both syntactic and semantic methods. First, we introduce a natural deduction system for infinitary predicate logic and study some of its basic properties. We then extend neighbourhood semantics to this setting, providing a soundness and completeness theorem for th...
The shallow embedding of higher-order modal logic in classical higher-order logic, used in Benzm\"uller and Scott's Notes on G\"odel's and Scott's variants of the ontological argument (2025), reaches beyond the modal object language of the arguments: its property quantifiers range over terms that may also express nomin...
RmbC is a self-extensional paraconsistent logic in the family of Logics of Formal Inconsistency (LFIs). This system is obtained from mbC (the basic LFI) by adding the replacement property via two global inference rules. RmbC is characterized by a non-explosive negation $\neg$ and a consistency operator $\circ$, which r...
This paper provides an expository comparison of two foundational proof systems in classical propositional logic: Gentzen's sequent calculus and Beth's semantic tableaux. Gentzen's sequent calculus is presented as a rule-based system built upon the single axiom $\alpha \Rightarrow \alpha$, whose key feature — the subfor...
Zuzanna Rygiewicz· Reason· 0 citations
We use cookies to run the site and, with your consent, for analytics and to show ads.
See our Cookie Policy.
