Ω-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 $\omega$ oder $\omega _{0}$ bezeichnet wird.

Formulierung

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

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

${\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 $\phi$, daher sprechen manche Autoren in solchen Fällen nicht von einer Regel, sondern einem Regelschema.

Dabei bedeutet die Notation $\phi (n)$, dass $\phi$ eine Formel der betrachteten Sprache ist und die Variable $n$ darin nur frei vorkommt. Die Instanzen $\phi (0)$ usw. stehen für $\phi [0/n]$, also für eine Version der Formel $\phi$, in der alle Vorkommen von $n$ durch eine geeignete Darstellung von $0$ und allen anderen Konstanten für natürliche Zahlen ersetzt wurden. In der Sprache der Peano-Arithmetik ist beispielsweise für $0$ ein Konstantensymbol vorhanden, für $1$, $2$ usw. wird die Nachfolger-Funktion $S$ auf dem Konstantensymbol $0$ iteriert, also $1=S(0)$, $2=S(S(0))$ usw.

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

${\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: $\phi (0)$ und $\forall n.\phi (n)\to \phi (S(n))$.

Problematik

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

Definitionen:

• Eine Regel $V/\kappa$ heißt finitär (oder endlich-stellig), wenn ihre Voraussetzungsmenge $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 formal betrachtet haben finitäre Regelsysteme erhebliche Vorteile. Betrachtet man den Ableitungsoperator $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 $F$ von Formeln ist $\phi \in A(F)$ genau dann, wenn es eine Regel $V/\phi$ mit $V\subseteq F$ gibt, also wenn es eine Regel gibt, deren Voraussetzungen alle in $F$ liegen und deren Konklusion genau $\phi$ ist. Dabei ist der kleinste Fixpunkt von $A$ von Interesse, also die kleinste Formelmenge $F$, für die $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 $\mu (A)$.

Damit ein solcher Fixpunkt überhaupt existiert, muss der Operator monoton sein, also für $F\subseteq G$ muss auch $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:

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

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

für alle aufsteigenden Ketten $F_{1}\subseteq F_{2}\subseteq \cdots$ von Formelmengen gilt. (Mit dem Vereinigungssymbol als Grenzwert gelesen, bedeutet die Voraussetzung, dass der Operator $A$ mit Grenzwerten vertauschbar ist. Daher wird diese Eigenschaft als Stetigkeit bezeichnet.) Mit der ω-Regel schwächen sich aber die Eigenschaften des Ableitungsoperators $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

$\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. Dazu betrachtet man eine Formel $\phi$ für die gilt, dass der Ableitungsbaum $B_{n}$ von $\phi (n)$ die Höhe $n$ (oder größer) hat. Da insbesondere $\phi (n)$ für jedes $n$ ableitbar ist, kann die ω-Regel für $\phi$ angewendet werden. Der resultierende Ableitungsbaum $B_{\omega }$ sieht so aus:

$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 $B_{\omega }$ hat unendliche Höhe, denn für jede infragekommende endliche Höhe $n$ ist mit dem Teilbaum $B_{n}$ plus der Anwendung der ω-Regel die Höhe von $B_{\omega }$ mindestens $n+1$.

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

$(\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 $\forall n.\phi (n)$ dann nicht ohne ω-Regel aus dem Kalkül beweisbar.

Ein konkretes Beispiel für ein solches $\phi$ 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

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

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