ANÁLISE CRÍTICA DA TEORIA DE TIPOS INTUICIONISTAS DE PER MARTIN LÖF
Keywords:
tipos, categorias, provas, linguagem, revisão.Abstract
A Teoria de Tipos de Per Martin Löf é um sistema formal que combina lógica intuicionista e teoria dos tipos, com aplicações na formalização de provas matemáticas e na computação. No entanto, apesar de sua estrutura rigorosa, a teoria apresenta desafios conceituais fundamentais. Este artigo investiga a relação entre julgamento e proposição, a formalização da disjunção, a distinção entre conjuntos e categorias, e a definição intuicionista de verdade. Concluímos que a teoria necessita de revisões conceituais para garantir maior precisão e coerência em suas aplicações.
Downloads
References
AWODEY, S. “Type theory and homotopy”. In Dybjer, P.; Lindstrom, ¨ Sten; Palmgren, Erik; et al. Epistemology versus Ontology. Logic, Epistemology, and the Unity of Science. Springer. pp. 183–201. doi:10.1007/978-94-007-4435-6 9. ISBN 978-94-007-4434-9, 2012.
BISHOP, E. Foundations of constructive analysis. McGraw-Hill, 1967.
LÖF, M. Constructive Mathematics and Computer Programing. University of Stockholm, 1982.
______. An intutitionistic theory of types. University of Stockholm, 1972.
______. Intuitionistic type theory. Bibliopolis, edizioni di filosofia e scienze, Napoli, ISBN 88-7088-105-9, 1984.
______. A path from logic to metaphysics. Atti del Congresso Nuovi problemi della logica e della filosofia della scienza, 1990.
______. Verificationism Then and Now. M. van der Schaar (ed.), Judgement and the Epistemic Foundation of Logic, 3 Logic, Epistemology, and the Unity of Science 31, DOI 10.1007/978-94-007-5137-8_1, © Springer Science+Business Media Dordrecht, 2013.
______. Truth of a proposition, evidence of a judgement, validity of a proof. Synthese 73 407-420, by D. Reidel Publishing Company, 1987.
______. On the meaning of logical constants and the justifications of the logical laws. Nordic Journal of Philosophical Logic, Vol. 1, No. 1, pp. 11–60. ! Scandinavian University Press, 1996.
MINTS, G. Short introduction to intuitionistic logic. Kluwer Academic Publishers, New York, ISBN: 0-306-46975-8, 2000.
PRAWITZ, D. The fundamental problem of general proof theory. Studia Logica, https://doi.org/10.1007/s11225-018-9785-9, 2018.
RUY, J. G. B. de Queiroz, From Tractatus to Later Writings and Back. Manuscript. April 2022. (submitted for publication).
___________. de Veras, T. M. L., Ramos, A. F., de Queiroz., and de Oliveira, A. G. On the calculation of fundamental groups in homotopy type theory by means of computational paths. April 2018. https://arxiv.org/abs/1804.01413.
Downloads
Published
How to Cite
Issue
Section
License
Copyright (c) 2025 Revista Paranaense de Filosofia
This work is licensed under a Creative Commons Attribution 4.0 International License.
Artigo publicado em acesso aberto sob a licença Creative Commons Attribuition 4.0 International Licence.
Os autores cedem o direito exclusivo de primeira publicação à Revista, sendo o trabalho licenciado simultaneamente sob a licença Creative Commons Attribution 4.0 International (CC BY). Esta licença permite que terceiros remixem, adaptem e criem a partir do trabalho publicado, atribuindo o devido crédito de autoria e publicação inicial neste periódico. Os autores têm autorização para assumir contratos adicionais separadamente, para distribuição não exclusiva da versão do trabalho publicada neste periódico (por exemplo: publicar em repositório institucional, em site pessoal, publicar uma tradução ou como capítulo de livro), com reconhecimento de autoria e publicação inicial neste periódico.
