nLab
predicate

Idea

In logic, a predicate is a statement with (potentially) a free variable in it. More specifically, a predicate in (say) the variables $x,y,z$ is a statement whose free variables may include $x$, $y$, and $z$; a predicate on (say) the types $X,Y,Z$ is a statement whose free variables may include a variable of type $X$, a variable of type $Y$, and a variable of type $Z$.

The term proposition may be used synonymously with ‘predicate’, or it may be restricted to the case when there are no free variables.

In modern logic, it's often cleaner to speak of the propositions (or predicates) that can be stated in any given context; the context specifies the free variables available.

In categorical logic

In the internal logic of a category, types are given by objects of the category predicates of type $T$ are given by subobjects $\varphi \hookrightarrow T$.

We think of $T$ as the analogue of the “set” of possible values of variables $t$ and of $\varphi$ as being the subset on those $t$ for which the statement $\varphi (t)$ is true.