Abstract
The decidability of the logic of pure ticket entailment means that the problem of inhabitation of simple types by combinators over the base { B, B′, I, W } is decidable too. Type-assignment systems are often formulated as natural deduction systems. However, our decision procedure for this logic, which we presented in earlier papers, relies on two sequent calculi and it does not yield directly a combinator for a theorem of \({T_\to}\) . Here we describe an algorithm to extract an inhabitant from a sequent calculus proof—without translating the proof into another proof system.
Similar content being viewed by others
Rferences
Anderson A.R.: Entailment shorn of modality (abstract). J. Symb. Log. 25, 388 (1960)
Anderson, A.R., Belnap, N.D.: Entailment. The logic of relevance and necessity, vol. I. Princeton University Press, Princeton (1975)
Anderson, A.R., Belnap, N.D., Dunn, J.M.: Entailment. The logic of relevance and necessity, vol. II. Princeton University Press, Princeton (1992)
Awodey, S.: Category theory. Oxford logic guides, vol. 52, 2nd edn. Oxford University Press, Oxford (2010)
Barendregt H., Ghilezan S.: Lambda terms for natural deduction, sequent calculus and cut elimination. J. Funct. Program. 10, 121–134 (2000)
Bimbó K.: Types of i-free hereditary right maximal terms. J. Philos. Log. 34, 607–620 (2005)
Bimbó, K.: Logics, relevance. In: Jacquette, D. (ed.) Philosophy of logic. In: Gabbay, D., Thagard, P., Woods, J. (eds.) Handbook of the Philosophy of Science. vol. 5, pp. 723–789. Elsevier (North-Holland), Amsterdam (2007)
Bimbó, K.: Combinatory logic: pure, applied and typed. Discrete mathematics and its applications. CRC Press, Boca Raton (2012)
Bimbó, K., Dunn. J.M.: New consecution calculi for \({R_\to^{\,\mathbf{t}}}\). Notre Dame J. Form. Log. 53, 491–509 (2012)
Bimbó K., Dunn J.M.: On the decidability of implicational ticket entailment. J. Symb. Log. 78, 214–236 (2013)
Church, A.: The Calculi of Lambda-conversion, 1st edn. Princeton University Press, Princeton (1941)
Curry, H.B.: Foundations of mathematical logic. McGraw-Hill Book Company, New York (1963). (Dover, New York, NY, 1977)
Curry, H.B., Feys, R.: Combinatory Logic. Studies in logic and the foundations of mathematics, vol. I, 1st edn. North-Holland, Amsterdam (1958)
Dunn, J.M.: A ‘Gentzen system’ for positive relevant implication, (abstract). J. Symb. Log. 38, 356–357 (1973)
Dunn. J.M.: Relevance logic and entailment. In: Gabbay, D.,Guenthner, F. (eds.) Handbook of philosophical logic, vol 3, 1st edn. pp. 117–224. D. Reidel, Dordrecht (1986)
Dunn J.M., Meyer R.K.: Combinators and structurally free logic. Log. J. IGPL. 5, 505–537 (1997)
Gallier, J.: Constructive logics. Part I. Theor. Comput. Sci. 110(2), 249–339 (1993)
Gentzen G.: Investigations into logical deduction. Am. Philos. Q. 1, 288–306 (1964)
Helman, G.H.: Restricted lambda abstraction and the interpretation of some nonclassical logics. Ph.D. thesis, University of Pittsburgh (1977)
Herbelin, H.: A λ-calculus structure isomorphic to Gentzen-style sequent calculus structure. In: Computer Science Logic (CSL’94). Lecture Notes in Computer Science, vol. 933, pp. 61–75. Springer, New York (1995)
Hindley, J.R.: Basic simple type theory. Cambridge tracts in theoretical computer science, vol. 42. Cambridge University Press, Cambridge (1997)
Kripke, S.A.: The problem of entailment, (abstract). J. Symb. Log. 24, 324 (1959)
Meyer R.K.: A general Gentzen system for implicational calculi. Relev. Log. Newsl. 1, 189–201 (1976)
Padovani, V.: Ticket entailment is decidable. Math. Struct. Comput. Sci. 23, 568–607 (2013)
Pottinger G.: Normalization as a homomorphic image of cut-elimination. Ann. Math. Log. 12, 323–357 (1977)
Sørensen, M.H., Urzyczyn, P.: Lectures on the Curry–Howard Isomorphism. Studies in logic and the foundations of mathematics, vol. 149. Elsevier, Amsterdam (2006)
Trigg, P., Hindley, J.R., Bunder, M.W.: Combinatory abstraction using B, B’ and friends. Theor. Comput. Sci. 135, 405–422 (1994)
Urquhart A.: The undecidability of entailment and relevant implication. J. Symb. Log. 49, 1059–1073 (1984)
Urquhart A.: Four variables suffice. Australas. J. Log. 5, 66–73 (2007)
Author information
Authors and Affiliations
Corresponding author
Rights and permissions
About this article
Cite this article
Bimbó, K., Michael Dunn, J. Extracting BB′IW Inhabitants of Simple Types From Proofs in the Sequent Calculus \({LT_\to^{t}}\) for Implicational Ticket Entailment. Log. Univers. 8, 141–164 (2014). https://doi.org/10.1007/s11787-014-0099-z
Received:
Accepted:
Published:
Issue Date:
DOI: https://doi.org/10.1007/s11787-014-0099-z