O Método dos Tableaux Aplicado ao Cálculo Trivalente e Intuicionista I1

Abstract

O cálculo I¹ foi introduzido em 1995 por Sette e Carnielli. Este sistema possui 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 Intuicionista, ou construtivista, por exemplo, ¬ ¬A → A não ser uma tautologia em I¹. Ademais, o cálculo I¹ é 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 ambiente semântico dessa lógica, há apenas um valor distinguido. Neste trabalho, desenvolvemos um método dedutivo alternativo ao axiomático para o sistema I¹, ou seja, introduzimos um sistema de tableaux analíticos para tal lógica. Estabelecemos, por meio de teoremas, que toda dedução obtida do sistema axiomático também será deduzida pelo sistema de tableaux proposto.