Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

Proof-theoretic Semantics for Classical Propositional Logic with Assertion and Denial

Alexander V. Gheorghiu, Yll Buzoku

TL;DR

This work develops a proof-theoretic semantics for classical propositional logic by reinterpreting logic over literals representing assertion and denial, and by equipping this framework with a duality operation that flips truth values. Classical propositional logic is shown to be equivalent to intuitionistic logic plus duality (IPL + Duality) within a base-extension semantic setting, yielding a harmony-like natural deduction system $\mathsf{NK}^\pm$ that treats CPL components uniformly. Soundness and completeness are established: $\Gamma \vdash \varphi$ iff $\Gamma \Vdash \varphi$, with completeness proved via a simulation base and a flattening/sharpening methodology that connects semantic support to syntactic derivability. The approach offers a principled, constructive semantics for CPL that parallels existing P-tS for intuitionistic logic and opens avenues for systematic study of classical logics within a proof-theoretic paradigm.

Abstract

The field of proof-theoretic semantics (P-tS) offers an alternative approach to meaning in logic that is based on inference and argument (rather than truth in a model). It has been successfully developed for various logics; in particular, Sandqvist has developed such semantics for both classical and intuitionistic logic. In the case of classical logic, P-tS provides a conception of consequence that avoids an \emph{a priori} commitment to the principle of bivalence, addressing what Dummett identified as a significant foundational challenge in logic. In this paper, we propose an alternative P-tS for classical logic, which essentially extends the P-tS for intuitionistic logic by operating over literals rather than atomic propositions. Importantly, literals are atomic and not defined by negation but are defined by inferential relationships. This semantics illustrates the perspective that classical logic can be understood as intuitionistic logic supplemented by a principle of duality, offering fresh insights into the relationship between these two systems.

Proof-theoretic Semantics for Classical Propositional Logic with Assertion and Denial

TL;DR

This work develops a proof-theoretic semantics for classical propositional logic by reinterpreting logic over literals representing assertion and denial, and by equipping this framework with a duality operation that flips truth values. Classical propositional logic is shown to be equivalent to intuitionistic logic plus duality (IPL + Duality) within a base-extension semantic setting, yielding a harmony-like natural deduction system that treats CPL components uniformly. Soundness and completeness are established: iff , with completeness proved via a simulation base and a flattening/sharpening methodology that connects semantic support to syntactic derivability. The approach offers a principled, constructive semantics for CPL that parallels existing P-tS for intuitionistic logic and opens avenues for systematic study of classical logics within a proof-theoretic paradigm.

Abstract

The field of proof-theoretic semantics (P-tS) offers an alternative approach to meaning in logic that is based on inference and argument (rather than truth in a model). It has been successfully developed for various logics; in particular, Sandqvist has developed such semantics for both classical and intuitionistic logic. In the case of classical logic, P-tS provides a conception of consequence that avoids an \emph{a priori} commitment to the principle of bivalence, addressing what Dummett identified as a significant foundational challenge in logic. In this paper, we propose an alternative P-tS for classical logic, which essentially extends the P-tS for intuitionistic logic by operating over literals rather than atomic propositions. Importantly, literals are atomic and not defined by negation but are defined by inferential relationships. This semantics illustrates the perspective that classical logic can be understood as intuitionistic logic supplemented by a principle of duality, offering fresh insights into the relationship between these two systems.

Paper Structure

This paper contains 8 sections, 10 theorems, 39 equations, 3 figures.

Table of Contents

  1. Introduction
  2. Classical Propositional Logic
  3. Syntax & Consequence
  4. Proof Theory
  5. Base-extension Semantics
  6. Soundness
  7. Completeness
  8. Conclusion

Key Result

Proposition 2.3

For any valuation $v$,

Figures (3)

  • Figure 1: Natural Deduction System $\mathsf{NJ}$ and $\mathsf{NK}^\pm$
  • Figure 2: Support for Classical Propositional Logic
  • Figure 3: Simulation Base $\mathscr{N}$

Theorems & Definitions (27)

  • Definition 2.1: Valuation
  • Definition 2.2: Classical Consequence
  • Proposition 2.3
  • Definition 2.4: Natural Deduction System $\mathsf{NK}^\pm$
  • Example 2.5
  • Theorem 2.6: Soundness & Completeness
  • proof : Proof of Soundness
  • proof : Proof of Completeness
  • Example 3.1
  • Definition 3.2: Atomic Rule
  • ...and 17 more