We show that intuitionistic logic is deductively equivalent to Connexive Heyting Logic (CHL), hereby introduced as an example of a strongly connexive logic with an 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.
Intuitionistic logic is a connexive logic
davide fazio;francesco paoli
2024-01-01
Abstract
We show that intuitionistic logic is deductively equivalent to Connexive Heyting Logic (CHL), hereby introduced as an example of a strongly connexive logic with an 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.File in questo prodotto:
File | Dimensione | Formato | |
---|---|---|---|
Articolo formato stampa.pdf
accesso aperto
Tipologia:
versione editoriale
Dimensione
533.93 kB
Formato
Adobe PDF
|
533.93 kB | Adobe PDF | Visualizza/Apri |
I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.