Fuente TeX:

y \not\in FV(\{P_1(x), (\forall w)(P_1(w)\to(\forall z)\neg P_2(w,z)), \bot\})