Structurele inductie

Structurele inductie of structuurinductie is een bewijsmethode waarmee bewezen kan worden dat een bepaalde eigenschap geldt voor alle elementen van een inductief gedefinieerde verzameling. Het is een vorm van wiskundige inductie. Een inductief (of recursief) gedefinieerde verzameling bestaat uit een aantal basisobjecten en wordt vervolgens afgesloten onder een aantal operaties. Voorbeelden van inductief gedefinieerde verzamelingen zijn logische formules, wiskundige termen, en veel structuren uit de theoretische informatica, zoals bomen.

Het idee achter structuurinductie is dat als

1. alle mogelijke basisobjecten een bepaalde eigenschap $P$ hebben; en
2. alle manieren om een nieuw object te maken uit oude objecten waarvoor die eigenschap $P$ geldt, weer een object opleveren waarvoor $P$ geldt

de eigenschap dan geldt voor alle objecten in de verzameling.

Inductie in het algemeen is een bewijsmethode die gebruikt kan worden voor welgefundeerde verzamelingen (verzamelingen met een welgefundeerde ordening). Structuurinductie onderscheidt zich van inductie op de natuurlijke getallen (volledige inductie) omdat de gebruikte ordening niet totaal is. Bovendien wordt de ordening meestal impliciet gedefinieerd in de inductieve definite. De kleinste objecten zijn de basisobjecten en wanneer objecten samengesteld worden ontstaat een groter object. Structuurinductie komt vaak voor binnen de algebra, logica, theoretische informatica en andere gebieden waarin formules, termen, lijsten, programma's en andere inductief gedefinieerde verzamelingen een rol spelen.

In de grondslagen van de wiskunde worden de natuurlijke getallen soms inductief als volgt gedefinieerd:

• $0$ (nul) is een natuurlijk getal.
• Als $x$ een natuurlijk getal is, dan is ook $S(x)$ (lees: opvolger van $x$, of $x+1$) een natuurlijk getal.
• Niets anders is een natuurlijk getal.

Als we de natuurlijke getallen zo definiëren, is de volledige inductie op natuurlijke getallen een speciaal geval van structuurinductie; dat wil zeggen, dat structuurinductie een generalisatie van volledige inductie is.

Voorbeeld

Definitie. De verzameling van positieve formules is de kleinste verzameling zodat:

• een atomaire propositie $p_{i}$ (voor $i\in \mathbb {N}$) een positieve formule is;
• als $\varphi$ en $\psi$ positieve formules zijn, dan ook $\varphi \wedge \psi$, $\varphi \vee \psi$ en $\varphi \to \psi$;

Stelling. Een positieve formule $\varphi$ is vervulbaar. Sterker: $\varphi$ wordt vervuld door de evaluatie die aan alle atomaire proposities die in $\varphi$ voorkomen de waarheidswaarde waar toekent.

Bewijs.

Basisstap. Een atomaire formule $p_{i}$ wordt vervuld door de valuatie die aan $p_{i}$ de waarheidswaarde waar toekent.

Inductiestap.

Stel dat $\varphi$ van de vorm $\varphi _{1}\wedge \varphi _{2}$ is. Volgens de inductiehypothese kunnen we aannemen dat $\varphi _{1}$ en $\varphi _{2}$ vervuld worden door de valuaties die aan alle atomaire proposities in $\varphi _{1}$ resp. $\varphi _{2}$ waar toekenennen. Dat betekent volgens de semantiek van $\wedge$ dat $\varphi _{1}\wedge \varphi _{2}$ vervuld wordt door de valuatie die aan alle atomaire proposities waar toekent.

Stel dat $\varphi$ van de vorm $\varphi _{1}\vee \varphi _{2}$ is. Volgens de inductiehypothese kunnen we aannemen dat $\varphi _{1}$ en $\varphi _{2}$ vervuld worden door de valuaties die aan alle atomaire proposities in $\varphi _{1}$ resp. $\varphi _{2}$ waar toekenennen. Dat betekent volgens de semantiek van $\vee$ dat $\varphi _{1}\vee \varphi _{2}$ vervuld wordt door de valuatie die aan alle atomaire proposities waar toekent.

Stel dat $\varphi$ van de vorm $\varphi _{1}\to \varphi _{2}$ is. Volgens de inductiehypothese kunnen we aannemen dat $\varphi _{1}$ en $\varphi _{2}$ vervuld worden door de valuaties die aan alle atomaire proposities in $\varphi _{1}$ resp. $\varphi _{2}$ waar toekenennen. Dat betekent volgens de semantiek van $\to$ dat $\varphi _{1}\to \varphi _{2}$ vervuld wordt door de valuatie die aan alle atomaire proposities waar toekent.

Daarmee is de stelling bewezen.