La sostituizone proposizionale è un meccanismo che permette di costruire nuove formule a partire da una formula data, sostituendo le due variabili proposizionali con formule arbitrarie.
Idea: date due formule $A$ e $B$, e una variabile proposizionale $p, A[H / p]$ è la formula ottenuta sostituendo simultaneamente $H$ al posto di ogni occorrenza di $p$ nella formula $A$.
Ad esempio, se $A=(p\rarr q)\lor (q\rarr p)$ e $H=p\lor r$, allora
$$ A[H/p]=(p\lor r\rarr q)\lor (q\rarr p\lor r) $$
Osservazioni:
Definizione: Siano $A$ e $H$ delle formule, e $p$ una variabile proposizionale. La formula $A[H/p]$, ottenuta sostituendo $H$ per $p$ in $A$, è definita induttivamente su $A$ nel seguente modo:
$$ A[H/p]=\begin{cases} \perp &\text{se }A=\perp \\ A &\text{se }A\in PV, A\neq p \\ H &\text{se }A=p \\ \neg (B[H/p]) &\text{se }A=\neg B \\ B[H/p]C[H/p] &\text{se }A=BC\ (*\in \{\land, \lor ,\rarr\}) \end{cases} $$
Le formule ottenute da $A$, operando delle sostituzioni, prendono il nome di istanze di $A$.
Proposizione: siano $H$ e $K$ due formule, e $v$ una valutazione tale che $v(H)=v(K)$. Allora, per ogni formula $A$ e per ogni variabile proposizionale $p$:
$$ v(A[H/p])=v(A[K/p]) $$
Corollario: siano $H$ e $K$ due formule tali che $H\equiv K$. Allora, per ogni formula $A$:
$$ A[H/p]\equiv A[K/p] $$