Proposition 26: Let x and y be variables, and \phi a statement. Recall the usual notation for universal statements.
(a) The variable substitution [\forall x \phi | x \to y] is given by \forall x \phi .
(b) Given a variable z from which x is distinct, [\forall z \phi | x \to y] is given by \forall z [\phi | x \to y].

Proof: Recall the usual notation for negation and existential quantification. We note that since \forall w \phi is short for \neg \exists w \neg \phi , we get by (g) in the definition of substitution that [\forall w \phi | x \to y] is the same as \neg [\exists w \neg \phi | x \to y] , for any w .

(a): By (e) in the definition of substitution, [\exists x \neg \phi | x \to y] is \exists x \neg \phi , hence by the above our statement is the same as \neg \exists x \neg \phi , for which \forall x \phi is short.

(b): Since z is distinct from x , we get by (h) in the definition and the above note that [\forall z \phi | x \to y] is the same as \neg \exists z [\neg \phi | x \to y] ; this is again, by (g) in the definition, the same as \neg \exists \neg [\phi | z \to y] , i.e. \forall z [\phi | x \to y] . \square