Intuitionistic Logic is a Connexive Logic

TL;DR

This paper demonstrates that intuitionistic logic is equivalent to a new connexive logic called CHL, which has intuitive semantics and is algebraically related to Heyting algebras, with proof systems and computational interpretations provided.

Contribution

It introduces Connexive Heyting Logic (CHL), establishing its equivalence with intuitionistic logic and providing formal proof systems and semantics.

Findings

CHL is deductively equivalent to intuitionistic logic

Proof systems for CHL are developed (Hilbert and Gentzen)

A computational interpretation of the connexive conditional is suggested

Abstract

We show that intuitionistic logic is deductively equivalent to Connexive Heyting Logic (CHL), hereby introduced as an example of a strong connexive logic with intuitive semantics. We use the reverse algebraisation paradigm: CHL is presented as the assertional logic of a point regular variety (whose structure theory is examined in detail) that turns out to be term equivalent to the variety of Heyting algebras. We provide Hilbert-style and Gentzen-style proof systems for CHL; moreover, we suggest a possible computational interpretation of its connexive conditional, and we revisit Kapsner's idea of superconnexivity.