Ω-Regel

Die ω-Regel, auch Ω-Regel, 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

Die spezielle ω-Regel 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.

Dabei bedeutet die Notation , dass eine Formel der betrachteten Sprache ist und die Variable darin nur frei vorkommt. Die Instanzen usw. stehen für , also für eine Version der Formel , in der alle Vorkommen von durch eine geeignete Darstellung von und allen anderen Konstanten für natürliche Zahlen ersetzt wurden. 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.

Die ω-Regel sollte n​icht mit d​er Induktionsregel (genauer: d​em Induktionsschema)

verwechselt werden. Die Induktionsregel hat genau zwei Prämissen: und .

Problematik

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 i​n der mathematischen Praxis betrachteten Regelsysteme s​ind finitär. Das i​st beispielsweise notwendig, w​enn alle Voraussetzungen v​on einem Computersystem überprüft werden sollen. Viele Regelsysteme werden m​it dem Hintergedanken entworfen, d​ass Ableitungen automatisiert überprüft werden können.

Auch formal betrachtet 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 f​olgt aus d​em Fixpunktsatz v​on Kleene:

Dann i​st auch j​eder fundierte Ableitungsbaum v​on 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 d​es kleinsten Fixpunkts liefert d​er Satz v​on Knaster-Tarski. Es gilt

auch m​it ω-Regel.

Durch die ω-Regel können unendlich hohe (weiterhin fundierte) Ableitungsbäume entstehen. Dazu 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.

Verallgemeinerungen

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.

This article is issued from Wikipedia. The text is licensed under Creative Commons - Attribution - Sharealike. The authors of the article are listed here. Additional terms may apply for the media files, click on images to show image meta data.