How to define substitution using ZFC

Question

One question I've had regarding ZFC is how to define substitution. I cannot see how it's possible, despite the frequent use of substitution within both pure and applied mathematics.

Just to be clear, I define substitution as follows: for all well-defined mathematical objects $a$ and $b$ that are equal, and any function $f$ such that $f(a)$ and $f(b)$ are well-defined, $f(a) = f(b)$. $$ \forall a \forall b \forall f [(a = b \, \wedge f(a),f(b) \text{ are defined}) \Rightarrow f(a) = f(b)]$$

Any ideas?

Answer 1

Substitution is "governed" by the axioms for equality.

We can substitute equals into a formula $\varphi$ :

$a = b → (φ[a/x] → φ[b/x])$, for any formula $φ(x)$,

or we can substitute into a function $f$ :

$a=b \to f(\ldots,a,\ldots) = f(\ldots,b,\ldots)$, for any function symbol $f$.

Example in $\mathsf {ZF}$, using the formula $(z \in x)$ as $φ(x)$ :

$a = b \to ((z \in a) \to (z \in b))$.

Answer 2

You can actually formulate ZFC in FOL without equality: with extensionality reading

$ \forall z ( z \in x \iff z \in y ) \implies \forall z ( x \in z \iff y \in z ) $

define a binary predicate to mean the consequent in the last sentence

$ xRy :\iff \forall z ( x \in z \iff y \in z ) $

reflexivity, transitivity and symmetry following easily from FOL alone; and then with the usual comprehension/separation scheme and weak-pair

$ \forall x \exists y\forall z(z \in y \iff z \in x \wedge \varphi) $

$ \forall x \forall y \exists z (x \in z \ \wedge \ y \in z) $

prove substitution for $ R $, ie:

$ xRy \implies (\varphi x \iff \varphi y) $