Class-based Classical Propositional Logic

Matthew Doty 📧

December 15, 2022

This is a development version of this entry. It might change over time and is not stable. Please refer to release versions for citations.


We formulate classical propositional logic as an axiom class. Our class represents a Hilbert-style proof system with the axioms \(\vdash \varphi \to \psi \to \varphi\), \(\vdash (\varphi \to \psi \to \chi) \to (\varphi \to \psi) \to \varphi \to \chi\), and \(\vdash ((\varphi \to \bot) \to \bot) \to \varphi\) along with the rule modus ponens \(\vdash \varphi \to \psi \Longrightarrow \; \vdash \varphi \Longrightarrow \; \vdash \psi\). 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.


BSD License


Session Propositional_Logic_Class