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\"{o}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.

翻译：本文引入一个简单的自然演绎系统，用于推理"存在φ的证明"这类判断，以遵循Martin-Löf关于判断与命题区分的方法论来探讨判断存在性的概念。在该系统中，存在判断可被内化为一种命题存在性的模态概念，这种概念与截断模态（获取证明无关性的关键工具）及松弛模态密切相关。我们采用Curry-Howard同构风格为存在模态提供计算解释，并证明相应系统具备强正规化、主体归约等优良性质。