Propositional variable elimination
= Propositional variable elimination
{title2=$A\equiv(A[p:=\top]\wedge p)\vee(A[p:=\bot]\wedge\neg p)$}
The displayed identity follows by testing the two possible truth values of $p$. Existentially forgetting $p$ gives $A[p:=\top]\vee A[p:=\bot]$. Repeating this operation produces a <propositional formula> on a specified remaining vocabulary. Logical truth constants are needed if that vocabulary is empty.