Analytical Tableaux for da Costa's Hierarchy of Paraconsistent Logics

In this paper we present a new hierarchy of analytical tableaux systems TNDCn,1≤n<ω, for da Costa's hierarchy of propositional paraconsistent logics Cn,1≤n<ω. In our tableaux formulation, we introduce da Costa's “ball” operator “∘”, the generalized operators “k” and “(k)”, and the negations “∼k”, for k≥1, as primitive operators, differently to what has been done in the literature, where these operators are usually defined operators. We prove a version of Cut Rule for the TNDCn,1≤n<ω, and also prove that these systems are logically equivalent to the corresponding systems Cn,1≤n<ω. The systems TNDCn constitute completely automated theorem proving systems for the systems of da Costa's hierarchy Cn,1≤n<ω.3