Widerspruchsfreier Aufbau einer typenfreien Logik

Mathematische Zeitschrift, Band 55, Heft 3, S. 364--384 (1952).

Widerspruchsfreier Aufbau einer typenfreien Logik. (Erweitertes System).

Yon

Wilhelm Aekermann in Liidenscheid.

w 1.

Einleitung.

Das Ziel dieser Untersuchungen ist das folgende: Es soll ein typenfreies logisches System aufgestellt werden, fiir das derWiderspruchs- freiheitsbeweis geftihrt werden kann. Das System soll gentigend welt sein: um daraus ohne Hinzuffigung besonderer mathematischen Axiome die Zahlentheorie und in einem gewissen Umfang auch die Analysis ableiten zu kOnnen. Der Grundgedanke des Systems ist eine gewisse Revision des Aussagenl~alktils. die ich bereits an anderer Stelle aus- ftihrlich diskutiertel). Das vorliegende System entsteht aus dem frfi- heren d u r c h eine Erweiterung, die in der Hauptsache dazu dient, eine Einbeziehung des Satzes vom ausgeschlossenen Dritten vorzu- nehmen. Die Gedanken, die" der Revision" des Aussagenkalktils zugrunde liegen, sind die folgenden: 1. Da der Definitionsbereich der Pr~dikat% d. h. der Bereich der Dinge, ftir die das Zutreffen eines Pr~tdikates sinnvoller Weise als richtig oder falsch bezeic.hne(~ werden kann~ im ailgemeinen besehr~nkt ist~ so kann als Grund!age nur eine positive Logik genommen werden, die den Satz vom ausgeschlossenen Dritten nicht yon vorneherein zugrunde legt. 2. Die Richtigkeit yon Implikationen setzt im Prinzip voraus, dal~ zwischen Vorder- und Hinterglied der Implikation eine gewisse Gleichheit der s em an t i s chen Stufen besteht. 3. Die Einftihrung der Negation geschieht in eigen- ttimlicher Weise. D i e Unvertr~glichkeit der Richtigkeit und Falsch- heir einer Aussage wird postuliert. Die Falschheit der Identit~tt zweier Dinge l~Bt sich unter Umst~nden di rekt beweisen. Im tibrigen wird die Negation komplizlerterer Ausdrticke auf die einfacherer zurtickgeftihrt. 4 . Es kommen nur 'allgemeine Dingvariable vor, for die beliebige Dinge eingesetzt werden kSnnen und (wenigstens der Idee nach) allgemeine Aussagenvariable, fiir die beliebige Aussagen eingesetzt werden kiinnen. Diese Einsetzung ist auch dann gestatte L

~) W. ACKSRMA~N, Widerspruchsfreier Aufbau der L0gik I. Typenfreies System ohne tertium non datur. Journal of Symbol Logic 15, Nr. 1 (1950),. S. 33--57.

w. A&ermann: Widerspru&sfreier Aufbau einer typenfreien Logik. '~65

wenn z. B. das Prinzip 2. dadureh ver le tz t wird, da t rotzdem die wesentl iche Form des Schlusses gewahr t bleibt. - - (2berhaupt wird eine Impl ikat ionsbeziehung bei beliebigen Einsetzungen ffir Variable als gfiltig angesehen, falls sie richtig ist, wenn man die Variablen auf gewisse verntinft ige Wer te besehr~tnkt. Ha t man n~mlieh mit Formeln zu tun, die nieht no twendig riehtig oder falseh sind, so kann die Implikat ion nur als ein rein formaler l~bergang yon einer Formel zur ande ren aufgefafl t warden, der bei Einsetzungen fiir e twa vorkommende Variablen gi i l t ig bleibt.

w

Das Axiomensystem.

Das Zeichenmaterial bes teht aus ( a )Ze i chen ffir freie Variable a, b, c, a, , a.,, . .. ; (b) Zeiehen fib" gebundene Variable x, y, z, x,, x.~, . . . ; (e) Zeichen ftir Aussageverknf ipfungen &, v , - - , - - ~ ; (d) den Zeichen 2, ~), 2 # , . . . ; ( e ) den Zeiehen { }, ( ) , ( , ) , . . . ; ( f ) d e n Zeiehen (x), (Ex), (y), ( E y ) , . . . ; (g) Zeichen ffir spezielle n-steltige Pr~dikate (z. B. kleine o'riechische B u ch s t ab en ) a s,/~k, evtl. auch andere Symbole wie = (Zeichen fiir ein s pezialles zweistelliges Pradikat) .

Die Definition yon ,,Formel" und ,Term" gesehieht durch simul- tane Rekurs ion naeh dan folgenden Regeln:

(1) Zeiehen ftir freie Variable und fttr spezielle Pr~dikate sind Terme.

(2) Sind ~,, .... , a~ und b Terme, so ist {b} (a~, . . . , a,) eine Forinel, (Stat t {~} (a, b) schreiben wir a ~ lb).

(3) Mit ~/ ist ~.l Formel. (4) Mit 9.1 u n d ~ sind (~[)& (~), (~[)v (~), (~)-~ (~) Formeln. (5) Es sei ~ ( a , , .... , a,,) eine Formel mit den freien Variablen

a, , . . . . a,,, in tier die gebundenen Variablen x , , . . . , x , ~ nieht auftreten. 9 / ( x , , . . , x,) bezeichnet das formel~thnliehe Gebilde, das man erh~tlt, wenn man in ?I(a,, . . . , a,,) jedes vorkommende a~ durch x~ ersetzt, k, . . . ~ ( ~ l ( x , , . . . , x,,)) ist dann ein Term. Ebenso wie ftir a, , . . . , as und x , , . . . , x,, gilt die Regal entsprechend aueh ftir andere freie und gebundene Va~:iable.

(6) Die Formel ~.l(a) enthalte die freie Variable a, abet nieht die gebundene Variable x. Dann sind aueh :(x)~(x) und ( E x ) ~ ( x ) For -" meln, wobei ~[(x) aus ~/(a) so ents teht wie ~/(x,, ..., x,,) aus ~ (a , , ..., a,~) bei der vor igen Regel. Die Regel gilt entsprechend ftir andere freie und gebundene Variable.

�9 Beim prakt ischen Gebraueh der Formeln lassen wir die Klammern vielfaeh w e g , wenn .die Art der Wiederhinzuf t igung eindeutig ist. Start {y}(x, , . . . , x,i) sebrejben wit z . B . YX~ . . . x,,; bei &, . . . 2, lassen wir die folgende Klammer meist fort, und ebenso in vielen anderen F~tllen. Weitere Klammerersparnis erzie]en wir dadureh, dal~

Mathematiache Zeitschrift. Bd, 55. 24

366 W. A&ermann:

wir festsetzen, d a ~ V stKrker binder als & und -~, ferner & starker. als ~ . Fehlen hinter (x), (Ex), . . . die zugeh~irigen Klammern, so is t das so zu verstehen, daft die Zeichenkombination bis vor das n~tchste Zeichen v, &~ -~ in Klammern einzuschliel~en ist~ bis zu dem diese Kombination eine Formel ist, bzw. durch Ersetzung yon gebundenen Variablen durch ;freie in eine Formel tibergeht:

Wir geben das Axiomensystem in Form von Axiomenschemata~ indem wir auf die 'explizite Einfiihrung yon Aussagevariablen ver- zichten. 9/,!~, ~ bedeilten dabei bel'iebige Formeln , 9/(a) eine solche, die die freie Variable a enthalt, usw. Der Zusammenhang yon gleich- zeitig auftretenden 9/(a) u.nd ~[(x) ist wie bei der Regel (6) zur Bil- dung yon Formeln und Termen. ~0,, . . .~ b,, u,, . . . bedeuten irgendwelche gebundene Var iable ; a, b, r irgendwelche Terme.

I. G r u n d f o r m e l n d e r p o s i t i v e n A u s s a g e n l o g i k .

(la) 9 / & ~ - ~ 9/ (lb) 9 / & ~ - ~ 8 (2 a)_2-~ 9 /v ~ (2 b) _~-* 9/v 8 (3) ?l:&8 v(~-->.8 v (9/&~) (4) ( :9 / - /8 i & (~ --,- ~) -,- (~ ~ 8 & ~)

(5) ( ~ - , . ~ ) a (8 ~ : ) - , . (.9/v ~) ~ ~) (6) (9/.-,. 8) a (8 --,. ~) -,. (~ ~ e) (7) ( z '~ 9/)--,. (8 ~ 9/): (s) ( s 9 /v 8). ~ (s 9/) v (F ~ 8) (9) ( / ~ 9/) -~ 2:

(1) (2) (3) (a) (5) (6)

(7)

(Sa) (8 b)

(J)

II. F o r m e l n d e r F r ~ d i k a t e n l o g i k .

(x) 9/(x) -~ 9/(a) ~(a) ~ (Ex) ~(x) (x) (9/-~ 8 (x)) -~ (~ ~ (x) 8 (x)) (x) (9/(x) -,- 8 ) -,. ((E x) ~I (x) -~ !~)

(x) (9 / v 8 (x)) ~ ~ v (x) 8 (x) 9/ & (S x) f8 (x) -,. (E x) (?l & 8 (x))

( F ~ (E x) 9/(x)) -~ (E x)(F-~ 9/(x))

(F-~ 7 1 ( a , , . . . , a,))-~ {~, . . . &, ,~/(x, , . . . , xn)} (a,, �9 . . , a,) (x, , . . xn 9i (x:,, . : . , x,} (a,, .... , a,~)~ (F ~ 9/(a,, . . . , a,)).

t, II. F o r m e l n f t i r d i e N e g a t i o n .

(2b) ~ -+9 /

Widerspruchst~reier Aufbau einer typenfreien Logik. 36~

(3a) 2 v ! ~ o 2 & ! ~ (3b) 9.1& !~-~ ? i v

(5 b), ( F - . S) a (6 a) (E x) ~ (x) ~ (x) ~I (X) (6 b) (x) 2 (x) -~ (E x) 9/(X) (7 a) (x) 2 (x) ~ (E x) ?l (x) (7 b) (E x) 9.1 (x) -~ (x) ~/(x)

(S a) {~ , . . . . ~~ 9.1 (x,, :.., x.)} (a,,..., an) -~ {s . . . k~ 9/(xl, ..., x~)} (a,, ..., a,) (8 b) {k , . . &~ ~ (x,, ..., x[)} (a . . . . . , a~) ~ {2 2 . . . &~, 9/(x, , . . . , x.)} (a,, . . . , a,).

Bei II 3, II 5, II 6 darf ~I, bei II 4 ~ nicht die gebundene Variable x enthal ten.

IV. F o r m e l n f i i r s p e z i e l l e P r ~ t ' d i k a t e .

(1) a _ a (2)

Bei diesen Grundformeln enthal ten a und lb keine freie Variable. IV 2 ist dann und nur, d a n n zul~tssig, wenn a und b weder .vo l l s t~nd ig gleichgestal te t sind , noch durch Umbenennung der gebundenen Va- r iablen ineinander fibergehen. - - Wei tere Grundf0rmeln ftir spezielle Pr~tdikate kSnnen nach An~Iogie yon I V 1 und IV 2 in der folgenden Art gebildet werden : Ftir die geordneten n - T u p e l a,, . . . , an yon kons tan ten Termen sei" eine Klasse definiert, so daft sich ftir jedes derar t ige n - T u p e l angeben l~iI~t, ob es zu der Klasse geh(irt oder nicht. Sei a n ein Zeichen fiir ein spezielles n-stelliges Pritdikat. D a n n s ind alle Formeln a na 1 . . . a~ u n d a nb, . , . b~ Grundformeln , falls a,, . . . , am zu der K l a s s e geh(irt und b, , . . . , b,, nicht. Die Klasse

v o n n-Tupe!n mu]~ dabei so definiert sein, dal~ m i t a , , . . . , a,, a u c h a ' , , . . . , n'n dazu geh(irt, falls die a~ und at gleich sind oder ausein- ander d u t c h Umbenennung der g e b u n d e n e n Variablen (entsprechend der foigenden Regel (A)) entstehen. J e d e s Zeiehen a ~ darf nur ftir eine A r t yon Grundformeln gebraucht werden.

A b l e i t u n g s r e g e l n .

(A) In einer Formel darf man die gebundenen Variablen umbe- nennen. Dies geschieht so, dal~ eine gebundene Variable u i n n e r h a l b eines Zeiehens (u) oder ( E u ) o d e r fi, fi fi, usw. und innerhalb der zu- gehSrigen Klammer~ die den Wirkungsbere ich die~es Zeichens ab- grenzt, iiberall durch eine andere Variable t~ ersetzt wird, vorausge- setzt dait dutch die Umbenennung [iberhaupt wieder eine Formel entsteht .

(B) In einer Formel darf man e ine freie Variable an allen S te l l en ihres Vorkommens durch den gleichen Term ersetzen.

24".

368 W. Ackermann:

(C) Aus 91 und~3 erhglt man ,91 & ~. (D) Aus 92 und 92-~ ~3 erhglt man ~3. (E) Aus 9.1 erhglt man F-~ 92. (F) Aus einer Formel 92(a)erh~tlt man (x)92(z). Alle GrUndformeln Sind nut zul~tssig, wenn sie wirklieh Formeln

im Sinne unserer frtiheren Definition sind.. Ebenso diirfen die Ab- leitungsregeln nur gebrgueht werden, wenn sie wieder Formeln lie- fern. Das Zeiehen F, das bei der Aufstellung der Grundformeln gebraueh.t wurde, ist eine 2;bktirzung ftir die Formel -- _ _ , die dutch Einsetzung in IV 1 beweisbar ist.

Es dfirfen nun zu dem bisherigen System weitere Grundformeln hinzugefiigt werden, die wit abet nieht von vorneherein angeben

r - - " O " " kiinnen, sondern bei denen die Z.ulass~,ke~t ihrer Aufstellung yon einer beweisthe0retisehen ~Tberlegting abh~tngt. Wir wollen zun~tehst jeder F ormel, die mit tlilfe von Grundformeln I IV und Regeln (A)--(F) abgeleitet wird, eine natiirlighe Z aht beziiglieh dieser Her- Ieitung zuordnen, (lie wir ihren Rang nennen. Eine Grundformel er- h~ilt den Rang 1 mit Ausnahme der Grundformeln I 4. I 6. II 3. III 52, die den Rang 3. erhalten. Aul~erdem erhalten diejenigen Grundform~'ln I 2a . I 2b und III 2a . die mit F-~ beginnen, den Rang 2. Die Regeln A, B und F lassen den Rang unver~tndert. E erh~iht den Rang um 1. Bei C ist der Rang der Konklusion gleieh dem Maximmn der Rangzahlen tier Pr~imissen. Bei D ist der Rang der Konklusion gleieh dem Rang yon 9.i. falls.-.d_e! 7 Rgng yon ~ ~ 1 i s t . Ist im tibrigen der Rang yon 9 2 - ~ n + l und m d e r Rang von 92, so ist der Rang von ~ Max(re, n). Den Rang der End- f0rmel einer Herleitung nennen wir aueh kurz den Rang der Her- leitung. ~ Es sei nun 92(al irgend eine Formel. die die freie Variable a enthNt. Fiir jeden konstanten Term a. ftir den 92(a) tlberhaupt eine Formel darstellt, lasse sieh eine Herleitung ftir 92(a) angeben. und z~var so, dalt keine Herleitung einer Formel 92(a) einen gr61~eren Rang hat als eine bestimmte Zahl lc und dal3 dieser Rang bei einer Herleitung aueh wirklieh vorkommt. Dann dtirfen wir 92(a) als weitere Grundformel hinzuf~igen, deren Rang tibrigens k sein soll, Wir wollen derartige Grundformeln mit V 1 bezeiehnen. Wir dtirfen weiter Grundformeln ~(a) hinzuftigen, wenn ftir jeden konstanten Term a. f(ir den ~(a) tiberhaupt eine Formel darstellt, sieh" eine gerlei tung f[ir ~(a) aus Grundformeln I IV und V 1 .angeben Iggt uncl zwar so, daI~ bei allen Herleitungen ftir eine Formel ~(a) ein bestimmter Rang nieht tibersehritten wird. So kommen wit zu Grundformeln V 2 und welter entspreehend zu Grundformeln V 3, V 4 usw. Wit haben dabei yon der Aufstellung neuer Grundformeln gesproehen und nieht ges:/gt, daf~ es sieh bei der (~ewinnung dieser Formeln V 1, V2, . . . um eine besondere Ableitungsregel handeit. In der Tat seheint m~s der Ausdruek ,,Ableitung'sregel" nieht ganz am Platze.

Widerspruchsfreier Aufbau einer typenfreien Logik. 369

Denn einmal wttrde es sich um eine Ableitungsregel mit unendlich vielen Pr~missen handeln, so dal~ keine 'strenge Formalisierung des Denkens erfolgt, da ja die Tatsache, dal~ ftir jede der unendlich vielen Pr~tmissen eine formale Ableitung angegeben werden kann, ein Er- gebnis inhaltlicher I3bertegungen ist. Zum and~ren kommt bei uns der besondere Umstand hinzu, dab bei einer Regel dieser Art die Gewinnung der Konklusion nicht nur davon abh~ngen wiirde, dal~ die Pr~tmissen iiberhaupt gewonnen werden, sondern auch wie sie gewonnen werden. Das wiirde meiner Ansicht nach allein die Nicht- zul~tssigkeit der Rege l ars logisches SchluItverfahren bewirken. Es kommt mir hier nun darauf an zu zeigen, dal~ man gewisse weitere, nach bestimmten Prinzipien gewonnenen Grundformeln zu den For- meln I--IV hinzuftigen darf, ohne dal~ die Widerspruchsfreiheit verloren geht. U n t e r einem bestimmten formalen System wiirde das System de r Grundformeln I - - I I l und eine bestimmte Auswahl aus den Grundformeln IV, V zu verstehen sein, die sich yon vorneherein beschreiben l~tBt. Die Gesamtheit der Grundformeln V in den Wider- spruchsfreiheitsbeweis einzubeziehen, bestehen keinerlei Bedenken. Regeln yon ~thnlichem Charakter wie unsere Regel zur Aufstellung, der Grundformeln V sind yon P. LORENZEN und K. SCH{JTTE verwandt worden~). Sie fiihren dort den Namen Regel der Induktion oder Regel d e r unendlichen Induktion.

Um ein Beispiel fiir eine Aufsteilung yon Grundformeln V zu geben, zeigen wir, dab die Formel a --= b v a ~ b eine Grundformel V 2 ist. Es sei n~tmlich 5 irgend ein konstanter Term. Fiir jeden anderen konstanten Term a ist dann entweder a ~ 5 nach IV 1, eventuell unter Hinzunahme der Regel (A) beweisbar, oder abet nach IV 2 a ~ 15. In jedem Falle ist also mit Hilfe der Grundforme[ I 2a oder I 2 b u n d d e r R e g e l ( D ) a - - = b v a - - = w beweisbarundz~vardurch einen Beweis yore Range 1. Demnach i s t abet a -- 5 v a -- w eine Grundformel V 1. Da dies fiir jeden Term 15 gilt, ist a ~ - b v a = b eine Grundformel V 2. Im allgemeinen werden iiberhaupt die Grund- formeln V in der Hauptsache dazu benutzt, den Satz vom ausgeschlossenen Dritten ffir besondere F~ille einzuftihren.

Zum Gebraueh der Identitgt in unserem Kalkiil bemerken wir noeh: a ~ 15 bedeutet nicht nut, dab a und 5 die gleiche Bedeutung haben, sondern dab sie auch formal in gleicher Weise gebildet sind (abgesehen yon der Benennung der gebundenen Variablen). Die Rela- tion --= hat also einen metalogischen Charakter. Das gilt aueh zum Teil ftir andere mit Hilfe tier Grundformeln I V eingeffihrten spe-zielle

2) p..LoRE~-ZF,.X., Konstruktive Begriindung der Mathematik. Math. Zeitschrift 53 (1950), S. 162--20-9.

K. Scai~'rwE, Beweistheoretische Erfassung der tmendlichen Induktion in der Zahlentheorie. Math. Ann. 122 (1951): S. 369--389,

370 W. A&ermann:

Pr~tdikate. D~s entspricht tibrigens ganz der Tendenz d.ieser Arbeit, die ein Nebeneinander yon mehreren metalogischen Stufen m6gli~hst vermeiden will.

Um die Widerspruchsfreiheit des Axiomensystems zu zeigen, ge- niigt es, die Nichtableitbarkeit yon F darzutun.

w

Ein zweites Axiomensystem.

Die Durchftihrung des Widerspruchsfreiheitsbeweiscs geschieht im Prinzip nach der gleichen Methode wie in meiner in Anm. 1 zitierten Arbeit, in der ein Widerspruchsfreiheitsbeweis ftir das System ohne die Grundformeln V und IV angegeben wurde. Der friihel:e Beweis beruhte darauf, dal~ sich die Abtrennungsregel aus einer Beweisfigur entfernen liefl. Infolge der zus~tzlichen Grundformeln V ist aber nicht mehr eine vollst~tndige, sondern nur noch eine teilweise Entfernung der Abtrennungsregel miiglich, die damit zusammenh~tngt, dad der intuitionistische Charakter des Axiomensystems verloren gegangen ist.

Zur Durchffihrung des Widerspruchsfreiheitsbeweises ist nun das in w 2 angegebene Axiomensystem weniger geeignet. Ich benutze dazu einen anderen, im folgenden zu entwickelnden Formalismus, der nur zu diesem Zwecke eingeftihrt wird und sonst weniger prak- tisch ftir deduktive Zwecke ist, schon weil er (ab_sichtlich) nicht der Bedingung der Unabh~ngigkeit der vorhandenen Schlugiweisen gentigt. Um die Grundidee der teilweisen Entfernung der Abtrennungs- regel durchzuftihren, erweist sich eine Form des Kalkfils als zweck- m ~ i g , die in gewisser Weise an den GENTZE~chen Sequenzenkaikfil erinnert a). Doch werden keine Sequenzen benutzt, sondern statt dessen Formelreihen 21, 2 , . . . , 2 , , wobei die ~l bis 2 , Formeln im Sinne von w 2 sind, Die Nebeneinanderstellung der dutch Kommata getrennten Formeln hat den Sinn einer Disjunktion, obwohi formal zwischen 2 v !~ und 2, !~ unterschieden wird4).

A n g a b e des A x i o m e n s y s t e m s : ,,Formel" und ,,Term" haben die gleiehe Bedeutung wie in w 2. Unter einer Formeireihe verstehen wir eine Reihe von durch Kommata getrennten Formeln oder auch eine einzige Formel, wenn die Formelreihe nur aus einem einzigen Glied besteht. Das Axiomensystem gibt an, wie Formelreihen abgeleitet werden.

Grundreihen sind alle Grundformeln des Systems yon w 2, ferner auch alle solche Formeln, die aus Grundformeln I III dadurch ent-

8) C~. GENTZEN. Untersuchungen fiber das logische Schliei~en. Math. Zeitschr. 39 (1934), 176--210 und 405--431.

~)-Disjunktionsreihen statt der GENTZF.Nschen Sequenzen werden auch yon K. SCHUTTE in der Abhandlung: SchluBweisenkalkfile der Pr~dikatenlogik, Math. Ann. 122 (1950), 47--65, benutzt.

Widerspruchsfreier Auibau einer typenfreien Logik. 37~

stehen, dais ffir die allgemeinen freien Variablen entsprechend der Regel B yon w 2 irgendwelche Terme eingesetzt werden. Eine Aus- n a h m e bilden die Grundformeln der Form T ' - ~ F v ? t ; F - ~ I y F ; F-~ F . Diese s ind keine:,GrUndreihen. Mit jeder Grundreihe ist ferner jede andere Formelreihe ~Grundreihe, die daraus durch Umbenennung der gebundenen Variablen entsteht.

A b l e i t u n g s r e g e l n .

Wir bezeichnen, ~Lhnlich wie GENTZ~N, mit ~ O, ~ , , O~, . . . Formel- reihen unbestimmter Art; leere Formelreihen sind dabei eingeschlossen. Wir geben die Ableitungsregeln in Form von Ableitungsschemata, die i m allgemeinen keiner weiter.en Erk]~rung bedtirfen. Die Sche- mata zerfallen in drei verschiedefie Gruppen, die wi r durch ein vor- gesetztes S, N oder U andeuten.

S 1 , - -

N1.

*N 3.

N5 .

N T . - - - -

N9 .

N l l .

*N 13.

N 15.

N16.

*N 17.

U 1.

U4.

U7 .

~,O 8 2 . ~ ,~ ,~ ,O $3 . ~ ,~ ,~ ,O W, ~, O W, 2, 0 ~, ~, 2, O

W,~[,~,O N 2. q~,~[,O W,~'O ~,?I V ~,O ~P', ~ & ~, o

~ , 2 - ~ ~, o ~ , ~ / - * ~ & ~, o

~,~1 V ~ ~, O ~ , ~ ~, O

~ , ~ , 0 ~,~,O N 10. ~,*~,O ~ , ~ - ~ , O

~, 2(a), O *N 12. ~' 2(a), O ~, ( E x) 2 (x), 0 % (x) ~ (x), 0

W, ~/-~ ~(a), O *N 14. W' ~[(a)~ ~' ~ ~, ~1 ~ (x) ~ (x), O ~, (E x) 2 (x) -~ ~, O

W, ~ (~, ..., a~), O

T, ~(a,, ..., a,~), O w, { ~, ... ~ ~ (Xl, ..., x~)l (a,, ..., a,~),

~, ~ (a), 0 N 18. ~u, ~ (a), O

~, ..., ~,,, 0,~, ..., ~)~

372 W. A&ermann:

Alle Schemata gelten nat~h'lieh nur unter der Bedingung, dab wieder eine Formeh'eihe herausk0mmt. Mit jedem Schema d[irfen Um- benennungen der gebundenen Variablen verbunden werden, ohne dab dies als ein besonderer Sehritt zghlt. Im tibrigen bedtirfen die mit S und N bezeichneten Schemata im allgemeinen keiner weiteren Erklgrung. Die mit einem * versehenen Sehem0Aa d~rfen nur mit gewissen Einsehr~tnkungen gebraueht werden. Bei N 3, N 4, N 13 daft nieht mit [' identiseh sein ; bei N 12, N 13, N 14, N 17 dtirfen ~P" und O, aul~erdem bei N 13 ~2[ und bei N 14 ~ nieht die freie Variable a enthalten. Bei den U-Schemat, a bedeutet *F, (~1} eine der Formelreihen, die aus gr dadureh entstehen, dal3 man sa einmat oder mehrere Mate zwisehen die Formeln der Reihe ~/r einsehiebt, und zwar a n beliebiger Stelle, aueh am Anfang oder am Ende. Bei U 7, das n + 1 Pr~tmissen enth~tlt (n => 1), bedeutet Igi eine Formel der Gestalt ~ I i - , 3 ) ~ ( l ~ ] ~ n ; l ~ i < m ) .

Jede Formel, die aus dem Axiomensystem yon w 2 abgeleitet werden kann, l~ff3t sich aueh hier als Pormeh'eihe mit einem einzigen Glied gewinnen. Denn zun~tehst sind s~tmtliehe Grundformeln des fr{~heren Systems jetzl~ Grundreihen mit alleiniger Ausnahme der Pormeln F~-9.1V f ' ; / ' - , FV r2[ ; F-~ F. Diese lassen sieh aber aus der Grundreihe F mit Hilfe yon $1, N1, N 6 bzw. N7, N 6 gewinnen. Ferner sind d i e Ableitungsregeln C, D, E, F in den Regeln N 2, U 7, N 6, N 12 enthalten. Die Regel A, angewa~ldt auf Grundformeln, gibt wieder Grundreihen; im ~ibrigen dfirfen wir ja die Umbenennungsregel mit jedem Ableitungs- schema verbinden. Die Einsetzungsregel brauehen wir nieht; denn wir kOnnen, falls Einsetzungen vorkommen, diese immer weiter his zu den Grundformeln zuriickverlegen. Einsetzungen in die Orundformeln I - - I I I ergeben aber wieder Grundreihen. Einsetzungen in die Grundformeln V sind entweder wieder selbst derartige Grundformeln oder, falls es sieh um die Einsetzung yon konstanten Termen ftir alle freien Variablen handelt, beweisbar.

Um zu zeigen, dal~ das System yon w 2 widerspruehsfrei ist, dal~ also in ihm die Formel /~ nieht abgeleitet werden kann, gentigt es zu zeigen, dag das gleiehe fiir das vorliegende System zutrittt.

w Ordnungszahl einer Herleitung.

Eine He-rleitung f~ir eine Formelreihe in dem System des w 3 denken wir mls immer so aufgeschrieben, dal~ jede Formeh'eihe rim' einmal als Priimisse eines Schl'usses benutzt wird, indem wit die benutzten Grundreihen entspreehend oft hinschreil}en und eventuell Beweisketten wiederholen.

Wir ffihren zunltehst versehiedene Hilfsbep'riffe ein. deder Formel (nieht Formell'eil~e) der Herleitung ordnen wir zwei natiil'liehe Zahlen zu, (tie wir ihren Ra~y und ihren Grad nmmen.

Widerspruchsfreier Aufbau einer.tyoenfreien Logik. 373

Der Grad einer Formel ist durch ihre Gestalt alteill bestimmt, nicht aber der Rang. Dieser h~tngt yon der Stellung der Formel in der Her- leit, ung ab. Es kSnnen auch Fo{'meln der gleichen Formelreihe verschie- denen Rang haben, sogar wenn sie gleichgestaltet sind. Um den Rang bequemer zu definieren~ wollen wir bet den Schemata S 1--S3~ N ! - -N 18, U 1--U 7 zwischen Haupt- und Nebenformeln des betreffenden Schemas Unterscheiden. D i e Hauptformeln sind d i e , die mit deutschen Buch- staben bezeichnet sind, w~hrend die Reihe der Nebenformeln durch W, O usw. angedeutet ist. Jeder Forme]: der Konklusion eines Schemas~ mit Ausnahme der zu S 1 gehSrlgen Hauptformel sind Formeln der Pr~h~issen zugeordnet, n~tmlich eifier Hauptformel der Konklusion die Hauptformeln der Pr~missen und einer Fonnel der Reihe ~F oder t9, usw. die gleiche Formel yon "~P~ to usw. bet den Pr~tmissen.

Der Rang der einzigen Formel einer Grundreihe I - - IV ist nun 1, mit Ausnahme von 1 4, I 6, II 3, III 5 a, die den Rang 3 haben. Der Rang einer Formel der Konklusion eines Schemas bestimmt sich fiir die Schemata S 1 ~ S 3, N 1--N 5, N 7--N 9, N 11--N 14, N 17, N 18, U 1--U 3, U 6 dadurch, dal~ er der gr(ii~te Rang ist, der unter den zugeordneten Formeln der Pr~tmissen vorkommt. Das gleiche giit ffir alle Neben- formeln der Konklusion eines der tibrigen Schemata. Bet N6, N 15, N 16 und U 4 ist der Rang der Hauptformel der Konklusion um eins hSher, als er sieh nach dieser Regel ergeben wtirde. Bet N 10 ist der Rang yon ?{-~ ~ gleich der gr!)f~ten der beiden Zahlen m + 1 und n, wenn m de," Rang von ?[ und n der Rang von !~ ~ P ist. Die Haupt- formel der Konklusion yon S 1 hat den Rang 1. Bet U 5 hat die Formel .9[ den Rang ~n, falls n der gr5ftte Rang ist~ der bet den Formeln F->`9i vorkommt. ( ~ n = n - - 1 fiir n > 1; ~l = 1). Bet U 7 ist der Rang einer Formel c~i gleich Max (m~ 8n), falls @i die Gestalt ~ l j - ~ hat, m der maximale Rang unter den Formeln ~ in Wj~ (`9ij} und n der maximale Rang unter den Formeln ~,: ist. - - Fiir die Grundformeln V war der Rang schon in w 2 angegeben. Falls iibrigens die Herleitung im Rahmen des w 2 bleibt, ist der Rang einer Formel nach unserer jetiigen Definition der gleiche wie tier damals angegebene.

Der Grad ether Formel wird rekursiv definiert. Formeln der Gestalt {I)}(a~,..., a,) oder 9.I-~ !~ haben den Grad 1. Der Grad yon ~ ist um eins hSher als der yon 9/, der yon (x)gg(x) und (Ex)~[(x) um eins hOher als der yon ~I(a). Die Formeln ~l&!~ und 9 /v ~ haben den Grad m + n, wenn m der Grad yon ~ und n der yon ~ ist.

W.ir wollen wetter jeder Formelreihe einer Herleitung eine Ord- nungszahl zuordnen. Ich benutze dabei eine Symbolik fiir Ordnungs- zahlen, die ich an anderer Stelle entwickelt babeS). Mit HiKe dieser Symbo!ik wurden die Ordnungszahlen, von der Ordnungszahl 1 aus-

5) W. ACKERMANN, Konstruktiver Aufbau eines Abschnitts der zweiten Can- torschen Zahlenklasse. Math. Zeitschr. 53 (1951), 403--413.

374 W. Ackermann:

gehend, mit Hilfe des Zeichens q- und eines dreistell igen Klammer- zeichens dargestell t . Ftir 1 Jr l, 1 + 1 + 1, . gebrauehen wir die ge- wOhnlichen Zeichen 2, 3 , . . . als Abkfirzungen: Fiir I(1, 1, a) gebrauchen wir auch, falls a < (1, 2, 1), die gew~ihnliche Schreibweise co ~ als Ab- ktirzung ; ftir co~ + coe, coe q_ coe + co~, usw. schreiben wir a u c h co'~. 2, co e , 3, usw. Kleine griechische Buchs taben brauchen' wir im folgenden f t i r Ordnungszahlen t iberhaupt ; m, n, k, l, ftir Ordnungszahlen kleiner als co. Von den Ergebnissen der g e n a n n t e n Arbeit werden vor allen Dingen die Kriterien zur GrS~envergle ichung der 0 rdnungszah len im fop genden gebraucht , die ich daher hier noch einmal zusammenstel le . Es bezeichnen dabei ~, 0, ~, , ~ , a, usw. Ordnungszahlen der Form 1 oder (a, fl, ~,,).

I. l < a ( a ~ 1). II. zq + . . . + ~,, < z~ + . . . . {- z~,~ + z,,+~ + .., + ~m+k.

III. ~, + ..- q- ~ + 0, + " " + Ok < ~, + "'" + ~,,, + a, + �9 .. + ~ , falls 0, < a, (m => 0).

~v. (~, ~, ~,) < (., ~, r~), falls 7, < re. V. (a, fl,, 7,) < (a; fie, re), fails fl, < fix und 7, < (a, fl~, Y~).

VI. (a,, fl,, ~, ,) < (a,, fie, 7e), falls a, < a~ und /~,, 7, beide < (a~, fl~, 7e)- VII. (a,, fl,, r,) < (a,, fie, r,), falls (a,, ~,, 7,) ~ r, oder (a,, fl,, r,) ~ t~,

oder (a~, ill, 7~)--~__ a~. Mit Hilfe dieser Kri ter ien kann man fiir zwei verschiedene Ordnungs-

zahlen immd~" feststellen, welche die kleinei'e und welche die griil/iere ist. Das wird im folgenden ohne weitere Erkl~rung benutzt .

Die Zuordnung yon Ordnungszahlen zu den Formelreihen geschieht so: J ede Grundre ih% mit Ausnahme einer Grundreihe V, e r h ~ l t die Ordnungszahl 1. Grundreihen V 1, V 2, V 3~. . . haben die Ordnungs=

�9 zahlen (co~, 1, 1), (co~ + 1, 1, 1), (co~ + 2, 1, 1), . . . . Ha t die Pr~misse bei einem der S- oder N-Schemata die Ordnungszahl a (bzw. die Pr~missen die Ordnungszahlen a und fl), so ist a + 1 bzw. (a ~ f l )+ 1 die Ord- nungszahl tier Konklusion. Unter a + fl vers tehen wit dabei 'd ie ,,nattir- liche Summe" von a und fl im Sinne HESSENBnRGS; d. h. wenn . a-----a, + . - - § und f l - = : f l , + - - - + f l ~ wo die a~ und ~ en tweder 1 sind oder die Form (o ~, ~, ~) haben, so ist a ~/~ = 7, + ~'e + ' " + 7 , ~ + , , wobei die Reihe ~,,, 7 e , . . . , 7~+- eine abste igende Ordnung der a~ und fl~ darstellt . Ist bei den Schemata U 1 - -U 5 a die Ordnungszahl der Pr~misse bzw. die natiirliche Summe der Ordnungszahlen der Priimissen, so ist (1, 1, a) die der Konklusion. Bei U 6 sei r tier grOl~te Rang, tier unter den Formeln 9.1 und ~ vorkommt, g der Grdd yon ~, a die natiirliche Summe der Ordnungszahlen der Pr~tmissen. Die Ordnungszahl der Konklusion ist dann (co~r§ 1, a)o Bei U 7 m6ge r der maximale Rang sein, tier unter den F0rmeln ~) , , . . . , ~),~ der K~vaklusion vorkommt. Die Pr~tmissen ~P'~,(92,) . . . . ~/)',~,(~) und O,(~,}, . . . , (~m) mOgen die Ordnungszahlen ~ , . . . , a~ und fl haben. Die Ordnungszahl tier Kon-

Widersprud~sfreier Aut'bau einer typenfreien Logik 375

klusion ist dann (co' r + co,/~, , , -i- % ~- "'" -i- u,,). Unter der Ordnungszahl einer Herleitung ve r s t ehen wit die Ordnungszahl der Endreihe der Herleitung.

I. Eine Herleitung, ,die die Grundre ihen 'v nicht benutzt, hat eine Ordnungszahl, die k le iner .als @3 1, 1) ist.

Die Grundreihen I IV haben n~mlieh die Ordnungszahl 1, die kleiner als (co3, 1, 1) ist.. Ferner gilt: Ist , < (co~, 1, 1), so aueh ~ + 1

u n d (1, 1, ~). Sind u und {~ beide kleiner als (co'~, 1, 1), so aueh a-i-/~, (co-~ + g, l, a) und (co'~r - co, ~, t~). Das ergibt sieh mit Hilfe der ange- gebenen Kriterien fiber die Gr66envergleichung der Ordnungszahlen. Ebenso k6nnen wir zeigen, dal~ die Ordnungszahl einer Hefleitun~, die nut Grundreihen I IV und V 1-benutzt, kleiner als (co'~+ 1, 1, 1) ist, usw. Dieser Satz besagt also nichts anderes, als dal~ wir die Ord- nungszahlen der Grundreihen V. die ja die Form ~(a) haben, so fest- gesetzt haben, dal~ wir fur jede Formel ~(ct) mit konstantem a eine Herleitung mit kleinerer Ordnungszahl angeben k6nnen.

II. Andert man bei einer Herleitung den Beweis fiir eine dort be- nutzte Formelreihe so ab, dal~ die Ordnungszahl dieser Formelreihe sieh verkleinert und dal~ keine Formel dieser Formelreihe einen gr61~eren Rang als vorher erh~tlt, und l~l~t man im fibrigen die Herleitung un- verandert, so wird die Ordnungszahl der gesamten Herleitung verkleinert.

Zun~,ehst geht n~mlieh aus der Definition des Rangs h~rvor, dal~ in dem unverEnderten Teile der Herleitung keine Formel einen gr61~eren Rang' erh~tlt. Ferner geht aus tier Art der Zuordnung yon Ordnungs- zahlen zu den Formelreihen hervor, dal~ die Ordnungszahl einer Kon- klusion kleiner wird, falls die Ordnungszahl wenigstens einer tier Pr~missen kleiner, die der etwa vorhandenen anderen nieht grSl~er wird und tier Rang keiner Formel grSfSer ist als vorher.

III. Man habe eine Herleitung ftir eine Formelreihe. die eine einzige freie Variable enth~lt. Betrachten wir nun eine zweite Formelreihe, die aus der ersten dadurch entsteht, dal~ die freie Variable fiberall dureh einen konstanten Term erset i t wird. Ffir diese Formelreihe l~l~t sieh dann eine Herleitung angeben, deren Ordnungszahl nicht grtil~er ist als die der ersten. Ferner hat jede Formel der zweiten Endreihe einen nicht grS~eren Rang als die entsprechende Formel der ersten Endreihe.

Wit verlegen n~tmlieh die Einsetzungen bis in die Grundreihen zurfic.k, wobei der Beweiszusammenhang dutch die Schemata erhalten bleibt. Der Tatsache, dal~ einige Formeln der Herleitung infolge tier Einsetzung ihren Formelcharakter verlieren kSnnten, kSnnert wit leicht dadurch begegnen,, daf5 wit mit einigen Schemata geeignete Um- benennungen tier gebundenen Variablen verbinden. Einsetzungen in die Grundreihen I III ergeben aber wieder Grundreihen vom gleichen Rang und der gleichen Ordnungszahl. Einsetzungen in die Grund-

376 w. Ackermann:

formeln V lassen sich beweisen und zwar so, daft die Ordnungszahl der dureh Einsetzung entstehenden Formel n ieh t grSger ist (Satz I). Der Rang ist ebenfalls gem~tl3 der Definition der Grundformeln V nieht griSger.

w

Der Widerspruchsfreiheitsbeweis.

Wit betrachten im folgenden nur solche Iierleitungen, bet denen die Endreihe keine freien Variablen enth~tlt. Ferner diirfen wir an- nehmen, dal~ eine derartige Her le i tung keine aberfltissigen freien Variablen enth~lt. Eine freie Variable heii~t iiberfliissig, wenn sie in ether der Pr~tmissen, abet nicht in der Konklusion auftritt, abgesehen von den bet den Schemata N 12, N 13, N 14, N 17 wesentlichen freien Variablen. Diese tiberfi~issigen freien Variablen kSnnen wit. n~mlich immer dutch Einsetzung entfernen. Unter dem Endsti~ck ether Her- leitung verstehen wir folgendes: Es geh0rt dazu die Endformelreihe, ferner mit jeder Formelreihe auch deren Pr~missen, soweit diese keine freien Variablen emhalten, sonst aber nichts. Eine ,,oberste" Formel- reihe eines Endstiicks kann also nur nach "N 12, ~ 13, N 14, N 17 zustande kommen, falls sie nicht Grundreihe ist, keinesfalls aber dm'ch ein U-Schema.

Es liege nun eine Herleitung vor, bet der eine Formelreihe des Endstiicks durch ein U-Schema zustande kommt. Wir zeigen, dal~ wir dann die Herleitung so ver~tndern kSnnen, dal~ sie eine kleinere Ord- nungszahl erh~tlt. Dieser Nachweis wird den Hauptteil der nachfolgenden Ausftihrungen ausmachen. Zun~tdhst k(innen wir im Endsttick eine Formelreihe finden, die nach einem der Schemata U I ~ U 7 zustande kommt, w~hrend ihre Pr~missen entweder Grundformeln sind Oder aber nach einem der Schemata S 1--S 3, N 1--N 18 sich ergeben. Wir unterseheiden die folgenden F~lle:

A) Es set (~ die Formelreihe, die als Konklusion des U-Schemas auftritt. Eine Pr~tmisse ~von ~ entstehe dfirch ein Schema S 1--S 3, oder dureh ~ ein Schema N 1--N 18, im tetzten Faile abet so, da~ keine Hauptformel des U-Schemas auch Hauptformel des N-Schemas ist~

Handelt es sich um ein Schema mit e t h e r PrStmisse ~, to wird diese ~ /~ormelreihe ~ jetzt als die eine Pr~misse des U-Schemas genommen; denn die Hauptformeln des U-Schemas kommen hier ja in gleieher We.ise vor. Auf d i e Kon.klusion d'es U-Sch.emas wird dann das betreffende N-Schema angewandt uud man erh~lt direkt oder naeh Anwendungen des Schemas S 3 w. ieder ~. Ebeliso ist es, falls es sieh um ein Schema. S 1--S 3 statt des N-Schemas" handelt. Unter Um- st~tnden erh~tlt man dann auch aus ~ direkt ff~ naeh S 1, oder ~ ist mit @ identiseh. Der Rang der Formeln in der Formelreihe, deren Beweis ge~tndert wurde, ist dabei nicht gr61~er geworden. ~ habe nun

Widersprud~sfreier Aufbau einer typenfreien Lbgik. 377

die Ordnungszahl a. Die Ordnungszahl von N bei der urspranglichen Herleitung is t a) (1, 1, ~ + 1), b) (toUr+m, 1. ~ - i - ~ + l ) , c) (ro~r+oJ, ~ + I, fl),

Bei der ver~tnderten Herleitung ist sie hSehstens

a) (1, 1, ~ )+ n, b) (o~r + m, 1, r fl) + n, c) (~r ~ , . , ~)<n, d) (co'r+co, fl, a-~7,+ .. . +Tk)q-n oder tiberhaupt nur a + n. Sis ist also in jedem Falle kleiner geworden.

Handelt es sich um ein N-Schema mit zwei Pr~tmissen ~, und ~._,, so geht man ~thnlich vor, indem auch hier dis Reihenfolge des U- Schemas und des N-Schemas vertauseht wird. Wir wenden das U- Schema zweimal an, indem eimnal ~, und zum anderen ~ als die sine Pr~tmisse des U-Schemas genommen wird, w~thrend die anderen bleiben. Auf d i e beiden Konklusionen der U-Schemata wendet man das N-Schema an und erhglt dann (~, eventuelt unter weiterer An- wendung yon S 3. ~:)und ~ mSgen die Ordnungszahle n a und .fl haben. Die Ordnungszahl yon @ bei der ursprfingtiehen Herleitung ist

a) (1, ~, ~ 4 ~ + 1), b) (~ , -+, , , , 1, ~-~4r+1), c) (~o-~r + ~o, . r r), d) (eo'~r+co, 7, a @ f l - i - d , ; . . -~ dk+ l ) .

Bei der neuen Herleitung ist sie

a) (1, 1, ~ ) 4 (1, ~, ~) + . , b) (roar+m, 1, a-~),)Jc(co2r+m, 1, f l+7)+n,

6) (~o' r + ~o, ~, ~,) ~- (o,' r + ~o, ~, ~,) + ~,

d) (co'r+ to, 7, a ; d , + ' " + 8~)+(d~r+r~ Y, ~ 2 t - a , 4 " " ~ - 8 * ) + n -

Sie ist also kleiner geworden. B ) Der Fall A sei ausgeschlossen, Jede Pr~tmisse des U-Schemas

ist also entweder Grundreihe, und zwar eine Grundreihe I--IV, da die Orunch'eihen V freie Variable enthalten, oder abex sie entsteht dureh ein N-Schema so,. dab eine Hauptformel der Konklusion des N-Schemas aueh Hauptformel der Pr~tmisse des U-Set)emas ist. Dieser Fail erfordert eine ausfahrliehe Behand.lung.

B 1) Es handele sich um ein U-Schema mit einer Pr~imisse, also um U1, U3, U4, U5.

Die Hauptformeln der Pramissen des U-Schemas haben hier die Gestalt 9 /v ~, ~, (Ex) ~(x) oder "F--, 9/. Keine dieser Pr~tmissen kann

378 W. Ackermann:

Grundreihe sein. Eine der Hauptformeln der Pramisse mug also Haupt- formel der Konklusion eines N-Schemas sein. D a s ist bei U 3 nicht m0glich, so dag dieser Fall a:usscheidet. Im iibrigen entsteht ~F, (9/v !~) ; ~F. ((Ex) ~(x)) oder ~F, ( P ~ 9/) entweder aus W,, ~, ~, ~ ; yr , 9/(a), ~F~; oder ~P,, 9/, ~/t bzw. aus W,, 9/, ~, W~, (9/v !~) ; ~F,, 9/(a), W, ((E x) 9.I'(x)) oder ~P'~, 9/, W~, (I '-+ 9/} nach N1, N l l oder N6. Im zweiten schwie- rigeren Falle wende t man auf die genannten Formeln j e t z t das betreffende U-Schema an, das W,, 9/, !~, ~I~.,, 9.I, !~; W,, 9/.1 (a), ~P'~, (E x)(F-+ 9.1 (x)); ~P',, 9/, W.~, 9/ liefert (~P',, ~P'2 ist mit ~ identisch).

Die erste und letzte Formel ergeben' durch Anwen.dung yon S- Schemata die ursprfingliche Konklusion des U-Schemas; die mittlere nach Anwendung yon N 6, N 11 und S-Schemata. Im ersten Falle ist es entsprechend einfacher, da die Anwendung des U-Schemas ganz wegfallt. Der Rang der Formeln der Reihe ~R, deren Beweis geandert wurde, ist nicht gr61~er geworden. Hat nun die Formelreihe, aus :der die Pramisse des urspriinglichen U-Schemas .naeh einem N-Schema entstand, die,Ordnungszahi a, so ist die Ordnungszahl yon ~ bei der m'sprtinglichen Herleitung (1, 1, a + 1), bei der neuen Herleitung hSchstens (1, 1, a ) + n (n < co), unter Umstanden auch kleiner. Demnach hat sich die Ordnungszahl verrin~ert.

B 2) Es handele sich um U 2. Hier kann O, <(E x) !~ (X)} nur nach N 11 aus einer Formel O, L!~ (a)i O.,

oder O,, !~ (a), O,, ((Ex) ~(x)} zustande kommen. Beim neuen Beweis erhalt man aus W,(9/} nach S 1 - - $ 3 W, O, i ?I, O, ; aus O,,~3(a),O~ naeh S 1 W, 0,, f~(a),O)~, aus den zule tz t erhaltenen Formeln naeh N 2 ~P', O,, 9/& !~ (a), O~, wel te r nach N 11 W, Oi, (E x) (9/& !~ (x)), O.~ und dann W, O, (Ex)(9/& !~ (x)) eventuell nach S 3. - - Ode r man erhalt aus W, (9/} und O~, !~(a), O~, ((Ex) !~(x)} zun~ichst nach U 2 W, O,, !~(a), O.,, (E x) (9/& ~ (x)), ferner ~P; O,, 9.I, O.,, (E x) (9/& ~ (x)) aus W, (9/) durch S 1 S 3, aus den letzten beiden Formeln W, O, (E x) (9/& !~ (x)), O,, (S x)(9/&!D(x))nach N 2 und N 11, dann W, O, (E x)(9/& ~ (x))durch S 2 und S 3. Es habe W~ (9/~ die Ordnungszahl a, die Pramisse yon O, ((Ex) f~ (x)} die Ordnungszah] ft. Die 0rdnungszahl yon W, O, (Ex)(9/& ~(x)) bei der ursprfinglichen Herleitung ist (1, 1, a + f l § 1), bei der neueh ist sic a ~ f l + n bzw. (1, 1, a ~ f l ) ~ a + n , also kleiner als vorher. Der Rang der einzelnen Formeln in der letzten Formelreihe ist dabei nicht grSl~er geworden.

B 3) Es handele sich um U6, also um das Schema W' (~) o,(~> ~,O 9./[ hs~t eine der Gestalten 1) ~, 2) ~ & ~, 3) ~ v ~, 4) 05} (a,, . . . , a,~),

5) -(x) ~ (x), 6 ) (E x) ~ (x), 7) ~ -~ ~. Abgesehen yon dem Falle 7) ist weder O', (g} noch O, (~} Grundreihe. ?l mtil~te namlieh 'dann die Gestalt 4) haben und ]5 ware ein Zeiehen ffir e in spezielles Pradikat. Da weder 9/ noch 9/ dann die Hauptformel der Konklusion eines N- Schemas sein k/innteu, mtil~ten beide Grundreihen sein, was nieht m0glieh

Widersprudasfreier Aufbau einer typenfreien Logik. 379

ist. - - In den anderen Fal len mOgen ~, (bzw. ~:, und ~ ) die Pr~tmissen yon ~P; (9/}, gO, (bzw. ~, und fie_.) die von O, (~) sein. Ferner woilen wit im folgenden eine leicht verst~indliehe Symbolik ffir Beweise gebrauehen. Unter Nk(~ , ; ~ ) verstehen wit eine Formelreihe, die aus ~, und '~.~ naeh Nk entsteht, unter UI($) eine solche, die aus der einzigen Pramisse t5t naeh U1 entsteht, usw.

1) 9/ habe die Gestalt ~. ~, ist hier O , , ~ , O , bzw. O , , ~ , O , , ( ~ ) . U6(ffr W,(~)) oder

U 6 (U6 (W, (~);:@,); W, (7~)) gibt bei der neuen Iterleitung, naehdem man , eventuell noah einige Male S 2 u n d S 3 angewandt hat, W, O. ~, (~) habe die Ordnungszahl a, m sei der maximale Rang der Formeln

in dieser Reihe, g tier Grad von ~. (~, habe die Ordnungszahl fl und k sei der maximale Rang tier Formeln ~ und ~ i n dieser Reihe. Sei ferner r b M a x (rn, k). ~F, O hat zuerst die Ordnungszahl (co 'r+g+ 1, 1, a 4 fl + 1) und hinterher ' die kleinere (co'r + g, 1, a -i- fl) + n bzw. (co~- r, + g, 1, (ro2 r; + g + 1, 1, a 4- fl) 4- •) + n (r,, r~ ~ r).

�9 2) 9/ habe die Gestalt !~ & ~. ~, ist_ ~',, ~, ~ bzw. W,, ~_, ~ ; , ( ~ & ~); ~ , . i s t ~,~, ~, ~.~ bzw.

~F,, ~, ~ , , ( ~ & ~ ) ; ~, ist O,, ~, (~, O.~ bzw. O, , !~ l ,~ ,O, , ( !~&~) . - - Es geniige, wenn wir hier und im folgenden die kompliziertere Gestalt der Pr~missen betrachten, da die einfacheren F~tlle immer entsprechend erle- digt warden, es sind nur wie schon bei 2) einige U-Schemata entbehrlich.

u 6 ( U 6 (i~, ; O, (~ a ~)); U6 (U6 (lt~; O, (~ &~)); U6 (~', ( ~ a ~ ) ; ~,))) gibt bei der verEnderten Herleitung ~, O, nachdem eventuell noch S-Schemata angewandt worden sind. Es bedeuten a; fl; 7; r ; g , ; g., die 0rdnungszahlen yon ~ ; ~ ; ~ , ; den maximalen Rang der Formeln ~, ~, !~, Is !~&~, ~ & ~ in ~, , ~, und 1~,; den Grad von !~; den Grad von ~. Die urspriingliehe Ordnungszahl yon W, O ist'(oo'*r + g, + g,, 1, a 4-fl 4- y + 2); bei der neuen Herleitung hat sie die kleinere Ord- nungszahl ( ~ r , + g,, 1, ~, 4- ~,) + n, wo

~, = (~r., + g , + g~, 1, a 4- 7 + 1),

d~ -= @'r, + g, + g,, 1, ft.4- ~, + 1), d , - ~ - @ ' r , + g , + g ~ , 1, a 4- fl 4 - / , + 1)

und r,, r.~, r~, r,, r.. ~ r: 3) 9/ habe die Gestalt ~ v ~ . ~__, ist .hier ~ , , !~t, ~, W,, ( ! ~ v ~ ) ; (~, ist O,, N,O,, (!~ v (~); (~, ist

O,, ~, O,, (i~ v ~). Die Vereinfaehung der Herleitung gesehieht ganz ~ihnlich wie im Falle 3).

4) 9/ habe die Gestalt (5} (a,, . . .~ a,). Soll die letzte Formal Hauptformel der Konklusion eines N-Schemas

sein, so ist die Gestalt yon 9.I genauer {~ . . . :~, ~ (x,, . . . , x,,)} (a,, . . . , a~). ~, ist k~,, ~(a i , . . . , an), ~I~, (9/}; t~, i s t O,, i~(a,, . . . , a,,), 0 , , (~1).

380 W. Ackermann:

U{) (U6 (~l; O' <~>); U 6 (~/]9 (~[); '(~l)) gibt (lie neue Herleitung yon ~P; O. ~ und fl seien die Ordmmgszahle n yon ~l und | r der maximale Rang der Formeln 9.1 und ~ in ~F, (g{) und O, (~), g der Grad yon !~(a, . . . , o,,). ~P', O hat zuerst die Ordnungszahl (~'~r + 1, 1, t~ ~- fl-~ 2) und hinterher h(ichstens die Ordntmgszahl

(r, < r ; r.-,, r, < r).

5) ~ habe did Gestalt (x)!8(x). ~, ist ~F,, ~3 (a), ~'~, ((x) ~ (x)} ; C~, ist O,, !3 (a), O.~, <(x) !3 (x)}. Naeh

Satz III yon w 4 erh~tlt man eine Herleitung ftir k~'~, ~3 (a), W.~, ((x) ~ (x)}, deren Ordnungszahl nicht grCif~er ist als die yon ~, und bei der keine Formel einen hOheren Rang hat als die en tsprechende vorher. Im iibrigen verfahren wir wie bei 4).

6) ?l habe die Gestalt (Ex)~3(x). ~, ist ~ , , 93(a), ~P;, ( (Ex)~(x)}; | ist O,,~(a), 0~, ((Ex)~(x)}.

Wit verfahren anah)g zu ,~). 7) ?1[ habe die Gestalt ~ - ~ ~. ~, ist O , ~, O~, ( ~ 2 ~ } ; ~ ist O1, ~ F, O~, (~--2~}. Der neue

Beweis fiir gr, O wird durch

u a ( u 7 (U7 (U6(~ , (~l>; ~ , ) ; '~, (~t)); u 6 ( ~ , (~) ; ~,)))

und eventuelle Anwendungen yon S-Schemata gegeben . Sei ~/ die Ordnungszahl yon W, (g[!; fl und 7 die yon qr und | m tier Rang von ~3 ir~ qr ; n d e r Rang yon ~ - + F i n @.~; k der maximale Rang der Formeln ~3--, @ in qr und @~; 1 der maximale Rang der Formeln !3-~ ~ in W~ (~-~ ~}. Die urspriingliche Ordnungszahl von ~, O ist ( co~r+l , J ,a~- f l~ -7+l ) , wo r ~ Max (m + l, n, k; l). Die neue ist h/3ehstens (1, 1, d,) + p (#< co), wobei

~, ---- (co ~ r, + co, ~ , ~,) (r~ Max (m, ~ ~, ~ n),

o~ = l~o "~ r~ + co, ~, ~) ' (r, = Max (m, ~ ~),

~ , = : @ ~ r + l , 1, a~-7), d . - ~ ( c o ' r § l , . 4 f l ).

Sic ist also kleiner geworden. B 4) ES handele sich um das Schema U 7, also um das Schema

~',, (~i> . . . ~ , (~d .O, <~,>, . . . , <~>

Wit unterscheiden folgende Falle: 1. 0 , (~1 ) , . . . , (@m>' se i Grundreihe, bestehe also aus einer einzigen

Forme] ?i ~ ~3; auf~erdem kann d a n n nut eine einzige andere Pr~misse des U-Schemas yon der Form ~, (?I) vorhanden sein. Die Konklusion ist gr, !3.

Widerspru&sfreier Aufbau einer typenfreien Logik. 381

Bei der Ver~inderung der Herleitung mfissen wir die einzelnen Grundreihen besonders behandeln. Die Nummer bei den folgenden, (~berlegungen zeigt jedesmal, um welche Grundreihe es sich handelt.

1) I 2 a : I 2 b , I I2 , I I I 2 a . In diesen Fi~llen erhalten wir W, ~ sofort aus W, (92} mit Hilfe

yon S-Schemata und N 1, N 11 oder N 7. Die Ordnungszahl yon W,.~ ist zuerst (co2 r + co, 1, a) und hinterher a + n. Der Rang yon ~ ist nieht grN~er als vorher.

2) 92 habe die Form ~ & 33. Das betrifft die Grundreihen I 1 a, I 1 b, I 3, I 4, I 5, I 6, II 6, III 1, III 4 a, III 5 a. W, (~ & 33} entsteht naeh N2 aus zwei Formelreihen WI, ~, ~2, (~&33} und W,, 33, W,, (~&33}, die die Ordnungszahlen a und fi haben, Sei r der maximale Rang der Formeln 92 in W, (92}. Die Ordnungszahl yon W~ ~ ist bei der gegebenen Herleitung (co '~ k ~ co, 1, r @ fl + 1). Hierbei ist k r, bzw. im Falle der Grundreihen 14, I I I 5 a , I 6 k = M a x ( r , 2). D e r R a n g yon ~ in W, 93 ist k. Wit wendei~ nun auf jede der beiden Prlimissen von W, (~.1} und die gleiehe Grundreihe wieder U 7 an und erhalten ~F,, ~, W~, und ~F,, 33, W~, ~. Beide Form61reihen'haben hSehstens die Ordnungs- zahten (~2 k + co, 1, a / und (co~" k + co, 1, fl), die wir zur Abkfirzung mit ~i und d~ bezeiehnen. Wir wollen di.ese Formelreihen ~ und | nennen. Der Rang der Formeln ~ und 33 in ~ und @ ist hSehstenS r, der yon !~ in beiden Reihen hOehstens k. Weiter gehen wir versehieden V0r, je naehdem um welehe Grundreihen es sieh handelt.

I 1 a, I lb." ~, ~ entsteht dann aus t~ bzw. | dureh S-Schemata. Die Ordnungszahl dieser Reihe ist also ~, + n bzw. ~ + n.

I3 . 92 hat d ie Form ~&33v@. Aus N, d .h . W~,33v~, ~ , ! ~ ergibt sieh naeh U 1 W,, ~ , ~ , W~, ~. Aus ~, d.h. W,, ~, ~P~, ~ e r g i h t sieh dureh S-Schemata W,, 33, 6., W~, 93, welter naeh N2 W~, 33, ~&~, W~, ~, naeh N 1 ~P',, 33 V (G& ~), ~/r2, ~, daraus naeh S 2 und S 3 W, ~ . Die Ordnungszahl der letzten Forme! ist (1, 1, ~) ~- ~, + n. Der Rang von ~ in W, ~ ist nieht grOf~er als vorher.

I4 , I5 , I6 , I I 6 , I I I 4 a . Aus ~ und'61 erhalten wir W,!~ dureh N 4 , N5, N3, U2, N9.

Bei I 4 und I 6 mtissen wir allerdings zun~tehst die Fiille aussehliegen, dal~ g[ die Form (F--* fs 8~ (F 2- 33) bzw. (F- , ~)& (~ -* 33) hat, da sonst die Schemata N 4 und N 3 nieht anwendbar sind. Die neue Ordnungs- zahl von W, ~ ist d~:q: d.. + n bzw. (I, 1, ~ j- ~,)+ n. Der Rang v o n ~

i s t niel~t grOi3er als vorher. I 4. 92 habe die Form (-P--* ~)& (F-* 3)). N 6 (N 2 (U 5 (~); U 5 (61))) und Anwendung von S-Schemata gibt den

neuen Beweis fiir gr, !~, ohne dai3 sieh der Rang yon ~ vergrOl3ert hat. Die neue Ordnungszahl ist (1, 1, ~,) ~ (1, 1, ~) + n.

I 6. 92 babe die Form (F--* fg)&(~--* 33). N 6 (U 7 (U 5 @); N)) und Anwendung yon S-Schemata gibt den neuen

Beweis ftir W,~3. Die neue Ordnungszahl ist hSehstens (co'~r+ co, d,,

Mathematische Zeitschrift. l~d. 55. 25

~8~ W. /kckermann:

(1, i, 6,)) + n; also kleiner als vorher i d a ~ r < Max (r, 2). Der ~R~.ng von ist nicht grSf~er geworden .

III 5 a. N 10 (U 5 (~); ~) und Anwendung von S-Schemata geben den neuen

Beweis ffir W, ~. (1, 1; ~,) 4 6~ § n ist die neue Ordnungszahl. III 1. U 6 (~; (~) und Anwendung yon S-Schemata. yr, ~ hat die Ordnun~'s-

zahl (co~r + g, 1, 6, ~ &2) q- n. 3) II 8 a. N 15 (U 5 (~P, (~f})) gibt die neue Herleitung. Die Ordnungszahl v0n

ist zuerst (co'~r + co, 1, a) und sp~ter (1. 1, a )+ n. Der Rang yon ~ is t nicht grOl~er geworden~ da mindestens eine der Formeln ~ in W, (~), n~mlich diejenige, die Hauptformel der Konklusion eines N-Schemas ist, einen Rang > 1 hat.

4) In den iibrigen F~illen, d . h . dem Vorliegen der Grundreihen I7 , I 8 , I 9 , II 1, II3~ I I4 , II5~ I I7 , I I 8 b , I I I 2 b , I I I 3 a , I I I 3b~ , I I I 4 b , I I I 5 b , I I I6a~ I I I 6 b , I I I 7 a , I I I7b~ I I I 8 a , I I I 8 b entsteht ~P', (~[} aus einer bzw. zwei Pr~imissen, die wir ~ bzw. ~:. und ~ nennen wollen und denen wir die Ordnungszahlen ~ und fl zuschreiben, nach N6, N G N6, N12, N12, N12, N12, N6~ N15, N7, N1, N8, N9, N10 , N l l , N18, N12, N17, N15, N16. S e i r der maximt~le Grad der Formeln ?i in ~, (~)2 k sei gleieh r bzw. gleich Max(r, 2), falls es s ich um II 3 handelt. Die Ordnungszahl von ~, ~ ist (~ k + r 1, a + 1) bzw. (o~*k+co, l , a ~ f l + l), Der Rang yon ~ in ~ , ! ~ ist k. Bei der neuen Her le i tung wenden wir zunliehst U 7 auf jede der Formeln und $ und die gleiehe Grundreihe an, entsprechend wie bei 2). Die entstandenen Reihen nennen wir ~ , bzw. ~:, und (~. Ihre Ordnungs- zahlen s ind hS~hstens (a~ ~ k + co, .1, ~) bzw. (~ k + co, 1, a ~ fl), die wit mit ~, und G bezeichnen. Aus ~, bzw. ~, und | erhalten wir nun ~/', !B in der folgenden Weise, wobe_i wir zum Sehluf~ angewandte S- Schemata nicht besonders erwiihnen. 17: N 6 (~,). 18: N 1 (N 6 (N 6 (U i (~,)))). 1 9 : durch S=Schemata allein. II 1 : dureh Einsetzung in die Herleitung fiir ~, :gemais Satz III yon w 4. II 3: N 13 (~,). Der Fall, daiS 9.I die Form (x)(T'=, G(x)) hat, mul~ unten besonders behandelt werden, d a in diesem Falle N t3 nieht anwendbar ist. II4: N 14 (~,). II 5: N 1 (N 12 (U 1 (~,))), I I 7 : U4(~,) . I I 8 b : N6. I I I 2 b : nur S-Schemata. I I I 3 a : N8(~,) . III 3b : N 1 (~,). I I I 4 b : N2(~, ;(~,) . I I I 5 b : N 1 0 ( ~ , ; ~ , ) . I I I 6 a : N 18(~,). I I I 6 b : N l l(~,) . I I I 7 a : N17(~,) . I I I 7 b : N12(~,). I H 8 a : N16(~,) . III 8b" N 15(~:,). - - D i e neue Ordnungszahl yon W, !~ ist h0ehstens ~, + n bzw. ~, ~ ~ + n, mit Ausnahme der F~ille I 8 u n d II 5. Hier ist sie (1, t, 6.,) + n, in' jedem Fal le aber kleiner als vorher. Ferner ist der Rang von !~ in ~ , i~ nich t grSiSer ats vorher. In den F~illen niimlich, in denerr bei der neuen Herleitung die den Rang einer Formel erh0henden Schemata N6, N 10 und U4 gebraucht ~erden, War d e r Rang tier betreffenden Formel in ~, kleiner als r.

Widerspruehsfreier Aufbau einer typenfreien Logik. 383

II 3. ~.1 hat die Form (x ) (F-~ ~(x)). N 6 (N 12 (U 5 (~,))) und Anwendung yon S-Schemata geben die neue

Herle i tung ft~r W, 23. Die Ordnungszahl der letzten Formel • (1, 1, d,).+n. Der R a n g von 23 • 67"+ 1, also ~ k, da in diesem Falle k - - Ma x (r, 2).

II. Be• dem Schema U 7 entstehe die Pr~tmisse O, (~,}, . . , (~,} durch ein N-Schema. In Frage k o m m e n nur die Schemata N 3, N 4, N 5, N 6, N 13 und N 14, Wir wollen die Pr~tmissenvon O, ~ , } , . . . , (~n} ~ und bzw. ~ nennen. Sic mSgen die Ordnungszahlen /~ und y bzw. ~I haben. Die Re• W,, (9.1,} . . . W,, (gin} haben die Ordnungszahlen a , , . . . , an. Die Ordnungszah! von g~,-d, h. W,, . . , W., O, ~1, - - ; ~m •

( c o ~ r + ~ , { ~ 4 - ~ + l , ~ , + . . . + ~ n ) bzw. ( ~ o ' r + c o , ~ + ~ , ~ , 4 . . . + a n ) ,

~ffenn 7" der max• Rang der Formeln ~ , , . . . , ~3,, • N3 . ~ • O , , ~ ( ~ . - ~ , 02, (~ ,} , . . .+ (~,,} und | • O , , ~ k ,

o=, ((~,}, .. ( ~ } . Aus ~ u n d den Re• W,, {~1,} . . . W,, {91n} erhalten wir naeh U 7 ~/r . . . , ~P,, O, ~, ~3,, . . . , ~m und aus dieser Formelreihe, W,, ('~1,} . . . q~n, (~ln) und (~ naeh g 7 e ineFormel re ihe , aus de• ~ sieh g~ durch S-Schemata ergibt. Die neue Ordnungszahl yon g~ • h6ehstens

(co'r + ~o, ~, ~, + . . + ~n + (co'~r + ~, ~, , , 4 " ' 4 ~-)) + n,

also kleiner als vorher . N 4. ~ • O,, 91j-, ~, O~, (~,}, . . . , (~,~} und (~ ist .O,, ~(j-+ $~, O~,,

(~,} . . . . . ( ~ } . ~&t~' • mit einem tier ~ identisch. Aus ~ , (9I,}.. .W,, {9.1n} und je einer der be• Formelreihen ~ und | erhalten wir naeh U7 W,. W,. 6). ~. ~),, . . . . ~ , , und W,, . . . . W,. 6), R, ~ , , . . . . ~m- aUS den letzten be• Formeln dutch N 2 und S-Schemata wieder g). Die Ord- nungszahl von g) • jetzt h6ehstens

~ ~"- r - co. ~ , ~ , 4- " ' + ~n ~ ; ~ co~- r + co , r , , , • " " -i- ~,~ l + m

N 5 . ~ ist 6),, ~ - ~ 3 ~ . O~, ~} , . . . . .{~} und ~ ist O~, g ~ , O.~. (~,}, . . . . (~m}, wobei ~ v ~' mit einem ~ identiseh ist. Wir erhalten zun~tehst aus W~, {?lj} naeh U I q~, ~. ~'~. welter aus W,, (91 . . . Wn, {9.In} und W~, ~, ~ und ~ naeh U 7 ~/x, . . . . W,. ~. 6), ~ , , . . . . ~),,. aus der letzten Formel. W,, X'?l,} . . . W,~. {9/[,~} und .(~ naeh U 7 und weiteren Gebrauch yon S-Schemata g). Die Ordnungszahl yon g) ist je tz t h0chstens

(co~r - - c o , ~', ~, 5_ . . . . @ ~ n + (co~r 4 - c o , fl , a , T " " S a n • 1, 1. a j ) ) ) + , .

N 6. ~ • 6)~, ~ . 6),, (~,}, . . . . ( ~ } . Aus W,, {9.1,'), . . . . ~ , , 91,,} und ~ ergibt sieh nach U 7 und S-Schemata g~. Die Ordnungszahl tier letzten Re• • (co~ r + co. ~, ~, - . . . @ an) - n.

N 13: ~ hat die Form O,. 2 l ~ ~(a), O.~, (~,}, . . . . {~,,~. Aus

~ , , ~ i ) , . . . . ~ , . (~tn)

und ~ ergibqc sieh naeh U 7 W,, . . . , W,, 6), ~'(a), ~ , , . . . . ~?,~, weiter naeh N 12 und S-Schemata g). Die Ordnungszahl •

(co~' + co, ~, ~, 4- - - -~- ~n) + - . 25 *

384 W. Ackermann: Widerspruchsfreier Aufbau einer typenfreien Logik.

N 14. ~ ist O,, @(a)--, ~3, 02, (~,), . . . . (~,~). Hierbei ist (Ex)@(x) gleich einem 9j~. ~ , (~j3 entsteht aus Wjl. @ (a), Wj~, (~j) nach N 11. Aus der letzten Formel, W,, (?I,) . . . W,, (~,,) (ohne We, (9~-)) und O, (~,~, . . . , (~m) erhalten wir nach U 7 W1, . . . . ~P~, ~.~, ~ (a), W~.I, 8, ~31 . . . . , ~)m. Nach Satz III yon w gibt es eine Herleitung ftir ~1, d. h. O1, $ ( a ) ~ ~3~. O,, ( ~ ) , . . . , (~m)~ so dal~ diese F0rmelreihe keine grtil~ere Ordnungs: zahl als ~ und keine Formel in ihr einen grtifSeren Rang als die entsprechende in ~ hat. Aus yr , . . . , W~, Wj,, $ (a), z/ss~ , ~3, , . . . . ~m und W~, (~,) . . . W,, (9~) und ~, erhalten wir naeh U 7 eine Reihe~ aus der sich ~ durch S-Schemata ergibt. Die Ordnungszahl yon $3 ist jetzt

(co~r + co. fl, ~ , - i - " ~ ~ -~ (co~r-~ co./~ + 1, ~, 4 - . - i - .j-1

_i_ ~; • ,~+~ 4 . . . 4- ,,)) + n, wobei a~ ~- 1 = aj.

Damit haben wir nun allgemein gezeigt~ dal~ man jede,Herleitung, bei der die Endreihe keine freie Variable enth~tlt und bei der eine Formelreihe des Endstficks durch ein U-Schema zustande kommt, in eine andere mit der gteichen Endreihe, abet kleinerer Ordnungszahl verwandeln kann. Dureh Fortsetzung des Verfahrens gelangt man also zu einer Herleitung~ bei d e r keine Formelreihe des Endstficks mehr dutch ein U-Schema entsteht. Zum Beweise der Widerspruchs- freiheit b le ib t -zu ~eigen, dab F nicht Endreihe einel, derartigen Herleitung sein kann. Wir wollen allgemeiner zeigen, dal~ eine Reihe F~ . . . . F nicht Endreihe sein kann. Eine derar t ige Reihe ist n~mlich keine Grundreihe. Ferner kann keine ihrer Formeln Hauptformel der Konklusion eines N-Schemas sein. Geh~irt also eine solche Reihe zum Endsttick, so mull sie nach S 1, $ 2 oder S 3 aus einer Formel der gleichen Ar~ zustande kommen, d. h. es mtil~teeine ,,oberste" Formel des Endstiicks v6n dieser Gestalt geben. Da abet die obersten Formel- reihen des Endstiicks, soweit sie nicht Grundreihen sind, nach N 12. N ]3, N 14 oder N 17 zustande kommen, kann tiberhaupt im Endsttick keine Formelreihe F,/~, . . . , F auftreten. Damit i s t die Widerspruchs- freiheit des Systems yon w und damit aueh die des Systems yon w gezeig~.

Die Herleitung der Mathematik aus dem in w 2 aufgestellten System wird in einer sich anschliel~enden Abhandlung erfolgen.

(Eingegangen am 29. Januar 1952.)

Widerspruchsfreier Aufbau einer typenfreien Logik

Documents

Transcript of Widerspruchsfreier Aufbau einer typenfreien Logik