Ω-Regel

Die ω-Regel[1] kommt in Kalkülen vor, deren Sprache die natürlichen Zahlen hinreichend gut beschreiben kann, sodass die Symbole ${\displaystyle 0}$ (null), ${\displaystyle 1}$ (eins), ${\displaystyle 2}$ (zwei) usw. eine sinnvolle Bedeutung haben. In der üblichen Darstellung von Schlussregeln hat die ω-Regel folgende Definition:

Für jede Formel ${\displaystyle \phi (n)}$ gelte

${\displaystyle {\frac {\;\phi (0)\qquad \phi (1)\qquad \phi (2)\qquad \cdots \;}{\forall n.\phi (n)}}\,\Omega _{\phi }}$

Strenggenommen gibt es nicht eine einzelne ω-Regel, sondern eine ω-Regel für jede geeignete Aussage ${\displaystyle \phi }$, daher sprechen manche Autoren in solchen Fällen nicht von einer Regel, sondern einem Regelschema.[2]

Dabei bedeutet die Notation ${\displaystyle \phi (n)}$, dass ${\displaystyle \phi }$ eine Formel der betrachteten Sprache ist und die Variable ${\displaystyle n}$ darin nur frei vorkommt. Instanzen wie ${\displaystyle \phi (0)}$ stehen für ${\displaystyle \phi [0/n]}$, also für eine Version der Formel ${\displaystyle \phi }$, in der alle Vorkommen von ${\displaystyle n}$ durch den links vom Schrägstrich stehenden Term ersetzt wurden; im Beispiel ${\displaystyle \phi [0/n]}$ ist das eine geeignete Darstellung von ${\displaystyle 0}$. In der Sprache der Peano-Arithmetik ist beispielsweise für ${\displaystyle 0}$ ein Konstantensymbol vorhanden, für ${\displaystyle 1}$, ${\displaystyle 2}$ usw. wird die Nachfolger-Funktion ${\displaystyle S}$ auf dem Konstantensymbol ${\displaystyle 0}$ iteriert, also ${\displaystyle 1=S(0)}$, ${\displaystyle 2=S(S(0))}$ usw.

Weil unendlich viele Prämissen erst als herleitbar nachgewiesen sind, bevor auf die Schlussformel übergegangen werden darf, nennt man dieses Regelschema auch halbformal oder einen Halbformalismus.[3]

Die ω-Regel sollte nicht mit der Induktionsregel (genauer: dem Induktionsschema)

${\displaystyle {\frac {\,\phi (0)\qquad \forall n.\phi (n)\to \phi (S(n))\,}{\forall n.\phi (n)}}\,{\text{Ind}}_{\phi }}$

verwechselt werden. Die Induktionsregel hat genau zwei Prämissen: ${\displaystyle \phi (0)}$ und ${\displaystyle \forall n.\phi (n)\to \phi (S(n))}$; die ω-Regel hat jedoch unendlich viele Prämissen.

Allgemein haben Schlussregeln die Form ${\displaystyle V/\kappa }$, wobei ${\displaystyle V}$ eine Menge von Formeln ist, die als Voraussetzung interpretiert werden und ${\displaystyle \kappa }$ als die Konklusion. Die ω-Regel (genauer: jede Instanz des ω-Regelschemas) hat allerdings unendlich viele Voraussetzungen: Konkret ist ${\displaystyle V=\{\phi (0),\phi (1),\phi (2),\dots \}}$.

Definitionen:

• Eine Regel ${\displaystyle V/\kappa }$ heißt finitär (oder endlich-stellig), wenn ihre Voraussetzungsmenge ${\displaystyle V}$ endlich ist.
• Eine Menge von Regeln (Regelsystem) heißt finitär, wenn jede einzelne Regel finitär ist; dabei ist unerheblich, ob die Menge der Regeln selbst endlich ist (meist ist sie es nicht).

Die meisten in der mathematischen Praxis betrachteten Regelsysteme sind finitär. Das ist beispielsweise notwendig, wenn alle Voraussetzungen von einem Computersystem überprüft werden sollen. Viele Regelsysteme werden mit dem Hintergedanken entworfen, dass Ableitungen automatisiert überprüft werden können.

Auch in formaler Hinsicht haben finitäre Regelsysteme erhebliche Vorteile. Betrachtet man den Ableitungsoperator ${\displaystyle A}$ zu einem Regelsystem, der eine Menge von Formeln auf die Menge der mit dem Regelsysteme ableitbaren Formeln abbildet, das heißt, für eine Menge ${\displaystyle F}$ von Formeln ist ${\displaystyle \phi \in A(F)}$ genau dann, wenn es eine Regel ${\displaystyle V/\phi }$ mit ${\displaystyle V\subseteq F}$ gibt, also wenn es eine Regel gibt, deren Voraussetzungen alle in ${\displaystyle F}$ liegen und deren Konklusion genau ${\displaystyle \phi }$ ist. Dabei ist der kleinste Fixpunkt von ${\displaystyle A}$ von Interesse, also die kleinste Formelmenge ${\displaystyle F}$, für die ${\displaystyle F=A(F)}$ gilt, da er genau die Formeln enthält, für die es einen fundierten Ableitungsbaum gibt. (Fundiert heißt, dass jeder Zweig im Ableitungsbaum endlich ist.) Für diesen kleinsten Fixpunkt schreibt man ${\displaystyle \mu (A)}$.

Damit ein solcher Fixpunkt überhaupt existiert, muss der Operator monoton sein, also für ${\displaystyle F\subseteq G}$ muss auch ${\displaystyle A(F)\subseteq A(G)}$ gelten. (Mit mehr Annahmen darf es nicht weniger Konklusionen geben.) Jeder Regeloperator ist monoton, solange keine Regeln existieren, die Urteile aufheben, was in üblichen Regelsystemen nicht der Fall ist.

Für finitäre Regelsysteme folgt aus dem Fixpunktsatz von Kleene:

${\displaystyle \mu (A)=\bigcup _{n\in \mathbb {N} }A^{n}(\emptyset )=A(\emptyset )\cup A(A(\emptyset ))\cup \cdots }$

Dann ist auch jeder fundierte Ableitungsbaum von endlicher Höhe.

Eine Voraussetzung dafür ist, dass

${\displaystyle A{\Bigl (}\bigcup _{n\in \mathbb {N} }F_{n}{\Bigr )}=\bigcup _{n\in \mathbb {N} }A(F_{n})}$

für alle aufsteigenden Ketten ${\displaystyle F_{1}\subseteq F_{2}\subseteq \cdots }$ von Formelmengen gilt. (Mit dem Vereinigungssymbol als Grenzwert gelesen, bedeutet die Voraussetzung, dass der Operator ${\displaystyle A}$ mit Grenzwerten vertauschbar ist. Daher wird diese Eigenschaft als Stetigkeit bezeichnet.) Mit der ω-Regel schwächen sich aber die Eigenschaften des Ableitungsoperators ${\displaystyle A}$ auf ${\textstyle \bigcup _{n\in \mathbb {N} }A(F_{n})\subseteq \mu (A)}$ ab.

Eine erheblich weniger konkrete Darstellung des kleinsten Fixpunkts liefert der Satz von Knaster-Tarski. Es gilt

${\displaystyle \mu (A)=\bigcap \{\,F{\text{ Formel}}\,|\,A(F)\subseteq F\,\}}$

auch mit ω-Regel.

Durch die ω-Regel können unendlich hohe (weiterhin fundierte) Ableitungsbäume entstehen. Für ein einfaches Beispiel für diesen Fall betrachtet man eine Formel ${\displaystyle \phi }$ für die gilt, dass der Ableitungsbaum ${\displaystyle B_{n}}$ von ${\displaystyle \phi (n)}$ die Höhe ${\displaystyle n}$ (oder größer) hat. Da insbesondere ${\displaystyle \phi (n)}$ für jedes ${\displaystyle n}$ ableitbar ist, kann die ω-Regel für ${\displaystyle \phi }$ angewendet werden. Der resultierende Ableitungsbaum ${\displaystyle B_{\omega }}$ sieht so aus:

${\displaystyle B_{\omega }={\frac {\,{\stackrel {\underset {|}{B_{0}}}{\phi (0)}}\qquad {\stackrel {\underset {|}{B_{1}}}{\phi (1)}}\qquad {\stackrel {\underset {|}{B_{2}}}{\phi (2)}}\qquad \cdots \,}{\forall n.\phi (n)}}\,\Omega _{\phi }}$

Der resultierende Baum ${\displaystyle B_{\omega }}$ hat unendliche Höhe, denn für jede infragekommende endliche Höhe ${\displaystyle n}$ ist mit dem Teilbaum ${\displaystyle B_{n}}$ plus der Anwendung der ω-Regel die Höhe von ${\displaystyle B_{\omega }}$ mindestens ${\displaystyle n+1}$.

Sind die Ableitungen ${\displaystyle B_{n}}$ von minimaler Höhe (das heißt, ${\displaystyle \phi (n)}$ kann nicht durch einen kleineren Baum als ${\displaystyle B_{n}}$ abgeleitet werden), so ist

${\displaystyle (\forall n.\phi (n))\in A{\Bigl (}\bigcup _{n\in \mathbb {N} }A^{n}(\emptyset ){\Bigr )}\setminus \bigcup _{n\in \mathbb {N} }A^{n}(\emptyset )\subseteq \mu (A)}$

und insbesondere ist ${\displaystyle \forall n.\phi (n)}$ dann nicht ohne ω-Regel aus dem Kalkül beweisbar.

Ein konkretes Beispiel für ein solches ${\displaystyle \phi }$ ist der Satz von Goodstein im Kontext der Peanoaxiome plus ω-Regel.

In allgemeineren Fassungen ist die ω-Regel nicht auf die natürlichen Zahlen zugeschnitten, sondern läuft über alle Terme der betrachteten Sprache. So formuliert ist die ω-Regel

${\displaystyle {\frac {\,\{\phi (t)\}_{t{\text{ ein Term}}}\,}{\forall x.\phi (x)}}\,\Omega _{\phi }}$,

wobei die Voraussetzungsmenge aus den Varianten der Formel ${\displaystyle \phi }$ besteht, in der die Variable ${\displaystyle x}$ durch jeden Term der Sprache ersetzt wird.

• Carnap Rule in der Encyclopedia of Mathematics

• Gerrit Haas: Induktion, unendliche. In: Jürgen Mittelstraß (Hrsg.): Enzyklopädie Philosophie und Wissenschaftstheorie. 2. Auflage. Band 3. Springer-Verlag GmbH, ISBN 978-3-476-02108-3, S. 596 f. (4750 S.).
• David Hilbert: Die Grundlegung der elementaren Zahlenlehre. In: Mathematische Annalen. Nr. 104, S. 485–494, doi:10.1007/BF01457953.
• Rudolf Carnap: Logische Syntax der Sprache. 2. Auflage. Wien 1968, ISBN 978-3-662-23330-6 (Erstausgabe: 1934).
• Stephen Cole Kleene: Introduction to Metamathematics. Amsterdam / Groningen 1952, ISBN 978-0-923891-57-2 (englisch).
• John Barkley Rosser: Gödel Theorems for Non-Constructive Logics. In: The Journal of Symbolic Logic. Nr. 2, S. 129–137, doi:10.2307/2266293.
• Kurt Schütte: Beweistheorie. In: Grundlehren der mathematischen Wissenschaften. Springer Berlin, Heidelberg, 1960, ISSN 0072-7830.
• Christian Thiel: Halbformalismus. In: Jürgen Mittelstraß (Hrsg.): Enzyklopädie Philosophie und Wissenschaftstheorie. 2. Auflage. Band 3. Springer-Verlag GmbH, ISBN 978-3-476-02108-3, S. 259 (4750 S.).
• Paul Lorenzen: Die Widerspruchsfreiheit der klassischen Analysis. In: Mathematische Zeitschrift. Band 54. Bonn 1951, doi:10.1007/BF01175131.
• Paul Lorenzen: Metamathematik. In: Hochschultaschenbücher. 2. Auflage. Band 25. Bibliographisches Institut, Mannheim 1980 (173 S., Erstausgabe: 1962).
• Wolfgang Stegmüller: Unvollständigkeit und Unentscheidbarkeit. „Die metamathematischen Resultate von Gödel, Church, Kleene, Rosser und ihre erkenntnistheoretische Bedeutung.“ 3. Auflage. Springer-Verlag, Wien / New York 1973, ISBN 3-211-81208-3 (116 S., Erstausgabe: 1959).
• Gereon Wolters: Metamathematik. In: Jürgen Mittelstraß (Hrsg.): Enzyklopädie Philosophie und Wissenschaftstheorie. Band 2. Mannheim / Wien / Zürich 1984, ISBN 978-3-476-02108-3 (XIX + 601 S.).

1. Die summative Induktion in der Form der ω-Regel hat David Hilbert 1931 (Math. Ann. 104 (1931), S. 485–494) eingeführt, nachdem er den Gödelschen Beweis für die ω-Unvollständigkeit der axiomatisch aufgebauten Arithmetik kennengelernt hatte (siehe auch Hilberts Werke, Band III, S. 193 und S. 215).
2. Gerrit Haas: Induktion, unendliche. In: Jürgen Mittelstraß (Hrsg.): Enzyklopädie Philosophie und Wissenschaftstheorie. Zweite Auflage. Band 3, S. 596 f.
3. Kurt Schütte: Beweistheorie, 1960, S. 168