Palavras-chave
Identidade das provas
Tese de Church-Turing
Derivação
Forma normal
Como Citar
Resumo
Este artigo é uma discussão metodológica de abordagens formais para a questão da identidade de provas de um ponto de vista filosófico. Primeiramente, é feita uma introdução à questão da identidade das próprias provas, seguida de uma breve reconstrução da chamada tese de normalização, proposta por Dag Prawitz em 1971, na qual alguns de seus traços matemáticos e conceituais centrais são apresentados. Em seguida, uma comparação entre a tese da normalização e a mais conhecida tese de Church-Turing sobre computabilidade é feita em três partes principais: a primeira dedicada a destacar algumas das analogias entre elas; o segundo, suas diferenças mais notáveis; e a terceira, às possíveis relações de dependência entre os dois. Com base nessas considerações, algumas observações finais sobre o potencial da tese de normalização e abordagens semelhantes para a questão da identidade das provas são feitas na última seção.
Referências
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).
Este trabalho está licenciado sob uma licença Creative Commons Attribution 4.0 International License.
Copyright (c) 2020 Manuscrito: Revista Internacional de Filosofia
Downloads
