Motivation. Database transactions use predicate operations (e.g., SELECT ... WHERE) to access a set of items matching a condition. Under concurrency, such operations may expose predicate anomalies that a consistency model must specify as admissible or forbidden. Yet consistency model theories that account for predicates remain inadequate. (1) Specification frameworks: the Adya lineage reasons via dependency graphs, yet these accounts stay informal (e.g., the key notion of changing matches is vague) and vary across papers; Cerone et al.'s framework offers declarative axioms for consistency models but misses predicates. (2) Characterization theorems: serializable (SER) histories without predicates can be characterized by acyclic dependency graphs, and the Adya lineage incorporates predicate edges into such graphs, but surprisingly none of them establishes a correctness argument. The graph characterization of snapshot isolation (SI) is likewise predicate-free. To our knowledge, no prior work gives an SI characterization for histories with predicates.

Contributions. (1) We present an axiomatic specification framework for consistency models with predicates, serving as a rigorous correctness criterion. (2) We provide the first formal definition of dependency graphs constructed from histories with predicates. We then propose the SER and SI characterization theorems in terms of dependency graphs, and prove them with respect to the axiomatic framework. Our theory provides rigorous foundations for consistency models with predicates, enabling history checking, protocol verification, and robustness analysis in the presence of predicates.

Approach. First, we extend the execution model with predicate reads (predicate writes are predicate reads followed by writes on matched items). To this end, we classify each predicate read in a transaction item-wise as internal or external. The key Ext-Pred axiom requires that an external predicate read on a covered item is explained by the matching write.