DA INTERPRETAÇÃO BHK À TEORIA INTUICIONISTA DOS TIPOS: A CONSTRUÇÃO MENTAL COMO CONCEITO PRIMITIVO FUNDAMENTAL

EM 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. PALAVRAS-CHAVE: FUNDAMENTOS DA MATEMÁTICA, INTUICIONISMO, LÓGICA DE HEYTING, DEDUÇÃO NATURAL, INTERPRETAÇÃO BHK, TEORIA INTUICIONISTA DOS TIPOS, MARTIN-LÖF.