Predicate

Definition

In type theory, a predicate on types $X_0,\dots ,X_{n-1}$ is a function $P:X_0\to \cdots \to X_{n-1}\to \mathrm{Prop}.$

In classical set theory, a predicate is represented semantically as a subset $P\subseteq X_0\times \cdots \times X_{n-1}.$

Relations

A binary relation between sets $X$ and $Y$ is a predicate $R:X\to Y\to \mathrm{Prop}$. When $X=Y$, we call $R:A\to A\to \mathrm{Prop}$ a homogeneous relation on $A$.

Homogeneous relations on a set $A$ support properties such as:

• reflexivity and irreflexivity
• symmetry and asymmetry
• anti-symmetry
• transitivity

These properties combine to give structured relations such as equivalence relations, preorders, partial orders, and total orders.

Functions as Relations

A binary relation $R:X\to Y\to \mathrm{Prop}$ is a function iff it is:

• left-total: $\forall x\in X.\exists y\in Y.Rxy$
• right-unique: $\forall x\in X,y,y^{\prime }\in Y.Rxy\to Rx{y}^{\prime }\to y=y^{\prime }$

Category Pred

Define the category $\mathbf{Pred}$ as follows:

• objects are $(I,P)$ where $I:\mathrm{Set}$ and $P:I\to \mathrm{Prop}$.
• $\mathrm{Pred}[(I,P),(J,Q)]$ is given by:
  • $u:I\to J$ such that
  • $X(i)⟹Y(u(i))$ for each $i:I$

The treating each predicate as a subset, the last step could be written condition could be also be written When $\mathrm{Prop}$ is in $\mathrm{Set}$, then $\mathbf{Pred}$ can be regarded as the slice category $\mathbf{Set}/\mathrm{Prop}$.

Write ${\mathbf{Pred}}_I$ for the subcateory of categories indexed by a particular set $I$. Looked at another way, ${\mathbf{Pred}}_I$ is the category of poset of inclusion of subsets of $I$.

Related Concepts

• Reflexive Relation
• Symmetric Relation
• Transitive Relation
• Anti-Symmetric Relation
• Equivalence Relation
• Preorder
• Partial Order
• Total Ordering

Refereces

jacobs1999-categorical-logic