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

Página do item simplificado
dc.contributor.advisor1Porto, André da Silva
dc.contributor.advisor1Latteshttp://lattes.cnpq.br/3598537464598916pt_BR
dc.contributor.referee1Porto, André da Silva
dc.contributor.referee2Filho, Abilio Azambuja Rodrigues
dc.contributor.referee3Legris, Javier
dc.contributor.referee4Pereira, Luiz Carlos Pinheiro Dias
dc.contributor.referee5Queiroz, Ruy José Guerra Barretto de
dc.creatorAlbernaz, Filipe Borges
dc.creator.Latteshttp://lattes.cnpq.br/5284099051035395pt_BR
dc.date.accessioned2022-05-10T12:14:59Z
dc.date.available2022-05-10T12:14:59Z
dc.date.issued2022-03-31
dc.description.abstractIn 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.eng
dc.description.provenanceSubmitted by Leandro Machado (leandromachado@ufg.br) on 2022-05-09T16:36:37Z No. of bitstreams: 2 Tese - Filipe Borges Albernaz - 2022.pdf: 2452545 bytes, checksum: fbf9742755bd6202e16bc30e49b49418 (MD5) license_rdf: 805 bytes, checksum: 4460e5956bc1d1639be9ae6146a50347 (MD5)en
dc.description.provenanceApproved for entry into archive by Luciana Ferreira (lucgeral@gmail.com) on 2022-05-10T12:14:58Z (GMT) No. of bitstreams: 2 Tese - Filipe Borges Albernaz - 2022.pdf: 2452545 bytes, checksum: fbf9742755bd6202e16bc30e49b49418 (MD5) license_rdf: 805 bytes, checksum: 4460e5956bc1d1639be9ae6146a50347 (MD5)en
dc.description.provenanceMade available in DSpace on 2022-05-10T12:14:59Z (GMT). No. of bitstreams: 2 Tese - Filipe Borges Albernaz - 2022.pdf: 2452545 bytes, checksum: fbf9742755bd6202e16bc30e49b49418 (MD5) license_rdf: 805 bytes, checksum: 4460e5956bc1d1639be9ae6146a50347 (MD5) Previous issue date: 2022-03-31en
dc.description.resumoEm meio a uma disputa de fundamentos filosóficos que dura mais de uma centena de anos, a fundamentação intuicionista da matemática parece cada vez mais próxima de ser uma alternativa à fundamentação clássica. Interpretação de noções fundamentais e primitivas e consequências para a interpretação dos conectivos lógicos são algumas das questões a serem tratadas neste texto, em uma estrutura que pretende mostrar o papel fundamental e primitivo da noção de construção mental no Intuicionismo, desde a proposta de Brouwer até a Teoria Intuicionista dos Tipo de Martin-Löf. A discussão dos aspectos particulares da proposta de Martin-Löf não nos permite perder de vista que ela se trata essencialmente de um sistema formal, universal, porém, aberto, mas também uma linguagem para a prática da matemática intuicionista. Essas e outras características próprias do intuicionismo formal de Martin-Löf precisaram ir além das elucidações e conceitos do intuicionismo original de Brouwer, até então, considerado como mais especulativo e pouco viável do ponto de vista prático. Justamente, o aprofundamento conceitual do sistema de Martin-Löf trouxe luz ao intuicionismo e fazem dele único e tão importante, não apenas para a matemática, mas também para a lógica, filosofia e, até mesmo, para a computação. Com uma adequada compreensão da Teoria Intuicionista dos Tipos, especialmente a partir da interpretação intuicionista fundamental de provas como construções mentais, temos uma medida mais exata de o que se trata o intuicionismo e suas principais consequências. Algumas delas tratadas neste trabalho são a recusa do princípio do terceiro excluído, a interpretação de noções como “existência”, “construção”, “proposição” e “asserção”, além do caráter construtivo compulsório para provas matemáticas formais. Em se tratando especificamente do sistema de Martin-Löf, discutimos ainda as ideias de “verdade” e “bivalência das proposições”, “domínios primitivos” e “domínios proposicionais”, imprescindíveis para o sistema e distintas das concepções clássicas, apesar da coincidência terminológica.pt_BR
dc.description.sponsorshipCoordenação de Aperfeiçoamento de Pessoal de Nível Superior - CAPESpt_BR
dc.description.sponsorshipFundação de Amparo à Pesquisa do Estado de Goiáspt_BR
dc.identifier.citationALBERNAZ, F. B. Da interpretação Bhk à teoria intuicionista dos tipos: a construção mental como conceito primitivo fundamental. 2022. 138 f. Tese (Doutorado em Filosofia) - Universidade Federal de Goiás, Goiânia, 2022.pt_BR
dc.identifier.urihttp://repositorio.bc.ufg.br/tede/handle/tede/12054
dc.languageporpt_BR
dc.publisherUniversidade Federal de Goiáspt_BR
dc.publisher.countryBrasilpt_BR
dc.publisher.departmentFaculdade de Filosofia - FAFIL (RG)pt_BR
dc.publisher.initialsUFGpt_BR
dc.publisher.programPrograma de Pós-graduação em Filosofia (FAFIL)pt_BR
dc.rightsAttribution-NonCommercial-NoDerivatives 4.0 International*
dc.rights.urihttp://creativecommons.org/licenses/by-nc-nd/4.0/*
dc.subjectFundamentos da matemáticapor
dc.subjectIntuicionismopor
dc.subjectLógica de Heytingpor
dc.subjectDedução naturalpor
dc.subjectInterpretação BHKpor
dc.subjectTeoria intuicionista dos tipospor
dc.subjectMartin-Löfpor
dc.subjectFoundations of mathematicseng
dc.subjectIntuitionismeng
dc.subjectHeyting's logiceng
dc.subjectNatural deductioneng
dc.subjectBHK interpretationeng
dc.subjectIntuitionistic type theoryeng
dc.subjectMartin-Löfeng
dc.subject.cnpqCIENCIAS HUMANAS::FILOSOFIApt_BR
dc.titleDa interpretação Bhk à teoria intuicionista dos tipos: a construção mental como conceito primitivo fundamentalpt_BR
dc.title.alternativeFrom the Bhk interpretation to the intuitionistic type theory: the mental construction as a fundamental primitive concepteng
dc.typeTesept_BR

Arquivos

Pacote Original
Agora exibindo 1 - 1 de 1
Nenhuma Miniatura disponível
Nome:
Tese - Filipe Borges Albernaz - 2022.pdf
Tamanho:
2.34 MB
Formato:
Adobe Portable Document Format
Descrição:
Baixar
Licença do Pacote
Agora exibindo 1 - 1 de 1
Nenhuma Miniatura disponível
Nome:
license.txt
Tamanho:
1.71 KB
Formato:
Item-specific license agreed upon to submission
Descrição:
Baixar

Coleções

Doutorado em Filosofia (FAFIL)