Admissible Tools in the Kitchen of Intuitionistic Logic
Andrea Condoluci, Matteo Manighetti

TL;DR
This paper introduces a calculus that captures admissible inferences in intuitionistic logic, extending its capabilities while preserving intuitionistic properties, and demonstrates this with the Kreisel-Putnam logic KP.
Contribution
It presents a novel calculus representing admissible inferences in intuitionistic logic, maintaining normal forms as intuitionistic terms, and proves key properties for the extended logic KP.
Findings
The calculus can represent admissible inferences within intuitionistic logic.
Strong normalization and disjunction property are proved for the extended logic KP.
The approach advances understanding of admissible rules in intuitionistic logic.
Abstract
The usual reading of logical implication "A implies B" as "if A then B" fails in intuitionistic logic: there are formulas A and B such that "A implies B" is not provable, even though B is provable whenever A is provable. Intuitionistic rules apparently do not capture interesting meta-properties of the logic and, from a computational perspective, the programs corresponding to intuitionistic proofs are not powerful enough. Such non-provable implications are nevertheless admissible, and we study their behavior by means of a proof term assignment and related rules of reduction. We introduce V, a calculus that is able to represent admissible inferences, while remaining in the intuitionistic world by having normal forms that are just intuitionistic terms. We then extend intuitionistic logic with principles corresponding to admissible rules. As an example, we consider the Kreisel-Putnam logic…
Peer Reviews
No public reviews on file for this paper yet. If you reviewed it on a platform where reviews are public (OpenReview, ICLR, NeurIPS, ICML), you can paste yours below so the community can read it here.
Videos
No videos yet. Explain this paper in a talk, walkthrough, or lecture? Add one.
