A logic of judgmental existence and its relation to proof irrelevance
<|reference_start|>A logic of judgmental existence and its relation to proof irrelevance: 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.<|reference_end|>
@article{pezlar2024a,
    title={A logic of judgmental existence and its relation to proof irrelevance},
    author={Ivo Pezlar},
    journal={arXiv preprint arXiv:2405.14481},
    year={2024},
    archivePrefix={arXiv},
    eprint={2405.14481},
    primaryClass={cs.LO math.LO}
}