Uploaded November 2024 | Updated September 2026, 12 hours ago

---

Recorded as part of the CFvW Colloquium on 20. November 2024

A logic of judgmental existence and its relation to proof irrelevance -
Dr. Ivo Pezlar (Institute of Philosophy of the Czech Academy of Sciences)

Abstract:
In this talk, we introduce a simple natural deduction system for reasoning with judgments of the form "there exists a proof of A" 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 normalization or subject reduction.

Explore our colloquium schedule on our website: uni-tuebingen.de/en/research/centers-and-institutes/carl-friedrich-von-weizsaecker-center/news-and-events/carl-friedrich-von-weizsaecker-colloquium