30

Werner Mellis

У У^ У ^ У

Wenn -nN. und jR. ^ ^ und R., ^, ^, dann R ,^ ,, ^. Nimmt man wieder b bs^iz) b'sjib^z) t2{b,b\z)

an , daß F an der Stelle s^{z) mit f{si{z))<J{z) schon definiert ist und setzt

У У ^

b = F(Sj^{z)), dann ist die Voraussetzung —liV"!^ ^ ^^^Ri.. . . .• So berechnet

F ( si ( z ) ) F(z)s^(z)

у

aus b=F(si{z)) eine Stelle S2iF{si(z)),z), so daß R\^, ,^^,, ч aus

t2 ( F ( si ( z ) ) , b , z )

у z

^L / /Г-/ / ЧЧ Ч f^lgt- Es wird angenommen, daß F an der Stelle S2(F(si(z)),z)

mit /(s2(F(si(z)),z))<^/(z) schon definiert ist und es wird b = F(s2(F(5i(z)), z)) gesetzt. Im zweiten Fall wird also definiert:

r { Si { z ) )

tJ Z j.y Z

F ( z ) s , ( z ) F(z)s2(F(si(z)),z) ^F(z) : = t2(F(5i(z)), F(s2(F(si(z)), z)), z).

F ist also durch eine verschachtelte Rekursion definiert. Die Versuche inhaltliche Argumentationen in Z(a,r^+J zu formaUsieren zeigen, worauf man bei der Untersuchung der Z-Beweise zu achten hat. Von Relevanz ist offenbar, wie in den Z-Beweisen oberhalb einer <^—IR(2'^+i) (Gen) für y und (B) für z aufeinander folgen. Denn wird in einer (B)-Regel für z 5^ beseitigt und kommt unterhalb dieser (B)-Regel eine GeneraHsierung für y vor, die die freie Variable yi eliminiert, so kann

y .

Sj von yi abhängen. Bei der Ersetzung von y^ durch F{r) geht daher Sj in Sj über. (Vgl. 3.13 und 3.14, wo t die Rolle von F übernimmt.)

3 . 1

Es werden nun beginnend mit einer obersten alle <^ —IR(I'^+i) durch <д — Ш(Я J ersetzt. Die Axionenmenge der Theorie wird erweitert um eine Menge v4i von Formeln mit höchstens m Quantoren, die gegen Substitution sen ist. Die Sprache wird um endlich viele Terme erweitert. Die mata der Substitution, der primitiven und der transfiniten Rekursion seien für diese erweiterte Sprache formuliert. Da die Axiome nicht mehr als m Quantoren enthalten, können im Oberbeweis b^ der betrachteten <^ — №(2"^+1) alle Schnitte, deren Schnittformeln mehr als m Quantoren enthalten, beseitigt werden. Die

Oberformel dieser <«-IR(2;^+i) sei -i'iz'lf{z')<J(z)-^3yR^/jw3yR. Die

„ Geschichte " der Quantoren 3z, V_v und 3y wird einen Term t bestimmen, für den

/ y z\ У

der entsprechend modifizierte Beweis die Formel —i Vz'l /(z") <g^f{z)-^R , ) ^ Ä

beweisen wird. Es wird vorausgesetzt, daß 3yR pränex ist mit m +1 abwechselnden