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.03028OpenAlexW2135096857MaRDI 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

decidabilitysequent calculicombinatorsrelevance logicstype assignment systemsinhabitationticket entailmentAckermann constantsstructurally free logics

Mathematics Subject Classification ID

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

Related Items

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

Cites Work

• 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
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item