Relational Logic

Relational logic is a formal system for reasoning about relations between objects, rather than properties of individual objects. Where first-order logic quantifies over individuals and their predicates, relational logic takes relations as primitive and provides operators for combining, composing, and constraining them. It is the logical foundation of Alloy and of database query languages, and it provides a natural notation for describing the structure of complex systems as networks of typed relationships.

The basic syntax of relational logic includes relational composition, union, intersection, and transitive closure. A relation R from type A to type B is a set of ordered pairs (a, b); the composition R.S is the relation that connects a to c whenever there exists a b such that (a, b) is in R and (b, c) is in S. These operations are familiar from relational algebra and from the mathematics of binary relations, but relational logic adds logical quantification and constraints that make it a specification language rather than merely a query notation.

The expressive power of relational logic is carefully calibrated. It is less expressive than first-order logic in some respects — it cannot express certain quantifier patterns directly — but it has the finite-model property: any satisfiable formula has a finite model. This property is what makes Alloy's bounded verification possible. The analyzer can search all models up to a given scope, knowing that if no counterexample exists within that scope, the property holds for all smaller models.

Relational logic is not merely a technical device for software verification. It is a formalization of how we think about structure in general. A social network is a relation between people; a food web is a relation between species; a dependency graph is a relation between software components. The ability to express constraints on these relations — transitivity, acyclicity, multiplicity bounds — is the ability to state design intentions formally, regardless of the domain.

Alloy | First-Order Logic | Relational Algebra | Formal Methods