For any formula $A$ and atom $P$, $\vDash A \rightarrow \left(A\left(\top / P\right) \vee A\left(\bot / P\right)\right)$ in propositional logic?

Question

$\newcommand{\true}{\operatorname{true}}$ $\newcommand{\false}{\operatorname{false}}$ $\newcommand{\atoms}[1]{\mathscr{A}\left(#1\right)}$

In propositional logic, we seem to have the following statement: for any formula $A$ and atom $P$, $\vDash A \rightarrow \left(A\left(\top / P\right) \vee A\left(\bot / P\right)\right)$, where $\top$ and $\bot$ are atoms such that for any truth assignment $\tau$, $\tau\left(\top\right) = \true$ and $\tau\left(\bot\right) = \false$, and $A\left(\top / P\right)$ denotes the result from replacing every occurrence of $P$ by $\top$ in $A$. But I am having difficulty proving it. My proof goes as follows.

Let $\atoms{\cdot}$ denote the set of atoms in a formula. The case where $P \not\in \atoms{A}$ is trivial. We wish to prove the following statement: for any formula $A$, for any atom $P \in \atoms{A}$, $\vDash A \rightarrow \left(A \left(\top / P\right) \vee A \left(\bot / P\right)\right)$. I wish to prove the statement using structural induction.

First assume that $Q$ is an atom. It is our wish to prove that for any atom $P$, if $P \in \atoms{Q}$, then $\vDash Q \rightarrow \left(Q \left(\top / P\right) \vee Q \left(\bot / P\right)\right)$. Let $P$ be an atom such that $P \in \atoms{Q}$. Then we have \begin{equation*} P \equiv Q. \end{equation*} As a result, we have \begin{equation*} Q\left(\top / P\right) \equiv \top \end{equation*} and \begin{equation*} Q\left(\bot / P\right) \equiv \bot. \end{equation*} It is obvious that \begin{equation*} \vDash Q \rightarrow \left(\top \vee \bot\right). \end{equation*}

Next, assume that $A$ is a formula such that for any atom $P \in \atoms{A}$, $\vDash A \rightarrow \left(A \left(\top / P\right) \vee A \left(\bot / P\right)\right)$. We wish to prove that for any atom $P \in \atoms{\neg A}$, $\vDash \neg A \rightarrow \left(\neg A \left(\top / P\right) \vee \neg A \left(\bot / P\right)\right)$. Let $P \in \atoms{\neg A}$. Immediately we have $P \in \atoms{A}$. Then $\vDash A \rightarrow \left(A \left(\top / P\right) \vee A \left(\bot / P\right)\right)$, and thus, we have $\vDash \neg A \vee A \left(\top / P\right) \vee A \left(\bot / P\right)$. Thus, for any truth assignment $\tau$, either $\tau\left(A\right) = \false$ or $\tau\left(A\left(\top / P\right)\right) = \true$ or $\tau\left(A\left(\bot / P\right)\right) = \true$. Further, we have \begin{equation*} \neg A \left(\top / P\right) \equiv \neg \left( A \left(\top / P\right)\right) \end{equation*} and \begin{equation*} \neg A \left(\bot / P\right) \equiv \neg \left( A \left(\bot / P\right)\right). \end{equation*} As a result, \begin{equation*} \left(\neg A \left(\top / P\right) \vee \neg A \left(\bot / P\right)\right) \Leftrightarrow \neg \left(A\left(\top / P\right) \wedge A\left(\bot / P\right)\right). \end{equation*} Thus, it is our wish to prove that \begin{equation*} \vDash A \vee \neg \left(A\left(\top / P\right) \wedge A\left(\bot / P\right)\right). \end{equation*} Then I cannot proceed. Further, assume that $\tau$ is an assignment such that $\tau\left(A\right) = \false$ and $\tau\left(A\left(\top / P\right)\right) = \true$ and $\tau\left(A\left(\bot / P\right)\right) = \true$. Then we have $\tau\left(A \vee \neg \left(A\left(\top / P\right) \wedge A\left(\bot / P\right)\right)\right) = \false$. Seems that we cannot deal with the case of $\neg A$ in structural induction.

Answer 1

$\newcommand{\true}{\operatorname{true}}$ $\newcommand{\false}{\operatorname{false}}$ $\newcommand{\atoms}[1]{\mathscr{A}\left(#1\right)}$

Thanks to Mauro's remind, I developed the following answer.

To prove the theorem in the title, we need to prove the following cases:

(1) For any formula $A$, for any atom $P$, for any assignment $\tau$, if $\tau\left(P\right) = \true$, then $\tau\left(A\left(\top / P\right)\right) = \tau\left(A\right)$;

(2) For any formula $A$, for any atom $P$, for any assignment $\tau$, if $\tau\left(P\right) = \false$, then $\tau\left(A\left(\bot / P\right)\right) = \tau\left(A\right)$.

We prove (1) only and (2) should follow from (1).

It is trivial to show the case where $P \not\in \atoms{A}$. From now on, assume $P \in \atoms{A}$. Thus, it is our desire to prove the following statement: for any formula $A$, for any atom $P \in \atoms{A}$, for any assignment $\tau$, if $\tau\left(P\right) = \true$, then $\tau\left(A\left(\top / P\right)\right) = \tau\left(A\right)$.

First let $Q$ be an atom and $P \in \atoms{Q}$. Immediately we have \begin{equation*} P \equiv Q. \end{equation*} Let $\tau$ be an assignment such that $\tau\left(P\right) = \true$. Then $\tau\left(Q\right) = \true$. Then \begin{equation*} Q\left(\top / P\right) \equiv \top. \end{equation*} and thus, \begin{equation*} \tau\left(Q\left(\top / P\right)\right) = \tau\left(\top\right) = \true. \end{equation*} Consequently, we have \begin{equation*} \tau\left(Q\left(\top / P\right)\right) = \tau\left(Q\right). \end{equation*}

Next, let $A$ be a formula such that for any $P \in \atoms{A}$, for any assignment $\tau$, if $\tau\left(P\right) = \true$, then $\tau\left(A\left(\top / P\right)\right) = \tau\left(A\right)$. Now consider $\neg A$. Let $P \in \atoms{\neg A}$ and $\tau\left(P\right) = \true$. Clearly, we have \begin{equation*} P \in \atoms{A}. \end{equation*} Then we have \begin{equation*} \tau\left(A\left(\top / P\right)\right) = \tau\left(A\right). \end{equation*} It is then clear that \begin{equation*} \tau\left(\neg\left(A\left(\top / P\right)\right)\right) = \tau\left(\neg A\right). \end{equation*} Further, as \begin{equation*} \left(\neg A\right)\left(\top / P\right) \equiv \neg \left(A \left(\top / P\right)\right), \end{equation*} we have \begin{equation*} \tau\left(\left(\neg A\right)\left(\top / P\right)\right) = \tau\left(\neg\left(A\left(\top / P\right)\right)\right) = \tau\left(\neg A\right). \end{equation*}

Further, assume that $A$ and $B$ are formulae such that (1) for any $P \in \atoms{A}$, for any assignment $\tau$, if $\tau\left(P\right) = \true$, then $\tau\left(A\left(\top / P\right)\right) = \tau\left(A\right)$; (2) for any $P \in \atoms{B}$, for any assignment $\tau$, if $\tau\left(P\right) = \true$, then $\tau\left(B\left(\top / P\right)\right) = \tau\left(B\right)$. Now consider $\left(A \vee B\right)$. Let $P \in \atoms{A \vee B}$ and $\tau\left(P\right) = \true$. Then either $P \in \atoms{A}$ or $P \in \atoms{B}$. Let $P \in \atoms{A}$. Then we have \begin{equation*} \tau\left(A\left(\top / P\right)\right) = \tau\left(A\right). \end{equation*} Clearly, \begin{equation*} \left(A \vee B\right)\left(\top / P\right) \equiv \left(A\left(\top / P\right) \vee B\left(\top / P\right)\right). \end{equation*} We have two cases to consider: $P \in \atoms{B}$ and $P \not\in \atoms{B}$. First let $P \in \atoms{B}$. Then we have \begin{equation*} \tau\left(B\left(\top / P\right)\right) = \tau\left(B\right). \end{equation*} Then we have \begin{equation*} \tau\left(\left(A \vee B\right)\left(\top / P\right)\right) = \tau\left(A\left(\top / P\right) \vee B\left(\top / P\right)\right) = \tau\left(A \vee B\right). \end{equation*} Next, let $P \not\in \atoms{B}$. In this case, \begin{equation*} B\left(\top / P\right) \equiv B. \end{equation*} Then \begin{equation*} \tau\left(B\left(\top / P\right)\right) = \tau\left(B\right). \end{equation*} Thus, \begin{equation*} \tau\left(\left(A \vee B\right)\left(\top / P\right)\right) = \tau\left(A\left(\top / P\right) \vee B\left(\top / P\right)\right) = \tau\left(A \vee B\right). \end{equation*} The case for $P \in \atoms{B}$ uses the same reasoning.

Finally, assume that $A$ and $B$ are formulae such that (1) for any $P \in \atoms{A}$, for any assignment $\tau$, if $\tau\left(P\right) = \true$, then $\tau\left(A\left(\top / P\right)\right) = \tau\left(A\right)$; (2) for any $P \in \atoms{B}$, for any assignment $\tau$, if $\tau\left(P\right) = \true$, then $\tau\left(B\left(\top / P\right)\right) = \tau\left(B\right)$. Consider $\left(A \wedge B\right)$. Let $P \in \left(A \wedge B\right)$ and $\tau\left(P\right) = \true$. Then we have \begin{equation*} P \in \atoms{A} \end{equation*} or \begin{equation*} P \in \atoms{B}. \end{equation*} Assume $P \in \atoms{A}$. Under this assumption, we have \begin{equation*} \tau\left(A\left(\top / P\right)\right) = \tau\left(A\right). \end{equation*} We have two cases to consider for $B$: $P \in \atoms{B}$ and $P \not\in \atoms{B}$. First let $P \in \atoms{B}$. Then \begin{equation*} \tau\left(B\left(\top / P\right)\right) = \tau\left(B\right). \end{equation*} Further, \begin{equation*} \tau\left(\left(A \wedge B\right)\left(\top / P\right)\right) = \tau\left(A\left(\top / P\right) \wedge B\left(\top / P\right)\right) = \tau\left(A \wedge B\right). \end{equation*} Next, let $P \not\in \atoms{B}$. In this case, \begin{equation*} B\left(\top / P\right) \equiv B. \end{equation*} Then we have \begin{equation*} \tau\left(\left(A \wedge B\right)\left(\top / P\right)\right) = \tau\left(A\left(\top / P\right) \wedge B\left(\top / P\right)\right) = \tau\left(A \wedge B\right). \end{equation*}