# Principle of propositional congruence

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!

• What is the definition of propositional formula in use here? It doesn't coincide with the standard one. Feb 1, 2015 at 14:28
• @GitGud Thank you for the comment! I've written my book's (Vincenzo Manca's "Logica matematica", 'Mathematical Logic') definition in the question. Feb 1, 2015 at 14:38
• I can't make sense of the current definition either. If one takes $\varphi =(p\lor q)\to r$, then $(p\lor q)\to r(\psi)$ is not even a well formed formula. Edit: "a formula containing propositional symbols and connectives only" all formulas respect this. Feb 1, 2015 at 14:48
• Something that would make sense to me is if $\varphi$ is a a well formed formula with exactly one propositional symbol $p$, $f$ a function defined on all formulas $\psi$ and whose output $f(\psi)$ is the formula one gets by replacing $p$ by $\psi$ in $\varphi$, and one wants to prove that for all formulas $\psi,\chi$, it holds that $$\models\psi\leftrightarrow\chi \iff \models f(\psi)\leftrightarrow f(\chi).$$ Feb 1, 2015 at 14:54
• @GitGud Thank you! As coffeemath also observes, it isn't impossible that the book contains a typo or implicitly assumes something that it doesn't state. Feb 1, 2015 at 15:08

$\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.)

• I suspect that there is a typo, or that "$\forall\varphi\quad\models\varphi(\psi)\leftrightarrow\varphi(\chi)$" is intended. Thank you very much! Feb 1, 2015 at 15:10
• @Self-teachingDavide Yes, either a typo or somewhere in the text before the equivalence was stated maybe an implied "for all $\varphi.$ Feb 1, 2015 at 15:35

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$.