Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

Fundamental Propositional Logic with Strict Implication

Zhicheng Chen

TL;DR

This work extends fundamental propositional logic (FPL) by incorporating strict implication, providing axiomatizations for the R and F fragments over reflexive and pseudosymmetric DG-models. It develops a rigorous canonical-model construction, including a Fixpoint-Existence Lemma and a baby-model stage, to prove completeness alongside the established soundness results. The approach unifies IPL and OL within a single semantic framework while addressing the technical complexities introduced by strict implication. The results advance the understanding of non-classical logics with Fitch-style foundations and offer a robust method for proving completeness via a pairwise-set canonical model.

Abstract

``Fundamental logic" is a non-classical logic recently introduced by Wesley Holliday. It has an elegant Fitch-style natural deduction system and, in a sense, it unifies orthologic and the $\{\land,\lor,\neg\}$-fragment of intuitionistic logic. In this paper, we incorporate strict implication into fundamental propositional logic (and a slightly weaker logic, respectively). We provide the axiomatization and prove the soundness and completeness theorems.

Fundamental Propositional Logic with Strict Implication

TL;DR

This work extends fundamental propositional logic (FPL) by incorporating strict implication, providing axiomatizations for the R and F fragments over reflexive and pseudosymmetric DG-models. It develops a rigorous canonical-model construction, including a Fixpoint-Existence Lemma and a baby-model stage, to prove completeness alongside the established soundness results. The approach unifies IPL and OL within a single semantic framework while addressing the technical complexities introduced by strict implication. The results advance the understanding of non-classical logics with Fitch-style foundations and offer a robust method for proving completeness via a pairwise-set canonical model.

Abstract

``Fundamental logic" is a non-classical logic recently introduced by Wesley Holliday. It has an elegant Fitch-style natural deduction system and, in a sense, it unifies orthologic and the -fragment of intuitionistic logic. In this paper, we incorporate strict implication into fundamental propositional logic (and a slightly weaker logic, respectively). We provide the axiomatization and prove the soundness and completeness theorems.

Paper Structure

This paper contains 13 sections, 21 theorems, 16 equations, 1 figure.

Table of Contents

  1. Introduction
  2. Fundamental propositional logic
  3. FPL with implication
  4. Technique for the completeness proof
  5. Syntactic and semantic consequence relation
  6. Semantic consequence
  7. Syntactic consequence
  8. Soundness
  9. Completeness
  10. Main idea
  11. Technical preparations
  12. Baby canonical model and basic lemmas
  13. Fixpoint-Existence Lemma and the canonical model

Key Result

lemma thmcounterlemma

Let $\mathfrak{M}=\langle \mathfrak{F},V\rangle$ be a DG model. For each formula $\varphi$, $\Vert \varphi \Vert$ is a $\text{DG}_{\mathfrak{F}}$-fixpoint.

Theorems & Definitions (49)

  • definition thmcounterdefinition
  • definition thmcounterdefinition: Interpretation of formulas
  • definition thmcounterdefinition
  • definition thmcounterdefinition: DG model
  • lemma thmcounterlemma
  • definition thmcounterdefinition: Semantic consequence
  • lemma thmcounterlemma
  • definition thmcounterdefinition: "$\phi \vdash (\alpha_1, \ldots, \alpha_n)$"
  • definition thmcounterdefinition
  • definition thmcounterdefinition: $\vdash^{i}_{\gamma}$
  • ...and 39 more