148

Dieter Rodding

ist sie selbst schon aus €"(^o)» <^®r ^^ in ihr beschriebene Funktion geht durch eine der Operationen der Variablenidentifikation, Einsetzung oder beschränkten Rekursion aus gewissen Funktionen aus €**(S5o) hervor. In jedem dieser drei Fälle liefert <13> eine äquivalente Umformung in einen Ausdruck, in dem nur Normalgleichungen aus 6^ (S5o) vorkommen, und im Falle der Variablenidentifikation bzw. Einsetzung ist der so entstehende druck in der Tat ein Normalausdruck aus 6'*(95o) (vgl. <13: (3), (4)>!). Im Falle der beschränkten Rekursion, also der Umformung (5) aus <13>, gentigt wohl der Eünweis auf die Äquivalenzen

ß (c, d, 0) = aaW ^ 3 « (/S (c, rf, 0) = a л а.^ == «)>

ß (с, d,i + l) = a^ (jc, », ß (c, dy i)) ^

3^1 3^2 («8 (jp, t, 6i) = 62 л ^ (c, rf, i + l) = 61),

die durch die Abschätzung

ß ( c , d , i ) <c (vgl. <5» legitimiert sind. Wegen

ß (c, d, 0), ß (c, d, t + 1) e S5o С €»(S5o)

erhält man nämlich mm eine äquivalente Umformung in einen druck aus ß»(S5o).

b ) Im Falle eines beliebigen Normalausdruckes aus (5*>+i (23^) genügt die wendung von (a) auf jede in seinem Innern vorkommende Normalgleichung.

16 . Im folgenden verwenden wir die Redeweise „pränex" nur für solche drucke A, bei denen alle beschränkten Quantoren an den Anfang von А bracht sind. Dann gilt:

Hilfssatz 3 : Jeder Normalausdruck aus & (S3o) läßt sich äquivalent umformen in einen pränexen Normalausdruck aus 23o.

Beweis : Zunächst läßt sich jeder Normalausdruck aus 6**(^o) àxxrch. eine Reihe von Anwendungen von <14> äquivalent umformen in einen ausdruck aus €o(S3o) ^also 25o), und mit den Umformimgen

. 4 л V » B{%)^\fi {A л B{%)) (6)

^ Л 3 ♦ B{%) ЧН.3 ♦ (-4 л B{%)) /7)

i^x i^x ^

( die bei der durch <11 : (bg)) beschriebenen aussagenlogischen Struktur der Normalausdrûcke auereidien) kann man noch die pränexe Form erreichen.