Completeness of the First-Order Logic of Partial Quasiary Predicates with the Complement Composition

Abstract

Partial quasiary predicates are used in programming for representing program semantics and in logic for formalizing predicates over partial variable assignments. Such predicates do not have fixed arity therefore they may be treated as mappings over partial data. Obtained logics are not expressive enough to construct sound axiomatic systems of Floyd--Hoare type. To increase expressibility of such logics, oriented on quasiary predicates, we extend their language with the complement operation (composition). In the paper we define one of such logics called first-order logic of partial quasiary predicates with the complement composition. For this logic a special consequence relation called irrefutability consequence relation under undefinedness conditions is introduced. We study its properties, construct a sequent calculus for it and prove soundness and completeness of this calculus.

Keywords

• partial predicate
• quasiary predicate
• program logic
• predicate logic
• soundness and completeness