{
  "id": "2405.14481",
  "version": "v1",
  "published": "2024-05-23T12:13:55.000Z",
  "updated": "2024-05-23T12:13:55.000Z",
  "title": "A logic of judgmental existence and its relation to proof irrelevance",
  "authors": [
    "Ivo Pezlar"
  ],
  "categories": [
    "cs.LO",
    "math.LO"
  ],
  "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.",
  "revisions": [
    {
      "version": "v1",
      "updated": "2024-05-23T12:13:55.000Z"
    }
  ],
  "analyses": {
    "keywords": [
      "judgmental existence",
      "simple natural deduction system",
      "existence modality",
      "modal notion",
      "computational interpretation"
    ],
    "note": {
      "typesetting": "TeX",
      "pages": 0,
      "language": "en",
      "license": "arXiv",
      "status": "editable"
    }
  }
}