Propositional substitution
= Propositional substitution
{title2=$\varphi 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.