Submitted by Roger Hindley
Date: Known since 1973!
Statement. Is ticket entailment decidable?
Problem Origin. The problem was ﬁrst posed by Robert Meyer.
The question is whether there is a decision-algorithm for the implicational fragment T of the propositional logic called ticket entailment. Equivalently, is there one for the simple type-theory of the restricted combinatory logic based on , , , ? The logic T has just one deduction-rule ((E) or modus ponens), and four axiom-schemes:
Alternatively, let CL be the system of combinatory logic whose terms are built by application from four basic combinators with reduction rules:
(Abstraction in CL is much weaker than in full combinatory logic; see [Trigg et al., 1994, 3] for a characterization by P. Trigg.) Let types be built by the operation from type-variables , and let types be assigned to terms as usual, starting from these four axiom-schemes:
Is there an algorithm that, when applied to any type , will decide whether there exists a term in this system such that is provable?
System T ﬁrst appeared in print in [Anderson, 1960], although it dates back at least to work of Belnap in 1957. It was motivated and described in detail in [Anderson and Belnap, 1975, Chapter 1 6 and 8.3.2 (pp. 41–50 and 76)]. Its decidability question was ﬁrst raised on p. 69 of that book. Proofs of the decidability and undecidability of several related systems were given in [Anderson et al., 1992, 60–67 (pp. 267–391)]; for example in 65.2 the logic T of ticket entailment was shown to be undecidable, but the method did not apply to its implicational fragment T. A decidability result for a restricted class of formulas can be found in [Broda et al., 2004].
Warnings: (1) In the 30 years since 1975 the T problem and its combinatory equivalent have been tried by several very able workers without success. For example some relevant results are in [Bimbó, 2005] and [Bimbó, 2006].
(2) In papers on entailment, omitted parentheses are usually restored by “association to the left”, not “to the right” as in types in type theory!
Solution: Two independent conﬂuence proofs have been proposed in 2010. The solution by Katalin Bimbó and J. Michael Dunn is published in [Bimbó and Dunn, 2013]. The solution by Vincent Padovani is published in [Padovani, 2013].