Ticket Entailment

Origin. Anderson and Belnap (1975). Between strict implication and relevant. Ticket analogy: proof uses but needn't consume. Variable sharing without use constraint. System T.

Models. Ticket: permission to use premise once. Not necessarily used. Between intuitionistic and relevance logic. Ternary Routley-Meyer frames.

Formalism.

Ticket intuition: A → B: "Given ticket for A, can get B." Ticket may or may not be used. Contrast: linear (must use), relevant (must share).

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. Between S4 and R.

Fragment: Implication-only fragment. Connection to combinatory logic. BCI combinator basis.

Decidability: Propositional T decidable. PSPACE-complete.

Symbols.

Symbol	Unicode	Name	Meaning
→	U+2192	Ticket entailment	Conditional
T	—	System T	Ticket logic
R	—	Relevance	For comparison
¬	U+00AC	Negation	Standard

Metatheory. Decidable. Between intuitionistic and relevant. Algebraic: T-algebras. Combinator correspondence.

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

Limitations. Less studied than R. Philosophical niche. Limited applications. Between systems.