In substitution, what is the word for the expression substituted in and the pattern replaced?

Question

This is just a question about terminology.

As part of a project in a mathematical logic course, I'm working through parts of Whitehead & Russell's Principia Mathematica. W & R use quite a neat notation to explain the substitutions they use to explore consequences of the axioms in the formal theory they present:

$$\left[\text{axiom}\frac{a}{b}\right]$$

where axiom is the name of the axiom being used, $a$ is the expression being introduced, and $b$ is the pattern in the axiom that is being replaced.

For example, the substitution $\displaystyle\left[\text{Taut}\frac{\sim p}{p}\right]$ means to replace $p$ with $\sim p$ in the axiom "Taut", which is $p\lor p\;.\supset.\; p$, to give us $\sim p\;\lor \sim p\;.\supset.\; \sim p$.

What is the correct word for the expression being introduced, and the pattern in the axiom that is being replaced?

Answer 1

Usually, what is stated in the question as "the expression being introduced" is called substitution instance and that stated as "the pattern in the axiom that is being replaced" is called propositional form.

It should be remarked that

• In many presentations of logical systems, this distinction is deemed as somewhat pedantic and it is not marked at all.
• There is a fine distinction between substitution and replacement, usually overlooked, but worth being noted. Briefly to state:

We replace X with Y which is of the same kind as X. For example, we replace one proposition with another proposition.

We substitute X with Y which is not of the same kind of X. For example, we substitute a variable $x$ with a constant $c$.