Quantified Conditional Logics are Fragments of HOL
Christoph Benzmueller, Valerio Genovese · 2011
A semantic embedding of propositional conditional logic in classical higher-order logic HOL (Church’s type theory) has been presented in [3]. This embedding exploits the natural correspondence between selection function semantics for conditional logics [10] and HOL. In fact, selection function semantics can be seen as an higher-order extension of well-known Kripke semantics for modal logic and cannot be naturally embedded into first-order logic. In this paper we extend the embedding in [3] to also include quantification over propositions and individuals. This embedding of quantified conditional logic in HOL is sound and complete.