Email Gateway (Jan 11 2023 at 15:03): Email Gateway (Jan 11 2023 at 15:03):From: Tobias Nipkow <nipkow@in.tum.de>
Class-Based Classical Propositional Logic
Matthew Doty
We formulate classical propositional logic as an axiom class. Our class
represents a Hilbert-style proof system with the axioms ... along with the rule
modus ponens. In this axiom class we provide lemmas to obtain Maximally
Consistent Sets via Zorn's lemma. We define the concrete classical propositional
calculus inductively and show it instantiates our axiom class. We formulate the
usual semantics for the propositional calculus and show strong soundness and
completeness. We provide conventional definitions of the other logical
connectives and prove various common identities. Finally, we show that the
propositional calculus embeds into any logic in our axiom class.
https://www.isa-afp.org/entries/Propositional_Logic_Class.html
Enjoy!
smime.p7s
Last updated: Apr 19 2024 at 08:19 UTC