Conservative Extensions of Intuitionistic Logic with Epsilon Terms over Predicate Abstraction

Extensions of Intuitionistic logic with Hilbert’s epsilon terms are famously non-conservative over Intuitionistic quantification. Partial solutions rely on weaker axioms, extensions to existence predicate or stronger intermediate logics, but do not scale well to theories. In this talk, I present a new approach, implicit in early papers by Melvin Fitting on Herbrand’s theorem for modal logics. Fitting extends quantified S4 modal logic with epsilon terms and predicate abstraction, using lambda binders to create a scoping mechanism for terms that mimics that of quantifiers. The resulting logic is conservative over S4. An immediate but overlooked consequence is its faithful embedding of Intuitionistic quantifiers over their modal and epsilon translation. I show that this result can be improved by internalizing the S4 modalities directly into lambda abstractors, thus eliminating modalities from the language entirely. The resulting logic is still conservative extension over Intuitionistic quantification, and remains so when adding identity and term extensionality, opening the way for applications to constructive theories.