Ticket Entailment

Origin. Anderson and Belnap (1975). System T, the weakest of the main Anderson–Belnap systems: T ⊊ E ⊊ R. The name is from Ryle's "inference tickets" — a conditional is a licence to infer, not a further premise, and T is built so that only genuine ticket-uses license the arrow.

Models. The antecedent must be used, as in every relevant logic; what T drops relative to E and R is permutation, so the order in which tickets are presented matters. Ternary Routley-Meyer frames.

Formalism.

Ticket intuition: A → B: "Given a ticket for A, can get B." The ticket must be used — T is relevant, so variable sharing holds. Contrast: linear (must use exactly once, no distribution), R (must use, and may permute).

System T axioms: A → A (identity) (A → B) → ((B → C) → (A → C)) (suffixing) (A → (A → B)) → (A → B) (contraction) (A → B) → ((C → A) → (C → B)) (prefixing) A ∧ B → A, A ∧ B → B (simplification) (A → B) ∧ (A → C) → (A → B ∧ C)

Key differences: From relevance logic R: T lacks: A → ((A → B) → B) (assertion) Has: (A → B) → (¬B → ¬A) (contraposition)

Semantics: Ternary relation R(a,b,c). Modified accessibility conditions. T ⊊ E ⊊ R.

Fragment: Implication-only fragment T→. Combinator basis B, B′, I, W — not BCI. C is permutation, which T rejects; B′ is the converse compositor that survives without it, and W is contraction, which T keeps.

Decidability: Full propositional T is undecidable (Urquhart 1984), along with E and R. The pure implicational fragment T→ is decidable — a problem open since Anderson posed it in 1960, settled independently by Bimbó and Dunn (2013) and by Padovani (2013). No PSPACE bound is claimed for either.

Symbols.

Metatheory. T is the weakest of the three Anderson–Belnap systems, T ⊊ E ⊊ R, and what separates it is permutation: T has prefixing and suffixing but not (A → (B → C)) → (B → (A → C)), and correspondingly not assertion, A → ((A → B) → B). Contraction is retained, so the implicational fragment T→ corresponds under Curry–Howard to the combinator basis B, B′, I, W rather than to BCIW. T is complete for the Routley–Meyer ternary relational semantics, and variable sharing holds: a theorem A → B has a propositional variable common to A and B. Urquhart, "The undecidability of entailment and relevant implication" (Journal of Symbolic Logic, 1984), proved T undecidable along with E and R, by a reduction through von Neumann's coordinatization of modular lattices, and Urquhart (1993) showed that Craig interpolation fails for all three. The decision problem for T→ was open from Anderson's posing of it in 1960 and was settled affirmatively by Bimbó and Dunn (2013) and independently by Padovani (2013).

Applies to. Philosophy of entailment. Substructural hierarchy. Conditional logic. Fine-grained implication.

Limitations. Full propositional T is undecidable, so the positive decidability result covers only the pure implicational fragment, and neither the Bimbó–Dunn nor the Padovani proof yields an elementary complexity bound: T→ is known to be decidable without being known to be feasibly so. Craig interpolation fails, removing the standard definability and modularity results. Without permutation the order in which antecedents are discharged matters, so T's fusion is not commutative and T has no algebraic characterization as economical as the De Morgan monoids that characterize R; the Routley–Meyer frame conditions for T are correspondingly more intricate than R's. Variable sharing holds but is only necessary, not sufficient, so it does not characterize theoremhood. Disjunctive syllogism is unavailable inside the arrow, and the deduction theorem holds only in the relevant form.

© 2026 Lingenic LLC