Relations

Abstract

Let us next look at how relations are handled in higher-order logic. Relations, like predicates, form a complete Boolean lattice and thus have essentially the same set of inference rules as predicates. We can define new operations on relations, giving additional properties. In particular, relations combine a lattice and a category structure. Relations also provide us with a more expressive way of describing state changes, where the effect can be nondeterministic in some states and undefined in other states.