Email Gateway (Dec 21 2021 at 10:46): Email Gateway (Dec 21 2021 at 10:46):From: Jørgen Villadsen via Cl-isabelle-users <cl-isabelle-users@lists.cam.ac.uk>
Hi,
The soundness and completeness of a Hilbert system for classical propositional logic are formalized here:
https://www.isa-afp.org/entries/Propositional_Proof_Systems.html
We have recently formalized other systems based on either implication and falsity or disjuction and negation:
Asta Halkjær From, Agnes Moesgård Eschen & Jørgen Villadsen:
Formalizing Axiomatic Systems for Propositional Logic in Isabelle/HOL
In Proceedings of the 14th Conference on Intelligent Computer Mathematics (CICM 2021)
We have now formalized 12 additional systems based on implication and negation - please see attached slide.
Our formalizations are stand-alone and do not use the AFP entry.
We wonder if other axiomatic systems have been formally proved complete.
We have not yet formalized single-axiom systems and we have only considered classical logic.
Regards, Jørgen
FormalizingAxiomaticSystems.pdf
Last updated: Jan 04 2025 at 20:18 UTC