previous up next
Go backward to B.5.2 Quantifier Consequences
Go up to B.5 Deriving New Knowledge
RISC-Linz logo

B.5.3 Substitutions

The equality axioms and the properties of logical equivalence allow us to draw the following conclusions.

Proposition 157 (Substitutions) For all terms S and T, formulas A and B, variables x and formula patterns C with variable F, the following holds:
Equality Subsitutions
S=T /\  A[x <- S]
A[x <- T]
Equivalence Substitutions
A <=> B /\  C[F <- A]
C[F <- B]

The substitution laws allow us to replace in a goal "terms by equal terms" and "formulas by equivalent formulas". These laws are applied when we say

We have to prove F[x <- T]. Because T=U, it suffices to prove F[x <- U].

and thus reduce a problem to an equivalent subproblem.

Author: Wolfgang Schreiner
Last Modification: October 4, 1999

previous up next