Strong Normalization for Truth Table Natural Deduction

• Autorzy: Geuvers Herman , van der Giessen Iris , Hurkens Tonny

Identyfikatory

DOI

10.3233/FI-2019-1858

• Języki publikacji: EN

Abstrakty

EN

We present a proof of strong normalization of proof-reduction in a general system of natural deduction called truth table natural deduction. In previous work, we have defined truth table natural deduction, which is a method for deriving intuitionistic derivation rules for a connective from its truth table. This yields natural deduction rules for each connective separately. Moreover, these rules adhere to a standard format which gives rise to a general notions of detour and permutation conversion for natural deductions. The aim is to remove all convertibilities and obtain a deduction in normal form. In general, conversion of truth table natural deductions is non-deterministic, which makes it more challenging to study. It has already been shown that this conversion is weakly normalizing. To prove strong normalization, we construct a conversion-preserving translation from deductions to terms in an extension of simply typed lambda calculus which we call parallel simply typed lambda calculus and which we prove to be strongly normalizing. This makes it possible to get a grip on the non-deterministic character of conversion in the intuitionistic truth table natural deduction system.

Słowa kluczowe

EN

natural deduction; truth tables; intuitionistic logic; detour conversion; permutation conversion; strong normalization

• Wydawca: IOS Press
• Czasopismo: Fundamenta Informaticae
• Rocznik: 2019
• Tom: Vol. 170, nr 1-3
• Strony: 139--176
• Opis fizyczny: Bibliogr. 23 poz., rys., tab.

Twórcy

autor

Geuvers Herman

• Institute for Computing and Information Science, Radboud University Nijmegen, The Netherlands

autor

van der Giessen Iris

• Department of Philosophy and Religious Studies, Utrecht University, The Netherlands

autor

Hurkens Tonny

• Haps, The Netherlands

Bibliografia

• [1] Gentzen G. Untersuchungen über das logische Schliessen. In: The Collected Papers of Gerhard Gentzen, Studies in logic and the foundations of mathematics. North-Holland Pub. Co., 1969 doi:10.1006/inco.2002.3147.
• [2] Prawitz D. Natural deduction: a proof-theoretical study. Almqvist & Wiksell, 1965. doi:10.2307/2271676.
• [3] Geuvers H, Hurkens T. Deriving Natural Deduction Rules from Truth Tables. In: Logic and Its Applications - 7th Indian Conference, ICLA 2017, Kanpur, India, January 5-7, 2017, Proceedings, volume 10119 of Lecture Notes in Computer Science. 2017 pp. 123-138. doi:10.1007/978-3-662-54069-5_10.
• [4] Geuvers H, Hurkens T. Proof Terms for Generalized Natural Deduction. In: Abel A, Forsberg FN, Kaposi A (eds.), 23rd International Conference on Types for Proofs and Programs, TYPES 2017, May 29-June 1, 2017, Budapest, Hungary, volume 104 of LIPIcs. Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik, 2018 pp. 3:1-3:39. doi:10.4230/LIPIcs.TYPES.2017.3.
• [5] de Groote P. On the Strong Normalisation of Intuitionistic Natural Deduction with Permutation-Conversions. Inf. Comput., 2002. 178(2):441-464. doi:10.1006/inco.2002.3147.
• [6] Howard W. The formulae-as-types notion of construction. In: Hindley JR, Seldin JP (eds.), Essays on Combinatory Logic, Lambda Calculus and Formalism, pp. 479-490. Academic Press, London, 1980. Dedicated to Haskell B. Curry on the occasion of his 80th birthday.
• [7] Sørensen M, Urzyczyn P. Lectures on the Curry-Howard Isomorphism, Volume 149 (Studies in Logic and the Foundations of Mathematics). Elsevier Science Inc., New York, NY, USA, 2006. ISBN 0444520775.
• [8] Terese. Term Rewriting Systems, volume 55 of Cambridge Tracts in Theoretical Computer Science. Cambridge University Press, 2003.
• [9] Nederpelt R, Geuvers H. Type Theory and Formal Proof: An Introduction. Cambridge University Press, 2014. ISBN 9781107036505. URL https://books.google.nl/books?id=wzTJBAAAQBAJ.
• [10] Tait W. Intensional Interpretations of Functionals of Finite Type I. J. Symbolic Logic, 1967. 32(2):198-212. URL https://projecteuclid.org:443/euclid.jsl/1183735831.
• [11] van der Giessen I. Natural Deduction Derived from Truth Tables, Master Thesis Mathematics, Radboud University Nijmegen, July 2018. URL https://www.ru.nl/math/@1060423/master-theses-per-year/.
• [12] Takahashi M. Parallel Reductions in λ-Calculus. Information and Computation, 1995. 118(1):120-127. doi:https://doi.org/10.1006/inco.1995.1057.
• [13] Plotkin G. Call-by-name, call-by-value and the λ-calculus. Theoretical Computer Science, 1975. 1(2):125-159. doi:https://doi.org/10.1016/0304-3975(75)90017-1.
• [14] von Plato J. Natural deduction with general elimination rules. Arch. Math. Log., 2001. 40(7):541-567.
• [15] Schroeder-Heister P. A Natural Extension of Natural Deduction. J. Symb. Log., 1984. 49(4):1284-1300.
• [16] Negri S, von Plato J. Structural Proof Theory. Cambridge University Press, 2001.
• [17] Prawitz D. Ideas and Results in Proof Theory. In: Fenstad J (ed.), 2nd Scandinavian Logic Symposium, pp. 237-309. North-Holland, 1971.
• [18] von Plato J. Natural deduction: some recent developments, summary of four lectures at the summer school on proof theory, computation, and complexity. Technische Universität Dresden, June 23 - July 4, 2003. URL http://www.helsinki.fi/~negri/dresum.pdf.
• [19] Troelstra AS. Metamathematical Investigations of intuitionistic arithmetic and analysis, volume 344 of Lecture Notes in Mathematics. Springer Verlag, 1973.
• [20] Simpson AK. The Proof Theory and Semantics of Intuitionistic Modal Logic. Ph.D. thesis, University of Edinburgh, 1994.
• [21] Milne P. Inversion Principles and Introduction Rules. In: Wansing H (ed.), Dag Prawitz on Proofs and Meaning, pp. 189-224. Springer International Publishing, Cham. ISBN 978-3-319-11041-7, 2015. doi:10.1007/978-3-319-11041-7_8.
• [22] Read S. Harmony and Autonomy in Classical Logic. Journal of Philosophical Logic, 2000. 29(2):123-154. doi:10.1023/A:1004787622057.
• [23] Francez N, Dyckhoff R. A Note on Harmony. Journal of Philosophical Logic, 2012. 41(3):613-628. doi:10.1007/s10992-011-9208-0.

Uwagi

Opracowanie rekordu w ramach umowy 509/P-DUN/2018 ze środków MNiSW przeznaczonych na działalność upowszechniającą naukę (2019).