Abstract

We present two proof systems for first-order logic with identity and without function symbols. The first one is an extension of the Rasiowa-Sikorski system with the rules for identity. This system is a validity checker. The rules of this system preserve and reflect validity of disjunctions of their premises and conclusions. The other is a Tableau system, which is an unsatisfiability checker. Its rules preserve and reflect unsatisfiability of conjunctions of their premises and conclusions. We show that the two systems are dual to each other. The duality is expressed in a formal way which enables us to define a transformation of proofs in one of the systems into the proofs of the other.