First-Order Quasi-Canonical Proof Systems

Abstract

Quasi-canonical Gentzen-type systems with dual-arity quantifiers is a wide class of proof systems. Using four-valued non-deterministic semantics, we show that every system from this class admits strong cut-elimination iff it satisfies a certain syntactic criterion of coherence. As a specific application, this result is applied to the framework of Existential Information Processing (EIP), in order to extend it from its current propositional level to the first-order one—a step which is crucial for its usefulness for handling information that comes from different sources (that might provide contradictory or incomplete information).