substitution lemmas for first order logic

324 Views Asked by At

How can i prove $ \text{$\models$}_{\Sigma} ((\forall x \ \varphi ) \ \Leftrightarrow \ (\forall y \ [\varphi]_{y}^{x}))$.

Being $ \Sigma $ a signature, $ \varphi$ a formula, and $ [\varphi]_{y}^{x} $ the subsistution of $ x$ by $ y $.

When $ y$ is not in the free variables of $ \varphi$ and $y \triangleright_{\Sigma} x : \varphi$, which means that $x$ is free for $y$ in $ \varphi $

In my opinion i would have to use the substitution's lemma or the one of the hidden variables but i just can't seem to find a way to prove it.