[Next]  [Previous]  [Up]  

Problem # 2 [SOLVED]

Submitted by Roger Hindley
Date: Known since 1973!
Statement. Is ticket entailment decidable?
Problem Origin. The problem was first 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 B  ,   ′
B , I  , W  ? The logic T→ has just one deduction-rule ((→ E) or modus ponens), and four axiom-schemes:

(α →  β) → ((γ →  α) →  (γ →  β))  , α →  α  ,

(α →  β) →  ((β →  γ) →  (α →  γ))  , (α →  (α →  β)) → (α →  β)  .

Alternatively, let CL   ′
B,B ,I,W  be the system of combinatory logic whose terms are built by application from four basic combinators with reduction rules:

BXY   Z ⊳ X(Y  Z),  B  XY  Z ⊳ Y (XZ),   IX  ⊳ X,  W  XY  ⊳ XY  Y.

(Abstraction in CLB,B ′,I,W  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 a,b,c,...  , and let types be assigned to terms as usual, starting from these four axiom-schemes:

B : (α →  β) → ((γ →  α) →  (γ →  β))  , I : α → α  ,

B  : (α  → β) →  ((β →  γ) →  (α →  γ))  , W  : (α → (α →  β)) →  (α →  β)  .

Is there an algorithm that, when applied to any type τ  , will decide whether there exists a term X  in this system such that X  : τ  is provable?

System T→ first 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 first 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 confluence 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].

References for # 2

[Anderson, 1960]    Anderson, A. R. (1960). Entailment shorn of modality. Journal of Symbolic Logic, 25:388. (Abstract).

[Anderson and Belnap, 1975]    Anderson, A. R. and Belnap, N. D. (1975). Entailment. The Logic of Relevance and Necessity, Volume 1. Princeton University Press, U.S.A.

[Anderson et al., 1992]    Anderson, A. R., Belnap, N. D., and Dunn, J. M. (1992). Entailment. The Logic of Relevance and Necessity, Volume 2. Princeton University Press, U.S.A.

[Bimbó, 2005]    Bimbó, K. (2005). Types of I-free hereditary right maximal terms. Journal of Philosophical Logic, 34:607–620.

[Bimbó, 2006]    Bimbó, K. (2006). Relevance logics. In Jacquette, D., editor, Philosophy of Logic, volume 5 of Handbook of the Philosophy of Science, pages 723–789. North-Holland/ Elsevier, Amsterdam.

[Bimbó and Dunn, 2013]    Bimbó, K. and Dunn, J. M. (2013). On the decidability of implicational ticket entailment. Journal of Symbolic Logic, 78(1):214–236.

[Broda et al., 2004]    Broda, S., Damas, L., Finger, M., and e Silva, P. S. (2004). The decidability of a fragment of BB’IW-logic. Theoretical Computer Science, 318(3):373–408.

[Padovani, 2013]    Padovani, V. (2013). Ticket entailment is decidable. Mathematical Structures in Computer Science, 23(3):568–607.

[Trigg et al., 1994]    Trigg, P., Hindley, J. R., and Bunder, M. W. (1994). Combinatory abstraction using B, B’ and friends. Theoretical Computer Science, 135:405–422.

[Next]  [Previous]  [Up]  
© 2006 Dip. Informatica - Universita di Torino
Last modified: July 21, 2014