Formalizing Implicational Axiomatics for Classical First-Order Logic with Functions in Isabelle/HOL

We present a concise formalization in the proof assistant Isabelle/HOL of classical first-order logic with functions. Our standalone formalization is based on entries in the Isabelle Archive of Formal Proofs and has recently been used for teaching logic and automated reasoning. The soundness and completeness theorems hold for languages of arbitrary cardinalities. The axioms and rules start from classical implicational logic and add falsity and universal quantification. Relatively simple functional programs are provided for substitution and other operations. We consider the axiomatics a stepping stone for learning about higher-order logic and structured natural deduction proofs in Isabelle/HOL.