diff --git a/metadata/entries/Propositional_Logic_Class.toml b/metadata/entries/Propositional_Logic_Class.toml
new file mode 100644
--- /dev/null
+++ b/metadata/entries/Propositional_Logic_Class.toml
@@ -0,0 +1,44 @@
+title = "Class-based Classical Propositional Logic"
+date = 2022-12-15
+topics = [
+ "Logic/General logic/Classical propositional logic",
+ "Logic/Proof theory",
+]
+abstract = """
+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."""
+license = "bsd"
+note = ""
+
+[authors]
+
+[authors.doty]
+email = "doty_email"
+
+[contributors]
+
+[notify]
+doty = "doty_email"
+
+[history]
+
+[extra]
+
+[related]
+dois = []
+pubs = []
diff --git a/thys/Propositional_Logic_Class/Classical_Connectives.thy b/thys/Propositional_Logic_Class/Classical_Connectives.thy
new file mode 100644
--- /dev/null
+++ b/thys/Propositional_Logic_Class/Classical_Connectives.thy
@@ -0,0 +1,1308 @@
+chapter \ Classical Logic Connectives \label{sec:logical-connectives}\
+
+theory Classical_Connectives
+ imports
+ Classical_Logic_Completeness
+ List_Utilities
+begin
+
+text \ Here we define the usual connectives for classical logic. \
+
+no_notation FuncSet.funcset (infixr "\" 60)
+
+section \ Verum \
+
+definition (in classical_logic) verum :: "'a" ("\")
+ where
+ "\ = \ \ \"
+
+lemma (in classical_logic) verum_tautology [simp]: "\ \"
+ by (metis list_implication.simps(1) list_implication_axiom_k verum_def)
+
+lemma verum_semantics [simp]:
+ "\ \\<^sub>p\<^sub>r\<^sub>o\<^sub>p \"
+ unfolding verum_def by simp
+
+lemma (in classical_logic) verum_embedding [simp]:
+ "\<^bold>\ \ \<^bold>\ = \"
+ by (simp add: classical_logic_class.verum_def verum_def)
+
+section \ Conjunction \
+
+definition (in classical_logic)
+ conjunction :: "'a \ 'a \ 'a" (infixr "\" 67)
+ where
+ "\ \ \ = (\ \ \ \ \) \ \"
+
+primrec (in classical_logic)
+ arbitrary_conjunction :: "'a list \ 'a" ("\")
+ where
+ "\ [] = \"
+ | "\ (\ # \) = \ \ \ \"
+
+lemma (in classical_logic) conjunction_introduction:
+ "\ \ \ \ \ (\ \ \)"
+ by (metis
+ modus_ponens
+ conjunction_def
+ list_flip_implication1
+ list_implication.simps(1)
+ list_implication.simps(2))
+
+lemma (in classical_logic) conjunction_left_elimination:
+ "\ (\ \ \) \ \"
+ by (metis (full_types)
+ Peirces_law
+ pseudo_scotus
+ conjunction_def
+ list_deduction_base_theory
+ list_deduction_modus_ponens
+ list_deduction_theorem
+ list_deduction_weaken)
+
+lemma (in classical_logic) conjunction_right_elimination:
+ "\ (\ \ \) \ \"
+ by (metis (full_types)
+ axiom_k
+ Contraposition
+ modus_ponens
+ conjunction_def
+ flip_hypothetical_syllogism
+ flip_implication)
+
+lemma (in classical_logic) conjunction_embedding [simp]:
+ "\<^bold>\ \ \ \ \<^bold>\ = \<^bold>\ \ \<^bold>\ \ \<^bold>\ \ \<^bold>\"
+ unfolding conjunction_def classical_logic_class.conjunction_def
+ by simp
+
+lemma conjunction_semantics [simp]:
+ "\ \\<^sub>p\<^sub>r\<^sub>o\<^sub>p \ \ \ = (\ \\<^sub>p\<^sub>r\<^sub>o\<^sub>p \ \ \ \\<^sub>p\<^sub>r\<^sub>o\<^sub>p \)"
+ unfolding conjunction_def by simp
+
+section \ Biconditional \
+
+definition (in classical_logic) biconditional :: "'a \ 'a \ 'a" (infixr "\" 75)
+ where
+ "\ \ \ = (\ \ \) \ (\ \ \)"
+
+lemma (in classical_logic) biconditional_introduction:
+ "\ (\ \ \) \ (\ \ \) \ (\ \ \)"
+ by (simp add: biconditional_def conjunction_introduction)
+
+lemma (in classical_logic) biconditional_left_elimination:
+ "\ (\ \ \) \ \ \ \"
+ by (simp add: biconditional_def conjunction_left_elimination)
+
+lemma (in classical_logic) biconditional_right_elimination:
+ "\ (\ \ \) \ \ \ \"
+ by (simp add: biconditional_def conjunction_right_elimination)
+
+lemma (in classical_logic) biconditional_embedding [simp]:
+ "\<^bold>\ \ \ \ \<^bold>\ = \<^bold>\ \ \<^bold>\ \ \<^bold>\ \ \<^bold>\"
+ unfolding biconditional_def classical_logic_class.biconditional_def
+ by simp
+
+lemma biconditional_semantics [simp]:
+ "\ \\<^sub>p\<^sub>r\<^sub>o\<^sub>p \ \ \ = (\ \\<^sub>p\<^sub>r\<^sub>o\<^sub>p \ \ \ \\<^sub>p\<^sub>r\<^sub>o\<^sub>p \)"
+ unfolding biconditional_def
+ by (simp, blast)
+
+section \ Negation \
+
+definition (in classical_logic) negation :: "'a \ 'a" ("\")
+ where
+ "\ \ = \ \ \"
+
+lemma (in classical_logic) negation_introduction:
+ "\ (\ \ \) \ \ \"
+ unfolding negation_def
+ by (metis axiom_k modus_ponens implication_absorption)
+
+lemma (in classical_logic) negation_elimination:
+ "\ \ \ \ (\ \ \)"
+ unfolding negation_def
+ by (metis axiom_k modus_ponens implication_absorption)
+
+lemma (in classical_logic) negation_embedding [simp]:
+ "\<^bold>\ \ \ \<^bold>\ = \ \<^bold>\ \ \<^bold>\"
+ by (simp add:
+ classical_logic_class.negation_def
+ negation_def)
+
+lemma negation_semantics [simp]:
+ "\ \\<^sub>p\<^sub>r\<^sub>o\<^sub>p \ \ = (\ \ \\<^sub>p\<^sub>r\<^sub>o\<^sub>p \)"
+ unfolding negation_def
+ by simp
+
+section \ Disjunction \
+
+definition (in classical_logic) disjunction :: "'a \ 'a \ 'a" (infixr "\" 67)
+ where
+ "\ \ \ = (\ \ \) \ \"
+
+primrec (in classical_logic) arbitrary_disjunction :: "'a list \ 'a" ("\")
+ where
+ "\ [] = \"
+ | "\ (\ # \) = \ \ \ \"
+
+lemma (in classical_logic) disjunction_elimination:
+ "\ (\ \ \) \ (\ \ \) \ (\ \ \) \ \"
+proof -
+ let ?\ = "[\ \ \, \ \ \, \ \ \]"
+ have "?\ :\ (\ \ \) \ \"
+ unfolding disjunction_def
+ by (metis hypothetical_syllogism
+ list_deduction_def
+ list_implication.simps(1)
+ list_implication.simps(2)
+ set_deduction_base_theory
+ set_deduction_theorem
+ set_deduction_weaken)
+ hence "?\ :\ \