ANÁLISE CRÍTICA DA TEORIA DE TIPOS INTUICIONISTAS DE PER MARTIN LÖF
Palabras clave:
tipos, categorias, provas, linguagem, revisão.Resumen
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.
Descargas
Citas
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.
Descargas
Publicado
Cómo citar
Número
Sección
Licencia
Derechos de autor 2025 Revista Paranaense de Filosofia
Esta obra está bajo una licencia internacional Creative Commons Atribución 4.0.
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.
