Pc-Compactness, a Necessary Condition for the Existence of Sound and Complete Logics of Partial Correctness

摘要

If a structure has a complete Hoare's logic then its first-order theory must be PC-compact (each asserted program true in all of its models is already implied by a finite subset of the theory); moreover its partial correctness theory must be decidable relative to this first-order theory. An example is given of a structure statisfying both conditions, on which Hoare's logic is incomplete but which does possess a sound and complete logic of partial correctness. Transformation of two-sorted structures into single-sorted ones is used.