Da interpretação Bhk à teoria intuicionista dos tipos: a construção mental como conceito primitivo fundamental

• Ano de defesa: 2022
• Autor(a) principal: Albernaz, Filipe Borges
• Orientador(a): Porto, André da Silva
• Banca de defesa: Porto, André da Silva, Filho, Abilio Azambuja Rodrigues, Legris, Javier, Pereira, Luiz Carlos Pinheiro Dias, Queiroz, Ruy José Guerra Barretto de
• Tipo de documento: Tese
• Tipo de acesso: Acesso aberto
• Idioma: por
• Instituição de defesa: Universidade Federal de Goiás
• Programa de Pós-Graduação: Programa de Pós-graduação em Filosofia (FAFIL)
• Departamento: Faculdade de Filosofia - FAFIL (RG)
• País: Brasil
• Palavras-chave em Português: Fundamentos da matemática; Intuicionismo; Lógica de Heyting; Dedução natural; Interpretação BHK; Teoria intuicionista dos tipos; Martin-Löf
• Palavras-chave em Inglês: Foundations of mathematics; Intuitionism; Heyting's logic; Natural deduction; BHK interpretation; Intuitionistic type theory; Martin-Löf
• Área do conhecimento CNPq: CIENCIAS HUMANAS::FILOSOFIA
• Link de acesso: http://repositorio.bc.ufg.br/tede/handle/tede/12054

In the midst of a dispute over philosophical foundations that has lasted for over a hundred years, the intuitionistic foundations of mathematics seems ever closer to being an alternative to classical foundation. Interpretation of fundamental and primitive notions and consequences for the interpretation of logical connectives are some of the issues to be addressed in this text, in a framework that intends to show the fundamental and primitive role of the notion of mental construction in Intuitionism, from Brouwer's proposal to Martin-Löf's Intuitionistic Type Theory. The discussion of particular aspects of the Martin-Löf’s proposal does not allow us to lose sight of the fact that it is essentially a formal system, universal, however, open, but also a language for the practice of intuitionist mathematics. These and other characteristics of Martin-Löf’s formal intuitionism needed to go beyond the definitions and concepts of Brouwer's original intuitionism, until then, considered as more speculative and impractical from a practical point of view. Precisely, the conceptual deepening of the Martin-Löf’s system brought light to intuitionism and make it unique and so important, not only for mathematics, but also for logic, philosophy and even for computation. With an adequate understanding of the Intuitionistic Type Theory, especially from the fundamental intuitionist interpretation of proofs as mental constructions, we have a more accurate measure of what intuitionism is about and its main consequences. Some of them dealt with in this work are the refusal of the law of excluded middle, the interpretation of notions such as “existence”, “construction”, “proposition” and “assertion”, in addition to the compulsory constructive character for formal mathematical proofs. In the specific case of the Martin-Löf’s system, we also discuss the ideas of truth and bivalence of propositions, primitive domains and propositional domains, essential for the system and distinct from classical conceptions, despite the terminological coincidence.