Propositional Substitution

Propositional substitution is a logical substitution in predicate logic involves replacing every instance of one or more atom with propositions:

Definition §

Propositional Substitution ^definition

A propositional substitution, $\theta$, is a logical substitution in propositional logic that maps atoms to propositions (which can also be atoms)

$$\theta :\{P,Q,R,\dots \}\to \phi$$

• $\{P,Q,\dots \}$ represents the set of all atoms
• $\phi$ represents any proposition

Conventionally, we tend to use $[P:=Q]$ to show a propositional substitution from $P$ to $Q$.

Examples §

For example, take the formula:

$$\neg (P\wedge Q)$$

We can convert this to a disjunction by substituting $P$ with $\neg P$ and $Q$ with $\neg Q$:

$$\phi [P:=\neg P,Q:=\neg Q]=\neg (\neg P\wedge \neg Q)$$

which is logically equivalent to a disjunction.

$$\neg (\neg P\wedge \neg Q)\equiv (\neg \neg P\vee \neg \neg Q)\equiv (P\vee Q)$$

Theorems §

T1: Propositional Substitution preserves validity

That is, a proposition $P$ that is valid will remain valid after any propositional substitution $\theta$

$$\text{If P is valid, then P[θ] is valid}$$

$$\models P⟹\models P[\theta ]$$

C1: Propositional Substitution preserves unsatisfiability

That is, a proposition $P$ that is unsatisfiable will remain so after any valid substitution $\theta$

$$\text{If P is unsatisfiable, then P[θ] is unsatisfiable}$$

$$/\models P⟹/\models P[\theta ]$$

Proof theorem 1 by #TODO

This can be proved from

T2: Propositional substitution preserves logical equivalence

If we have two propositions $F$ and $G$ that are logically equivalent, then any substitution $\theta$ applied on both formulae preserves this equivalence:

$$\text{If }F\equiv G,\text{ then }F[\theta ]\equiv G[\theta ]$$

T3: Propositionally Substituting equivalences preserves all semantic properties ^t3

If $\theta =\{F\mapsto G\}$ where $F$ and $G$ are logically equivalent, then:

$$H\equiv H[\theta ]$$

That is, if we replace part of a formula with any equivalent part, that formula’s semantics is unchanged.