Mathematical Structures in Computer Science


Ticket Entailment is decidable


Equipe Preuves, Programmes et Systèmes, Université Paris VII – Denis Diderot, Case 7014, 75205 PARIS Cedex 13, France Email: [email protected]


We prove the decidability of the logic T of Ticket Entailment. This issue was first raised by Anderson and Belnap within the framework of relevance logic, and is equivalent to the question of the decidability of type inhabitation in simply typed combinatory logic with the partial basis BB′IW. We solve the equivalent problem of type inhabitation for the restriction of simply typed lambda calculus to hereditarily right-maximal terms.

(Received June 19 2010)

(Revised March 06 2012)

(Online publication July 09 2012)