# 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?

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

• In my opinion you have to consider the truth table for $A$. Consider a single row corresponding to a valuation $v$ such that $v(P)=\text V$, where $\text V$ is one of the two truth values. If $v(P)=\top$, then $v(A(\top/P))=v(A)$, while if $v(P)=\bot$, then $v(A(\bot/P))=v(A)$. Thus, we have that in that line the truth value of the consequent is $v(A) \lor \text V$ where $\text V$ is an unspecified truth value. But then two cases: if $v(A)= \bot$ we have $\bot \to (v(A) \lor \text V)$ and the result will be $\top$. Commented May 18, 2023 at 6:36
• If instead we have $v(A)= \top$, we have $\top \to (\top \lor \text V)$ which is $\top$, irrespective of $\text V$. Commented May 18, 2023 at 6:36

$$\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*}$$