Constructive Decision via Redundancy-Free Proof-Search

摘要

We give a constructive account of Kripke-Curry's method which was used to establish the decidability of Implicational Relevance Logic (R_→). To sustain our approach, we mechanize this method in axiom-free Coq, abstracting away from the specific features of R_→ to keep only the essential ingredients of the technique. In particular we show how to replace Kripke/Dickson's lemma by a constructive form of Ramsey's theorem based on the notion of almost full relation. We also explain how to replace Konig's lemma with an inductive form of Brouwer's Fan theorem. We instantiate our abstract proof to get a constructive decision procedure for R_→ and discuss potential applications to other logical decidability problems.