Admissible tools in the kitchen of intuitionistic logic

Authors: Matteo Manighetti and Andrea Condoluci

Paper Information

Title:Admissible tools in the kitchen of intuitionistic logic
Authors:Matteo Manighetti and Andrea Condoluci
Proceedings:CL&C Full papers and abstracts
Editor: Stefano Berardi
Keywords:Proof theory, Intuitionistic logic, propositional logic, admissible rules

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.

Talk:Jul 07 16:00 (Session 31A)