Ticket Entailment is decidable

TL;DR

This paper proves that Ticket Entailment, a problem in relevance logic, is decidable by analyzing type inhabitation in a restricted lambda-calculus, resolving a longstanding open question.

Contribution

It establishes the decidability of Ticket Entailment by linking it to type inhabitation in a specific lambda-calculus fragment, providing a new proof approach.

Findings

Decidability of Ticket Entailment is proven.

Type inhabitation in hereditarily right-maximal terms is decidable.

The problem is reduced to a fragment of simply-typed lambda-calculus.

Abstract

We prove the decidability of Ticket Entailment. Raised by Anderson and Belnap within the framework of relevance logic, this question 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.