Definition 26: Let x and y be variables. We recursively define when x is said to be freely substitutable for y in a statement:
(a) Base cases: x is freely substitutable for y in a membership statement.
(b) Recursion: If x is freely substitutable for y in both of \phi and \psi , then so is it in the conjunction (\phi \wedge \psi) .
(c) Recursion: If x is freely substitutable for y in \phi , then so is it in the negation \neg \phi .
(d) Recursion: For a variable z distinct from y , if x is freely substitutable for y in \phi , then so is it in the existence statement \exists z \phi .