## 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: | 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. |

Pages: | 5 |

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

Paper: |