Extracting \(\mathsf{BB'IW}\) inhabitants of simple types from proofs in the sequent calculus \(LT_\to^t\) for implicational ticket entailment

DOI10.1007/s11787-014-0099-zzbMath1344.03028MaRDI QIDQ2254561

J. Michael Dunn, Katalin Bimbó

Publication date: 5 February 2015

Published in: Logica Universalis (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/s11787-014-0099-z

zbMATH Keywords

decidability; sequent calculi; combinators; relevance logics; type assignment systems; inhabitation; ticket entailment; Ackermann constants; structurally free logics

Mathematics Subject Classification ID

03B47: Substructural logics (including relevance, entailment, linear logic, Lambek calculus, BCK and BCI logics)

03B40: Combinatory logic and lambda calculus

Related Items

Current trends in substructural logics, New consecution calculi for \(R^{t}_{\to}\)

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• New consecution calculi for \(R^{t}_{\to}\)
• Combinatory logic. With two sections by William Craig.
• Types of I-free hereditary right maximal terms
• Lectures on the Curry-Howard isomorphism
• Constructive logics. I: A tutorial on proof systems and typed \(\lambda\)- calculi
• Completeness of the normal typed fragment of the \(\lambda\)-system \(U\)
• Combinatory abstraction using \({\mathbf B}\), \({\mathbf B}^ \prime\) and friends
• The undecidability of entailment and relevant implication
• Normalization as a homomorphic image of cut-elimination
• Combinators and structurally free logic
• On the decidability of implicational ticket entailment
• Ticket Entailment is decidable
• Lambda terms for natural deduction, sequent calculus and cut elimination