Saved in:
| Main Author: | |
|---|---|
| Format: | Preprint |
| Published: |
2024
|
| Subjects: | |
| Online Access: | https://arxiv.org/abs/2405.14481 |
| Tags: |
Add Tag
No Tags, Be the first to tag this record!
|
| _version_ | 1866929355006935040 |
|---|---|
| author | Pezlar, Ivo |
| author_facet | Pezlar, Ivo |
| contents | We introduce a simple natural deduction system for reasoning with judgments of the form "there exists a proof of $φ$" to explore the notion of judgmental existence following Martin-Lö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. |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_2405_14481 |
| institution | arXiv |
| publishDate | 2024 |
| record_format | arxiv |
| spellingShingle | A logic of judgmental existence and its relation to proof irrelevance Pezlar, Ivo Logic in Computer Science Logic We introduce a simple natural deduction system for reasoning with judgments of the form "there exists a proof of $φ$" to explore the notion of judgmental existence following Martin-Lö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. |
| title | A logic of judgmental existence and its relation to proof irrelevance |
| topic | Logic in Computer Science Logic |
| url | https://arxiv.org/abs/2405.14481 |