A Sequent Calculus for Satisfiability and Validity

This paper presents a new sequent calculus that integrates rules for testing both satisfiability and validity within the same logical system. Its notion of deduction encompasses both nonlogical and logical assumptions. A formula is considered consistent when it has a certain deduction from nonlogical assumptions, and it is considered provable if there is a certain deduction for it from logical assumptions. The equivalences between provability and validity, as well as between consistency and satisfiability, are proved. All the structural rules are admissible, and extensions with nonlogical rules are shown to overcome Post-completeness.