ANÁLISE CRÍTICA DA TEORIA DE TIPOS INTUICIONISTAS DE PER MARTIN LÖF
Palavras-chave:
tipos, categorias, provas, linguagem, revisão.Resumo
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
Referências
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
Publicado
Como Citar
Edição
Seção
Licença
Copyright (c) 2025 Revista Paranaense de Filosofia
Este trabalho está licenciado sob uma licenç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.
