A logic of judgmental existence and its relation to proof irrelevance
Ivo Pezlar
TL;DR
This paper distinguishes judgmental existence from propositions by introducing a simple natural deduction system for judgments of the form '$a \therefore \varphi$' and an internalized modal operator '$\triangle \varphi$' for existence. It presents both a purely logical variant and a Curry–Howard–style computational variant, proving strong normalization and subject reduction, and it links the existence modality to propositional truncation and lax modality. The work clarifies how existence interacts with implication and truncation, and demonstrates that the lax logic of Pfenning and Davies can be recovered from this framework, while also highlighting prospects for extensions to richer logics and dependent types. Overall, it provides a rigorous foundation for judgmental existence and its role in proof irrelevance, with potential implications for formalizing mere propositions and controlled proof content in type theories.
Abstract
We introduce a simple natural deduction system for reasoning with judgments of the form "there exists a proof of $\varphi$" to explore the notion of judgmental existence following Martin-Löf's methodology of distinguishing between judgments and propositions. In this system, the existential judgment can be internalized into a modal notion of propositional existence that is closely related to truncation modality, a key tool for obtaining proof irrelevance, and lax modality. We provide a computational interpretation in the style of the Curry-Howard isomorphism for the existence modality and show that the corresponding system has some desirable properties such as strong normalization or subject reduction.