Ω-Regel
Die ω-Regel, auch Carnap’s Rule, ist eine unendlich-stellige Ableitungs- oder Schlussregel (genauer: ein Regelschema) in verschiedenen erweiterten Regelsystemen oder Kalkülen der Arithmetik, mit der All-Aussagen über natürliche Zahlen abgeleitet werden können. Der griechische Buchstabe ω ist ein übliches Symbol für die kleinste unendliche Ordinalzahl, die mit oder bezeichnet wird.
Formulierung
BearbeitenDie ω-Regel[1] kommt in Kalkülen vor, deren Sprache die natürlichen Zahlen hinreichend gut beschreiben kann, sodass die Symbole (null), (eins), (zwei) usw. eine sinnvolle Bedeutung haben. In der üblichen Darstellung von Schlussregeln hat die ω-Regel folgende Definition:
Für jede Formel gelte
Strenggenommen gibt es nicht eine einzelne ω-Regel, sondern eine ω-Regel für jede geeignete Aussage , daher sprechen manche Autoren in solchen Fällen nicht von einer Regel, sondern einem Regelschema.[2]
Dabei bedeutet die Notation , dass eine Formel der betrachteten Sprache ist und die Variable darin nur frei vorkommt. Instanzen wie stehen für , also für eine Version der Formel , in der alle Vorkommen von durch den links vom Schrägstrich stehenden Term ersetzt wurden; im Beispiel ist das eine geeignete Darstellung von . In der Sprache der Peano-Arithmetik ist beispielsweise für ein Konstantensymbol vorhanden, für , usw. wird die Nachfolger-Funktion auf dem Konstantensymbol iteriert, also , 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)
verwechselt werden. Die Induktionsregel hat genau zwei Prämissen: und ; die ω-Regel hat jedoch unendlich viele Prämissen.
Problematik
BearbeitenAllgemein haben Schlussregeln die Form , wobei eine Menge von Formeln ist, die als Voraussetzung interpretiert werden und als die Konklusion. Die ω-Regel (genauer: jede Instanz des ω-Regelschemas) hat allerdings unendlich viele Voraussetzungen: Konkret ist .
Definitionen:
- Eine Regel heißt finitär (oder endlich-stellig), wenn ihre Voraussetzungsmenge 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 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 von Formeln ist genau dann, wenn es eine Regel mit gibt, also wenn es eine Regel gibt, deren Voraussetzungen alle in liegen und deren Konklusion genau ist. Dabei ist der kleinste Fixpunkt von von Interesse, also die kleinste Formelmenge , für die 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 .
Damit ein solcher Fixpunkt überhaupt existiert, muss der Operator monoton sein, also für muss auch 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:
Dann ist auch jeder fundierte Ableitungsbaum von endlicher Höhe.
Eine Voraussetzung dafür ist, dass
für alle aufsteigenden Ketten von Formelmengen gilt. (Mit dem Vereinigungssymbol als Grenzwert gelesen, bedeutet die Voraussetzung, dass der Operator mit Grenzwerten vertauschbar ist. Daher wird diese Eigenschaft als Stetigkeit bezeichnet.) Mit der ω-Regel schwächen sich aber die Eigenschaften des Ableitungsoperators auf ab.
Eine erheblich weniger konkrete Darstellung des kleinsten Fixpunkts liefert der Satz von Knaster-Tarski. Es gilt
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 für die gilt, dass der Ableitungsbaum von die Höhe (oder größer) hat. Da insbesondere für jedes ableitbar ist, kann die ω-Regel für angewendet werden. Der resultierende Ableitungsbaum sieht so aus:
Der resultierende Baum hat unendliche Höhe, denn für jede infragekommende endliche Höhe ist mit dem Teilbaum plus der Anwendung der ω-Regel die Höhe von mindestens .
Sind die Ableitungen von minimaler Höhe (das heißt, kann nicht durch einen kleineren Baum als abgeleitet werden), so ist
und insbesondere ist dann nicht ohne ω-Regel aus dem Kalkül beweisbar.
Ein konkretes Beispiel für ein solches ist der Satz von Goodstein im Kontext der Peanoaxiome plus ω-Regel.
Verallgemeinerungen
BearbeitenIn 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
- ,
wobei die Voraussetzungsmenge aus den Varianten der Formel besteht, in der die Variable durch jeden Term der Sprache ersetzt wird.
Weblinks
BearbeitenLiteratur
Bearbeiten- 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.).
Einzelnachweise
Bearbeiten- ↑ 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).
- ↑ Gerrit Haas: Induktion, unendliche. In: Jürgen Mittelstraß (Hrsg.): Enzyklopädie Philosophie und Wissenschaftstheorie. Zweite Auflage. Band 3, S. 596 f.
- ↑ Kurt Schütte: Beweistheorie, 1960, S. 168