A Mechanised and Constructive Reverse Analysis of Soundness and Completeness of Bi-intuitionistic Logic
Conference on Certified Programs and Proofs 2024, 2024
Abstract
Using the Coq proof assistant, we investigate the minimal non-constructive principles needed to show soundness and completeness of propositional bi-intuitionistic logic. Before being revisited and corrected by Goré and Shillito, the completeness of bi-intuitionistic logic, an extension of intuitionistic logic with a dual operation to implication, had a rather erratic history, making it an ideal case for computer mechanisation. Moreover, contributing a constructive perspective, we observe that the completeness of bi-intuitionistic logic explicates the same characteristics already observed in an ongoing effort to analyse completeness theorems in general.
Recommended citation: Shillito, Ian and Dominik Kirst. (2024). "A Mechanised and Constructive Reverse Analysis of Soundness and Completeness of Bi-intuitionistic Logic" CPP 2024.
Download Paper