Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

Strong Negation is Definable in 2Int

Hrafn Valtýr Oddsson

TL;DR

The paper proves that strong negation is definable in Wansing's constructive bi-intuitionistic logic $2Int$ by exhibiting a specific definability formula and constructing derivations that simulate the introduction and elimination rules of strong negation within $2Int$, using the bilateral proofs framework. It clarifies how bidirectional negation interacts with co-implication in a constructive setting and shows that no additional axioms (such as Peirce's law) are needed. The result sharpens the expressive power of $2Int$ and informs the understanding of negation in bi-intuitionistic logics, with potential implications for refutation-style reasoning in constructive systems.

Abstract

I show that the strong negation is definable in 2Int, Wansing's bi-intuitionistic logic.

Strong Negation is Definable in 2Int

TL;DR

The paper proves that strong negation is definable in Wansing's constructive bi-intuitionistic logic by exhibiting a specific definability formula and constructing derivations that simulate the introduction and elimination rules of strong negation within , using the bilateral proofs framework. It clarifies how bidirectional negation interacts with co-implication in a constructive setting and shows that no additional axioms (such as Peirce's law) are needed. The result sharpens the expressive power of and informs the understanding of negation in bi-intuitionistic logics, with potential implications for refutation-style reasoning in constructive systems.

Abstract

I show that the strong negation is definable in 2Int, Wansing's bi-intuitionistic logic.
Paper Structure (2 sections, 1 theorem, 2 equations)

This paper contains 2 sections, 1 theorem, 2 equations.

Table of Contents

  1. Preliminaries
  2. Strong Negation in $\mathrm{2Int}$

Key Result

Theorem 1

The strong negation is definable in $\mathrm{2Int}$ via the formula

Theorems & Definitions (2)

  • Theorem 1
  • proof