A logic of judgmental existence and its relation to proof irrelevance

TL;DR

This paper develops a natural deduction system for judgmental existence, linking it to proof irrelevance and truncation modalities, with a computational interpretation ensuring properties like normalization.

Contribution

It introduces a novel logical system for judgmental existence that integrates modal notions and provides a Curry-Howard style interpretation.

Findings

System supports judgmental existence reasoning.

Ensures strong normalization and subject reduction.

Connects judgmental existence with proof irrelevance and truncation modalities.

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