How would one prove that satisfaction of closed formulas is valuation-independent? (In FOL)

Consider this proposition in first-order logic:

For any interpretation $I$, any closed formula $\phi$ and any two valuations $\rho$, $\sigma$. $I\rho \models \phi \iff I\sigma \models \phi$

This is incredibly obvious yet i don't see how to prove it, the obvious induction doesn't really work since a formula is only closed when you have all the quantifiers.

You need a preliminary result, like in Herbert Enderton, A Mathematical Introduction to Logic (2nd ed - 2001), page 86 :

THEOREM 22A Assume that $$s_1$$ and $$s_2$$ are functions from $$V$$ [the set of variables] into $$|\mathfrak A|$$ [the domain of the structure] which agree at all variables (if any) that occur free in the wff $$\varphi$$.

Then

$$\mathfrak A \vDash \varphi[s_1]$$ iff $$\mathfrak A \vDash \varphi[s_2]$$.

The proof is by induction on the complexity of $$\varphi$$.

Then [page 87] :

COROLLARY 22B For a sentence $$\sigma$$, either

(a) $$\mathfrak A$$ satisfies $$\sigma$$ with every function $$s$$ from $$V$$ intto $$|\mathfrak A|$$, or

(b) $$\mathfrak A$$ does not satisfy $$\sigma$$ with any such function.

• Interesting. I did think of proving 22A. But my intuition somehow told me it didn't make sense. – Bumphe Dec 2 '14 at 19:25