Abstract

Deep and shallow embeddings of numerous logic formalisms in classical higher-order logic have been explored, implemented, and used in various reasoning tools in recent years. This paper presents a method for the simultaneous provision of deep and shallow embeddings of various degrees (maximal/minimal) in classical higher-order logic. This enables flexible, interactive and automated theorem proving and counterexample finding at meta and object level, as well as automated faithfulness proofs between these logic embeddings. The method is beneficial for logic education, research and application and is illustrated here initially using simple propositional modal logic. However, the approach is conceptual in nature and not limited to this simple logic context. For example, it also supports quantifiers. To illustrate this, this paper additionally introduces deep and shallow embeddings of quantified Boolean formulas, and, maintaining a high degree of proof automation, faithfulness between these embeddings is proved using respective lemmata, including a substitution lemma. This work demonstrates how mathematical proof assistant systems can facilitate the exploration and rapid prototyping of formal logics. This is relevant not only for formalisation of mathematical knowledge, but also for the mechanisation of legal and normative reasoning and the encoding of foundational metaphysical theories, for example.

The presented material significantly extents the work covered in the following two papers: Christoph Benzmüller: Faithful Logic Embeddings in HOL - Deep and Shallow. CADE 2025 : 280-301. Doi: 10.1007/978-3-031-99984-0_16 (Preprint: arXiv:2502.19311) Christoph Benzmüller: Faithful Logic Embeddings in HOL - Deep and Shallow (Isabelle/HOL dataset). Arch. Formal Proofs 2025 (2025). https://www.isa-afp.org/entries/FaithfulPMLinHOL.html

=== Online talk ===

Join Zoom Meeting https://cam-ac-uk.zoom.us/j/89856091954?pwd=Bba77QB2KuTideTlH6PjAmbXLO8HbY.1

Meeting ID: 898 5609 1954 Passcode: ITPtalk