×

Substitution contradiction, its resolution and the Church-Rosser theorem in TIL. (English) Zbl 1484.03006

Summary: I present an analysis according to which the current state of the definition of substitution leads to a contradiction in the system of Transparent Intensional Logic (TIL). I entail the contradiction using only the basic definitions of TIL and standard results. I then analyse the roots of the contradiction and motivate the path I take in resolving the contradiction. I provide a new amended definition of collision-less substitution which blocks the contradiction in a non-ad hoc way. I elaborate on the consequences of the amended definition, namely the invalidity of the Church-Rosser theorem (the so-called diamond property). I present a counterexample to the validity of the theorem in TIL with an amended definition of substitution.

MSC:

03A05 Philosophical and critical aspects of logic and foundations
03B40 Combinatory logic and lambda calculus
03B60 Other nonclassical logic

Software:

Automath
PDFBibTeX XMLCite
Full Text: DOI

References:

[1] Barendregt, H. P. (1992). Lambda Calculi with Types. ://ttic.uchicago.edu/ dreyer/course/papers/barendregt.pdf. Accessed 11 September 2017. · Zbl 0816.03007
[2] Church, A., A formulation of the simple theory of types, The Journal of Symbolic Logic, 5, 2, 56-68 (1940) · JFM 66.1192.06
[3] Church, A.; Henle, P.; Kallen, Hm; Langer, Sk, A Formulation of the Logic of Sense and Denotation, Structure, Method and Meaning: Essays in Honor of Henry M. Sheffer, 3-24 (1951), New York: The Liberal Arts Press, New York
[4] Duží, M., The Paradox of Inference and the Non-Triviality of Analytic Information, Journal of Philosophical Logic, 39, 5, 473-510 (2010) · Zbl 1221.03010
[5] Duží, M.; Jespersen, B.; Materna, P., Procedural Semantics for Hyperintensional Logic: Foundations and Applications of Transparent Intensional Logic (2010), Berlin: Springer, Berlin · Zbl 1207.03009
[6] Duží, M. (2012). Towards an extensional calculus of hyperintensions. Organon F, 19(supplementary issue 1), 20-45. · Zbl 1314.03031
[7] Duží, M.; Jespersen, B., Procedural isomorphism, analytic information, and B- conversion by value, Logic Journal of the IGPL, 21, 2, 291-308 (2013) · Zbl 1277.03024
[8] Duží, M.; Jespersen, B., Transparent Quantification into Hyperintensional objectual attitudes, Synthese, 192, 3, 635-677 (2015) · Zbl 1357.03062
[9] Duží, Marie, If structured propositions are logical procedures then how are procedures individuated?, Synthese, 196, 4, 1249-1283 (2017) · Zbl 1474.03015
[10] Duží, M.; Kosterec, M., A valid rule of β-conversion for the logic of partial functions, Organon F, 24, 1, 10-36 (2017)
[11] Friedmann, J.; Warren, Ds, λ-Normal Forms in an Intensional Logic for English, Studia Logica, 39, 311-324 (1980) · Zbl 0457.03010
[12] Hindley, J. R. (1997). Basic Simple Type Theory. Cambridge University Press. · Zbl 0906.03012
[13] Jago, M., The Impossible: An Essay on Hyperintensionality (2014), Oxford: Oxford University Press, Oxford
[14] Jespersen, B.; Materna, P., Are Wooden Tables Necessarily Wooden? Intensional Essentialism Versus Metaphysical Modality, Acta Analytica, 17, 1, 115-150 (2002)
[15] Jespersen, B.; Carrara, M., A New Logic of Technical Malfunction, Studia Logica, 101, 3, 547-581 (2013) · Zbl 1315.03007
[16] Materna, P. (1998). Concepts and Objects. Helsinki: Acta Philosophica Fennica 63.
[17] Muskens, R. (1995): Meaning and Partiality. CSLI Leland Stanford Junior University, California: Stanford.
[18] Kosterec, Miloš, On the number of types, Synthese, 194, 12, 5005-5021 (2016) · Zbl 1417.03079
[19] Kosterec, M. (submitted): On the Validity of the Church-Rosser Theorem for β-reductions in Transparent Intensional Logic. · Zbl 1484.03006
[20] Pezlar, Ivo, On Two Notions of Computation in Transparent Intensional Logic, Axiomathes, 29, 2, 189-205 (2018)
[21] Raclavský, J., Jména a deskripce (2009), Olomouc: Nakladatelství Olomouc, Olomouc
[22] Raclavský, J.; Peliš, M.; Punčochář, V., Semantic Paradoxes and Transparent Intensional Logic, The Logica Yearbook 2011, 239-252 (2011), London: College Publications, London
[23] Tichý, P., The Foundations of Frege’s Logic (1988), Berlin: Walter de Gruyter & co, Berlin · Zbl 0671.03001
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.