Sobre a adequação em tableaux para o sistema I

Abstract

O sistema I 1 foi introduzido em 1995 por Sette e Carnielli. Este sistema apresenta um caráter intuicionista, no mesmo sentido do sistema lógico desenvolvido por Arend Heyting (1898-1980), o qual surgiu como a lógica subjacente a matemática construtivista, por exemplo, ¬¬A → A não é uma tautologia em I 1 . Ademais, o sistema I 1 é uma lógica trivalorada que, ao contrário da lógica clássica, não admite apenas dois valores de verdade, mas sim três, estes são T, F ∗ e F. Os valores T e F denotam, respectivamente, verdade e falsidade, enquanto que F ∗ pode ser interpretado como “falsidade por falta de evidência positiva”. O objetivo deste trabalho é desenvolver um método dedutivo alternativo ao axiomático para a lógica intuicionista I 1 , propõe-se aqui, então, apresentar um sistema de tableaux analı́ticos para tal lógica e esboçar os caminhos para a adequação dedutiva entre os sistemas, explicitando os teoremas necessários para que toda dedução obtida em tableau, também seja deduzida no sistema axiomático original de I 1 . [...]