A mechanised and constructive reverse analysis of soundness and completeness of b...
summary
A Coq formalisation verifies propositional bi‑intuitionistic soundness and shows soundness forces classicality: soundness implies excluded middle in the metatheory. Completeness splits: model existence is equivalent to weak excluded middle, while quasi‑completeness is equivalent to a weaker weak excluded middle shift. Construction uses a Lindenbaum saturation into quasi‑prime theories and a universal Kripke model; the mechanisation works for the propositional case, first‑order remains open.
AI-written summary · about
chapters (9)
- 0:00Introduction
- 2:17Bi-intuitionistic logic
- 5:28Soundness and completeness
- 9:44Reverse mathematics approach
- 13:39Constructive completeness challenges
- 17:12Weak excluded middle
- 21:47Formalisation benefits
- 23:10Future directions
- 25:38Q&A
related talks
36mMcTT: Building A Correct-By-Construction Proof Checker For Martin-Loef Type Theory
01h 34mFormal Logic Undressed
18mCompleteness of an Axiomatization of Graph Isomorphism via Graph Rewriting in Coq
58mA New Perspective on Commutativity in Verification
30mRelatively Complete Verification of Probabilistic Programs
29mSynthesizing Axiomatizations using Logic Learning
24mAn Intrinsically-typed Probabilistic Programming Language in Coq (Extended Abstr...
42mMetaCoq as a tool to prevent future unsoundness in Coq