UMA ABORDAGEM SOBRE A CONCEPÇÃO DE PROPOSIÇÃO DA TEORIA INTUICIONISTA DE TIPOS

A TEORIA INTUICIONISTA DE TIPOS, DE MARTIN-LÖF, ALEGA, À LUZ DA CORRESPONDÊNCIA CURRY- HOWARD, QUE DEFINIR UMA PROPOSIÇÃO POR MEIO DO ESTABELECIMENTO DE COMO AS SUAS PROVAS CANÔNICAS SÃO FORMADAS É O MESMO QUE DEFINIR UM CONJUNTO POR MEIO DO ESTABELECIMENTO DE COMO OS SEUS ELEMENTOS CANÔNICOS SÃO FORMADOS, FAZENDO COM QUE UMA PROPOSIÇÃO POSSA SER VISTA COMO O CONJUNTO DE SUAS PROVAS. POR OUTRO LADO, ENCONTRAMOS NESSA MESMA TEORIA UMA DISTINÇÃO ENTRE AS NOÇÕES DE CONJUNTO E TIPO, SENDO QUE A DIFERENÇA DESTE EM RELAÇÃO ÀQUELE CON- SISTE NO FATO DE QUE PARA SE FORMAR UM TIPO NÃO É PRECISO APRESENTAR UMA PRESCRIÇÃO EXAUSTIVA DA FORMAÇÃO DE SEUS OBJETOS, BASTA SE TER UMA NOÇÃO GERAL DO QUE SERIA UM OBJETO ARBITRÁRIO QUE O HABITA. TENDO ISSO EM CONTA, ARGUMENTAMOS QUE PODEMOS EXTRAIR DA TEORIA INTUICIONISTA DE TIPOS DUAS CONCEPÇÕES DE PROPOSIÇÃO DISTINTAS, UMA QUE CONSIDERA PROPOSIÇÕES COMO TIPOS E OUTRA QUE CONSIDERA PROPOSIÇÕES COMO CONJUNTOS. TAL DISTINÇÃO IMPLICARÁ EM ALGUMAS CONSIDERAÇÕES ENVOLVENDO QUESTÕES SOBRE DEMONSTRAÇÕES HIPOTÉTICAS E A FORMAÇÃO DE CONJECTURAS.