arXiv Analytics

Sign in

arXiv:2405.14481 [cs.LO]AbstractReferencesReviewsResources

A logic of judgmental existence and its relation to proof irrelevance

Ivo Pezlar

Published 2024-05-23Version 1

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.

Related articles: Most relevant | Search more
arXiv:2001.03540 [cs.LO] (Published 2020-01-10)
A computational interpretation of Zorn's lemma
arXiv:1203.4754 [cs.LO] (Published 2012-03-21)
Computational interpretation of classical logic with explicit structural rules
arXiv:1611.09263 [cs.LO] (Published 2016-11-28)
Guarded Cubical Type Theory