Constructive Decision via Redundancy-Free Proof-Search
- PDF / 528,048 Bytes
- 23 Pages / 439.37 x 666.142 pts Page_size
- 23 Downloads / 186 Views
Constructive Decision via Redundancy-Free Proof-Search Dominique Larchey-Wendling1 Received: 17 April 2020 / Accepted: 20 April 2020 © Springer Nature B.V. 2020
Abstract 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 König’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. Keywords Constructive decidability · Relevance logic · Sequent calculi · Contraction rule · Redundancy-free search · Almost full relations · Mechanization in Coq Mathematics Subject Classification 03F03 · 03B35 · 03B47
1 Introduction In this paper, we give a fully constructive/inductive account of Kripke’s decidability proof of implicational relevance logic R→ , fulfilling the program outlined by Riche [17]. The result is known as Kripke’s but it crucially relies on Curry’s lemma [18] which states that if a sequent S2 is redundant over a sequent S1 and S2 has a proof, then S1 has a shorter proof. Our account of Kripke–Curry’s method is backed by an axiom-free mechanized proof of the result in the Coq proof assistant.1 However, their method and our constructivized implementation is in no way limited to that particular logic. As explained in [19], “Kripke’s procedure for deciding R→ can be seen as a precursor for many later algorithms that rely on the existence of a well quasi ordering (WQO).” From a logical perspective, Kripke–Curry’s method has been adapted to implicational ticket entailment [2] and the multiplicative and exponential 1 https://coq.inria.fr.
Work partially supported by the joint project ANR-FWF TICAMORE (No. ANR-16-CE91-0002).
B 1
Dominique Larchey-Wendling [email protected] Université de Lorraine, CNRS, LORIA, Campus Scientifique, BP 239, 54 506 Vandœuvre-lès-Nancy, France
123
D. Larchey-Wendling
fragment of linear logic [1]. However, both of these recent papers are now contested inside the community because of flaws in the arguments; see [9, footnote 1], [20, footnote 4], [6, pp 360-362] and [22]. This illustrates that the beauty of Kripke–Curry’s method should not hide its subtlety and justifies all the more the need to machine-check such proofs. From a complexity perspective, Schmitz [19] recently gave a 2- ExpTime complexity characterization of the entailment problem for R→ , implying a decision procedure. However, both theoretically and practically, the existence of a complexity characterization does not automatically imply a constructive proof of decidability. Indeed, the decision procedure itself
Data Loading...
