Hierarquias de sistemas de dedução natural e de sistemas de tableaux analíticos para os sistemas Cn de da Costa

Neste trabalho, introduzimos a hierarquia de sistemas proposicionais de dedução natural DNCn, 1£n£w, e a hierarquia de sistemas quantificacionais de dedução natural DNCn*, 1£n£w. Demonstramos que cada um dos sistemas das hierarquias é equivalente aos sistemas correspondentes da hierarquia de cálculos proposicionais paraconsistentes Cn, 1£n£w, e de cálculos quantificacionais paraconsistentes Cn*, 1£n£w, de da Costa. Demonstramos um Teorema de Normalização, à la Fitch, e uma Propriedade de Subfórmula para os sistemas DNCn e DNCn*, 1£n£w. .Introduzimos a hierarquia de sistemas de tableaux analíticos TNDCn, 1£n<w, nos quais o operador """"o"""" (""""bola""""), os operadores generalizados """"k"""" e """"(k)"""", 1£k, e as negações """"~k"""", k³1, de da Costa são operadores primitivos, diferentemente do que tem sido apresentado na literatura, onde esses operadores são usualmente definidos. Demonstramos uma versão da Regra do Corte para esses sistemas e demonstramos que cada um deles é equivalente ao correspondente sistema Cn, 1£n<w. Os sistemas TNDCn constituem provadores automáticos de teoremas para os sistemas da hierarquia Cn, 1£n<w, de Costa.