Ω-Regel

unendlich-stellige Ableitungs- oder Schlussregel (genauer: ein Regelschema) in verschiedenen erweiterten Regelsystemen oder Kalkülen der Arithmetik

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

Bearbeiten

Die ω-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

Bearbeiten

Allgemein 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

Bearbeiten

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

 ,

wobei die Voraussetzungsmenge aus den Varianten der Formel   besteht, in der die Variable   durch jeden Term der Sprache ersetzt wird.

Bearbeiten

Literatur

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
  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