A bilateral Hilbert-style investigation of 2-intuitionistic logic

Research output: Contribution to journalArticlepeer-review

Abstract

We develop a bilateral Hilbert-style calculus for 2-intuitionistic logic of Heinrich Wansing. This calculus is defined over signed formulas of two types: formulas signed with plus correspond to assertions, while formulas signed with minus correspond to rejections. In this way, the provided system is a Hilbert-style calculus, which does take rejection seriously by considering it a primitive notion on par with assertion. We show that this presentation is not trivial and provide two equivalent axiomatizations obtained by extending intuitionistic and dual intuitionistic logics, respectively. Finally, we show that 2-intuitionistic logic is in some sense definitionally equivalent to a variant of Nelson's logic with constructible falsity.

Original languageEnglish
Pages (from-to)665-692
Number of pages28
JournalJournal of logic and computation
Volume29
Issue number5
DOIs
Publication statusPublished - 1 Sep 2019

Keywords

  • 2-intuitionistic logic
  • Hilbert-style calculi
  • rejection
  • bilateralism
  • definitional equivalence
  • NEGATION

OECD FOS+WOS

  • 1.01.QL LOGIC
  • 1.02 COMPUTER AND INFORMATION SCIENCES

Fingerprint

Dive into the research topics of 'A bilateral Hilbert-style investigation of 2-intuitionistic logic'. Together they form a unique fingerprint.

Cite this