Keywords
Identity of proofs
Church-Turing thesis
Derivation
Normal form
How to Cite
Abstract
This article is a methodological discussion of formal approaches to the question of identity of proofs from a philosophical standpoint. First, an introduction to the question of identity of proofs itself is given, followed by a brief reconstruction of the so-called normalisation thesis, proposed by Dag Prawitz in 1971, in which some of its core mathematical and conceptual traits are presented. After that, a comparison between the normalisation thesis and the more well-known Church-Turing thesis on computability is carried out in three main parts: the first dedicated to highlighting some of the analogies between them; the second, their most remarkable differences; and the third, to the possible relations of dependence between the two. Based on these considerations, some concluding remarks concerning the potential of the normalisation thesis and similar approaches to the question of identity of proofs are made in the last section.
References
A. Blass, N. Dershowitz, and Y. Gurevich. When are two algorithms the same? Bulletin of Symbolic Logic, 15(02) (2009), pp.145–168.
T. de Castro Alves, Synonymy and Identity of Proofs – a Philosophical Essay, doctoral dissertation, EberhardKarls-Universität Tübingen, Tübingen (2018).
A. Church, Review of Turing 1936, Journal of Symbolic Logic, 2 (1937a), pp. 42–43.
A. Church, Review of Post 1936, Journal of Symbolic Logic, 2 (1937b), p.43.
B. J. Copeland, The Church-Turing Thesis, The Stanford Encyclopedia of Philosophy (Winter 2017 Edition), Edward N. Zalta (ed.), URL = .
M. Davis (ed.), The Undecidable: Basic Papers on Undecidable Propositions, Unsolvable Problems and Computable Functions, New York: Raven (1965).
N. Dershowitz and Y. Gurevich, 2008, “A Natural Axiomatization of Computability and Proof of Church’s Thesis”, Bulletin of Symbolic Logic, 14: 299–350.
K. Došen, Identity of proofs based on normalization and generality, The Bulletin of Symbolic Logic, vol. 9 (2003), pp. 477-50.
M. Dummett, The logical basis of metaphysics. Duckworth, London (1991).
R. Gandy, The Confluence of Ideas in 1936, in R. Herken (ed.), 1988, The Universal Turing Machine: A Half-Century Survey, Oxford: Oxford University Press (1988), pp.51–102.
G. Gentzen, Untersuchungen über das logische Schließen, Math. Z. 39 (1935), pp. 176-210, 405-431 (English translation: Investigations into logical deduction, in: The Collected Papers of Gerhard Gentzen, M.E. Szabo ed., North-Holland, Amsterdam, 1969, pp. 68-131).
Y. Gurevich, “What is an algorithm?” in SOFSEM: Theory and Practice of Computer Science (eds. M. Bielikova et al.), Springer LNCS 7147 (2012), pp. 31– 42.
C.B. Jay, N.Ghani, The virtues of eta-expansion. J. Functional Programming 5 (2), Cambridge University Press (1995), pp. 135-154.
L. Kalmár, An Argument Against the Plausibility of Church’s Thesis, in A. Heyting (ed.), Constructivity in Mathematics, Amsterdam: North-Holland, (1959) pp. 72–80.
G. Kreisel, A survey of proof theory II, in: J.E. Fenstad ed., Proceedings of the Second Scandinavian Logic Symposium, North-Holland, Amsterdam (1971), pp. 109-170.
E. Mendelson, Second thoughts about Church’s thesis and mathematical proofs. The Journal of Philosophy (1990), pp. 225–233.
Y.N. Moschovakis, What Is an Algorithm?, in: Engquist B., Schmid W. (eds) Mathematics Unlimited — 2001 and Beyond. Springer, Berlin, Heidelberg (2001).
R. Péter, Rekursivität und Konstruktivität,in A. Heyting (ed.), Constructivity in Mathematics, Amsterdam: North-Holland (1959), pp. 226-233.
J. Porte, Quelques pseudo-paradoxes de la “calculabilité effective”, Actes du 2me Congrès International de Cybernetique, Namur, Belgium (1960), pp. 332-334.
E.L. Post, Finite Combinatory Processes – Formulation 1”, Journal of Symbolic Logic, 1 (1936), pp. 103–105.
D. Prawitz, Natural Deduction. A Proof-Theoretical Study. Almqvist & Wiksell: Stockholm (1965).
D. Prawitz, Ideas and results in proof theory, in: J.E. Fenstad ed., Proceedings of the Second Scandinavian Logic Symposium, North-Holland, Amsterdam (1971), pp. 235-307.
L. San Mauro, Church-Turing thesis, in practice, in: Truth, Existence and Explanation, Springer (2018), pp. 225–248.
W. Sieg, “Calculations by man and machine: Conceptual analysis”, in: W. Sieg, R. Sommer, and C. Talcott (eds), Reflections on the Foundations of Mathematics. Essays in Honor of Solomon Feferman (Lecture Notes in Logic: Volume 15), Natick, MA: Association for Symbolic Logic (2002), pp. 396–415.
W. Sieg, “Church Without Dogma: Axioms for Computability”, in B. Lowe, A. Sorbi, and B. Cooper (eds), New Computational Paradigms, New York: Springer Verlag (2008), pp. 139–152.
G. Sundholm, Identity: Absolute. Criterial. Propositional. in: Timothy Childers (ed.), The Logica Yearbook 1998, The Institute of Philosophy, Academy of Sciences of the Czech Republic, Prague, (1999) pp. 20-26.
M.H. Sørensen, P. Urzyczyn, Lectures on the CurryHoward Isomorphism, Elsevier (2006).
A.S. Troelstra, Non-extensional equality, Fund. Math. 82 (1975), pp. 307-322.
A.M. Turing, On Computable Numbers, with an Application to the Entscheidungsproblem”, Proceedings of the London Mathematical Society (Series 2), 42 (1936–37), pp. 230–265; reprinted in Copeland 2004, pp. 58–90.
A.M. Turing, Solvable and Unsolvable Problems, Science News, 31, (1954), pp. 7–23; reprinted in Copeland 2004, pp. 582–595.
A.M. Turing, “Intelligent Machinery”, National Physical Laboratory Report, (1948), in: B.J. Copeland, The Essential Turing: Seminal Writings in Computing, Logic, Philosophy, Artificial Intelligence, and Artificial Life, Oxford: Oxford University Press, 2004, pp. 410–432.
H. Wang, From Mathematics to Philosophy, New York: Humanities Press (1974). 33. F. Widebäck, Identity of Proofs, doctoral dissertation, University of Stockholm, Almqvist & Wiksell, Stockholm (2001).
This work is licensed under a Creative Commons Attribution 4.0 International License.
Copyright (c) 2020 Manuscrito: Revista Internacional de Filosofia
Downloads
