×

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

Summary: The decidability of the logic of pure ticket entailment means that the problem of inhabitation of simple types by combinators over the base \(\{\mathsf {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.

MSC:

03B47 Substructural logics (including relevance, entailment, linear logic, Lambek calculus, BCK and BCI logics)
03B40 Combinatory logic and lambda calculus
68T15 Theorem proving (deduction, resolution, etc.) (MSC2010)
PDFBibTeX XMLCite
Full Text: DOI

References:

[1] Anderson A.R.: Entailment shorn of modality (abstract). J. Symb. Log. 25, 388 (1960)
[2] Anderson, A.R., Belnap, N.D.: Entailment. The logic of relevance and necessity, vol. I. Princeton University Press, Princeton (1975) · Zbl 0323.02030
[3] Anderson, A.R., Belnap, N.D., Dunn, J.M.: Entailment. The logic of relevance and necessity, vol. II. Princeton University Press, Princeton (1992) · Zbl 0921.03025
[4] Awodey, S.: Category theory. Oxford logic guides, vol. 52, 2nd edn. Oxford University Press, Oxford (2010) · Zbl 1194.18001
[5] Barendregt H., Ghilezan S.: Lambda terms for natural deduction, sequent calculus and cut elimination. J. Funct. Program. 10, 121–134 (2000) · Zbl 0949.03055 · doi:10.1017/S0956796899003524
[6] Bimbó K.: Types of i-free hereditary right maximal terms. J. Philos. Log. 34, 607–620 (2005) · Zbl 1089.03011
[7] 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)
[8] Bimbó, K.: Combinatory logic: pure, applied and typed. Discrete mathematics and its applications. CRC Press, Boca Raton (2012) · Zbl 1245.03001
[9] Bimbó, K., Dunn. J.M.: New consecution calculi for $${R_\(\backslash\)to\^{\(\backslash\),\(\backslash\)mathbf{t}}}$$ R t . Notre Dame J. Form. Log. 53, 491–509 (2012) · Zbl 1345.03046
[10] Bimbó K., Dunn J.M.: On the decidability of implicational ticket entailment. J. Symb. Log. 78, 214–236 (2013) · Zbl 1275.03159 · doi:10.2178/jsl.7801150
[11] Church, A.: The Calculi of Lambda-conversion, 1st edn. Princeton University Press, Princeton (1941) · JFM 67.0041.01
[12] Curry, H.B.: Foundations of mathematical logic. McGraw-Hill Book Company, New York (1963). (Dover, New York, NY, 1977) · Zbl 0163.24209
[13] Curry, H.B., Feys, R.: Combinatory Logic. Studies in logic and the foundations of mathematics, vol. I, 1st edn. North-Holland, Amsterdam (1958) · Zbl 0081.24104
[14] Dunn, J.M.: A ’Gentzen system’ for positive relevant implication, (abstract). J. Symb. Log. 38, 356–357 (1973)
[15] 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) · Zbl 0875.03051
[16] Dunn J.M., Meyer R.K.: Combinators and structurally free logic. Log. J. IGPL. 5, 505–537 (1997) · Zbl 0878.03008 · doi:10.1093/jigpal/5.4.505
[17] Gallier, J.: Constructive logics. Part I. Theor. Comput. Sci. 110(2), 249–339 (1993) · Zbl 0772.03026
[18] Gentzen G.: Investigations into logical deduction. Am. Philos. Q. 1, 288–306 (1964)
[19] Helman, G.H.: Restricted lambda abstraction and the interpretation of some nonclassical logics. Ph.D. thesis, University of Pittsburgh (1977) · Zbl 0355.02017
[20] Herbelin, H.: A {\(\lambda\)}-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) · Zbl 1044.03509
[21] Hindley, J.R.: Basic simple type theory. Cambridge tracts in theoretical computer science, vol. 42. Cambridge University Press, Cambridge (1997) · Zbl 0906.03012
[22] Kripke, S.A.: The problem of entailment, (abstract). J. Symb. Log. 24, 324 (1959)
[23] Meyer R.K.: A general Gentzen system for implicational calculi. Relev. Log. Newsl. 1, 189–201 (1976) · Zbl 0364.02010
[24] Padovani, V.: Ticket entailment is decidable. Math. Struct. Comput. Sci. 23, 568–607 (2013) · Zbl 1280.03014
[25] Pottinger G.: Normalization as a homomorphic image of cut-elimination. Ann. Math. Log. 12, 323–357 (1977) · Zbl 0378.02017 · doi:10.1016/S0003-4843(77)80004-1
[26] 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) · Zbl 1183.03004
[27] Trigg, P., Hindley, J.R., Bunder, M.W.: Combinatory abstraction using B, B’ and friends. Theor. Comput. Sci. 135, 405–422 (1994) · Zbl 0838.03012
[28] Urquhart A.: The undecidability of entailment and relevant implication. J. Symb. Log. 49, 1059–1073 (1984) · Zbl 0581.03011 · doi:10.2307/2274261
[29] Urquhart A.: Four variables suffice. Australas. J. Log. 5, 66–73 (2007) · Zbl 1168.03013
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. In some cases that data have been complemented/enhanced by data from zbMATH Open. This attempts to reflect the references listed in the original paper as accurately as possible without claiming completeness or a perfect matching.