Formally Correct Deduction Methods for Computational Logic

Some logics make it easier to say what we want than others and some methods of deduction are simpler to work with than others. One thing typically remains important: that we can deduce all valid things (completeness). In this thesis I tackle completeness of various deduction methods for various logics. The work is formalized in the proof assistant Isabelle/HOL which offers a common language for mathematics and computer science where proofs can be checked mechanically. This thesis discusses the following contributions of my PhD project in particular:
• A historical overview of formalized completeness proofs and a formalization that explains the essence of synthetic completeness proofs.
• A formalization of a concise completeness proof for first-order logic in Isabelle/HOL, including solutions to the issues of formalizing quantifiers and proving completeness for formulas with free variables.
• A verified prover for first-order logic with functions, with a formalized completeness proof that takes the search strategy of the prover into account.
• A synthetic completeness proof for a tableau system for basic hybrid logic which is both terminating and in the Seligman style where the proof rules reflect the local perspective that modal logic is based on.
• Formalized soundness and completeness results for epistemic and public announcement logic, instantiated to a range of concrete axiom systems.
• A best-first proof search tactic for the proof assistant Lean 4.
• An abstract framework for synthetic completeness proofs.