# Faithful Logic Embeddings in HOL -- Deep and Shallow

arXiv: https://arxiv.org/abs/2502.19311 · HTML: https://mlsanity.com/paper/2502.19311/

## Key facts

- Cited by 4 papers in the map (data through 14 Oct 2026).
- Builds on 10 of its 64 references that are in the map.
- First posted on arXiv 26 Feb 2025.

## Builds on (most cited first, 10 of 10)

- [Extensional Higher-Order Paramodulation in Leo-III](https://mlsanity.com/paper/1907.11501/) (2019)
- [Lean4Lean: Verifying a Typechecker for Lean, in Lean](https://mlsanity.com/paper/2403.14064/) (2024)
- [Automating Public Announcement Logic with Relativized Common Knowledge as a Fragment of HOL in LogiKEy](https://mlsanity.com/paper/2111.01654/) (2021)
- [Solving Quantified Modal Logic Problems by Translation to Classical Logics](https://mlsanity.com/paper/2212.09570/) (2022)
- [Normative Conditional Reasoning as a Fragment of HOL](https://mlsanity.com/paper/2308.10686/) (2023)
- [Systematic Verification of the Modal Logic Cube in Isabelle/HOL](https://mlsanity.com/paper/1507.08717/) (2015)
- [Mechanized HOL Reasoning in Set Theory](https://mlsanity.com/paper/2403.13403/) (2024)
- [Logical Modalities within the European AI Act: An Analysis](https://mlsanity.com/paper/2501.19112/) (2025)
- [Mechanizing Principia Logico-Metaphysica in Functional Type Theory](https://mlsanity.com/paper/1711.06542/) (2017)
- [Shallow Embedding of Type Theory is Morally Correct](https://mlsanity.com/paper/1907.07562/) (2019)

## Built on by (most cited first, 4 of 4)

- [Many Logics, One Methodology: A Plea for Logical Pluralism in Formalised Reasoning (preprint)](https://mlsanity.com/paper/2605.27246/) (2026)
- [Monadic Second-Order Logic in HOL: Deep and Shallow with Automated Faithfulness (Extended Preprint)](https://mlsanity.com/paper/2609.07345/) (2026)
- [First-Order Modal Logic in HOL: Deep and Shallow Embeddings with Automated Faithfulness (Extended Preprint)](https://mlsanity.com/paper/2607.10880/) (2026)
- [Mathematical Proof Assistants for Teaching Logic: The LogiKEy Methodology](https://mlsanity.com/paper/2610.08214/) (2026)

## Abstract (arXiv)

Deep and shallow embeddings of non-classical logics 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 deployment of deep and shallow embeddings of various degrees 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 using a simple propositional modal logic. However, this approach is conceptual in nature and not limited to this simple logic context.