  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.
