| ||||
| ||||
![]() Title:Admissible tools in the kitchen of intuitionistic logic Conference:CL&C 2018 Tags:admissible rules, Intuitionistic logic, Proof theory and propositional logic Abstract: The usual reading of logical implication φ → ψ as “if φ then ψ” fails in intuitionistic logic: there are formulas φ and ψ such that φ → ψ is not provable, even though ψ is provable whenever φ is provable. Intuitionistic rules apparently cannot derive interesting meta-properties of the logic and, from a computational perspective, the programs corresponding to intuitionistic proofs are not powerful enough. We propose a term assignment corresponding to the admissible rules of intuitionistic propositional logic, and employ it to study the admissible principles. We provide as an example a study of Kreisel-Putnam logic KP: we give a Curry-Howard correspondence for this system, proving the disjunction property and all the good constructive properties. This is a first step in understanding how to the programs of admissible rules look like. Admissible tools in the kitchen of intuitionistic logic ![]() Admissible tools in the kitchen of intuitionistic logic | ||||
Copyright © 2002 – 2025 EasyChair |