Stream: Mirror: Isabelle Users Mailing List

Topic: [isabelle] Formalizing Axiomatic Systems for Propositiona...


view this post on Zulip 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: Jul 15 2022 at 23:21 UTC