Sobre a existência de semântica finita para os fragmentos da lógica intuicionista

Resumo

Em um artigo de 1932, Gödel prova que a lógica proposicional intuicionista não pode ser vista como um sistema lógico multivalorado finito. Isso é feito mostrando que não existe uma função valoração com contradomínio finito que atribua a todas as fórmulas intuicionistas deriváveis, e somente essas, um valor distinguido. O presente trabalho consiste em generalizar a prova de Gödel provando, para certos fragmentos da lógica proposicional intuicionista, se estes podem ou não serem vistos como uma lógica multivalorada finita.