×

Extending the Curry-Howard interpretation to linear, relevant and other resource logics. (English) Zbl 0765.03005

It is known (Helman) that relevance restriction for implication corresponds to the condition: \(x\) actually occurs freely in \(t\) for the term \(\lambda xt\) corresponding (under Curry-Howard interpretation to \(\to\)-introduction. Similarly, linear restriction (relevance + no contraction rule) is: \(x\) has exactly one free occurrence in \(t\) (Girard). The authors note several similar restrictions for less popular logics. The paper contains a lot of motivations and semi-formal explanations.
Reviewer: G.Mints (Stanford)

MSC:

03B20 Subsystems of classical logic (including intuitionistic logic)
03B40 Combinatory logic and lambda calculus
03B47 Substructural logics (including relevance, entailment, linear logic, Lambek calculus, BCK and BCI logics)
03F05 Cut-elimination and normal-form theorems
PDFBibTeX XMLCite
Full Text: DOI

References:

[1] To H. B. Curry: Essays on combinatory logic, lambda calculus and formalism pp 479– (1969)
[2] Introduction to combinators and {\(\lambda\)}-calculus 1 (1986)
[3] Principal type-schemes and condensed detachment 55 pp 90– (1990)
[4] Grundzüge der Theoretischen Logik (1938) · JFM 64.0026.05
[5] Atti degli incontri di logica matematica 2 pp 203– (1985)
[6] Intuitionism. An introduction (1956) · Zbl 0070.00801
[7] On weakened quantification 11 pp 119– (1946)
[8] From Frege to Gödei: A source hook in mathematical logic. 1879–1931 (1967)
[9] Fundamenta Mathematicae 60 pp 223– (1967)
[10] Intuitionism and proof theory pp 101– (1970)
[11] DOI: 10.1111/j.1746-8361.1958.tb01464.x · Zbl 0090.01003 · doi:10.1111/j.1746-8361.1958.tb01464.x
[12] Proofs and types (1989) · Zbl 0671.68002
[13] DOI: 10.1016/0304-3975(87)90045-4 · Zbl 0625.03037 · doi:10.1016/0304-3975(87)90045-4
[14] DOI: 10.1016/S0049-237X(08)70843-7 · doi:10.1016/S0049-237X(08)70843-7
[15] Logic colloquium ’90 (1990)
[16] Proceedings of logic colloquium ’86 (1988)
[17] The basic laws of arithmetic. Exposition of the system (1964)
[18] Formulas-as-types for a hierarchy of sublogics of intuitionistic propositional logic (1990)
[19] DOI: 10.1007/BF00374052 · Zbl 0657.03009 · doi:10.1007/BF00374052
[20] Journal of Philosophical Logic 12 pp 173– (1983)
[21] Intensional interpretations of functionals of finite type I 32 pp 198– (1967)
[22] Formal systems and recursive functions pp 176– (1965)
[23] DOI: 10.1007/BF02770512 · Zbl 0692.03007 · doi:10.1007/BF02770512
[24] Proceedings of the Jena medical and scientific society (1891)
[25] Begriffsschrift, eine der arithmetischen nachgebildete Formelsprache des reinen Denkens (1879)
[26] Symbolic logic. An introduction (1952)
[27] DOI: 10.1007/BF00370633 · Zbl 0688.03012 · doi:10.1007/BF00370633
[28] DOI: 10.1007/BF00671566 · Zbl 0671.03018 · doi:10.1007/BF00671566
[29] Combinatory logic II (1972) · Zbl 0242.02029
[30] Proceedings of the symposium on automated deduction (Versailles, December 1968) 125 pp 237– (1970)
[31] Combinatory logic I (1958)
[32] DOI: 10.1007/BF01448013 · JFM 50.0023.01 · doi:10.1007/BF01448013
[33] Foundations of mathematical logic (1963) · Zbl 0163.24209
[34] Comptes rendus ébdomadaires des séances de l’Académie des Sciences 243 pp 1263– (1956)
[35] A theory of formal deducibility (1950) · Zbl 0041.34807
[36] Proceedings of the collogue sur la programmation (Paris) 19 pp 408– (1974)
[37] Methods of logic (1950)
[38] The combinatory foundations of mathematical logic 7 pp 49– (1942) · Zbl 0060.02207
[39] Fifth British colloquium for theoretical computer science (1989)
[40] DOI: 10.1002/malq.19910370904 · Zbl 0701.68078 · doi:10.1002/malq.19910370904
[41] DOI: 10.1002/malq.19900360505 · Zbl 0691.03042 · doi:10.1002/malq.19900360505
[42] DOI: 10.1073/pnas.20.11.584 · Zbl 0010.24201 · doi:10.1073/pnas.20.11.584
[43] DOI: 10.2307/1968422 · Zbl 0001.26101 · doi:10.2307/1968422
[44] The calculi of lambda-conversion (1941)
[45] Modal logic. An introduction (1980)
[46] Unification formalisms: syntax, semantics and implementation (1990)
[47] Grundgesetze der Arithmetik. I (1966)
[48] Journal of Philosophical Logic 18 pp 116– (1989)
[49] Logic colloquium ’91 (1991)
[50] The lambda calculus. Its syntax and semantics 103 (1981)
[51] DOI: 10.1111/j.1746-8361.1991.tb00979.x · doi:10.1111/j.1746-8361.1991.tb00979.x
[52] Entailment. The logic of relevance and necessity I (1975)
[53] Normalisation and the semantics of use 55 pp 425– (1990)
[54] Studia Philosophica 1 pp 1– (1935)
[55] Reports of the thirteenth international Wittgenstein symposium 1988 18 pp 259– (1989)
[56] DOI: 10.1111/j.1746-8361.1988.tb00919.x · Zbl 0676.03007 · doi:10.1111/j.1746-8361.1988.tb00919.x
[57] Proceedings of the second Scandinavian logic symposium (Oslo, June 18–20,1970) 63 pp 235–
[58] Natural deduction. A proof-theoretical study (1965) · Zbl 0173.00205
[59] The principles of arithmetic, presented by a new method pp 83– (1889)
[60] Logics without the contraction rule 50 pp 169– (1985) · Zbl 0583.03018
[61] Structural rules and a logical hierarchy pp 11– (1988)
[62] Intuitionistic type theory (1984)
[63] Proceedings of the international congress for logic, methodology and philosophy of science VI (Hannover, August 22–29, 1979) pp 153– (1982)
[64] Proceedings of the logic colloquium ’73 (Bristol, UK) 80 pp 73– · Zbl 0299.00011
[65] Compositie Mathematica 24 pp 93–
[66] Comptes rendus des séances de la Société des Sciences et des Lettres de Varsovie 23 pp 30– (1930)
[67] Intuitionism and proof theory pp 227– (1970)
[68] Intuitionistic prepositional calculus and definably non-empty terms 30 pp 263– (1965)
[69] Introduction to higher order categorical logic 7 (1986) · Zbl 0596.03002
[70] DOI: 10.1090/conm/092/1003201 · doi:10.1090/conm/092/1003201
[71] To H. B. Curry: Essays on combinatory logic, lambda calculus and formalism pp 375– (1980)
[72] DOI: 10.2307/2310058 · Zbl 0080.00702 · doi:10.2307/2310058
[73] Mathematica Japonka 34 pp 585– (1989)
[74] Reports of Faculty of Science, Shizuoka University 17 pp 13– (1983)
[75] Compositie Mathematica 4 pp 119– (1936)
[76] Studia Logica 1 pp 5– (1934)
[77] Lafont and Taylor’s Proofs and types 56 pp 760– (1991)
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.