LERNZIELE:
Am Ende dieser Lektion wird der Studierende in der Lage sein:

1. Das Konzept der Induktion über die Komplexität von Ausdrücken zu verstehen.
2. Die mathematische Induktion über die Komplexität von Formeln in der Aussagenlogik anzuwenden.
3. Den Beweis durch Induktion über die Komplexität und seine Anwendung in der Aussagenlogik zu verstehen.

INHALTSVERZEICHNIS
INDUKTION ÜBER DIE KOMPLEXITÄT
EIN EINFACHES BEISPIEL: DAS SUBSTITUTIONSTHEOREM

Induktion über die Komplexität

Nehmen wir an, wir wollen zeigen, dass eine Eigenschaft \mathcal{P} für jeden Ausdruck F gilt. Eine Möglichkeit, dies zu beweisen, ist die Verwendung der Variante der mathematischen Induktion, die als „Induktion über die Komplexität von Ausdrücken“ bekannt ist. Diese erfolgt in folgenden Schritten:

• Zuerst zeigen wir, dass alle atomaren Ausdrücke diese Eigenschaft erfüllen (dies entspricht dem Fall n=1 einer herkömmlichen Induktion).
• Dann, unter der Annahme, dass sie für beliebige Ausdrücke F und G gilt, zeigen wir, dass sie folglich auch für Ausdrücke der Form F\downarrow G gilt; oder äquivalent für \neg F und eine der folgenden Formen: F\wedge G, F\vee G, F\rightarrow G.

Wenn wir dies zeigen können, dann schließen wir, dass die Eigenschaft \mathcal{P} für alle Ausdrücke der Aussagenlogik gilt. Dies ist das, was wir als „mathematische Induktion über die Komplexität von Ausdrücken“ bezeichnen.

Ein Einfaches Beispiel: Das Substitutionstheorem

Um eine bessere Vorstellung davon zu bekommen, wie die Induktion über die Komplexität von Formeln durchgeführt wird, betrachten wir das (Meta-)Substitutionstheorem.

Angenommen, F\equiv G. Sei H ein Ausdruck, der F als Teilausdruck enthält, und sei H^\prime der Ausdruck, der durch Ersetzen aller Vorkommen von F durch G entsteht, dann gilt H\equiv H^\prime.

Beweis durch Induktion über die Komplexität von Formeln

Ein Beweis durch Induktion über die Komplexität bedeutet zu zeigen, dass zwei Dinge zutreffen: 1) ein Anfangsfall (für atomare Formeln) und 2) der Induktionsschritt (wenn es für beliebige Ausdrücke F und G funktioniert, dann funktioniert es auch für F\downarrow G, oder in einfacherer Form: es funktioniert für \neg F und mindestens eine der folgenden: F\vee G, F\wedge G, F\rightarrow G oder F\leftrightarrow G).

Angenommen, H ist ein atomarer Ausdruck, F ist ein Teilausdruck von H und F\equiv G. Wenn H^\prime das Ergebnis des Ersetzens aller Teilformeln F in H ist, dann gilt, da H atomar ist, notwendigerweise H^\prime \equiv G. Andererseits, da H atomar ist und F ein Teilausdruck davon ist, gilt H\equiv F. Schließlich ergibt sich daraus:

H\equiv F \equiv G \equiv H^\prime

Damit ist der Anfangsfall für atomare Ausdrücke bewiesen.

Betrachten wir nun den Induktionsfall.

Die Induktionshypothese

Angenommen, das Theorem gilt für zwei beliebige Ausdrücke H_1 und H_2, die jeweils F als Teilausdruck enthalten, wobei F \equiv G. Dann gilt: Wenn H_1^\prime das Ergebnis des Ersetzens aller F durch G in H_1 ist und H_2^\prime das Ergebnis des Ersetzens aller F durch G in H_2, dann gilt H_1\equiv H_1^\prime und H_2\equiv H_2^\prime.

Der Induktionsschritt

Hier untersuchen wir, ob infolge der Induktionshypothese das Theorem auch für \neg H_1 (oder \neg H_2, je nachdem) und mindestens eine der folgenden Aussagen gilt: H_1 \wedge H_2, H_1 \vee H_2, H_1 \rightarrow H_2.

Wenn H:= \neg H_1, dann gilt nach der Induktionshypothese H\equiv \neg H_1^\prime=: H^\prime , wobei H^\prime das Ergebnis des Ersetzens aller Vorkommen von F in H durch G ist. Daher gilt H\equiv H^\prime.

Analog dazu gilt: Wenn H:= H_1 \wedge H_2, dann folgt aus der Induktionshypothese H\equiv H_1^\prime \wedge H_2 \equiv H_1^\prime \wedge H_2^\prime =: H^\prime , wobei H^\prime das Ergebnis des Ersetzens aller Vorkommen von F in H durch G ist. Daher gilt H\equiv H^\prime.

Daher ist die Induktion vollständig, und das Substitutionstheorem gilt für alle Ausdrücke der Aussagenlogik.

Durch die Anwendung dieser Form der Induktion kann sichergestellt werden, dass eine Eigenschaft für alle Ausdrücke eines logischen Systems gilt, was besonders in der Aussagenlogik nützlich ist, um rigorose Beweise zu strukturieren. Darüber hinaus erstreckt sich ihre Nützlichkeit auf Bereiche wie die künstliche Intelligenz und die Softwareentwicklung, wo die Verifikation logischer Systeme wesentlich ist. Mit dieser Technik lassen sich Beweise automatisieren und die Konsistenz komplexer Ausdrücke sicherstellen, was das Fehlerrisiko verringert und die Genauigkeit in Umgebungen erhöht, die auf mathematische und logische Gültigkeit angewiesen sind.