= Term-value formula in relational coding
{title2=$E_t(z)$}
= Term-value formulas in relational coding
{synonym}
After replacing functions by graph predicates and constants by <singleton> predicates, $E_t(z)$ says that $z$ is the value of a term $t$. For a unary <function graph> $P$ and constant predicate $Q$, use $E_x(z)=(z=x)$, $E_c(z)=Q(z)$ and $E_{f(t)}(z)=\exists y(E_t(y)\land P(y,z))$. Fresh witnesses avoid variable capture. Totality and uniqueness axioms make each value formula have exactly one witness under every assignment.
Back to article page
