Insertion rule (logic)

The rule of substitution or dissipation through substitution is a rule of inference many logical calculations to derive which allows a set (a universal statement) further and to find equivalent statements to a statement:

Propositional logic

Be a general statement that includes the partial expression . If every occurrence of in is replaced by another expression , the result is a general statement. ${\displaystyle a}$ ${\displaystyle t}$ ${\displaystyle t}$ ${\displaystyle a}$ ${\displaystyle s}$

Example :

The general statement is given . If you replace through , then what can be transformed results as a new, generally valid statement. ${\displaystyle (p\vee \neg p)}$ ${\displaystyle p}$ ${\displaystyle (p\wedge q)}$ ${\displaystyle (p\wedge q)\vee \neg (p\wedge q)}$ ${\displaystyle ((p\wedge q)\vee \neg p\vee \neg q)}$

Application :

This rule can be used to transform expressions into simpler, equivalent ones.

If it is any expression, a partial expression contained in it can be replaced ( substituted ) by a new variable . If the resulting expression is converted equivalent according to other rules and the substitution is finally reversed, the result is a statement that is equivalent to the original expression. ${\displaystyle a}$

Example:

${\displaystyle (p\rightarrow (\neg p\wedge (q\vee p)))\wedge p}$

Now substitute with s and get ${\displaystyle (\neg p\wedge (q\vee p))}$

${\displaystyle (p\rightarrow s)\wedge p}$

${\displaystyle \leftrightarrow (\neg p\vee s)\wedge p}$

${\displaystyle \leftrightarrow (\neg p\wedge p)\vee (s\wedge p)}$

${\displaystyle \leftrightarrow (s\wedge p).}$

Resubstition results in , so ( falsum, false ). ${\displaystyle (\neg p\wedge (q\vee p)\wedge p)}$ ${\displaystyle \bot }$

Why is this procedure correct?

Obviously, is generally valid for all expressions with partial expression . After substituting with by , we get . Be equivalent to , is also generally valid, i.e. also after resubstitution . ${\displaystyle a[t]\leftrightarrow a[t]}$ ${\displaystyle a}$ ${\displaystyle t}$ ${\displaystyle t}$ ${\displaystyle s}$ ${\displaystyle a[s]\leftrightarrow a[s]}$ ${\displaystyle b[s]}$ ${\displaystyle a[s]}$ ${\displaystyle a[s]\leftrightarrow b[s]}$ ${\displaystyle a[t]\leftrightarrow b[t]}$

annotation

The now and then so called "installation rule"

Premises :

${\displaystyle a[t],s}$

Conclusion :

${\displaystyle a[{t \over s}]}$ (Replace partial expression t with s)

is not correct in every situation. For example, the "premises" s = "Socrates is a person" and a = "If Socrates is an animal, all people are animals." but not the statement created by replacing the partial statement t = "Socrates is an animal" with s = "If Socrates is a person, all people are animals." ${\displaystyle a[{t \over s}]}$

However, the rule applies (as a special case of the replacement rule)

Premises :

${\displaystyle a[t],t,s}$

Conclusion :

${\displaystyle a[{t \over s}]}$ (Replace partial expression t with s)

Predicate logic

If in a (in a model ) valid statement for an all-quantified variable a term is inserted equally for every occurrence of , a (more specific) valid statement results. ${\displaystyle x}$ ${\displaystyle x}$ ${\displaystyle t}$

Example :

If true, including (replaced by ) . ${\displaystyle \forall x,y:x+y=y+x}$ ${\displaystyle x}$ ${\displaystyle (x+x)}$ ${\displaystyle \forall x,y:x+x+y=y+x+x}$

See also

• Final rules
• Replacement rule

Further meaning:

• Appointment rule