Propositional substitution ($\phi S$)

A propositional substitution maps each atomic propositional variable to a propositional formula and extends recursively through every logical connective. Replacements are simultaneous: a variable appearing inside a replacement formula is not replaced again in the same substitution step. Since propositional logic has no variable-binding quantifiers, this operation has no variable-capture problem.