Structural induction

The structural induction is a proof method , inter alia, in the logic , the theoretical computer science and the graph theory is used. It is a more general form of complete induction . With the method, statements about the elements of recursively constructed sets (for example sets of lists , formulas , graphs ) can be proven.

In the case of complete induction, properties of natural numbers are proven; In structural induction, properties are proven for sets, the elements of which are created from basic elements through a finite number of construction steps (using already constructed elements) or by means of a generation system. So there are minimal (also: simplest or basic) elements and recursively defined (or: recursively formed) elements of the set. In the case of natural numbers, the basic element is (or , depending on the definition of the natural numbers) and the construction step is the transition from a number to a number . ${\displaystyle 0}$ ${\displaystyle 1}$ ${\displaystyle n}$ ${\displaystyle n+1}$

In order to prove a statement for the elements of a set, one shows the validity of the statement for the simplest elements in the induction start and the validity of the statement for the recursively formed elements in the induction conclusion, provided that the statement applies to the elements used in the construction . If both are met, the statement applies to all elements. So induction is carried out over the structural structure of the elements.

Structural induction is a special case of induction for sets with a well-founded (partial) order .

Example of a definition by structural induction

The set of propositional formulas can be defined using structural induction as follows:

Induction start: If is an atomic propositional formula, is a propositional formula. ${\displaystyle A\!\,}$ ${\displaystyle A\!\,}$

Induction step 1: If is a propositional formula, is also a propositional formula. ${\displaystyle F\!\,}$ ${\displaystyle \lnot F}$

Induction step 2: If and are propositional formulas, is also a propositional formula. ${\displaystyle F\!\,}$ ${\displaystyle G\!\,}$ ${\displaystyle (F\land G)}$

Induction step 3: If and are propositional formulas, is also a propositional formula. ${\displaystyle F\!\,}$ ${\displaystyle G\!\,}$ ${\displaystyle (F\lor G)}$

Induction step 4: If and are propositional formulas, is also a propositional formula. ${\displaystyle F\!\,}$ ${\displaystyle G\!\,}$ ${\displaystyle \!\,(F\to G)}$

Induction step 5: If and are propositional formulas, is also a propositional formula. ${\displaystyle F\!\,}$ ${\displaystyle G\!\,}$ ${\displaystyle (F\leftrightarrow G)}$

According to this definition z. B. the following terms propositional formulas:

• ${\displaystyle \lnot (A\land B)}$
• ${\displaystyle (A\to (B\lor \lnot C))}$
• ${\displaystyle ((A\lor \lnot B)\land (\lnot A\lor B))}$

Further examples of definitions through structural induction can be found in the articles Elementary Language and Word (Theoretical Computer Science) (Definition of Mirroring).

Example of a proof by structural induction

The proposition is proven:

For every propositional formula there is an equivalent propositional formula in which the only operators and appear. ${\displaystyle F}$ ${\displaystyle [F]}$ ${\displaystyle \lnot }$ ${\displaystyle \land }$

The proof:

Induction start: If is for an atomic propositional formula , is . ${\displaystyle F=A}$ ${\displaystyle A}$ ${\displaystyle [F]=A}$

Induction step 1: If for a propositional formula , is . ${\displaystyle F=\lnot G}$ ${\displaystyle G}$ ${\displaystyle [F]=\lnot [G]}$

Induction step 2: If for propositional formulas and , is . ${\displaystyle F=(G\land H)}$ ${\displaystyle G}$ ${\displaystyle H}$ ${\displaystyle [F]=([G]\land [H])}$

Induction step 3: If for propositional formulas and , is . ${\displaystyle F=(G\lor H)}$ ${\displaystyle G}$ ${\displaystyle H}$ ${\displaystyle [F]=\lnot (\lnot [G]\land \lnot [H])}$

Induction step 4: If for propositional formulas and , is . ${\displaystyle F=(G\to H)}$ ${\displaystyle G}$ ${\displaystyle H}$ ${\displaystyle [F]=\lnot ([G]\land \lnot [H])}$

Induction step 5: If for propositional formulas and , is . ${\displaystyle F=(G\leftrightarrow H)}$ ${\displaystyle G}$ ${\displaystyle H}$ ${\displaystyle [F]=\lnot (\lnot ([G]\land [H])\land \lnot (\lnot [G]\land \lnot [H]))}$

The equals sign stands for syntactic equality, i.e. H. Equality sign by sign. In every induction step it is assumed that for and respectively the equivalent formulas and exist which only use and (induction assumption ). ${\displaystyle G}$ ${\displaystyle H}$ ${\displaystyle [G]}$ ${\displaystyle [H]}$ ${\displaystyle \lnot }$ ${\displaystyle \land }$

In a concrete construction, the proof steps can also be applied in the reverse order, ie “from outside to inside”. For the middle of the propositional formulas given above, z. B. the following equivalences:

${\displaystyle {\begin{aligned}(A\to (B\lor \lnot C))&\equiv [(A\to (B\lor \lnot C))]\\&{\stackrel {\mbox{IS 4}}{=}}\lnot ([A]\land \lnot [(B\lor \lnot C)])\\&{\stackrel {\mbox{IS 3}}{=}}\lnot ([A]\land \lnot \lnot (\lnot [B]\land \lnot [\lnot C]))\\&{\stackrel {\mbox{IS 1}}{=}}\lnot ([A]\land \lnot \lnot (\lnot [B]\land \lnot \lnot [C]))\\&{\stackrel {3\times {\mbox{IA}}}{=}}\lnot (A\land \lnot \lnot (\lnot B\land \lnot \lnot C))\end{aligned}}}$

The applications of induction step 1 and induction start are empty here; i.e., they do not change the term. (With the first formula given above, all induction steps and the induction start would be empty.) Incidentally, the fact that the last formula can still be simplified is irrelevant here. ${\displaystyle \lnot (A\land (\lnot B\land C))}$

literature

• Hartmut Ehrig, Bernd Mahr, F. Cornelius, Martin Große-Rhode, P. Zeitz: Mathematical-structural basics of computer science . Springer, 2013, pp. 162–168

Web links

• François Bry: Theorem 2.1.4 (structural induction) . Script, LMU
• Christoph Walter: Structural induction and induction after recursion of procedures . Script, Darmstadt University