Principle of propositional congruence

Question

Let $\varphi$ be a propositional formula, defined as a formula containing propositional symbols and connectives only, and let $\psi,\chi$ be propositions. I read the following principle of propositional congruence:$$\models\psi\leftrightarrow\chi\quad\iff\quad\models\varphi(\psi)\leftrightarrow\varphi(\chi)$$where $\models$ means validity in every model.

If $\psi$ is equivalent to $\chi$, substituting each other in a propositional formula produce equivalent propositions, of course, therefore I understand the $\Rightarrow$ implication.

But how do wee see how $\models\varphi(\psi)\leftrightarrow\varphi(\chi)$ implies $ \models\psi\leftrightarrow\chi$? Thank you very much for any answer!

Answer 1

$\varphi(\psi) \leftrightarrow \varphi(\chi)$ could hold in the specific case wherein $\varphi(u)$ is false for all $u,$ and then one could not get $\models \psi \leftrightarrow \chi$ from $\models \varphi(\psi) \leftrightarrow \varphi(\chi)$ for the case of this specific choice of $\varphi.$ To make the converse work, it would have to be assumed that the right side was true for all choices of $\varphi.$ Once that is done, just choose $\varphi(x)=x$ i.e. the propositional formula that returns the given formula input to it. (Is that called the "identity propositional formula"? I don't know the right terminology.)

Answer 2

I suppose that $\varphi(\psi)$ abbreviates $\varphi[\psi / p_i]$, the result of substituting all occurrences of the propositional letter $p_i$ by the formula $\psi$. This notion can be defined recursively as follows (assuming we're working in a language of classical propositional logic):

$\varphi[\psi / p_i] = \begin{cases} \varphi & \text{, if $\varphi$ is atomic and $\varphi \not = p_i$};\\ \psi & \text{, if $\varphi = p_i$} \end{cases}$

$(\varphi ~\Box~ \chi) [\psi / p_i] = \varphi[\psi / p_i] ~\Box~ \chi [\psi / p_i]$ (where $\Box$ is some 2-place connective).

$(\neg \varphi)[\psi / p_i] = \neg \varphi[\psi / p_i]$

Now I may be deeply wrong, but I think the $\Leftarrow$ implication is simply wrong. For $\models p \lor \neg p = (q \lor \neg q) [p / q], \models \neg p \lor \neg \neg p = (q \lor \neg q) [\neg p / q]$, but $\not \models p \leftrightarrow \neg p$.