Dual-Intuitionistic Logic

Abstract

The sequent system LDJ is formulated using the same connectives as Gentzen’s intuitionistic sequent system LJ, but is dual in the following sense: (i)whereas LJ is singular in the consequent, LDJ is singular in the antecedent; (ii)whereas LJ has thesame sentential counter-theorems as classical LK but not the same theorems, LDJ has the same sentential theorems as LK but not the same counter-theorems. In particular, LDJ does not reject all contradictions and is accordingly paraconsistent. To obtain a more precisemapping, both LJ and LDJ are extended by adding a “pseudo-difference” operator ̅ which is the dual of intuitionistic implication. Cut-elimination and decidability are provedfor the extended systems LJ ̅ and LDJ ̅, and a simply consistent but ω-inconsistent SetTheory with Unrestricted Comprehension Schema based on LDJ is sketched. © 1996 by the University of Notre Dame. All rights reserved.