= Uniform substitution in modal logic
<Uniform substitution in modal logic> replaces each occurrence of a <first-order sentence> letter by the same <modal formula>. Normal modal <formal proof> systems with axiom schemes are closed under this operation: substituted axioms remain instances, modus ponens is preserved, and necessitation commutes with substitution. Fresh auxiliary letters permit substituting a derived fixed point into fixed-point uniqueness theorems without changing other parameters.
Back to article page
