LOGIC Course

Replacement & Equivalences


In semantic proofs, you have the right to replace a propositional variable with any formula. More precisely :

  • $p[p:=G]=G$
  • $q[p:=G]=G$ with $p \neq q$
  • $(F_1\diamond F_2[p:=G])=(F_1[p:=G])\diamond (F_2[p:=G])$ with $\diamond \in {\wedge, \vee, \Rightarrow}$
  • $(\neg F)[p:=G]=\neg(F[p:=G])$

From there, you have some additionnal rules (including all the equivalences presented in the bottom) :

  • If $\models F$ then $\models F[p:=G]$
  • If $F\equiv F'$ then $F[p:=G] \equiv F'[p:=G]$
  • If $G\equiv G'$ then $F[p:=G] \equiv F[p:=G']$


@F \wedge F \equiv F@ @F \vee F \equiv F@
@F \wedge G \equiv G \wedge F@ @F \vee G \equiv G \vee F@
@F \wedge (G \wedge H) \equiv (F \wedge G) \wedge H@ @F \vee (G \vee H) \equiv (F \vee G) \vee H@
@F \wedge (G \vee H) \equiv (F \wedge G) \vee (F \wedge H)@ @F \vee (G \wedge H) \equiv (F \vee G) \wedge (F \vee H)@
@\neg (F \wedge G) \equiv \neg F \vee \neg G@ @\neg (F \vee G) \equiv \neg F \wedge \neg G@
@F \Rightarrow G \equiv \neg F \vee G@ @\neg (F \Rightarrow G) \equiv F \wedge \neg G@
@\bot \wedge F \equiv \bot@ @\bot \vee F \equiv F@
@\neg \neg F \equiv F@