ISILC - Proof Theory Symposion: Dedicated to Kurt Schütte on the Occasion of His 65th Birthday. Proceedings of the International Summer Institute and ... in Mathematics) [1 ed.] 354007533X, 9783540075332 [PDF]

Zitiervorschau

Lecture Notes in Mathematics Edited by A. Dold and B. Eckmann

500 ~ ISILC Proof Theory Symposion Dedicated to Kurt SchLitte on the Occasion of His 65th Birthday Proceedings of the International Summer Institute and Logic Colloquium, Kie11974

Edited by J. Diller and G. H. MiJller

Springer-Verlag Berlin.Heidelberg-NewYork 1975

Editors Prof. Justus Diller Westf~.lische Wilhelms-Universit~t

Institut fQr mathematische Logik und Grundlagenforschung Roxeler Stra6e 64 44 M6nster/IBRD Prof. Gert H. MLiller Mathematisches Institut der Universit~t Heidelberg Im Neuenheimer Feld 288 69 Heidelberg 1/BRD

Library of Congress Cataloging in Publication Data

ISILC Proof Theory Symposium, University of Kiel, 1974. !S_TLC Proof 'Y'aeory Symposium. (Lectures notes in mathematics ; 500) Text in English oF German. i. Proof theory--Congresses. 2. Sch~tte, Kurt --Bibliography. I. Sch~tte, Kurt. II. Diller, Justus. IIl. M~Zler, Gert Heinz, 1923IV. International Summer Institute and Logic Colloquium, University of Xiel, 1974. V. Series: Lecture notes in mathematics (Berlin) ; 500. QA3.L28 no.500 [ Q A g . 5 L ] 510'.8s [511'.3] 75-40482

AMS Subject Classifications (1970): 02D05, 02D99, 02E05, 02F29, 02F40

ISBN 3-540-07533-X Springer-Verlag Berlin 9 Heidelberg 9 New York ISBN 0-387-07533-X Springer-Verlag New York 9 Heidelberg 9 Berlin This work is subject to copyright. All rights are reserved, whether the whole or part of the material is concerned, specifically those of translation, reprinting, re-use of illustrations, broadcasting, reproduction by photocopying machine or similar means, and storage in data banks. Under w 54 of the German Copyright Law where copies are made for other than private use, a fee is payable to the publisher, the amount of the fee to be determined by agreement with the publisher. 9 by Springer-Verlag Berlin 9 Heidelberg 1975 Printed in Germany Offsetdruck: Julius Beltz, Hemsbach/Bergstr.

Kurt Sch~tte

VORWORT Der v o r l i e g e n d e der P r o c e e d i n g s q u i u m Kiel

Band

" S y m p o s i o n on P r o o f T h e o r y "

des I n t e r n a t i o n a l

Summer

ist ein Tell

I n s t i t u t e and Logic C o l l o -

1974 - ISILC -, yon d e n e n der a n d e r e T e i l in e i n e m e i g e n e n

Band der L e c t u r e Notes

erscheint.

Die h i e r g e s a m m e l t e n A r b e i t e n b e h a n d e l n T h e m e n aus dem w e i t e r e n B e r e i c h der B e w e i s t h e o r i e M~nchen,

anli~lich

seines

65.

und sind P r o f e s s o r Dr. Kurt Sch~tte,

Geburtstages

gewidmet.

A r b e i t e n w u r d e n auf dem S y m p o s i o n ~ b e r B e w e i s t h e o r i e Kurt

Sch~tte

V i e r yon d i e s e n zu E h r e n yon

im R a h m e n des ISILC am 2 . 8 . 1 9 7 4 v o r g e t r a g e n ,

zehn A r b e i t e n w u r d e n in den S e k t i o n e n des ISILC v e r l e s e n auf der T a g u n g als A b s t r a c t elm s c h r i f t l i c h e s Kurt

Sch~tte

vor.

S y m p o s i o n an,

e i n g e l a d e n wurden,

weitere oder lagen

Der K i e l e r V e r a n s t a l t u n g

s c h l o ~ sich

zu dem F r e u n d e und n a h e K o l l e g e n yon die in K i e l nicht

anwesend

sein k o n n -

ten. Kurt S c h ~ t t e hat wicklung Salzwedel war dort

in der Altmark, 1933 David

beigetragen. studierte

Hilberts

es jedoch Paul Bernays, durch

in den l e t z t e n 30 J a h r e n w e s e n t l i c h

der B e w e i s t h e o r i e

nicht bei der m a t h e m a t i s c h e n

letzter Promovend.

Logik,

dienst und legte

1948 das A s s e s s o r e x a m e n

in GSttingen,

Logikern,

wurde

Mit

der H i l b e r t - S c h u l e ,

Seholz,

1936-1945

Noch w i h -

am M a t h e m a t i s c h e n

In-

er zu dem k l e i n e n K r e i s yon

die G r u n d l a g e n f o r s c h u n g

in D e u t s c h -

ihm A c k e r m a n n und A r n o l d S c h m i d t Behmann,

aus

H e r m e s und S c h r S t e r aus

Schule.

1950 f o l g t e nach Marburg~

Heinrich

Bedingt zunichst

in den S c h u l -

in H a n n o v e r ab.

er H i l f s k r a f t

die in der N a c h k r i e g s z e i t

der M ~ n s t e r a n e r

1945 g i n g e r

und s e i t d e m g e h S r t e

land w i e d e r a u f g e b a u t haben:

Sch~tte

s o n d e r n a r b e i t e t e yon

Nach dem Z u s a m m e n b r u c h

stitut

In e r s t e r Linie war [3] b e t r e u t e .

Lage b l i e b Kurt

als N e t e o r o l o g e .

rend s e i n e r S c h u l t i t i g k e i t

in

er in B e r l i n und G ~ t t i n g e n und

der seine D o k t o r a r b e i t

die s c h l e c h t e w i r t s c h a f t l i c h e

zur E n t -

G e b o r e n am 1 4 . 1 0 . 1 9 0 9

er als w i s s e n s c h a f t l i c h e r

wo er sich

1952 h a b i l i t i e r t e .

Assistent

Wihrend

A r n o l d Schmidt

er in den fri~hen

50er J a h r e n auch ~ b e r die G r u n d l a g e n der G e o m e t r i e und ~ b e r L a g e r u n g s probleme arbeitete,

konzentrieren

sich seine V e r ~ f f e n t l i c h u n g e n

seit

den s p i t e n 50er J a h r e n m e h r und m e h r auf die L o g i k und B e w e i s t h e o r i e . 1959 e r s c h i e n in der " G e l b e n S e r i e " Wiss.

S p r i n g e r Verlag)

der er s e i n e von G e n t z e n b e e i n f l u ~ t e gramms k l a r und u m f a s s e n d Neufassung

( G r u n d l e h r e n der Nathem.

seine gro~e N o n o g r a p h i e

in

A u f f a s s u n g des H i l b e r t s c h e n P r o -

f o r m u l i e r t hat.

in V o r b e r e i t u n g ,

"Beweistheorie",

Von d i e s e m Buch ist

eine

die yon C r o s s l e y ins E n g l i s c h e ~ b e r s e t z t

Vl

wird.

Im Jahr 1959/60 war Sch~tte als Castprofessor am Institute for

Advanced

Study in Princeton,

schen Hochschule versity. beiten,

1961/62 an der Eidgen~ssischen

in ZUrich und 1962/63 an der Pennsylvania

In diesen Jahren publizierte nimlich

die Arbeit

er drei besonders

TechniState Uni-

wichtige Ar-

[24] zur einfachen Typentheorie,

rer zu den ersten, n i c h t k o n s t r u k t i v e n

die spa-

Beweisen yon Takeutis Fundamen-

talvermutung

durch Takahashi

ten

[31], in denen er g l e i c h z e i t i g mit Feferman die genaue

[30] und

beweistheoretische stark kritische

und Prawitz gefUhrt hat, und die Arbei-

Stirke der verzweigten Typenlogik durch die erste

Ordinalzahl

charakterisiert

hat.

1963 nahm er einen

Ruf auf den Lehrstuhl fur Logik und Crundlagenforschung phischen Seminar der Universit/t matische

Institut

der Universitit

Sein Ergebnisbericht seher Logik" wurde 1952,

Kiel an,

"Vollstindige

1966 g i n g e r

M~nchen,

am Philosoan das Mathe-

an dem er seither t/rig ist.

Systeme modaler und intuitionisti-

1968 abgeschlossen.

Dazwischen,

beginnend

schon

arbeitete Kurt Sch~tte immer wieder Uber Systeme zur konstruk-

riven Bezeichnung yon Ordinalzahlen, Ver~ffentliehungen

[14],

[37],

was seinen Niederschlag

[38], [41] und [42],

schiedenen Arbeiten seiner SchUler gefunden hat. glied der Bayerischen Akademie Kurt SchUtte heiratete

Haus gef~hrt,

Seit

1973 ist er Mit-

der Wissenschaften. im Jahr 1937 Friulein Hanna Lechte.

Das Ehepaar Sch~tte hat zwei TSchter, sela MSncke.

in den

aber auch in ver-

Frau Sigrid Dreyer und Frau Gi-

Herr und Frau Sch~tte haben stets ein gastfreundliches das auslindischen

Kollegen

ein StUtzpunkt

in Deutsch-

land wurde und an das die zahlreichen Freunde und Ciste der Familie gem

denken. Die Herausgeber dieses Bandes danken zuerst den Kieler Kolle-

gen Arnold Oberschelp und Klaus Potthoff fur deren organisatorische Leistung und den erfolgreichen Verlauf des ISILC und darin des Symposions Uber Beweistheorie.

Ferner geht unser herzlicher Dank an Frau

HeBling und Frau Schaefer fur die Erledigung u m f a n g r e i c h e r arbeiten,

Schreib-

an Frau Ernst fur die Erstellung des Schriftenverzeichnisses

und an die Herren Dipl.-~athematiker

Vogel und Rath fur die Durchsicht

zahlreicher Manuskripte.

sagen wir dem Springer-Verlag

aufrichtigen

SchlieBlich

Dank fur seine entgegenkommende

J. Diller

(M~nster)

Mitwirkung.

G.H. M~ller

(Heidelberg)

INHALTSVERZEICHNIS

Verzeichnis Buchholz,

der P u b l i k a t i o n e n

Wilfried,

von Kurt

Curry,

J o h n N.,

in c o m b i n a t o r y

Feferman,

Solomon,

partial Felscher,

der A n a l y s i s

Walter,

type-free

Yoshito,

Calculability

functionals

of finite

(a r e v i s e d v e r s i o n ) Georg,

Leivant,

Daniel,

Lopez-Escobar,

on a t h e m e

E.G.K.,

pleteness Luckhardt,

of the p r i m i t i v e

type

Horst,

generalization

for a r i t h m e t i c

of P r a w i t z )

elements

logic

in a c o n s i s t e n c y

Wolfgang,

Church-Rosser-Theorem

endlich langen Termen 0sswald,

Horst,

198

proof 233

ffir X-Kalkiile mit u n -

.............................

Uber Skolemerweiterungen

s t i s c h e n L o g i k mit G l e i c h h e i t

182

com-

......

for s i m p l e type t h e o r y I . . . . . . . . . . . . . . . . . . . . . . . . . . Xaa2,

164

(va-

Intuitionistic

second-order

152

of

...................

and Wim V e l d m a n ,

The real

119

recursive

due to Schfitte ..............

of a r e s t r i c t e d

73

over the n a t u r a l n u m b e r s

on a recent

theorems

56

of

I .........

........................

Strong normalization

riations

theories

...............................

Observations

completeness

44

K o n s t r u k t i o n e n mit B e w e i -

sen und S c h n i t t e l i m i n a t i o n Hanatani,

26

Funktionalin-

and c l a s s i f i c a t i o n s ,

Kombinatorische

4

standardization

.........................

Non-extensional

operations

........

..............................

Justus und Helmut V o 6 e l , I n t e n s i o n a l e terpretation

Kreisel,

Sound functors

of g e n e r a l i z e d

logic

Sy-

...........................

and Anil Nerode,

H a s k e l l B., A study

Diller,

............

N o r m a l f u n k t i o n e n und k o n s t r u k t i v e

steme von 0 r d i n a l z a h l e n CrossleN,

Sch~tte

257

in der i n t u i t i o n i -

.....................

264

Vlll

Pfeiffer,

Helmut,

W(X) Pohlers~

Eine V a r i a n t e

f~r O r d i n a l z a h l e n

Wolfram,

Prawitz,

Dag,

inductive Comments

Bruno,

Schwichtenberg,

for the p r o v a b i l i t y

definitions

of truth

Bemerkungen

Helmut

Wainer,

and r e c u r s i o n in h i g h e r types Takeuti~

Gaisi,

Troelstra,

Consistency

Anne S., N a r k o v ' s

for t h e o r i e s

proofs

Infinite

.......

290 320

terms

...........

and M a r k o v ' s

sequences

271

and the

.....................

and o r d i n a l s

principle

of choice

procedures

.........................

zu Regel und S c h e m a

and S t a n S.

ite-

.......................

on G e n t z e n - t y p e

267

of

i n d u c t i o n in s y s t e m s w i t h n - t i m e s

classical notion Scar2ellini,

............................

An u p p e r b o u n d

transfinite rated

des B e z e i c h n u n g s s y s t e m s

341 365

rule

..................

370

VERZEICHNIS DER PUBLIKATIONEN VON KURT SCHUTTE Stand M~rz 1975 Monographien LI]

Beweistheorie. Springer Berlin-G~ttingen-Heidelberg 1960 (Bd. 103 der "Grundlehren der mathematischen Wissenschaften in Einzeldarstellungen").

[2]

Vollst~ndige Systeme modaler und intuitionistischer Logik. Springer Berlin-Heidelberg-New York 1968 (Bd. 42 der "Ergebnisse der Mathematik und ihrer Grenzgebiete"). Wissenschaftliche

Aufs~tze

[3]

Untersuchungen zum Entscheidungsproblem der mathematischen Logik. Math. Ann. I09 (1934), 572-603.

[4]

Uber die ErfGllbarkeit einer Klasse von logischen Formeln. Math. Ann. 110 (1934), 161-194.

[5]

Uber einen Teilbereich des AussagenkalkGls. Comptes Rendus des S@ances de la Soci6t6 des Sciences et des Lettres de Varsovie XXVI 1933, Classe III, I-3.

[6]

SchluBweisen-Kalkiile der Pr~dikatenlogik. (1950), 47-65.

[7]

Beweistheoretische Erfassung der unendlichen Induktion in der Zahlentheorie. Math. Ann. 122 (1951), 369-389.

[8]

Mit B.L. van der Waerden: Auf welcher Kugel haben 5, 6, 7, 8 oder 9 Punkte mit Mindestabstand Eins Platz? Math. Ann. 123

Math. Ann.

122

(1951), 96-124. [9]

Die Eliminierbarkeit des bestimmten Artikels in Kodifikaten der Analysis. Math. Ann. 123 (1951), 166-186.

[10]

Eine Bemerkung ~ber quasirekursive Funktionen. Logik u. Grundlagenforschung I (1951), 63-64.

Arch. f. math.

~I]

Beweistheoretische Untersuchung der verzweigten Analysis. Math. Ann. 124 (1952), 123-147.

~2]

Mit B.L. van der Waerden: Das Problem der dreizehn Kugeln. Math.

Ann. 125 (1953), 325-334. ~31

Zur Widerspruchsfreiheit (1953), 394-400.

~4]

Kennzeichnung von 0rdnungszahlen durch rekursiv erkl~rte Funktionen. Math. Ann. 127 (1954), 15-32.

~5 ]

Ein widerspruchsloses System der Analysis auf typenfreier Grundlage. Math. Zeitschrift 61 (1954),~160-179.

~6]

Uberdec~angen der Kugel mit h~chstens acht Kreisen. Math. Ann.

129 (1955), 181-186.

einer typenfreien Logik. Math. Ann.

125

2

[17]

Ein Schlies

[18]

Die Winkelmetrik in der affin-orthogonalen Ebene. Math. Ann.

[19J

Gruppentheoretisches Axiomensystem einer verallgemeinerten euklidischen Geometrie. Math. Ann. 132 (1956), 43-62.

~.oj

Schlie~ungss~tze fur orthogonale Abbildungen euklidischer Ebenen. Math. Ann. 132 (1956), 106-120.

[21]

Ein System des verknGpfenden Schlies u. Grundlagenforschung 2 (1956), 55-67.

[22]

Der projektiv erweiterte Gruppenraum der ebenen Bewegungen. Math. Ann. 134 (1957), 62-92.

[23]

Aussagenlogische Grundeigenschaften formaler Systeme. Dialectica 12 (1958), 422-442.

[24]

Syntactical and semantical properties of simple type theory. J. of Symbolic Logic 25 (1960), 305-326.

[25]

Ein formales System der klassischen Aussagenlogik mit einer einzigen GrundverknGpfung. Arch. f. math. Logik u. Grundlagenforschung 5 (1961), 113-118.

[26]

Logische .Abgrenzungen des Transfiniten. Freiburg/~ttuchen 1962, 105-I 14.

[27]

Der Interpolationssatz der intuitionistischen Pr~dikatenlogik. Math. Ann. 148 (1962), 192-200.

[28]

Lecture Notes in Mathematical Logic (On Metamathematics). The Pennsylvania State University 1962/63.

[29]

Minimale Durchmesser endlicher Punktmengen mit vorgeschriebenem Mindestabstand. Math. Ann. 150 (1963), 91-98.

[30]

Eine Grenze fur die Beweisbarkeit der transfiniten Induktion in der verzweigten Typenlogik. Arch. f. math. Logik u. Grundlagenforsehung 7 (1964), 45-60.

~1]

Predicative well-orderings. Formal systems and recursive functions, Proc. of the 8th logic coll. Oxford 1963, S. 280-303, Studies in Logic, Amsterdam 1965.

~2]

Probleme und Methoden der Beweistheorie. (1965), 562-567.

~3]

Neuere Ergebnisse der Beweistheorie. (einstGndiger Rahmenvortrag). Proc. of the International Congress of Mathematicians at Moscow 1966.

~4]

Nit J.N. Crossley: Non uniqueness at ~2 in Kleene's 0 . Arch. f. math. Logik u. Grundlagenforschung 9 (1967), 95-101.

~5]

Zur Semantik der intuitionistischen Aussagenlogik. Contributions to Mathematical Logic, North-Holland Publ. Company, Amsterdam 1968.

fur Inzidenz und 0rthogonalit~t.

Math. Ann.

129 (1955), 424-430. 130 (1955), 183-195.

Arch. f. math. Logik

Logik und Logikkalk~l,

Studium Generale 18

[36]

On simple type theory with extensionality. Logic, Methodology and Philosophy of Sc. III, North-Holland Publ. Company, Amsterdam 1968.

[37]

Ein konstruktives System von Ordinalzahlen I u n d II. Arch. f. math. Logik u. Grundlagenforschung 11 (1969), 126-137, und 12 (1969), 3-11.

[38]

Nit H. Levitz: A characterization of Takeuti's ordinal diagrams of finite order. Arch. f. math. Logik u. Grundlagenforschung 14 (1970), 75-97.

[ 39]

Mit J. Diller: Simultane Rekursionen in der Theorie der Funktionale endlicher Typen. Arch. f. math. Logik u. Grundlagenforschung 14 (1971), 69-74.

[4O]

Artikel zu den StichwSrtern "Beweistheorie","Finit", "Formales System", "Hilbertsches Programm", "Metamathematik", "Widerspruchsfreiheit" in: J. Ritter (Hrsg.), Historisches WSrterbuch der Philosophie, Schwabe & Co. Verlag Basel/Stuttgart, ab 1971.

[41]

Einftthrung der Normalfunktionen ~ ohne Auswahlaxiom und ohne Regularit~tsbedingung. Erscheint in: Arch. f. math. Logik u. Grundlagenforschung.

[42]

Mit W. Buchholz: Die Beziehungen zwischen den Ordinalzahlsystemen 2 und ~(~). E rscheint in: Arch. f. math. Logik u. Grundlagenforschung.

NORMALFUNKTIONEN

UND KONSTRUKTIVE

SYSTEME

VON 0RDINALZAHLEN Herrn Professor Dr. Kurt Schdtte 65~ Geburtstag

zum

gewidmet

W. Buchholz

Als Hilfsmittel

fGr beweistheoretische

verschiedenen Autoren konstruktlve zahlen elngefGhrt, lassen.

~(~) entwickelt

Im folgenden

werden

klassischen

0rdinalzahltheorle

sollen konstruktive

her

Bezeichnungssysteme

, die ihrem formalen Aufbau nach eng verwandt

slnd mit den Systemen E(N) , 2, W(X) yon SchGtte [12], die aber im Gegensatz llche Erkl~rung

wurden von

die zwar auf sehr einfache Welse induktlv definiert

slnd, sich aber nur schwer v o n d e r verstehen

Untersuchungen

Bezeichnungssysteme I)" fGr Ordinal-

[17] und Pfeiffer

zu Jenen eine relatlv einfache

in der klassischen 0rdlnalzahltheorie

[11]

und natGr-

besitzen.

Wir

werden dabei von gewissen von FEFERMAN und ACZEL [I] stammenden - und yon BRIDGE in [3] n~her untersuchten

- Normalfunktlonen

die sich sehr elnfach und ohne Bezugnahme sischen Theorie definieren

Arbeit:

Entwicklung gewisser

nisse Gber die Funktionen |

Dabel enth~lt

schon bei Bridge

Wohlordnungsbeweis

In w

behandelt In w

fGr die Systeme ~(T), ~({g~)

und mlt wird eln gegeben.

der Wohlordnungsbowelse

[19]

yon

, Od(1) yon Kino [8] , Z(N)

, 2 und W(X) yon Pfeiffer

nur

werden

[ 11],[ 12] .

I) z.B. die Systeme O(n) von Takeutl [17]

im wesentlichen

(ohne Beweise).

Dieser Bewels ist eine Verallgemeinerung

yon SchHtte

w

8(~) im Rahmen

[3] bewlesener Ergeb-

8(T) und ~({g})

den Systemen anderer Autoren verglichen

SCHU-TTE [ 17] und PFEIFFER

I- 3 beinhalten

mit zum Tell neuen Beweiseno

die speziellen Bezeichnungssysteme konstruktiver

Die Paragraphen

der Bezelchnungssysteme

der klassischen 0rdinalzahltheorie. eine Zusammenstellung

ausgehen, in der klas-

lassen.

Zum Inhalt der vorliegenden die nichtkonstruktlve

|

auf Hauptfolgen

[11],[12]

W. Buchh olz w

D i e

5

N o r m a 1 f u n k t i o n e n

Wir legen hier (in w

- w

8a

die axlomatlsche Mengenlehre yon Zermelo-

Fraenkel mlt Auswahlaxlom zugrunde. Die Klasse On der 0rdinalzahlen sei in fibllcher Weise so definlert, da6 ~ = {~ e On J ~ < a] fGr Jedes a ~ On ist. Ksei

die Klasse der Kardinalzahlen

~

, d.ho die Klasse derjenigen 0r-

dlnalzahlen > ~ ,

die sich nicht blJektlv auf eine kleinere 0rdinalzahl

abbilden lassen,

k~

sei die 0rdnungsfunktion der Klasse KU{0) , d.h.

die (elndeutig bestimmte) Funktion, die On ordnungstreu und bljektlv auf KU{0] abbildet. Es ist also_~ o =0 und ~ = M ~

fflr ~ > 0 .

Zu B ~ 0 n

gibt es

genau ein ~ e 0 n mlt ~ < B..~

mit ~ = ~ I + ' ' ' + ~ n ; wir definieren H[~] := {~I' .... ~n }_ und H[0] := ~ o Es gilt: K C H , Vv~0n(7~ H~-*H[v] = [~]) , H[q] C H [ ~ + q ] C H [ ~ ] U H[q] . Ist M eine wohlgeordnete Menge,

so bezeichnen wir mit IJMII ihren 0rd-

nungstyp, d.h. dlejenlge 0rdlnalzahl, die ordnungsisomorph zu M i s t . Wir verwenden folgende Mitteilungszeichen: , ~ , ~ , 6 , ~ , q , ~

(auch mit Indizes) f~dr 0rdinalzahlen,

, ~

ffir Elemente von K U [0] ,

i , k , m , n

f~r nat~rliche Zahlen,

A\B

ffir die Mengendifferenz

[xJ xr A A X @

B} .

Definition der Funktionen | Im folgenden bezeichne ~ eine abz~hlbare Menge von Funktionen f:D(f)--~K mit ~ @ D ( f ) ~ 0 n m , 1~ 0

-- g ~ ( h ) = h ) ]

wenn 8 = 6o + n sonst

mit

g~(6 o)._. = 80

{((~,~),g~) I (~,~)~ onxon}

Folge rungen (17)

A T = ~I+T

'

(18)

~T =

(19)

gel61 < gc~282 gilt genau dann, wenn elner der folgenden drei

~TIQI+T

F~lle vorliegt:

A[g} = min{~ I ~ = g~0 } , wenn

(17a)

K n Q I + T c CT(~,8)

w~
~>

darn% gilt:

sup(~ n I n r ~} = ~ 2 ( ~ + I )

~ < ~(~I) ~ < en~

Bewels. a) Durch Induktion nach n zelgt man: ~n ( ~ n

(~+I) < ~ G [ ~ + I )

und C n ( ~ , ~ o + 1 ) N ~ 4 c i

~x(x~M A

a~< x)

Ro

R u {o}

a und b slnd identisch

% , Q , R

(%,

a) Man zeigt durch Induktlon nach Gc :

c

b/IMan zeigt durch Induktion nach Gc :

c 4 {a.,b}

Lemma

~

c < ~ab c < gab

11

a)

c ~ Kua

....>

c ~ r

b)

C = C1+...+c n (mit n ~ 1

A

c 4

a

^

, c I .....c n ~ Q)

Sc4

A

u

Sc ~ u

>

KuC = {c I ..... C n} c)

v < Sc

d)

v,

KvSc c KvC

K~K~O=KvO

e)

u..

KvC < ~)av

nach Gc . Wir behandeln nur den Fall v < c =~clc 2 .

AUS { C l } U K u C I U K u C 2 = K~C < a folgt mit der I.V. < ~av . Ist Sc = v , so folgt(mit KvC I U {c2} < ~av

, also

Sc > v , so folgt

De

Lemma

KvC < ~3av

cI < a

und

11b) KvC = { e C l C e }

nach der Definition

KvC I U K v C 2

, cI < a

und

yon < . Ist

KvC = KvC I U KvC 2 < ~av .

r

W o h l o r d n u n g s b e w e i

s

De finitionen Q ' QI ' Q2

bezeichnen

Teilmengen

{ce Q

I

Q n u + :=

{ccQ

I Sc~< u}

W[Q]

:=

{aeQ

I QAa

:=

{a ] V V ( V r Q O u

Q0a

:=

WQu

yon

c < a }

ist wohlgeordnet

}

> Kv a c Q)}

:: wt nu +]

Folge rungen (24)

Qlr

,., = Q 2 n u

(25)

W Q ist der gr~Ste wohlgeordnete wohlgeordnet, a ~ wQ

;.

=

A

w uQI = wQ2

Abschnitt

yon ~ O u

+ , d.h. W Q Ist

und es gilt:


e Q

eab

~ Q

Beweis. a) Sei a+b ~ % ist a,b e Q O u

und a,b e Q

9 Wir

setzen u

+ -- w u ; a l s o ist a + b e M u , und

wohlgeordnet.

Wir

folgt d a r a u s

a + b ~ W u c Q . - Sei

man

z e i g e n nun,

sich l e i c h t H b e r z e u g t ,

treue und bijektive ist,

:= S(a+b)

folgt daraus

= Sa , a+O

Muna

und M u D b

dab M u O ( a + b ) w o h l g e o r d n e t ~

llefert

Abbildung

yon ~

die W o h l o r d n u n g

:= {d

I dr

die Z u o r d n u n g

yon ~P(a+b)

sind

ist; mit a+b r u

A

a~ Gab r Q Daraus schlie~t man durch "geschachtelte" Lemma

transfinite

Induktion fiber Q auf die B e h a u p t u n g

15

u r Mu

und

Beweis.

Aus u E M u und Muff u c Q folgt

~nu

c Q

~

w u ist a u s g e z e i c h n e t

und W u o u = Muff u . N a c h Lemma Daraus ffir v r u~a

b)

folgt nach

(24)

9 so ist S a = u E W

Definition

(da Q w o h l g e o r d n e t

13 ist Q c N u ; also ist

W~ u = W u n U +

u n u . W u erffillt also

(A2)

und

:=

~{Q

u ~ Wu ist) u r W u WuDu

= Q0u

.

W~ u = W v = Q O v + = W u 0 v +

(Seite

u . Ist a c W u n u

:

und

18)

Zu (At): Ist a~ W u und

9 so folgt S a c W u wegen WuflU=Qnu.

J Q Ist a u s g e z e i c h n e t

)

Anmerkung: Sel

vy(y

Pru[ Q~ Q~] :

nu § ^

dann gilt:

3QIV%( a ~ % A vx(x~ QI -* Sx~Q1) A A vn~Q I (Pr [ % % ] ^ ( Pru[%%l -~ Q1 n ~+ ~ %))) Satz 16 Ist ausgezeichnete

Teilmenge

von % .

Beweis. Hilfssatz:

Sind QI ' Q2

u r QI U Q 2 Bewels des Hilfssatzes

ausgezeichnet,

so gilt:

A u~< QI A u~< Q2 )Q10u+ = Q2nu+ durch transfinite Induktlon nach u ~ QIUQ2 :

Sel u ~ QI und u~< Q2 " Aus der I.V.

folgt

u c QI n u + = w QI = w Q2 . Mit Lemma

14 und ux 0,

let Y~, If

X

to

R

Let

D3

be a

Z.

be the n~nber of secondary contractions in

involve an induction on

occur in a stage

SC.

if primary, does not begin

and, if secondary, does not lie wholly to the

Then there is a standard reduction from

D3o + {R~ + D y

must

Pk+l"

is secondary, and hence,

Sk

whose starting redex lies entirely to the right of

Proof.

Sm

This proves (ii).

be a standard reduction from

to the left of the beginning of

If

S,.

is interchangeable with

standard reduction from

left ot it.

and

satisfying (iii). This completes the proof.

contraction of a secondary redex to

Sk

S,

is senior to

is not bypassed in the step, if any, before

Again each

V

is

This proves (i).

would not be the first stage with such an

we have a

Sr

k < m

D 3.

The proof will

m. be the first secondary redex contracted in and let its contraction reduce

m = 0,

D o3

let

be the whole of

Y*

to

Y'.

D3,

and

Y~

D;

let it

Let

D3

be

Z.

be Then

D o3

is a standard primary reduction, and, by E8 and an induction, no redex contracted in D o3 begins to the left of the beginning of S. Further D 3 is a standard reduction with only m-i secondary contractions; and the starting redex of D3, if primary, does not begin to the left of the beginning of

R

(Lemma i),

and if secondary does

not lie wholly to the left of it. By El0 there is a standard primary reduction D 2 from V to Y . No redex o contracted in D I + D 3 can begin to the left of the beginning of S. Therefore, by Lemma 3, the starting redex of of a redex bypassed by

S.

D2

does not either, and hence it cannot be residual

Thus the reduction

The last paragraph proves the lemma if that the lem~a holds if there are If

R

m-i

D1 + D2

m = 0.

is standard.

Henceforth we assume

secondary contractions in

will be the standard reduction sought.

By that lepta there is a stage

U"

in

D2

R;

D2,

then

D1 +

Otherwise we apply Lemma 7.

such that there is an

is senior to the redex contracted in the next step, has and has the same beginning as

and

D 3.

is not residual of a redex bypassed by the last step of

D 2 + {R} + D 3

m > 0

R

P~

in

U"

which

as sole residual in

Y ,

also its residuals, all of which are equiform,

are interchangeable with all the redexes contracted later in

D2 .

If we make these

H.B.

Curry

53

interchanges we have a standard primary reduction tracting before

R,

in

U',

If

9

*

is not the first stage in

D2,

redex, which is the starting redex of S.

Then

DI, 9

viz.

V 9,

the result of con-

D2,

O

then

D2

U"

is not residual of a redex bypassed by

is the first stage in

residual of a bypassed redex in

U.

D2, i.e.

V,

For suppose it were.

wholly to the left of the beginning of

D2

is not void and its starting

D1 + D2O + {R,}, will be a standard, reduction from

On the other hand, if

D3

from

U , to Y'. Further if D 2 consists of the steps, if any, of o D 2 + {P~} will be a standard reduction from V to V'.

then

U"

D2

O

S;

if

R

then

X

R,

to

V9

is not the

Then it would have to lie

should be the starting redex of

this would contradict the hypothesis about that starting redex; otherwise, since o D 3 begins to the left of the beginning of S, it would con-

no redex contracted in

tradict the hypothesis that reduction from

X

to

D3

be standard.

Then we get a

D1

which is a standard

V'.

Thus we have a situation similar to that at the close of Lemma 5. of this lemma with satisfied by a and

D3

DI,

defined as above, in the place of

in the place of

D3;

and

D3

has

m-I

DI, D~

Len~aa 9.

Let

D

from X

to

Z.

Proof.

If

P

be a primary redex in

be a standard reduction from

D

Y

X

in the place of

secondary contractions.

inductive hypothesis there is a standard reduction from

and let

The hypotheses

X, V, Y, Z, S interpreted as X, V', Y', Z, R~, respectively are

X

to

Z,

By the

q.e.d.

whose contraction reduces

to

Z.

D2,

X

to

Y~

Then there is a standard reduction

is a primary reduction this follows by El0.

be

the redex of the first secondary contraction in

D.

Let

D3

is a standard reduction whose

is a standard primary reduction, and

be

S

where

D~

D

If not, let

D~ + {S} + D3,

starting step, if primary, does not begin to the left of the beginning of otherwise does not lie wholly to the left of the beginning of Y

to

Y*,

and

{S}

reduce

Y*

to

Y',

the standard primary reduction from from

{P} + D O .

then

D

If

S

X

to

then

D3

Y

reduces

S. Y"

there is a standard reduction from

Proof.

X

to

If there is a reduction

Let

X

to

Xk

reduce Let

D

D

Z,

be

which is obtained according to El0

+ {S} + D 3 will be the standard reduction sought.

Theorem.

D~ Z.

and

is not residual of a redex bypassed by the last step of

D ,

Otherwise we can apply

Lepta 7 to obtain a situation which is a special case of Lemma 8.

reduction from

Let to

S,

By that lemma

q.e.d.

from

X

to

Y,

then there is a standard

Y.

(0 _< k _< n)

standard reduction from

Xn

to

be the k'th stage in Y,

and also from

Xn_ 1

D. to

Then there is a trivial Y.

Suppose that there

54

H.B.

is a standard reduction from reduces

Xm

tion from

to

Xm+ I. Y

If

Rm+ 1

Y.

Let

Rm+ 1

be the redex whose contraction

is a primary redex, then there is a standard reducif

Rm+ 1

Hence, by descending induction on

m,

there is a standard reduction from

m

to

to

by Ler~a 9;

for every

Xm

Xm+ 1

Curry

such that

Corollary.

0 ~m

~ n.

For

is secondary, this follows by Lemma 6.

m = 0

If there is a reduction

D

from

form, then there is a normal reduction from

Proof.

we have the theorem,

X

to

X

to

by Len~aa 2 there would be a residual of

Department of Mathematics Pennsylvania State University University Park, Pennsylvania

16802

R

in

R Y,

and

Y

to

Y

q.e.d.

is in normal

Y.

By the theorem there is a standard reduction

pose that at some stage the seniormost redex

Y

Xm

Y.

Sup-

were not the one contracted.

D

from

X

Then

which is impossible.

to

H.B. Curry Bibliography [i] Curry, Haskell B. and Feys, Robert. Combinatory logic, vol. I, Amsterdam, North Holland Publishing Co., 1958. Third printing 1974. [2] Curry, Haskell B., Hindley, J. Roger, and Seldin, Jonathan P. Combinatory logic, vol. II. Amsterdam, North Holland Publishing Co., 1972. [3] Hindley, J. Roger, Lercher, Bruce, and Seldin, Jonathan P.

Introduction

to combinatory logic. Cambridge, at the University Press, 1972. [4] Morris, James Hiram Jr. Lambda calculus models of progranming languages. Thesis, Massachusetts Institute of Technology, 1968.

INTENSIONALE Kurt

FUNKTIONALINTERPRETATION

SchGtte Justus

K. G~del hat Theorie

zum 65.

D i l l e r und Helmut

wurde

der B a r - F u n k t i o n a l e

und der i n t u i t i o n i s t i s c h e n sind die F o r m e l n

in

kutiert

wird,

HA

l~Bt

nete Theorie)

Deshalb

G e g e b e n sei EinfGhrung voraus, HA

von

Allein Vw~

B^:= 3vVwB

C A , abh~ngig in A b h ~ n g i g k e i t VzU

aus

und vonder

Annahme

Dieses

der I m p l i k a t i o n

a l l e i n in A b h ~ n g i g k e i t

fGr die ~ aus ~ folgt.

Da sich

wird m a n im a l l g e m e i n e n viele v e r s c h i e d e n e

~

Vereinigung

HA w (das

der T h e o r i e n

^ der D i a l e c t i c a - U b e r zu begriinden ist.

Dureh

C, in der

Implikations-

B ~ C . Wir setzen

, aber aueh B ^ , bereits vonder

eine H e r l e i t u n g definiert Wahrheit

ein y a u s r e c h n e n

Argument

yon

bezeich-

H einer F o r m e l

yon

sind. von

lassen,

wird auch bei der Dia-

angewandt.

Ist ein solches

durch B e t r a c h t u n g

yen

y be-

H A yon u n t e n

von z die Objekte w a u s z u r e c h n e n , nach

oben b i n ~ r v e r z w e i g e n kann, A s t e n yon H A endlich

Objekte w erhalten.

so da~ ~ aus

yon dem n o - c o u n t e r e x a m p l e - A r g u m e n t

Aw~W~ ab, das

Zusammenfassung

Es mu~ also

folgt.

[8] a n g e b e n und das auf der E n t s c h e i d b a r k e i t Als s c h e m a t i s c h e

Formu-

in den v e r s c h i e d e n e n

solche

liche M e n g e W geben,

N-HAw

auftritt.

C A := 3yVz~

man u m g e k e h r t

so versucht

Typen

yon v, also u n a b h ~ n g i g folgt.

T,

schon nicht

wie folgt

Herleitung

lectica-Ubersetzung oben,

SehGttes

und mit

Herleitung

frei

stimmt, nach

(vgl.

eine V a r i a n t e

H A yon oben nach u n t e n Vw~

Z a h l e n auf-

der T h e o r i e

endlicher

genannte natGrliche

eine n a t G r l i c h e

[6] u n t e r

hat und in [2], Ende yon w 2, dis-

die fGr I m p l i k a t i o n e n

B eventuell mehrfach

, mu~ sich aus

fGr das

die die

Diese

In d i e s e n S y s t e m e n

Fassung

Heyting-Arithmetik

erh~It m a n aus H e i n e

dab

fortgesetzt.

Typs a u f t r e t e n

wird in [2]

in der

der k l a s s i s c h e n

vom Typ der n a t G r l i c h e n

[13] "neutral"

D eingefGhrt,

eine A n n a h m e

Systeme

sich die D i a l e c t i c a - I n t e r p r e t a t i o n

fortsetzen,

und T ist.

HA

interpretiert. [11] und Howard

intensionaler

hGheren

auf die i n t e n s i o n a l e

setzung

von S p e c t o r

[3 ]). Wie Howard bemerkt

ist die in T r o e l s t r a HA

Funktionale

Analysis

zu G~dels

Gleiehungen

lierung

Vogel

auf e x t e n s i o n a l e

aus G l e i c h u n g e n

im Gegensatz

in der aueh

gewidmet

1958 in [4] die H e y t i n g - A r i t h m e t i k

Dialectica-lnterpretation

gebaut,

Geburtstag

T der p r i m i t i v - r e k u r s i v e n

Verwendung

DER A N A L Y S I S

Dieses

G~del in

sich

endweicht

[4] und K r e i s e l

von B beruht.

ergibt

eine

Argument

in

57

J. Diller, H. Vogel

",@

xB

(--,T)

3vVw~

xB

c B-~C

HA:

I

x

3vVw~

x

) (~I)

^

.

.

.

.

x

Vv3yVz 3 endl. Menge W:(Aw~W~ ~ U),

und aus der letzten Formel erh~lt man mit Auswahlaxiomen die ^-Ubersetzung der Implikation (B ~ C ) ^ := 3X,W,Y Vv,z(Ax < Xvz ~[v,Wxvz] ~ ~[Yv,z]) GSdels Theorie T wird also zun~chst durch einen beschr~nkten Allquantor

Ax

and V' = ~ .

~ : :

Finally we put

~0 _ SlqS 2

I

~-Sl~S2

O'm~m iw(~ @ij

"'" Qm'Wm ~i(

~ij

and

~ik

k is atomic.

~j ~ @ij

v : ~ik)

For each atomic formula

@ , let

if

@

is an ~(--~) atomic formula

if

@

is

Sl~S 2

(where

sI , s2

if @

is

Sl~S 2

(

sI , s2

: : aaWl "'" %~mi

(ii)

j

"

Then

are s "

. "

) .

k

~- = : Ql'Wl ... Qm'Wm ~ ( i

W @iJ V W ~ i k ) . j k

The following is then trivial.

Lemma 4.3. (i) iables as

hold.

(/~) and

~-

and

~-

are both

9,~-monotonic and have the same free var-

(~-~~~)

are consequences of

are useful when also

(~ -* ~+)

D~ .

and (if possible)

( ~ -~ ~-)

Roughly speaking, this occurs under certain conditions on the variables

which insure that Sl~--s2
~ (Sl~S2)

Sl~--s2

In anticipation of such we write A

(~) for any formula

.

holds whenever we meet

^

§

_

~(x,u) = : x(~ (x,u),~ (x,u)) ~ .

in

~+

or

~- ; for then

S. F e f e r m a n

I0S

Note that no Russell paradox arises in the use of (5). For the case that is

-7(Xqx)

and

ns c o n s e q u e n c e s o f

c

is

~(x)

(Zo) ~

;

it

we have

only fono~

The s i m p l e s t c a s e where we can u s e

~(x,~)

that

c~c

~+ , ~-

Sl~S 2

appearing in

of occurrences of the

ui

Suppose

vu{

has

s2

not being excluded).

case to assume that each Lemma 4.4.

~

~nd

c~c

Vx(x~c < - > x ~

.

i n t h e way s u g g e s t e d i s t h a t

. By this is meant that every

is elementary relative to the ~arameter s

atomic formula

(i)

VX(X~C X~X) and

equal to some

ui

(other kinds

Thus it is sufficient in this

ui~CL . In other words:

~(x,u)

is elementary.

uiNCL~Vx[~(x,E )
~+(x,~)] A Vx[~ ~(x,E)
~-(x,~)]]

l ~-)

S.

Feferman

(iii)

c~CL~

(iv)

c~CL A (f : c ~ CL) ~ (Zcf)~CL A (-~-cf)hCL

(v)

w~(Zx~efX)


Vx[xNc ~ (gx)G(fx)]}

(vii)

x~(ec)

.

Vx[x~/-]c
x~CLAx~c

(~ c)hCL .

this "weakness"

of

~ c

~x~y)]

> ~ x,y(~ : (x,y) A x~c A y~(f~))

Remark. There is no obvious definition of on

105

@e so that under very general conditions

Since operations are treated independently of classes~

is not significant;

the mathematical role t h a t

classically is here taken over by exponentiation. We have now established counterparts

~

plays

[]

of all the basic set-theoretical

erations by means of partial operations under which

CL

op-

is closed, except for P

as Just noted and for passage to equivalence classes, as we shall now discuss. For partial classifications o_~n c , and write

(9)

Equiv(e,c)

c

and

e , we call

e

an equivalence relation

, if it satisfies

(i)

e c (c X c)

(ii)

Vx[xNc -) (x,x)~e]

(iii)

Vx, y,z[(x,y)~o A (y,z)nc~ (x,z)~e a (y,x)nc] .

We then define

(io)

(i)

[x] e : : ?[(x,y)~e]

(ii)

c/e = : ~ x ( x ~ e

Note that for a certain

Lemma 4.6.

G~O,~ I

A z = [X]e ) . we have

[X]e = z

The following are consequences of

(i)

e~CL~ [X]e~CL

(ii)

c~CL-~ (c/e)~CL

(iii)

yq[x] e (x,y)~e

just in case

(Zo)j 9

G~O, ~l x ~ z .

106

S.

Feferman

(iv)

zq(c/e)
~ x ( x ~ c A z = [X]e)

(v)

Equiv(c,e) -~ Vx, y{(x,y)~e
xqc A [X]e -- [y]e ] .

Thus every equivalence relation is reduced to the single relation co-extensiveness. however,

q

In fact, we can prove failure of extensionality

(even) for universal classifications,

Proof.

- 7 V c [~x (xqc) ~ c = V]

in analogy to Theorem 3.6.11)

is a consequence of

(Z0)~

Suppose, to the contrary, that V c{~x(xqe) -~c = V] .

H = kf 9 ~ y ( f x [Tot(f) < - - >

of

In classical (extensional) systemS this is just the identity;

is not extensional.

Theorem 4.7.

~

~ y) .

Hf = V] .

Then for all Replace

0

Hf~

f , by

V

and

Let

[Vx(xqHf)
Tot(f)]

so

in the proof of 3.6 above and then

proceed to a contradiction as before.

Addendum.

The Frege-Russell program revisited.

There is no question here of fol-

lowing this program in the sense of reducing all of mathematics to principles of logic.

Rather we wish to re-examine the idea for initiating this progr~un by

defining such notions as cardinal number and ordinal number in terms of the equivalence classes for the relations of 1-1 correspondence between classes, reslm~~ isomorphism ~

well-ordered structures.

the present context have just been discussed.

The general obstacles to this in We shall now sketch to what extent

the program survives. i-i (1) (b-e)=: ~ f ( f : b

(Recall that ~ x ( f x -~ y) .)

f-i

> c) = : ~ f [ f q ( b c ) A f-lq(Cb)AVx(xqb ~ f-l(f~:) _~ x)] . onto

was defined in ~Sb

in such a way that

In order to obtain an equivalence relation

evidently restrict

b

to lie in

f(f-ly) = Y E

whenever

from this we must

CL ; in that case it follows from

(b ~c)

c~CL .

(2)

ECD = : ~ b , e [ z

= (b,c) A h ~ C T

A ~

Ab

~ e] .

ll) This also adapts and strengthens a corresponding result in [F ], ~3.4.

that

S.

N o w we m a y easily prove in on

CL

.

(Zo) ~

107

thit

ECD

is an equivalence

CD is a partial classification

cardinal numbers.

9 (CL/EcD)

=

Two cardinal numbers

~ one u s i n g the operation

.

which is not total.

We can consider two versions ke

z , w

are thus the "same"

of Cantor's

9 c[0,1)

We may call its members the

t h e o r e m that

and the other

~

proved b y forms of the standard argument that there is no f : c -----> [0,i} c , nor is there onto i-i f(f : c > [0, i} c) and ~ f ( f of the classical statement : if

f

with

A ~B

where the classical argument breaks terms of m e m b e r s h i p

in

A , B

f : c

:c l - l > ~ c )

A , does not h o l d here ; iO, l} V c V

.

>~c onto

.

K < 2K

.

for cardinals

Thus it is easily

f

with

Furthermore,

is a counterexample.

f

of

B

onto

It is easy to see

since the required map is defined in

. cannot b e pushed much b e y o n d

this point since we lack the a x i o m of choice and the p o s s i b i l i t y in terms of membership.

ever familiar approach)

z -= w

.

, then there exists a map

down,

if

Note also that the counterpart

It seems that the classical theory of cardinals

erations

relation

This leads us to take

(3) CD

Feferman

of definirg

Even the theory of finite cardinals

runs into troubles.

do not f o r m a total classification

In particular,

op-

(from which-

the finite cardinals

and the induction scheme cannot be established

in its full generality. W h e n we turn to w e l l - f o u n d e d further difficulties.

(4) the

Wf(c,r) formula

removable included

to take

_tea

Vx[x~eAVy((y,x)~r

given here has

even if

structures

(c~r)

we meet

If we define

= : ~b~CtAb ~(c,r)

and w e l l - o r d e r e d

cNCL

and

'bNCL'

r~CL .

care of the other

-~ y~b) -~ x~b] - + c - b }

in a negative

On t h e o t h e r

positions

of

position

which is not

hand, the hypothesis

b

in

~ .

Thus

bNCL

~+(c,r)

is

will

,%

not be equivalent

to

~

and

~=

.~ w ~ c,r[w = (c,r) A e ~ C L A r ~ C L A W f ( c , r ) }

not b e h a v e provably according to its definition. holds we cannot in general carry out induction

on

Moreover, r

even if

Wf(e,r)

with respect to all

does

108

S.

properties formnlable in ciples.

~(=,~,~

Feferman

, because of the limited comprehension prin-

The following section gives a means of incorporating such principles into

a (consistent)

extension of

(Z0) ~

(and

W~

more generally).

This will include

the natural numbers as a special case.

~e.

Inductively generated classifications.

We should now like to see under what

conditions we may obtain the existence of a classification numbers. (i)

N

for the natural

A fully satisfactory definition should have as consequences:

(i)

N~CL

(ii)

O~N A Vx[x~N ~ x' ~N]

(iii)

~(0) A y x [ # ( x ) ~ ( x ' ) ]

-~ Vx~(x)

(possibly with parameters)

of

, for each formula

~(x) ,

~-~, ~

The consistency of (i) with the principles considered so far is no problem. simplest way to obtain this is to take 0,'

~

having their standard interpretation9

to be an then

~-structure with

V

The

M = ~

serves the purpose of

and

N .

It is also not difficult if we want to show even more that the adJunction of (i) maintains the eonservati~ extension property. a simple modification of the proof of Theorem 4.1. which is an

s

(2)

x~0N : Yz_cM[o and

Then

~,~

theory containing

~o 1, < = >

:

-,

(x%~)

D R + (~)

Given any model

(Z0)_~ , designate

~ z~

N

as

(~,A)

(3,0)

of

T

and put

Vy(y ~ z---->y, c z) ---->x ~ z] ,

.

are defined as before for

is a model of

This may be accomplished by

~ > 0 , and the proof that

proceeds in the same way.

By

(~, A ~ Y ~ Y~

(2) , it is automatically

a model of (i). It is another matter, if we want to try to derive the existence of isfying (i) from the principles already accepted.

xVz[z~CL

A 0~z A

sat-

The obviouS choice would be to

try (3)

N

Vy(y~z ~ y'~z) ~ x~z]

S.

as the definition of rences of

z

the formula N

as

x~(x)

N 9 The clause

manageable. Wf

Feferman

'z~CL'

10g

is put in to make the other occur-

But now we have Just the same sort of difficulty as with

in (4) of ~4b Add. just preceding,

we do not see how to insure that

N

namely that for this choice of behaves according to its def-

inition.

Thus the possibility of deriving (1) by suitable definition of

hopeless,

at least in the 1st order

a consequence of

(Z0) ~

N

seemS

PC . However, we shall see below that (1) i s

in a semantics with stronger quantifiers.

We now turn to the corresponding questions for a more general class of inductive definitions.

Let

(3)

L : : kbkr 9 (3,b,r)

This is brought in for the following scheme; informally c

of

(IG)

b

inductively generated under the relation

Lbr

represents the part

r .

(Inductive generation) (i)

Vo, r (Lbr~)

(ii) V b , r,c{C~(b) A C~(r) A Lbr = c -* C~(c) A

W[x~b A Vy((y,x)~r ~ y~e) ~ xnc]] (iii) V b , r,c,u[C~(b) A C2(r) A Lbr -~ c

[Vx[x~b A V y ( ( y , x ) ~ r ~ ~(y)) -~ ~(x) ] -~ Vx(x~c -~ ~ ( x ) ] ]

of ~ ( % ~,~

.

Suppose

is an

theory which contains

If

(~l,A)

is any model of

of

~

for each formula

Theorem 4.8. (i)

(ii) Proof.

s

for

(~I,4Y, ~Y

+ (IG) .

T ~ + (IG)

or

(Z0)~_ .

~ , then we can find a model

is a conservative extension of

By modification of the proof of 4.1.

b#r . Y ~ ( ~

changed.

~(X,U)

~f)__ and

Vx[x~ e V x~ic]

%(~ 9

or

~' )

In

~ 9

(M~A) , Lbr --~ (3,b,r)

are defined by induction.

for any Write

4) (i), (iii) in the proof of 4.1 are left un-

4) (ii) is modified in such a way that we also arrange:

110

S. F e f e r m a n

4) (iii)'

xq~+l(Lbr ) ~ >

CI (Lbr) & xq~(Lbr)

or

x e ~ ] [ Z I Z ~M_ & Vz[zq b &Vy((y,x)q r = > y

CI (b)

and

e Z) = >

C~ (r)

and

z e Z]]

and x~#+l(Lbr ) ~

C~(Lbr)

& x~(Lbr)

or

C~(b)

and

C~(r)

and

x~+l(~br) The proof then proceeds as before to show that for (~,A,Y,Y~

satisfies

D q + (~q) .

In order to derive

(IG)

duce a generalized quantifier

where (5) If ulas

B CM

, R C M 2 9 and

includes

J

of structures.

For this (M;B,R~m)

m e M . _CM & Vz(z e B & Vy((y,z) e R ----~yeZ) ----~z e Z ~ .

@0(x,u) , @l(y,z,u) 9 we have a formula

finally any

These are of type

Q~ , and the symbolism is given by

that for any structure

,

is automatically satisfied by 4) (iii)'

in the sense of LindstrSm [ L ].

(M,B,R,m) e ~ : m e ~ [ Z I Z ~

, Y = U Y

in an appropriate extended semantics, we introQ~

we need only specify a class

(IG)

Y = 0 Y

s

q~

, then for any form-

Q~x,y,z[@0(x,u),@l(y,z,u),w]

~ = (~,A,Y,Y-~ , any assignment

a

to

u

in

M

such

and

m e M 9

(6) ~ ~ QJx, y,z[@0(x,~),O1(y,z,~),m] < ~ > (M,[xl~ Theorem 4.9.

@0(x,~)],[(Y,Z)l~

If the semantics

$

@l(Y,Z,~)}, m) e ~ .

contains

Q$ , then

(IG)

is a consequence of

(z0)J The proof of this is straightforward. Remark.

Theorem 4.8 is a corollary of 4.9 and 4.1.

does not already contain

Q~ , simply adjoin

To see that the principles for

N

Q~

to

If

T

is given in

S

which

~ .

may be taken as a special case of

(IG),

put

(7)

~=

: LB~

where

~=

~[x=o

vSy(x=y')1

and

R-- : u H y ( u =

(y,y')) .

S.

Addendum.

Feferman

111

Connection with a previous system of operations and classifications.

In [ F ] I introduced a constructive theory

TO

of partial operations and total

classifications.

The language used was that of ist order

relation symbols

~ , ~ , and

easily seen that

of

TO

xhc

by

A second theory

using an additional constant

(1)

vf[(f:

~ ~)

Using the preceding latter

theory

TI

(Zo)~,

can

by defining

C~(c)

It is

as is done

The operation existence axioms

namely

kuZ~x- gy~(x,y,~)

with

with axiom

~ 1) A (Q(N)f ~ o

interpret

m1

in

< - - > ~ x(xGNA f x = O ) ) ]

(Zo)~ + (IG)+ (V ~ )

r e m a r k and w h a t we saw a t t h e b e g i n n i n g

can b e m o d e l l e d on

(x,0) .

of "Borelian" character was introduced in [F ]~

Q (N)

we

It was shown in [ F ]

of this

section~

.

the

~ .

how to use (IG) to develop notions of constructive

ordinal classes (or tree ordinals) N .

(ZOn) ~

~ (Q(N)f_ ~ o v ~(N)f

By taking Q~ for Q~(~)

x' was defined as

[C~(c) A x~c] .

require only a weak part of

existential.

~ j

is interpretable in

here and interpreting

( , ) , and constant

0 ~ K ~ S ~ D , P ~ P1 ' P2 ' Z , L , and

for each elementary TO

with equality~ basic

C~( ) , a binary pairing symbol

symbols which are here denoted C~ = k ~ 9 ~ ( x , ~ )

PC

01,02~...

Thus the principles studied here with

and of transfinite types

(IG)

N

over

added are prima facie rather

rich mathematically.

The portions of constructive and classical mathematics which

are accounted for by

TO

~4d.

and

TI

are mapped out in general terms in

The situation over set theory.

If we take a suitable system

T

[ F ], w167

of set theory

for grantedj the deduction of the natural numbers~ cardinalsj and ordinals is already taken care of.

Our only interest here would be to see to what extent good

properties of sets carry over to classifications in a theory of operations and classifications over 0 ~ ' , and pairing

T . ( ~ )

Let

s

have

=

and

c

as basic symbols.

are defined in the usual way.

We assume

The extension of useful

properties is facilitated by the following strengthened separation principle.

@

112

S.

(Sep)

(Strong separation).

Feferman

For each formula

VuYa~bVx[x~br

@(x,u)

>x

of

~(~,~

c aAr

:

o

This leads us to consider

+ (Sep) for

T

in the language

Theorem 4oi0. Proof.

If

T

s of

contains

First note that if

some limit ordinal

ZF .

ZF , then

S ~

ZF .

with

S

K , then the model

satisfy Sep.

Now consider any sentence

finite and

S~

sentences ZF S .

in

, and let

so that Thus

from

~

(RK, e )

~

these assertions

such that

T#~@

for

are

.

be the set of s

Let in

the existence of a limit

K

S .

for which

of the universe with respect to all the

Then by the preceding we can define

A , Y , and

~

in

can be proved to satisfy all the remaining sentences in

and hence

@

holds

(in the universe),

We can also formulate a strengthened ~(~, ~ , ~

K

Y , and

and

~,

is a model of

(~,A,Y,Y~

+ (~ep)

[]

in the obvious way.

is inaccessible

the conservative below.

Ss

of

~=

T .

provided by Theorems

Moreover, ~

extension of

i.e., we have deduced

T .

language

(zFc)~

U [@] .

(~,A,Y,Y~ ~

Remark 1.

when

ZF

is an elementary substructure S

T , Joe.,

~ = (~,A~Y,Y~

By the reflection principle we prove in = (RK, g )

is a conservative

~I is a standard model of

3.2 (i) and 4.1 (i) automatically provable in

~

~=

is consistent.

replacement principle

It follows from 3.2 (i) and 4.1 (i) that

(RK~e)

is a model of Tq

+ (Rep)

.

T , then for some

A

As a corollary,

~owsver, the addition of

extension property]

(Rep) in the

(Rep)

does not maintain

the reason for this will be seen in Remark 2

S.

Feferman

Lemna 4.1_I. The following are consequences of

u

(i)

Vx[xuc ~

x ~ b] .

(ii) ~ _ { V X [ ~ SxO(y,uD

113

Z~

.

B a Vx[x ~ a xue]] ~(x,u)

-~ @(X, UD] -@ ~X@(X,U)] for each formtila

Both (i) and (ii) are direct consequences of (Sap).

o_~ ~ ( - - , ~ )

(i) expresses that any partial

classification which is bounded by a set is represented b y a set.

The converse is

A

immediate in the sense that if

~ = x(x 6 a) , then

(ii) is the principle of transfinite induction on if we take

aqCL e

and

~x[x6 a

xq[] .

for the full language.

Thus

N = : ~ , then the principle (i) of S40, i.e., (IG) specialized to

is a consequence of

~

N ,

. More generally, insofar as we are only concerned with

inductively generated sets, the principle (IG) is dispensable. Just as well strengthen Theorem 4.10 to

However, one can

T # + (IG) , providing for inductively

generated classifications in general. Note that the range Thus

U

of

ka- ~ , i.e.,

ka. x(x e a) , is itself in

CL .

is a total classification which represents the universe of sets qu_~asets.

Remark 2. over

U

If we introduce the variables

'X' 'Y', 'Z' , ~

to range by convention

C~ , then all of Bernays' axioms for sets and classes [ B ] are derivable from , except for replacement.

That is, of course, derivable if we add (Rep).

we can prove the consistency of

ZF

in this system by familiar arguments.

But

First,

using class variables we can formulate the notions of satisfaction and truth in the universe of sets. true.

By (Rep) one can establish that all the axioms of

are

~gen with induction available in the extended language by 4.11 (ii), one

can show that every consequence of than

ZF

ZF

ZF

is true.

and hence than Bernays' system. 12)-

Thus

ZF~

+ (Rep)

is stronger

On the other hand, though

Z~

does

not give (Rep), it goes beyond Bernays' system in expressive powers by providing a reasonable theory of the relation

X~u

where

X

need not be a set.

12)Note, incidentally, that all of this holds equally well if we interpret the class variables to range over

C~

and work in

ZF

plus (Rep) restricted to

.

114

S.

Appendix.

Fef erman

A theory of extensional total operations.

Given

s

we denote by

(ES)

the following set of sentences in

(ES)

(i)

Vf'x'Yl'Y2[fx ~ Yl A fx ~ Y2 ~ Yl = Y2 ]

(ii)

Vf[ ~ x(fx$)

~ Tot(f) ]

(iii)

Vf, g[Tot(f)

A f

(iv)

For each

~g~ f

~(x,y,u)

~{V~y~(x,y,~)

s (=) .

= g]

which is ~-monotonic,

~ ~f Vx, y[fx = y ~(x,y,~)]} .

This system is introduced by way of comparison with Theorem 3.6 and the question directly following it. Let

T

be any s

Theorem. (i)

For any infinite

s

~

we can find an expansion

(~,A)

which is a model of (ES). (ii)

If

T

has only infinite models, then

extension of Proof. in s

Let

~

We define

A~_C M 3

(f,x,y) ~ A 2)

(i)

A0

and

~

is a conservative

T .

be a well-ordering of

and assignment

T + (ES)

to

~

in

M . Associate with each s-monotonic ~(x,y,~) M

an element

by transfinite reeursion. Tot ~ (f)

for V x ~ y ( f x

Again

m~,~

in such a way taat

fx -~ y

is written for

: y) .

is empty.

(ii) fx -~+l y : f~ - ~ and G)

(~,A)

or ~ ~z,w(fz ~S)

kV~:~(z,w,a)

and (+) ~ ~ v < ~ , h { ~ A v )

~,a,

f = f~,a

A ~(x,y,~)

bv~;~(z,w,k)

Vz,w[ (~Av) I:@(z,w,b) : > and (@) ~ ~g ~ f ~ , _ ~ g

and for so~

~d

(~UlAk) ~: ~(z,w,a) ]]

= f~,h and (~,A) k Vz ~ '~(z,w,h) A Vz,w[~(z,w,b_)

~(~,w,~)]}.

S.

(iii)

~

= ~J

A

= Aq+ 1 9

for

fx ~

and

Tot

for

Tot(f)

(f) , and

f

g

for

gx = y] .

(ES) (i),

(ii) are easily proved for

It may be noted even more

(~,A)

that 4) ~ x , y ( f x ~-y) ----> Tot (f) . We now consider only (iii), f = f~,a

and there is a unique

--7~z,w(fz --~w) and

and

od(g) = V

fx = y

and

(~Av)

f .

for some

gx -~ Yl

so

contradicted

Tot(f)

If

f ~ g

Then for some

fx ~- +l y

and

SuppoSe

.

for some

If

V < ~ .

Then

, then

~ = v and

is not possible.

~;,b

gx -~V+ly , then

This contradicts

gives a contradiction.

r

such that

g : f~,b

(~,Av)~-~(x,y,b)

(~,A)~(x,y,a)

f -< g

od(f)

we have

by hypothesis.

, and whenever

f ; similarly

.

which we denote

Note that if

Y = Yl

so

~ < V

for

V .

so

fx = +ly

Similarly,

~

Tot +l(f ) .

I= Vz~'.w~(z,w,b_)

gx=y

Suppose

(iv).

gx -~v+ly

2)(ii)(~)

so for

g-< f , then (~)

Hence

f = g

is

and

(ES) (iii) is established. For (ES) c

to

(iv), suppose

u , (~,A)~

@(x,y,u_)

Vx~:y@(x,y,c_)

.

is s-monotonic Let

~

and that for an assignment

be least such that for some

~,a

we have

5)

(=,A)FVz~:w~(z,w,a)

Among all

~,a

and V z , w { ( ~ L , A ) ~ ( z , w , a )

"

By 4) i f

V < ~ .

But then we would have 5) satisfied at

are met so that

~ .

~z,w(fz

~-w) , t h e n

Hence - 7 ~ z,w(fz ~-- w)

fx = +i y ~ >

fx -~ y fx - ~ + #

the proof.

(D~,A)l=@(z,w,c_)~

satisfying 5), choose that one with the

and

Tot~(f)

.

(~,A)~(x,y,a)

fx -~ y < = >

and v

f~,a "

od(f) = V

in place of

Let

f o r some

~ , contradicting

Now all the conditions .

.

(~), (~),

(@)

But then

(~,A)~ ~(~,y,c_> by 5).

This c o . f e t e s

S. Feferman

116

Some consequences

Addendum i. Assume

T

contains

and limitations

I , all constant functions,

closed under composition, themselves

Tot

represented

inverse,

in

holds of every

(x ~ c) = : (cx = O) . - , X , ~ l , and ~ and

~-definable function,

P ' P1 ' P2 ' Sc , and and

Q~

Q V (though

D .

Tot

Q~

QV

C , J,

C~

holds of Whenever

whenever

Tot(f)

semantics

includes the generalized

C~(c)

and

V

C~(c) = : Tot(c)

and every

C~(c)

and

[al, a 2} .

C~

quantifier

Q~

then

, then

It follows that there is no class

Addendum 2.

~(V)

subsets of Tot(x)

~ .

that ~ x ~ f ( f

C~

~ Op

x .

sented, Vf~x(fx

when

-~ x)

x -~ f)

xy -~ z

and

defined for

D and

x,y,z ~ ~ (~)

Hence there is no

n

weak instances of comprehension

=>

Op

.

of

such that

~ (~)

f = g] 9

of all operations.

and some arithmetical kx(x-l)

M = the set of all

such

Thus

Op

Besides the

operations

are repre-

The first recursion theorem

such that is avoided.

nO ~ 0 , nx -~ 0

for

It appears that only

are satisfied in Scott's model.

Thus the interest in it lies in a different direction from the kinds of theories studied here.

.

is a class with more than one

Vf, g[f,g c Op & f ~ g

x ~ 0 , and thus paradoxical diagonalization comparatively

~ c C~(x)]

In [So ] Scott has defined a simple

system of representatives

0 , kx(x+l)

holds.

If the

does not exist as a class.

certain analogues of

including

b

There is a naturally defined subclass

and

C~(Uc)

is also closed

natural model of the k-calculus with domain

gives an extensional k-calculus,

c = bV

There is a relation

for each

, then

(IG).

Comparison with a system of Scott.

and mathematically

is closed under

C~(Zcf)

It can be proved with the Russell argument that ~ 3 c V x [ x

and that

are not

and

~x[x c c - ~ C ~ ( x ) ]

Vx[x ~ c - ~ C ~ ( f x ) ] ,

under inductive generation satisfying

element,

is

(ES)).

Next, in comparison with ~4 b), define

u,

These are only indicated.

Z0 .

First, in comparison with ~3 c), including

of (ES).

S. F e f e r m a n

117

Bibliography

[B]

P. Bernays, A system of axiomatic set theory, I., J. Symbolic Logic 2

(1937) 65-77. [B~]

S . L . Bloom, A note on the predicatively definable sets of N. N. Nepe~voda?

IBM Research Report RC 4829, #21499, May i, 1974. [C]

A. Chauvin, Theorie des objets et the~orie des ensembles, Th~se, Universite

de Clermont-Ferrand (1974). IF] Lo~ [Fil]

S. Feferman, A language and axioms for explicit mathematics, in (Proc. 1974 Summer Res. Inst., Monash) ed. J. N. Crossley~ to appear. F . B . Fitch, The system

CA

of combinatory logi c , J. Symbolic Logic 28

(1%3) 87~97. [Fi2]

F. B. Fitch, A consistent modal set theory, (abstract), J. Symbolic Logic

31 (1966) 701. [Fr]

H. Friedman, Axiomatic recursive function theory, in Lo ic Collo uium '6

eds. Gandy and Yates, North-Holland, Amsterdam (1971) 113-137. [G]

P.C.

Gilmore, The consistency of partial set theory without extensionality,

in Axiomatic Set T h e o ~

(1967 U.C.L.A. Symposium), Proc. Symposia in Pure Math.

XIII, Part II, ed. T. Jech, A.M.S., Providence, 1974, 147-i~3. [H,C]

G. E. Hughes and M. J. Cresswell, An Introduction to M

~

Methuen,

London (1968). [K]

S . C . Kleene, Recursive functionals and quantifiers of finite types, I.,

Trans. Amer. Math. Soc. 91 (1959) 1-32. ILl

P. LindstrS"m, First order logic and generalize d quantifiers, Theoria 32

(1966) i~-195. [M]

Y . N . MoschDvakis, Elementa

I dn uction on Abstract Structures, North-

Holland, Amsterdam (1974). IN]

N. N. Nepe~voda, A new notion of predicative truth and definability, (in

Russian), Mat. Zametki 13 (1973) 735-745. 13 (1973) 493-495.)

(English translation Mathematical Notes

118

[R]

S.

Feferman

B. Russell, Mathematical logic as based on the theory of types (1908),

reprinted in From F r e e

to GSdel

ed. J. van Heijenoort, Harvard University Press,

Cambridge (1967) 150-182. IS]

K. Sch~tte, ~eweistheorie

[Sc]

D. Scott, Data types as lattices (lecture notes, Kiel Summer School in

Logic~ 1972), to appear.

Springer, Berlin (1960) .

KOMBINATORISCHE KONSTRUKTIONEN MIT BEWEISEN UNO SCHNITTELIMINATION

K~rt SchQtte zur Gelegenheit seines 65ten Geburtstages

gewidmet

Walter Felscher

In dieser Arbeit wird untersucht, man an Beweisen vornimmt, Prinzip,

yon welcher Art die Manipulationen sind, die

um Schnitte zu eliminieren.

Oabei handelt es sich um, im

sehr einfache kombinatorische KonstruKtionen mit Beweisen, die zu diesem

ZweeKe als FunKtionen betrachtet werden, welehe auf 8~umen definisrt und deren Werte endliohe Mengen sind; die Elemente dieser Mengen sind abstraKte Terme oder Formeln.

Im ersten Tell der Arbeit wird daher mit solchen AusdrucKsmitteln allgemeine Begri%f des Probeweises

erKl~rt;

zun~chst der

die wegen der vorausgesetzten

abstrakten

Situation etwas langwlerigen technischen Oefinitionen sollten unmittelbar einsichtig sein,sobal~ man sie in den bekannten Sequenzenkalhulen deutet. S von Probeweisen,

Alsdann werden Mengen

die unter gewissen einfaohen KonstruKtionen abgesohlossen sind,

axiomatisch als Mengen yon Beweisen definiert. Eliminationstheorem bewiesen,

besagend,

FOr Mengen ~ yon Beweisen wird das

dass S unter Eliminationsverfahren

abgeschlos-

sen sei. Unmlttelbare Spezialf~lle davon sind die Eliminationss~tze der minimalen, intuitionistlschen

und KlassQschen Pr~diKatenlogiK einschliesslich allf~lliger infini-

t~rer aussagenlogischer Operationen. Eliminationslemmas

yon TAIT

88

Zum Beweis des Theorems wird ein Analogon des

bewiesen;

jedoch wird im Onterschied zu TAIT die

120

W.

Behandlung

yon @ u a n t o r e n

hen zurOcKgefOhrt, benBtigt

werden.

nicht

handelt

Von z e n t r a l e r

von denen

einmal

den A n w e n d u n g e n

als

yon E i n f O h r u n g s r e g e l n , formeln

Kleineren

dann

vonder

der Art A werden Pr~missen

fOhrung endet,

P

--

dutch des wurde.

Oabei

Gestalt

v und

Oie Pormeln v

positiven positiven

die reehte

Kopie v

Beweise

Grades

an die Stelle zerfallen

einer solehen

Hauptformeln

der andere

anderen

in zwei Arten,

Formel,

istj

von Neben-

so ist v

Heuptformeln

der Art B h~nnen mit m e h r e r e n

S~ , S I ,von

[vs) besagt:

denen

mit der E i n f O h r u n @

enth~lt

der eine mit der Ein-

von v

als Hauptformel

w von v einen

Beweis

von S 1 so, dass Sw

v* -EinfOhrung

der a b s c h l i e s s e n d e n

neben

ver allem die A n w e n d u n g e n

Grades

vonder

enthalten

w

denselben

Beweisbaum

Teilbeweis •

ist dabei w

sogar

ist w v o n d e r P

w

sie etwa im Fall

erlauben;

dass

geh~rende

gelegene

sehen gleish Gestalt

ist v o n d e r

Oer Beweis

entstehen,

Selte

formalen

des R e s u l t a t

man die deft zu v anderen

Pr~misse

mit denselben

von S I , w ~ h r e n d

der jeweils

F~llen

, suggeriert

der Art A , so gibt es zu j e d e r N e b e n f o r m e l

S w in S und eine P r ~ m i s s e

steht,

Pormulierung

Oie A b g e s c h l o s s e n h e i t s e i g e n s c h a f t

von v als Hauptformel,

Beweisb~ume

ist die Abge-

in z w e i f a c h e r

Formeln.

und der S c h n i t t r e g e l n

aus der Menge S zwei T e i l b e w e i s e

und ist v v o n

, pp.113-115

als rechte

mit n u t einer Pr@misse, werden.

deren

sind jeweils

Hauptformeln

treten. linKe,

88

einen Art A o d e r B , wenn

ersehlossen

ein Beweis

Regeln

bei denen

A und B ; ist v etwa die

ven Beweisen,

und OisjunKtio-

auch nut finite

for die E l i m i n a t i o n s v e r @ a h r e n

handeln,

linKe und einmal

Grades

KonjunKtionen

um des Folgende.

Beweise

struktureller

unendlicher

@uantorenlogiK

von S M U L L Y A N

es sioh im W e s e n t l i c h e m

gegeben,

genau

Bedeutung

(vsJ yon Mengen

Eliminationstheorem

Oie Formeln, v

auf d i e j e n i g e

sodass f o r die f i n i t ~ r e

schlossenheitseigenschaft abstraKte

Felscher

Kepie

w(y]

des M i n i m a l K a l k u l s die E i n f O h r u n g s r e g e l n ist v i e l m e h r

Nebenformel yon w .

hat wie der mit P

Sequenz

ersetzt

ist,

dureh w

besondere

deutlich,

der bei einer

solchen

F~llen

in der

y .

dass S e h w i e r i g K e i t e n ,

AufmerKsamKeit

die H i n z u f O g u n g

ent-

; in den q u a n t o r e n l e g i s e h e n

mit einer E i g e n v a r i a b l e n

macht

endende

, also die auf

In den a u s s a g e n l o g i s c h e n von v~

w

die aus Pw

mit einem Term t , und die N e b e n f o r m e l

des E l i m i n a t i o n s t h e o r e m s

Kritisch

yon Sw d i e j e o i g e

jener N e b e n f o r m e l

w[t)

Gestalt

Regelanwendungen

erfordern,

neuer Formeln Gelegenheit

wie

Kaum dedurch

els H a u p t f o r m e l n

eintretende

Wegfall

W. F e l s c h e r

von Nebenformeln,

aiso die Verklelnerung,

Im zweiten Tell der Arbeit wird gezeigt, gelten, wenn neben den aufbauenden

Pr

nicht die Vergresserung des Beweisergebnisses. dass Ellminationstheoreme

auch dann noeh

logisehen Regeln auch noch abbeuende Regeln vom

Peirce-Typ auftreten, wie sie yon CURRY in dem man v o n d e r

121

63

M, a~b ~-~ a

Umst~nden ist des Eliminationsverfahren

for den Spezialfall betrachtet wurden, auf

M-~

a

schliesst.

Auch unter diesen

noeh fundiert, wenn auch die LQngen der durch

Elimination gelieferten Beweise erheblich starker wachsen als des ohne abbauende Regeln der Fall ist.

Teil

I

Sei @ eine uhendliche regul~re Kardinalzahl, zahl; als finit~rer Fall wird derjenige bezeiehnet, Menge, sei

aufgefasst als kardlnale Anfangsin dem @ gleich m i s t .

eine involutorische BijeKtion von F auf sich.

mit Werten in @ definiert,

die jedem v aus F seinen Grad

Menge aller Elemente yon Grad o , die dann auch Atome

c~ (ff)

~O~allev:

veL

genau dann, wenn

die Menge P-F B , die d u r o h

(fvJ

auf

F-F

o

o

{vF) Fist

wenn

yeA

heissen. Weiter gelte:

R , die durch

vertauscht wet-

werden

kIv)

rechten und linKen H~Iften R und L v o n

@-{o}

definiert,

die jedem v

zuordnet

, so ist KCvJ endlich, und es gilt

dann eine Menge abstraKter Terme

Konjugation

sei F ~ die

zerf~llt in zwei disjunKte Teilmengen A und

ist eine Funktion k mit Werten in

seinen Verzweig~r~gsgrad

Ivl zuordnet;

v*eR

der Nicht-Atome vertauscht

Auf F sei eine GradfunKtion

,

F zerf~llt in zwe• disjunkte Teilmengen L u n d den:

~fff]

Ivl ~ I~*I

Sei F eime

[oder Formeln);

K{vJ ~ K{v*) die Abbildung

F miteinander vertauscht,

, welche die

heisst auch die

.

Ein B a ~

T •

eine geordnete Menge

mit Kleinstem Element e T derart,

dass jedes von e T verschiedene e aus E genau einen unteren Nachbarn besitzt, weiter jedes e aus E unterhalb eines maximalen Elementes liegt und, schliesslich,

for jedes

122

W. F e l s c h e r

maximale'e' bier

nut endlieh

betraehteten

der oberen

8~ume

Nachbarn

eine

GradfunKtion 9

alle

e' aus

die K n o t e n

als die

dann

besteht

derart,

o

dass

unterhalb Kleinste

noeh

ITI

sind.

for jedes

yon

= leTl

seien

e die M e n g e

@ hat.

Ordinalzahl

Weiter

AuF

m mit

le'l

. Oie E l e m e n t e

aus

einem

Baum

T

= und




mit

den i n d u z i e r t e n

%

eines

T',

T" von

bestimmt

Probeweis

ist und

s1 9

q

for die

gilt:

sI

for

alle

eeE

S ist

ein

~

e

mit

einer man

=

11 aller i mit ves2[eo][eol]

so liefert

dann die Folge

oder

OI~L

O o V {v} eueh D o vom Typ I ; das-

Aus S' erh@lt man nun S w dutch

Liegt der Typ I oder II vor,

, sodass

diese Abschw~chungen

h~chs-

so folgt aus vcL

s~mtlich

mit Elementen

aus L geschehen. [bbbb]

vER

wegen Beweis

FOr den Typ I kann dieser Fall nicht des Linksprinzips Sw

hBchstens

hOchstens

1 ~1 > o

v*

[d]

o oI > o

v = s 3 [ e o]

S o [ e o]

Typ I v o r ,

folgt.

d I Abschw~ehungen,

Nieder

da eus s3[eo]gL

erh~It

von denen

man aus S' den

im Falle des Typs II

aus R geschieht.

Oieser Fall

~ s3[e I ]

=

so e r h ~ l t

11 ~ o

eine mit einem Element

(c)

[da)

dann

eintreten,

ist symmetrisch

zu [b] 9

.

oder

S o [ e o)

man S w aus S eoo

= dutch

so muss veL , a l s o

.

Ist

h~chstens

v eR

gelten,

eoo d e r o b e r e N a c h b a r von e ~ , d I Abschw~chungen. s o d a s s wegen

D1 s

Liegt

der

diese

W.

Felscher

133

Abschw~chungen

nur mit Elementen

aus L gesehehen.

Kann h~chstens

eine dieser Absohw&chungen

Lie~t der Typ II vor, so

mit einem Element

aus R gesohe-

hen.

[db]

sole o) = 1 dass

o~ > o

und wegen

{da)

A geh~rt,

ist

Sei nun e

Wegen

Iv I = Iv*l > o

gelten

muss; wegen (c) Kann man auch

waiter

[vs)

so bestimmt,

S w = Sle w [dbaa)

nicht

yon e

dass S W

, nioht

{dbab)

St

von

nicht ves2{e o)

,

. Man definiere

das Skelett,

annehmen,

Elemente

veA

v, v

zu

vorauszusetzen.

eine Menge

W =

also auoh den Rang,

[s2{el)(ew ) - {sq(el][ew)})v

von

{w*)

liefert.

v ~s2{el](e 1) .

Man wende das Ausfege-Ver~ahren einen Beweis

o

= v*

so-

~ for jades wEW sei e w in N{e I) und S w in

hat und das Ergebnis ves2[e o)

kein Axiom,

s3(e l)

es keine Einschr~nKung der Allgemeinheit,

sq(e o) - (s2(eo)V s2(el]{el)) naeh

0 1 U {v*}

So(e ~ ) = I . Oa eines der beiden

der obere Nachbar

oo

ist dann

9 W

auf Sleoo

und die S W , S w an; es liefert

s2{eo]V s2{el)[e I) = O o W 01 v es2{el][e I) .

Sel W e die Menge aller w aus W mit v ~ s 2 ( e l ) [ e wj , sei W b der Rest yon W. FOr wow a liefert

die Induktionsannahme

se Sw% und S w~ mit Ergebnissen und

s2{eo)V

,

Wendet

S w mit woW b und die Sw% von

s2[e o] u {s2{el)(e w) - { v ~ ) ) ~ { s q [ e l ) { e w ) }

((s2{elJ(e W) - {v~})

v* ~ s4(el){e w)

S2(e o) v [s2(el)(el)

aus Sle ~ , S w und aus Sle ~ , S W 8ewei-

- {sq(el){ew)})v{~}

man das Ausfege-Verfahren 9 S W~

mit woW a

- {v*}]

= 0~

, da

v~ ~ ~

auf SIeoo

an, so erh&it

und

, W , die S W ,

man einen Bowels

St

01 .

#

{dbba)

ves2(e o]

,

nicht v es2[el){e I]

Oie InduKtionsannahme

liefert

aus

Sleoo

, Sle I

einen Beweis

S' mit dem

Ergebnis

(s2[e o) - {v}) U s4[e o) v s2[el)[e 1) . Man wends das Ausfege-

Verfahren

auf S', W

und die S

[s2(e O) - {v}) v s2{el][el) [dbbbJ

v~s2(e o]

w

, S W anj es liefert

Sw

= O o V 01 .

v es2~elJ[e I)

Man Konstruiere

S' wie im vorangehenden

Fall;

(s2[e o) - { v } ) u sq{e o ) v {s2[el){e I) - {v*}) wie im Palle

einen Bowels

{dbab).

Man wende

das Ergebnis . Welter

das Ausfege-Verfahren

lautet jetzt

definiere

man die Sw~,S W~

auf S', W und die S

oS W w

134

W.

mit

wEWb

(s2(eo]

und d i e Sw%, Sw% m i t - {v}] ~ L~,2(el](e I)

Oamit ist die Konstruktion tung

leicht,

jedenfalls

T i < o~

f2(T2,0~)+1

, f 3 ( T 3 , 0 3 )1+ 1

o F +d 1, [bbb)

o~ +1 ,

o~

mit 11 ~ o

fl(Ti,~,d+1)

mit

Funktion

der S w%

dutch f1[o~,~W,d+1]

9 f1(~

,max[T

f2[T2,o~),

f1[Tl,O~,d+k)+2,

von S j a b g e s c h ~ t z t Im

der S~ , iEI I , abgesch~tzt van S w wie gewOnecht.

dutch fq(T,ol,d+k] I

zw < ~I

;nach

dutch Im Falle

und die ersten

den K Anwendungen

der

w

I weWa),d+1

) + k um 2 , in jedem Falle abet hachstens

sodass man auch dann noah unterhalb

van

bleibt.

besitzen,

folgt

aus

h'(x'

# yJ + h

x'

auch

=

x'

h'[[x'

# y

# y)

angegebenen


~ -- and like the less familiar

languages

infinitary

LK~%~

in

are well ordered outwards).

of minimal

semi-valuations

of cut-free rules (of proof).

from the use of

are well founded is obviously related to

of the subformula relation (in contrast

for card

which strings of quantifiers (ii)

F C F-; otherwise

were envisaged).

The fact that the trees considered

languages

if

d+ and J- (n > O) is clear (enough for the intended n n -- subject to modification if~ for example, some computer

necessarily

implementation

and

Kreisel

in (i)~

We consider

in general

by means of finitary trees: finite sets

F.

As is evident

the set of distinct minimal

semi-valuations

which make

(~)

each

F : F C F+

true and each

has the power of the continuum.

F: F C F-

In any c a s %

false ,

at some nodes of the

sentation there are infinite sets of formulas~

'brutal' repre-

provided some existential

formula

is given the value false.

Exercise.

Given

semi-valuations

F+

satisfying

Nevertheless

and

F-~ show how to determine whether any or all minimal

(~) are infinite.

all minimal

semi-valuations

mined by

(F +, F-); specifically

formulas,

say

FN+

Warninss. fifties,

and

FN, at each node

familiar~

all minimal semi-valuations the property:

those trees, cultivated

the only point that needs verification

are coded (since completeness

if (~) has a model at a l l

sets seems pointless

or unordered

the sets

ability)

refinement

footnote

1 concerning much more delicate refinements

recursive

operations

when operations 2For example, F + U (B,B}

is that

only a tree with

iN, FN

theorem)

satisfying

are to be regarded

(but permitting repetitions)

in the present context,

(of the completeness

requires

since the

the tree codes some semi-valuation

(b) The familiar question whether

as ordered (as finite sequences) 'ordinary'

'coded' by binary trees, deter-

N.

(a) The rules for constructing

are perfectly

(~) above).

can be

by their infinite paths, with only finite sets of

or as

that is, for the on_._~e(defin-

discussed

in this paper; cf.

than such things as primitive

or -- as in [KMS], Part II -- the effect of those distinctions 2

on trees are involved.

the use of 'sets' with repetition ~- F" 0 (A~A}

derive

F + U (B}

and a contraction

~- ?- U CA}

as the rule Rep, discussed at length loc. cit.

rule:

from

has much the same effect

G.

Kreisel

171

Perhaps the most familiar construction is this (which differs from the literature of the fifties only in the use of constants of constants

c13 c2~ ...

N

O~ there is one node

is at level i

2n~ N

'successors ', if

if

FN

where 3xA

is

FN+

is

~ G~ A v B

cG i

often.

N'

or

3xA

FN+

is

(NB:

A[x/eG i]

~ G

A v B, namely

FN

and

F+ ~

F-.

If the node

or

~xA

namely

.

A' by one of the above,

and E' comes

from E by replacing A with A', then E 9 E'. We say then that ~ ~ E' by an inner re-

duction; A > A' by I.I-1.4 we call a main reduction. 1.6. A is strongly normalizable (s.n.), > A2 >

... > An is impossible.

minimal n satisfying 1.7. Remark.

if there is natural number n such that A ~ A I

If A is strongly normalizable

The treatment below may be modified

of permutative

reductions,

(for the case

of §

generalization

to apply to a more general definition

where 0 is allowed to be any inference rule except induction

such a reduction may, however,

of the derivation).

we write ~(A) for the

the above condition.

For applications

is superfluous.

alter the set of open assumptions

of the strong normalization

theorem, however,

this

We therefore prefer to treat the restricted definition,

allowing a greater clarity of the proofs.

2. IMPROPER REDUCTIONS,

STABILITY

2.1. A measure of complexity The measure ~ on formulae is defined by recursion on their length: ~(A)

:= 0 for A atomic

~(A&B)

:~ ~(AvB)

~(VxAx)

:~ ~(3xAx)

~(A§

:= max[~(A)+],

:= max[~(A),~(B)] := ~(A~) ~(B)]

For a derivation A with a derived 2.2. Improper reductions

formula A we also write U(A)

:= ~(A).

*)

Assume that the notion "stability"

and the reduction-step

>o are defined

for deri-

vations A such that ~(A) < n. For A s.t. ~(A) = n we then define

(i)

EO

El

AO

AI

>~

E. A.l l

(i=0, I)

A0&A I

*) Similar notions have been used byH.R. Jervell,

by P. Martin-Lof

and by R. de Vrijer.

186

D.

EA] (ii)

B

A EA] E

-to

A§

whenever

J

,

is stable

A

B

Z(a)

E(t) At

Aa

(iii)

Leivant

for every term t

VxAx E

(iv)

A.

E

l

(i=O, ! )

A, 1

AoVA1 E (v)

At

>o

At

3xAx

Note that these reductions have a combinatorial

do not preserve

the meaning of derivations.

They only

role in the proof of strong normalization.

2.39 We write A >'r A' if for some n _> 0

A -- A0>r A l'zr ...>~ An - A', where>~ is either

or>-. 2.4. Stability It is seen outright A >>

that if A >~ A' then U(A') ~-chain

starting with A is finite (this is

easily proven by induction on the usual logical complexity of the derived formula of A).

D.

Leivant

To prove the converse one needs, prima facie, the fan theorem, uniform bound required

in the definition

servative over Heyting's Arithmetic alternative

characterization

so as to obtain the

of s.n.; the fan theorem is, however,

(TROELSTRA [74]). Note that, in any case,

of stability

3. TREATMENT OF INTRODUCTION

187

conthis

is H 1 I"

INFERENCES AND INDUCTION

ao(a I ) p where p is an introduction-rule an atomic (Post)

If A =- ~

3.1. Proposition.

rule or the replacement rule, and A 0 (and A I) are s.s., then A is s.s.. Proof.

By 3.3, 3.7, 3.11 and 3.12 below.

3.2. Lemma. If A0,AI are stable then so is A B

A0 A

A1

-- A

B A&B

Proof. By induction on ~(A0) + W(Al).

If A > A' then this reduction

is necessarily

an

inner one,

i

v

A0 A' z A

A1 B A&B

where v(A~)+~(Ai)

A O A'

say, then

< ~(A0)+~(AI) , hence A' is stable by induction hypothesis.

A'

is stable by assumption.

By 2.7 A is stable.

If A ~o A'

D

3.3. Lemma. I f A0,A l of 3.2 are s.s., then so is A. Proof9 Immediate from 3.2. 3.4

Definition.

D

Let EA] be a derivation,

"

where [A] is a set of open assumptions F

A

of A

F

of the form A. We say that A is s.s. at [A] if for every stable derivation A' [A] is A stable. 3.5 9 Lemma. Let EA] A be s.s. at EA], EA] A ~ [A]' A' where [A ] ' is the set of copies of ele-

ments of [A]. Then A' is s 8. at EA]' Proof.

Immediate by induction on ~(A). (Note that the same P is substituted for every F occurrence A ~ [A] in 3.2, and that no assumption of F maybe discharged inA in[A].) D --

3.6. Lemma. I f

A

E~] i s s . s . B

a t EA], then

188

D.

Leivant

[A] A

Z -

B

A§

is stable. a v

Proof.

By induction

on v(A).

If Z > E' ~ ~

then v(A')

< v(A), A' satisfies

dition of the lemma by 3.5, and we are done by ind. hyp..

the con-

If

F Z ~o 2' = EA] A

(F

is stable)

B

then Z' is stable,

since A is s.s. at [A] by assumption.

3.7. Lemma. If E A]A is s.s.,

Hence by 2.7 Z is stable.

then

B

[A] A = l B

A§ is

S.8.

Proof.

.

Let

EA**] Z ~-+ 2" -

A, B

A* § B* A is s.s.,

hence A* is s.s. at [A*],

3.8. Lemma. If a is free in Z(a),

so by 3.6 Z* is stable.

So 2 is s.s..

Z > Z', then a is free in Z' (if it occurs there) and

Z(t) 9 Z'(t) for every term t. 3.9. Lemma. If A ~+ A* and a does not occur in any open assumption of A then A ~-+ A*[t/a]

for every term t.

The proofs

of 3.8 and 3.9 are immediate.

3. I0. Lemma. If a is free in A(a) and A(t) is stable for every t then Aa A(a) -

Aa VxAx

D.

Leivant

189

(if at all a correct derivation) is stable. Proof.

By induction

on v(A)

(as in 3.2).

If

A' (a) E >E'

-

Aa VxAx

then ~(A')

< v(A) and by 3.8 a is free in A' and A'(t)

the induction

hypothesis

by assumption. 3.11.

A' is stable.

By 2.7 2 is stable.

is stable

for every t. Hence by

If E ~o l' - A(t) then 2' is stable outright

D

If A(a) is s.s. then so is Aa

Lemma.

A(a) E

Aa

-

VxAx

Proof.

Let A*(a) I ~--+ E* -

A a

VxA*x By 3.9 A~-+ A*(t) required. 3.]2.

for every t, so A*(t)

is stable.

By 3.]0 then E* is also stable,

D

Lemma.

A (i) I f A t i s

A A F t's A A At ond At t=s . (ii) I f AA is s.s., then so are A , A AvB BvA BxAx As A (iii) If A is s.s. then so is ~ p where 0 is an atomic (Post) rule. Proof.

s.s., t h e n s o a r e

Similar

3.]3. Lemma.

to 3.2-3.3. (Note thatF s't is logic free, hence stable outright).

E is stable, and for every term t If A~

[At] is s.s. at [At], A(t)

then

[Aa] E

A(a)

H ~ A5

A(Sa)

IND

At

is stable for every term t. Proof.

By induction

on ~(I) + ~(A) + T(H), where T(H) is defined

T(t)

:= O,

if t is a term and for no term s

T(t)

:= T(S) + l, if ~ is SS,

~ = Ss,

as follows:

as

D.

190

T(H)

Leivant

:= T(t), if the main inference-rule

of the derivation H is IND,

with t as a proper term.

NOW if H > H' by an inner reduction in the proof of 3.10 H' satisfies hypothesis

then T(E') = T(H), 9(Z')+9(A') & by a main detour reduction.

is similar for &E and VE).

H!

I EA]

H ~

H0 ] [

L

F

B

HI

A§

>

A

H 0 and HI are assumed stable,

[A] F

~

A

B

so

ii I [A] H 0 >o

hence A is stable Case [d]:

A

-

F

(2.7).

(ii) applies,

and H > A by a main detour reduction.

H0

[Aa]

At

H|(a)

H ~ BxAx

B B

H0 [At] ~

HI(t) B

and by 4.|(i) -

~

A .

Take the case p = §

(the

192

D. Leivant

By condition Case [el:

(ii) A is stable outright.

(i) applies and H ~ & by a permutative

II O

H ---

!xO

reduction.

r 1 (a)

3

B B

3E (II 1 )

[Aa] Fl(a) ro

B

(E 1 )

3xAx

C

H 0 is stable by assumption,

p

_-- &

3E

H 0 > F! (by a semi-proper

reduction, 1

cf.

1.4), so F| is 0

stable, and v(Fl) < ~(H0).-- H ] is stable by assumption, hence A is stable. A = F 0 is 0 a subderivation of H , hence it is s.n. by 2.9, and v(A 0) s v(H 0) while %(A0) "'" >

(*)

@ At 3xAx

then @ [At]

r1(t)

-: E

B

(~1)

P

is stable. But if (*), then @ [At] H0 >

... Y

0

Fl(t)

=

;

B

so ~(E 0) < ~(H 0) and i(E) < i(H). H0 is assumed stable, hence H 0 is stable (2.7), while E I ~ H I is assumed outright.

Hence E satisfies case (i) of the conditions

duction hypothesis

E is stable. Hence A satisfies

and by the induction hypothesis

A is stable.

stable

of the lemma, and by the in-

case (ii) of the lemma's condition,

D.

193

Leivant

Case Eli: (ii) applies, and H ~ A by a permutative reduction.

(i) [Aa]

r0

rl(a)

3xAx

3yBy

(2) EBb]

(1) 3E

HI(b)

3yBy

C

[Aa]

(1)

(2) [Bb]

rl(a )

~[l(b )

3yBy

C

F0

C

3xAx

H 1 is stable at [Bb] under H0,

l

(2) 3E

(2) ~E

! A (a)

-- A .

I

(1) 3E

H 0 y FI, Hence (by 4.1(i)) H 1 is stable at [Bb] under

F I. We conclude that A| is stable, and that i(A) < i(H) like in case [el. It remains to show that for every t

Al(t) is stable at [At] under F0; i.e.,

that if

(*)

FO> ... >

0 At 3xAx

then @ [At]

[Bb]

rl_t.( )

(b) C

3~By

z: Z 3E

C is stable. But, like in [e], (*) implies that H 0 >

... > _0,a so z-0 is s.n., v(E 0)
o 4' is in general formalizable as a predicate of the form (3r < A') [Stn(F ) & F(&,4',F)] where F is a p.r. relation. 4 > > A '

is 2|0 in >~

is E 0I in St n.

hence A ~ > A '

Stn+l(r) ~ vA'EA>>A' § Sn(A')J, so Stl(A) is of the form V[E

§ E J which is classically a H3-predlcate;

we can see by induction that St

n

is classically equivalent to a H~+2-predicate.

7.2. Consequently, we may formalize within H~+k-arithmetic n) the normalization-proof

(where k is fixed for every

for all derivations A, satisfying:

~(A) ~ n". Some consequences

and for n e 2

"if A occurs in A then

of this are given by TROELSTRA ([73] IV.4).

D. Leivant

197

7.3. Our proof of normalization illustrates the essential role of implication in formulae complexity, since implication is the only logical symhol counted for the measure ~. By 7.2 normalization of derivations with a bound on the (negative) nesting of implications in the formulae (but with no bound on the alternations of quantifiers) is formalized within arithmetic. Thus, for example, Heyting's Arithmetic (HA) is not conservative over 0 Griss' positive arithmetic (NA. Cf. LOPEZ-ESCOBAR [74]) even for Nl~sentences, because the consistency of NA is provable in HA (in fact even in a simple fragment of HA).

REFERENCES G. GENTZEN [36], Die Widerspruchsfreiheit der einen Zahlentheorie, Math. Ann. I12 (1936) 493-565. D. LEIVANT [73], Existential instantiation in a system of natural deduction for intuitiouistic arithmetic, Report ZW 23/73, Mathematisch Centrum, Amsterdam, 1973. E.G.K. LOPEZ-ESCOBAR [74], Elementary interpretations of negationless arithmetic,

Fund. Math. 82 (1974) 25-38. D. PRAWITZ [65], Natural Deduction, Stockholm,

1965.

D. PRAWITZ [71], Ideas and results of proof-theory,

in: FENSTAD (ed.), Proceeding8

of the 2nd Scandinavian logic symposium, Amsterdam, 197|, pp. 235-307. A.S. TROELSTRA [73], Metamathematical

investigation of intuitiouistic arithmetic and analysis, Berlin etc., 1973.

A.S. TROELSTRA [74], Note on the fan theorem, Report 74-14, University of Amsterdam, Sept. 1974. J. ZUCKER [74], Cut-elimination and normalization, Annals of Math. Logic ~ (1974) |-||2.

INTUITIONISTIC COMPLETENESS OF A RESTRICTED SECOND-ORDER LOGIC Dedicated

to Kurt

of his

E.G.K.

w

INTRODUCTION,

icate calculus

Sch~tte

65 th

on o c c a s i o n

birthday

L O P E Z - E S C O B A R and W. V E L D M A N

The completeness of the c l a s s i c a l f i r s t - o r d e r pred-

is over

40

years old, n e v e r t h e l e s s most of the proofs

given for it are,

if not wrong,

at least misleading.

From the prelim-

inary discussions

one is often led to believe that what will be proven

is that every i n t u i t i v e l y valid formula of the ~ l a s s i c a l 2 r e d i c a t e ~alculus~

CPC, is derivable using the axioms and rules of CPC.

ever, what is shown,

is often no more than:

ValcPc(A) ~ > where

"ValcPc(A)"

valid

DercPc(A),

stands for "the formula

(i.e., true in all s e t - t h e o r e t i c

is an a b b r e v i a t i o n for "the formula Of course,

How-

A

A

of the CPC is f o r m a l l y

structures)", is derivable

and

"DercPc(A)"

in the CPC".

it doesn't take much to remedy the situation.

All that

remains to be shown is that every i n t u i t i v e l y valid formula of CPC is f o r m a l l y valid. ity of

A

tations,

The latter is justified on the grounds that the valid-

entails that

A

is true in all p o s s i b l e kinds of interpre-

including the s e t - t h e o r e t i c

structures.

The i_ntuitionistic predicate ~alculus, better.

IPC, has not fared much

To start with there is the t r a d i t i o n a l view that i n t u i t i o n i s m

is solely concerned with questions p e r t a i n i n g to specific m a t h e m a t i c a l constructions. terest

Thus,

from a t r a d i t i o n a l viewpoint,

there is little in-

in a t t e m p t i n g to c l a s s i f y those sentences which are intuition-

istically true i n d e p e n d e n t l y of the interpretation.

In addition,

Heyting has e x p r e s s e d the opinion that his system for the predicate calculus

(and the systems that have since been introduced)

are not

E.G.K. demonstrably

complete;

Lopez-Escobar,

for example

W. Veldman

in H e y t i n g

1966,

199 page

i02,

he

states:

It must be remembered that no formal system can be proved to represent adequately an intuitionistic theory. There always remains a residue of ambiguity in the interpretation of signs, and it can never be proved with mathematical rigour that the system of axioms really embraces every valid method of proof. In view of the fact that m o d e l - t h e o r y classical kind

of

mathematics,

there have

(intuitionistic)

such a m o d e l - t h e o r y (w.r.t.

if it is to be part

model-theory

is one of the

(w.r.t.

methods.

heuristic

use then any valid

istically

true

with respect E.W.

must

then be by

if the m o d e l l i n g (in the

sense

interpretations)

for any

probably

the

first

Predicate

sentence

A

person

Calculus.

In Beth

(0.2)

B - ValIPC(A)

~>

DerlPC(A) ,

(0.3)

ValidlPc(A)

~>

B - ValidlPc(A),

"B - ValIpc(A)"

that

and that

is an a b b r e v i a t i o n

"ValidiPc(A)"

combining

(0.4)

(0.2)

stands and

(0.4) no m e n t i o n

for

(0.3)

ValidlPc(A) in

Furthermore of the

intuitionisti-

of being

intuition-

also be valid

a modelling

1956 he

set out to

of IPC

B - ValIpc(A),

Note

theorem

the proof

who p r o p o s e d

~>

and

if

is to be of any

should

DerlPC(A)

models"

some

Obviously

requirements.

(0.i)

where

to obtain

a completeness

mathematics

use to

to the modelling.

Beth was

that

first

sentence

in all p o s s i b l e

for the I n t u i t i o n i s t i c prove

attempts

the m o d e l l i n g )

Finally

of great

for intuitionism.

of i n t u i t i o n i s t i c

theorem

cally a c c e p t a b l e

been many

is to be of any use then

that m o d e l l i n g )

completeness

has been

"A

for

"A

is true

is i n t u i t i o n i s t i c a l l y

we obtain

that:

--> DerlPC(A),

is made

in all

of the

Beth-models.

Beth

valid".

2~

E.G.K. Just

(0.3)

Lopez-Escobar,

as in the c l a s s i c a l

are of a quite

explicitly

defined

ValidiPc(A),

The

same

case,

as-constructions

counterparts, nature.

mathematical

although

definition. itionistie

different

and

obvious,

is true of

the proofs

(0.2)

constructs;

probably

ValidlPc,

W. Veldman

so it is not

closer

in

solely with

however

mathematical in the intu-

to the concept

immediately

and

(0.3),

no explicit

ValidcPc(A);

is much

(0.2)

is c o n c e r n e d

while

has

of

obvious

of proofs-

that

(0.3)

should

hold. As a m a t t e r cause

there

yields

(see Kreisel

principle

for p r i m i t i v e

Kreisel's

proof was not with

respect

to species

"S - ValIPc(A)".

is that the

to be more

easily

be-

of

of Kreisel

recursive

is yet another

of IPC.

It was

that

predicates

by K r i p k e - m o d e l s ;

(classical)

~>

interpretation, of

which

we shall

S - Vallp C

assumptions

in Beth ab-

over

can be shown to

S - ValIPC(A)

than of

introduced

is played

to v a l i d i t y

implication:

notion

of semantics

respect

An a d v a n t a g e

accepted

treatment

correct

point

(see the report

was a result

(which under a few r e a s o n a b l e

There

was a moot

1982).

ValidlPc(A)

formulae

(0.2)

Markov's

be equivalent)

tends

of

(0.3)

damaging

by

B - Valip C

in the proof

that

Even more

but with

breviate

out

1961).

Actually models,

it turned

was an error

Dyson/Kreisel (0.2)

of fact

(0.3).

(mathematical) in Kripke

for i n t u i t i o n i s t i c probably

completeness

1965.

formal

because

proof was

validity

for the

In the c l a s s i c a l

systems,

of the

a main part

fact that

given with respect

the first to this

type of models. Kripke

models

intuitionistic vative

theories.

extension

itionistically

are often

In addition,

properties,

acceptable

used to i n v e s t i g a t e through

some of those

(see T r o e l s t r a

the

of some

the use of some conser-

results

1973).

strength

can be made

intu-

E.G.K.

In the "valid

following

in e v e r y

The

abbreviate by

the

201

intuitionistic

notion

"K - V a l i P c ( ' ) " .

ValidiPc(A)

~>

in K r i p k e

1965,

justified

acceptance,

However,

even

intuitionistic

and

W. Veldman

implication:

is p a r t l y

an

we w i l l

Kripke-model"

(0.5)

versal

Lopez-Escobar,

S - Valip C

it has

its

if one

accepts

shown

and

although

it does

not h a v e

uni-

charms.

completeness can be

K - VallPc(A).

of

(0.5), IPC

Kripke

(i.e.

models

of

to be e q u i v a l e n t

are no use

(0.4))

since

(under

suitable

for

K - Valip C assump-

tions). In v i e w

of the

tuitionistie istie

proof

proof

with

to c o n c l u d e

notion

of

COMPLETENESS ity for

that

intuitionistic

state

the

FOR

of the

of

that

is not does

(logical)

unless

yield one

obviously

not

validity.

quite As

Is t h e r e

that an

an in-

intuition-

identifies

the

case.

correspond

a matter

intuitionistic

a mathematical predicate

such

that

(A)

the

notion

(B)

the

implication

[ValidiPc(A)

~>

(C)

the

implication

[ViPc(A)

DeriPC(A)]

intuitionistic

state

of

We to the

fact we

problem:

IPC:

VIPC(A)

to

IPC w o u l d

However,

S - Valip C

following

PROBLEM

formulae

it is c u s t o m a r y

principle.

S - ValiPc,

prefer

to

remarks

of the c o m p l e t e n e s s

of M a r k o v ' s

ValidiPc(A)

like

above

has

a semantical

~>

mathematics

without

notion

calculus,

of v a l i d -

say

VIPC(A)

character,

VIPC(A)]

is p l a u s i b l e , is p r o v a b l e

making

use

in c u r r e n t

of M a r k o v ' s

principle?

In this can be

solved

restricted

p a p e r we

will

try to

for a r e s t r i c t e d

second-order

show

that

second-order

language

in the

the

completeness

minimal

sense

that

logic the

~.

problem It is a

second-order

202

E.G.K.

variables

are

intended

definable

species.

are p r i m i t i v e towards order

to range

concepts.

is a

The format

over a subclass

It is minimal

problem

(conservative) of the paper

language

A calculus

w

~

w

A formal

w

Soundness

w

Explicit

theories.

w

A spread

which

w

Construction

of a u n i v e r s a l

w

Construction

of the

of a r e s t r i c t e d

as an extension

of the

semantics theorem

for for

generates

second-order

of the

spread

~.

w

"V"

spread

~.

w

"DerR"

w

The c o m p l e t e n e s s

w

Realizations

and the

explicit

IPC.

logic.

of

predicate

theories.

of explicit

theories.

Z.

~.

~, and

Kripke

models.

THE LANGUAGE OF A RESTRICTED SECOND ORDER LOGIC, can be b r i e f l y

of

described

The lanzuage

as follows:

~.

A denumerable

set

Var

A denumerable

set

Par I

For each

a denumerable

n,

calculus.

realization.

spread

spread

of

intuitionistic

spread

,,n,, and the

Symbols

second-

~.

w

I.i

it is a contribution

the r e s t r i c t e d

of the

falsity

~.

Some p r o p e r t i e s

~

nor

~.

w

of

negation

is as follows:

w

i.

neither

we believe,

extension

The

for

of the f i r s t - o r d e r

for IPC because

w

and the

because

Nevertheless,

the c o m p l e t e n e s s

logic

Lopez-Escobar, W. V e l d m a n

of i n d i v i d u a l of i n d i v i d u a l

variables:

v0, Vl,...

parameters:

set

p(n)

of

set

~ (n) of

a0,al, . . . .

n-ary predicate

variables:

n-ary

parameters:

p(n) _(n) (n) 0 ' ~I ' P2 ' .... For each

n,

a denumerable

predicate

E.G.K. Q(n) 0

^(n) ' UI

First-order

connectives:

universal

symbols:

Symbols

1.3

Pseudo-formulae,

1.4

not of

1965.

V

I~

of v a r i a b l e s

,

but u s e d

formulae

terms.

and s e n t e n c e s

occurrences.

Given

Ix0...Xm_iF

term.

only used

in the o p e r a t i o n

will

The a b s t r a c t i o n

Some n o t a t i o n a l

: U nin(n),

are d e f i n e d

in w h i c h

A sentence

as done

all o c c u r -

is a f o r m u l a

be omitted.

will abbreviate w i l l be u s e d

instead

occurring

ters o c c u r r i n g IXl...XnF,

variables

be c a l l e d terms

are

an

F

occurring m-ary

such that

in

F,

then

elementary

in the m e t a l a n g u a g e

ab-

and are

in

in

F.

F

duction having

FOR

of

variables

(parameters)

'(Aoi)'

then and

Parl(F) Par2(F)

Furthermore

then we d e f i n e

A CALCULUS

and p r e d i c a t e

'VPoP 0'.

is a p s e u d o - f o r m u l a ,

parameters

pseudo-formula

Par 2 : UnQ(n).

will usually

w

IR

conventions:

in the q u a n t i f i e r s

F

of

~, I, ~.

of s u b s t i t u t i o n .

Superscripts

If

a atomic

individual

straction

'~A'

in a b b r e v i a t i o n s :

is a p s e u d o - f o r m u l a

are b o u n d

are all the

the e x p r e s s i o n

'I'

V (2)

any p a r a m e t e r s .

x0,...,Xm_ I

P

n. (i)

quantifier

A formula

Abstraction

1.5

(i)

( , ).

1.2

in P r a w i t z

A, v,

quantifiers:

Second-order

without

20S

' ....

Propositional

rences

W. Veldman

~(n) ' U2

Auxiliary

Lopez-Escobar,

R,

the u s u a l

if

Pari(T)

With

~

T

is the

the set of p r e d i c a t e is the a b s t r a c t i o n

= Pari(F),

we a s s o c i a t e

introduction

set of i n d i v i d u a l parame-

term

i : i, 2.

a s y s t e m of n a t u r a l

and e l i m i n a t i o n

rules

for

de-

A, v,

204

E.G.K.

n, V (I)

and

3 (1).

Lopez-Escobar,

W. Veldman

For the s e c o n d - o r d e r q u a n t i f i e r

t r o d u c t i o n rule is standard

V (2)

the in-

(e.g. as in Prawitz 1965), h o w e v e r the

e l i m i n a t i o n rule is w e a k e n e d to: v p ( n ) A ( p (n))

(V(2)E)

A(T) where

T If

is any F

is a set of formulae of

d e r i v a t i o n in 'mere(A) '

w

R

n - a r y e l e m e n t a r y a b s t r a c t i o n term.

~

of

A

instead of

from ~_~A

F.

R

then

F~A

iff there is a

O c c a s i o n a l l y we shall write

@

AS AN EXTENSION OF THE INTUITIONISTIC PREDICATE CALCULUS,

Let us assume that the i n t u i t i o n i s t i c predicate caloulus,

IPC, has

been f o r m a l i z e d as a system of natural d e d u c t i o n w i t h the falsum symbol

's

as a p r i m i t i v e symbol and negation as a defined concept.

Then given a formula

A

of IPC let

A*

be the formula of

tained by r e p l a c i n g all occurrences of the atomic formula by the sentence

I ;

if

&

~ ~

obin

A

is a set of formulae of IPC then we let

&* = {A* : AEA}. is an e x t e n s i o n of IPC in the following sense:

3.I

THEOREM.

then

AU{A}

is a set of formulae of IPC and

A ~ iPC A

A* ~ A * .

PROOF. of

If

~

The only rule of inference of IPC not included in the rules is the rule for

plexity of

A

Moreover that if

&*~A*

I.

shows that,

~

However a simple i n d u c t i o n on the comfor any

A,

I~A

.

is a c o n s e r v a t i v e e x t e n s i o n of IPC in the sense then

n o r m a l i z a t i o n theorems make the following:

& ~ i P C A. for

~.

The latter is a c o n s e q u e n c e of To be a little more

specific let us

E.G.K. 3.2

DEFINITION.

iff

A

Lopez-Escobar,

A formula

is built up from

V, n, V (I)

and

A

of

~

is e s s e n t i a l l y f i r s t - o r d e r

and the atomic formulae by means of

A,

3 (1)

It should be clear that formula

I

A

205

W. Veldman

of IPC,

A

is e s s e n t i a l l y f i r s t - o r d e r iff for some

A = A*.

The d e f i n i t i o n of a normal d e r i v a t i o n in long to write down, however,

the d e f i n i t i o n

s e c o n d - o r d e r logic have been given

~

w o u l d take too

for the case of full-

(explicitly or implicitly)

in

Girard 1971, Prawitz 1971 and T r o e l s t r a 1973 so that it is a relatively simple m a t t e r for the reader to make the a p p r o p r i a t e changes r e q u i r e d for

~.

E i t h e r using the

(strong) n o r m a l i z a t i o n

for full s e c o n d - o r d e r

m i n i m a l logic or m o d i f y i n g the proof for f i r s t - o r d e r i n t u i t i o n i s t i c logic

(V (2)

causes no p r o b l e m because

formula than

VPA(P)),

ization for

A(T)

is always a simpler

it is possible to obtain a (strong) normal-

~.

Because of the r e s t r i c t i o n we have placed on derivation

3.2

~

in

PROPOSITION.

tially first-order order formulae

~

If

V(2)E

a normal

has the following kind of s u b f o r m u l a property.

~

formula

is a normal A

derivation

from a set

then every formula

occurring

F

in

~

of an essen-

of essentially in

~

first-

is essentially

first-order. An immediate c o n s e q u e n c e of 3.2 is the f o l l o w i n g c o n s e r v a t i v e e x t e n s i o n result.

3.3

then 3.4

THEOREM.

If

AU{A}

is a set of formulae

of IPC and

A*~A

A~IPcA. REMARK.

From (the proof of)

3.1 we obtain that n e g a t i o n in

~

206

E.G.K.

Lopez-Escobar,

W. Veldmsn

behaves in the same way as does i n t u i t i o n i s t i c n e g a t i o n in IPC. example the following are theorems of

An

For

~:

(~AnB)

(A n B) n ~(A

(~B ~ ~A) ^ ~A)

~ 3 x A n Vx~A

An~A w

A FORMAL SEMANTICS

FOR

R,

Our formal m o d e l l i n g for

~

will

be in the style of Kripke 1965.

4.1

DEFINITION.

such that

K

r e l a t i o n on for all

A model-structure

is an inhabited set, K

and

DI, D 2

is a quadruple ~

a reflexive and t r a n s i t i v e

are unary functions on

Dl(e)

is an inhabited

subset of

Parl,

(.2)

D2(a)

is an inhabited subset of

Par 2,

(.31

if

~ s ~

then

DEFINITION.

unary function

M

M(e)

(.2)

if

A (M(e)

(.3)

if

e S 8

4.4 Dz,M>

4.5

such that

on

K

and

D2(~) ! D2(8)"

on a m o d e l - s t r u c t u r e such that for all

is a

~,8 E K:

is a set of atomic formulae,

REMARK.

that "A

DI(~) ! DI(8)

A model

(.i)

4.3

K

e,B ~ K:

(.i)

4.2

then then

Parl(A) ~ DI(~)

A (M(a)

has been v e r i f i e d by stage

such that

DEFINITION.

A realization M

Par2(A) i D2(~),

M(e) c M(8).

If the atomic formula

DEFINITION.

and

of

then we shall say

e".

~

is a structure

is a model on the m o d e l - s t r u c t u r e

Given that

~ =

~

= ) = 0), (previously)

A spread

~,

i.e., on

c o n s t r u c t e d m a t h e m a t i c a l entities. (i -i)

function from the

set of finite sequences of natural numbers onto the set ural numbers such that

0

~

of nat-

is the code for the empty sequence.

will be used for the c o n c a t e n a t i o n function, = < n 0 , . . . , n i _ l , m 0 , . . . , m r _ l >.

Greek letters: functions and [(i)

If

Ec,

and whose range c o n s i s t s of

To simplify matters we use a standard

i.e.,

law

e

~

e,8,..,

is the c o u r s e - o f - v a l u e s

function d e t e r m i n e d by

e,

= . is such that

a member of

will be used for number t h e o r e t i c

Z,

Vi(Z(~(i))

and write:

It will be later shown, a spread

~ =

mappings

F(n), Dl(n) , D2(n)

: 0)

then we say that

~

is

a(Z. in Sections

9 through 13 that there is

whose c o m p l e m e n t a r y law

Zc

such that if we set

F

=

Um(~ F(am)

Die

=

Um(l~ DI (~m)

consists of three

210

E.G.K.

Lopez-Escobar,

D2e then the following Condition

7.1.

UmEi~ D 2 ([m)

conditions

If

set of formulae,

:

n

W. V e l d m a n

are satisfied:

is admitted

Dl(n) ! Par I

by

and

Z,

then

7.2.

If

eEZ,

then

Die 9 = Pari(F e) ,

Condition

7.3.

If

aEZ,

then

Fe

Condition

7.4 9

If

eEZ

and

following

are equivalent:

(ii)

(A~B)

7.5.

the following ({) (s163

VxA(x)

and

If

(s

i = i , 2,

then the

and

BEF8]. Pari(VxA(x))

! Die,

i = i, 2,

then

E Fe ~

7.6.

If

vp(n)A(p (n))

and eEZ

If

and

A(a)

6 FS].

Pari(vp(n)A(p(n)))

! Die,

i : i, 2,

( F e, and

term such that 7.7.

aEDIs ~ >

are equivalent:

VBSEzVT[Fe!F 8

Condition

theory.

are equivalent:

then the following (s

is an explicit

Par I.(AnB) ~ Die,

AEF B ~ >

eEL

V88E~Va[F e i F B

Condition

i = I, 2 .

E F ,

VBBEz[F ~F B

Condition

is a (finite)

D2(n) i Par 2.

Condition

({)

F(n)

T

Pari(T) A

is an

n-ary elementary

! Pari(F$),

is a sentence

of

abstraction

i : i, 2 = > ~

A(T)

e F8].

then the following

are

equivalent: ({) (ii)

w

Der~(A), VaaE~(AEFe).

CONSTRUCTION OF A UNIVERSAL REALIZATION, The spread

previous

section

can be used to define

a realization

~

~ of

of the ~

such

E.G.K.

Lopez-Eseobar,

that for all sentences

S

(8.1)

~ I=S = >

The d e f i n i t i o n of

~ B

~

iff

e,6 ( ~

=

DIs,

D2(e)

=

D2e,

]M(a)

=

{B : B

211

of Der~(S).

is as follows:

DI(~)

W. V e l d m a n

and

Let

F ~ ! F B,

is an atomic formula and

B s F }

and then set

= We prove

< ~ , S , D I , D 2 , ~ >.

(8.1) a s s u m i n g that the spread

~

satisfies conditions

7.1 -7.7. 8.2

LEMMA.

If

Par.(A) c D. 1

PROOF,

--

~

and

A

(i = 1,2),

is a formula of

~

such that

then

i~

By induction on the logical c o m p l e x i t y of

Basis ste~.

A

is an atomic formula.

quence of the d e f i n i t i o n of Induction step.

that

and

Then it is an immediate conseI= .

Let us c o n s i d e r the case when

Assume thus that ~I=~ A . V6BE~VT[8 ~ ~

~

and

T

A.

A = vP(n)B(p(n)).

Then

is an

n-ary e l e m e n t a r y a b s t r a c t i o n term such

Pari(T) ! D i ( 8 ) ,

Then u s i n g the d e f i n i t i o n of

i = 1,2 = > ~

~I=8B(T)].

we obtain that:

212

E.G.K.

V 8~EzVT[F B ~ F

and

such that

T

Lopez-Escobar,

is an

Pari(T)

From the induction

n-ary elementary

~ Pari(Fs),

hypothesis ~I=$B[T]

Using condition

that

( F s.

B(T)

7.6 we then conclude

is similarly

The proofs

abstraction

i = 1,2 ~ >

we obtain

term

~6~(T)].

that ~ F

vp(n)B(P (n))

The converse

W. V e l d m a n

proven.

for the other

compound

formulae

are analogous

(and

well-known). 8.3

If

COROLLARY.

A

i8 a sentence of

(i)

~I=A

iff

V~aEZ(AEF ) ,

(ii)

~ I=A

iff

VaaE%3m(A E F(~m)),

(iii)

~ I=A

iff

Der~(A).

PROOFS.

Of (i),

(ii), immediate.

For

w

CONSTRUCTION OF THE SPREAD ~

next

5 sections

we shall adhere

~,

then

(iii) use condition

OF EXPLICIT THEORIES, For the

to the following

FO,FI,...

is an enumeration

of the formulae

~0,~i~...

is an enumeration

of the derivations

~0 U 9 1 U

... is a partition

into a denumerable

of the set

sequence

7.7.

Par 2

conventions:

of in

of predicate

of pairwise

disjoint

parameters

deDumerable

sets. ~i = {Qio~Qil ''''} ~ o u ~ l U ...

is an enumeration

is a partition

of

of the set

~i Par I

of individual

param-

E.G.K. Lopez-Escobar, eters into a denumerable

sequence

Veldman

W,,

of pairwise

213

disjoint

denumerable

sets

Mi = {ciU'Cil''''} ~k,s

is an enumeration

is a (i-i) mapping ~k,Z,3~

= ek,i,2~

The functions recursion

from

+ 2,

F(m), Dl(m) ,

on the length of (the finite

Basis step.

Xi

~2 x {1,2,3}

+ 1 = ek,s

Z(m),

of

onto

and

and

~

such that

~0,0,1~

D2(m)

sequence

= 0.

are defined by

coded by)

m.

Z(< >) = 0

r(< >)

r

=

DI(< >) = K0 D2(< >) = Q0 Reeursion

step.

F(m), Dl(m)

Suppose that

and

ural numbers

k, s

D2(m) r

m =

have been defined.

=

We then determine

nat-

~k,Z,r~

and proceed by cases depending

on the value of

that if for some

its value is to be

E(m),

such that p

the convention

and that

i,

s,

E(m*~)

r.

We shall follow

is not specified then

and thus the finite

sequence

(coded by)

.,o^

m"s = Case i

~.

r = i.

SHb~__!a. (i)

is not admitted by

If

if for some

Pari(F k) ! Di(m), q ~ p,

q

i E i, 2

is a derivation

then we set: Z(m*l)

=

0

r(m*l)

=

F(m)

Dl(m*l)

=

Dl(m)

U {F k}

then of

Fk

from

F(m)

214

E.G.K~

D2(m*~)

=

hand

for all

(2) and if on the other tion

of

Fk

from

Lopez-Escobar,

F(m)

W. V e l d m a n

D2(m) , q ~ p,

~q

is not a deriva-

then we set:

Z(m*~)

=

0

Z(m*2)

=

0

r(m*~)

=

r(m) U {F k}

r(m*9)

=

F(m)

Dl(m*l)

=

Dl(m)

Dl(m*2)

=

Dl(m)

D2(m*~)

= D2(m)

D2(m*2)

= D2(m).

S~b~e_ib.

If e i t h e r

Parl(F k) ~ Dl(m)

or

Par2(F k) ~ D2(m)

then

we define Z(m*O)

: 0

r(m*~)

: r(m)

Dl(m*0 ) = Dl(m) D2(m*0) Case

= D2(m).

2

r = 2.

In this s > 0

Case

3

B(x),

functions.

That

is,

for each

~(m*s)

=

0

r(m*s)

=

r(m)

Dl(m*s)

=

Dl(m)

U {Cpj : j < s}

D2(m*s)

=

D2(m)

U {Qpj : j < s}.

r = 3. case we c o n s i d e r

in the previous

Sub~ase_~a. some

the domain

we define:

In this duced

ease we enlarge

formulae

If

the f o r m u l a

might

have

been

intro-

cases.

mp_ 2 = i AI, A2,

F k = 3xB(x)

which

(and hence

F k = (ALVA 2)

then we define

Fk

~ r(m))

and if either

or for some p s e u d o - f o r m u l a

for

E.G.K.

Z(m*l)

=

0

r(m*~)

=

Y(m)

Dl(m*l)

=

D2(m*l)

=

in the case that for all

where

Lopez-Escobar,

W. V e l d m a n

21B

E(m*2)

=

0

r(m*~)

=

F(m)

Dl(m)

Dl(m*2)

=

Dl(m)

D2(m)

D2(m*2)

=

D2(m) ,

U

{A I}

F k = (ALVA2) ;

and in case

U

{A 2}

F k = 3xB(x)

we define

s > 0

tl, t2,..,

Z(m*~)

:

0

r(m*Z)

=

r(m) U {B(ts)}

Dl(m*s)

:

Dl(m)

D2(m*~)

=

D2(m) ,

is some

(previously

agreed

upon)

enumeration

of

Dl(m). Subcase

3b.

Failure

of subcase

3a.

Then we set:

Z(m*~) = 0 F(m*8) ='F(m) Dl(m*O)

= Dl(m)

D2(m*~) = n2(m). r(m), Dl(m) ,

Combining we obtain 9.1

the spread

REMARKS.

(A)

m

and

Dl(m) , mitted (B)

m*O

~

two conditions m*0

by

has been defined

= D2(m)

Z.

is admitted

law

~c

by

Z.

so that for any

m

are equivalent:

are admitted

D2(m*0)

into the complementary

~ = .

The spread

the following

D2(m)

by

Z,

F(m*O)

and for all

= F(m),

s > 0,

m*s

Dl(m*0)

=

is not ad-

E.G.K.

216

A node

m

such that

Thus

m

is a p r o c r a s t i n a t i o n

node. ~.

Or in terms

~p

w tion

for

8EZ

and not w o r t h

If

For a p r o o f parameter

theory

aEZ

then

Q

and i n d i v i d u a l 7.3,

namely

is an i m m e d i a t e

tion of

D.

of i0.i it s u f f i c e s

Condition

node

iff

~.

That

),

to o b s e r v e

parameter

that e a c h

consequence

~

F

satisfies Condition

for any

7.2 is

n-ary

Der~(Qcc...c (for

of c a ses

eondi-

i = i, 2.

that

e,

is a d m i t t e d by

8p = 0.

repeating.

= Par.(F

a procrastination

~(Z)

1 and

n Qcc...c).

is an e x p l i c i t

3 of the d e f i n i -

~.

Conditions consider

contains

7.4 - 7 . 7

are a l i t t l e m o r e

complicated

so we shall

them separately.

"v"

AND THE S P R E A D far too m u c h

LEMMA.

i : i, 2

following

properties:

SEA ~ >

~.

For any g iven

information

To every

P a r i ( F a)

(III)

we h a v e that

7.1 is i m m e d i a t e

LEMMA.

(II)

m*0

OF THE S P R E A D

i0.i

(I)

iff

SOME P R O P E R T I E S

as a lemma.

ii.i

node

is a p r o c r a s t i n a t i o n

stating

W. V e l d m a n

(A) h o l d s w i l l be c a l l e d

of f u n c t i o n s

worth

w

Lopez-Escobar,

a(E,

so we f irst

formulae

there corresponds

A, B

sEZ

we find t h a t

cut it down to size.

such that

a subfan

~

of

Par.(A) l

~

with the

AEr~,

SEA

> F a _c r 8 ,

8E~,

p = ~k,Z,l~,

8p # 0 ~ >

p = ~k,Z,3~,

8p ~ 0,

A = Fk

or

F(Sp)J--F k

or

FkEFa, (IV)

8(4,

F~ = 3xCtx) ~ >




VkVs163

8(ek,~,l~)

= a(~k,s

VkV~([6(~k,~,3~) 8(~k,~,3~))]

= 0] v [6(~k,&,3m)

and

= fu(~(ek,~,3m),

= fl(~(~k,s

g' f0' fl

D2e ~ D28

= i),

+ g(8(~k,s

v [8((k,s

where the functions DIe ! DI8~

B(A

A

B({k,Z,&~))]),

are chosen so that

DI8

is sufficiently

(iii) ensures that

larger than

and so that (iv) ensures that the required instantiations junctions on existential

formulae are placed into

F B.

Dla,

of dis-

That such

functions can be found follows from the fact that the only time that constants from

Xp

are placed in

11.2

If

e(~

THEOREM.

Pari(A~B ) c Die ~

and

i = i, 2

Diy

(AnB)

(ii)

(AnB)

then the following

~ F ,

VBB~sEF e ~ r B

and

A(F B ~ >

is at the node

is a formula

equivalent. (i)

(y(Z)

BEF~].

of

~

~p.

such that

two conditions

are

218

E.G.K. Lopez-Escobar,

PROOF.

That

that

the

Let

A

Then

from

({) ~ >

FB's

are

be the

({i)

theories.

subfan

(ii)

and

is an

of

(II)

immediate

Thus

E

W. Veldman

assume

determined

of L e m m a

consequence

ll.1

(ii).

of the

We w i l l

according

fact

prove

to L e m m a

(i).

ll.1.

we o b t a i n

V B B ( A ( B ~ F B) and h e n c e

that

Using

the

monotonici•

there

is

a natural

of

r

number

and

PO

VB~EA(B We n e x t

prove,

If

A(m)

Basis

:

induction

0

can be

stated

Vs[~(m*~)

Furthermore F(m*s)

if

m

= F(m)

F , AI-~B.

Hence

k,

p = {k,~,r~. Case

1

Subcase

we c o n c l u d e

that

that

PO - l t h ( m )

~ PO

that

r(m), r , AI-~B.

then

B (r(m),

so

r(m),

p : lth(m).

Let

Then

F,

AI--RB.

the

induction

follows:

= 0 ~>

r(m*~),

induction

from now

theorem

(r(~P0)).

Then

as

fan

r ,

is a p r o c r a s t i n a t i o n

so the

procrastination Let

PO"

l t h ( m ) < PO"

step.

hypothesis

:

such

on

lth(m)

and

lth(m)

step.

Induction

by

the

node

hypothesis

on we

shall

AI-~B]. then

then

assume

A(m~O)

give

= 0

and

us that

that

m

F(m),

is not

a

node.

Z, r

be the u n i q u e

We p r o c e e d

natural

by cases

numbers

depending

such

that

on the v a l u e

of

r.

r = i. la.

A(m*~)

= O.

Then

the

construction

of

Z

tells

us t h a t

219

E.G.K. Lopez-Escobar, W~ Veldman F(m*l)

= F(m)

U {F k]

and

so the

induction

r(m),

Fk,

of

tells

hypothesis

gives

us t h e n

that:

But the

construction

Fk = A

or

F k E F e.

,A

Thus

as

lb.

A(m~2)

= 0.

Case

2

In this F(m).

case

3

Subcase C(a), ~uction

F(m)I--~F k

that

F(m*2)

= F(m)

and the

argument

is

node.

for

some

argument

s > 0

then

we h a v e

proceeds

as

= 0

A(m*s)

that

r(m*s) =

and

for a p r o c r a s t i n a t i o n

node.

r = 3. 3a.

For

some

F k = 3xC(x) hypothesis

s > 0,

(F(m),

Now u s i n g

condition

we o b t a i n

(IV)

A(m*s)

F(m~s)

= 0

= F(m)

and

for

some

U {C(b)}.

of L e m m a

r(m),

F r o m the

re,

AI-~B.

II.i

we c o n c l u d e

that

AI-~B

re,

or

r(m),

since

3xC(x)

E F(m)

3xC(x),

we h a v e

r(m),

Sub~ase_3b.

F k = (ClVC2).

formula

that

C(b),

F(m),.

But

or

r = 2.

The

Case

either

AI-~B.

Fe,

Then

for a p r o c r a s t i n a t i o n

us that

we o b t a i n

F(m),

Subease

AI--~B.

r,

re,

rei-~B.

that

in e i t h e r

case

A]--pB.

Analogous

to S u b c a s e

3a.

either

in-

E.G.K.

220

Lopez-Escobar,

We now consider the situation when

W. V e l d m a n m

is the empty sequence 9

Then

F ,A I-~B . From the latter it follows that theory we may conclude

w

that

"V" AND THE SPREAD

F I-R(AnB)

(AnB)

~,

any essential use of case 2 of the definition

second-order

quantifier

V(2);

F

is a

E F

In the case of

will be used for the quantifier

and since

"V".

,,n,, we did not make of the spread

~

We will only consider

the first-order

case being almost

As in Section ii we must first obtain an appropriate

fan of

(by essentially

12.1

LEMMA.

corresponds

To every a subfan

(I)

BEA ~ >

Q E D2B

(II)

B(A 2 >

F ~F 6

of

the same as ii.i

(III)

(IV)

the same as ii.i

(IV).

THEOREM.

such that

If

a E ~

and predicate p a r a m e t e r

~

(III)

12.2

sub-

the same method that was used in II.I).

a 6 ~ ~

It

%he

the same. ~

.

and

Q

there

with the f o l l o w i n g properties

vP(n)A(P (n))

Par.(vP(n)A(P (n) )) ~ Pari(F~) l

is a formula of

then the f o l l o w i n g

R two

conditions are equivalent:

(i)

vP(n)A(P (n))

(ii)

E F

VB~E~VT[F ~ i F B

and

term such that

Pari(T ) c Pari(F8)

T

PROOF.

The only interesting

Let

be an

Q

is an

n-ary elementary a b s t r a c t i o n

~>

case is (ii) ~ >

n-ary predicate

parameter

A(T) (i).

such that

E F8]. Thus assume Q ~ Par2(F a)

(ii).

221

E.G.K. Lopez-Escobar, W. Veldman and then let 12.1.

Then

A

constructed

be the subfan of

(ii) specializes

according

to Lemma

to

V 8 8 E A ( A ( I X l . . . X n Q X l . . . x n) E FS) , which in turn leads to

VSBEABP(A(Q) Proceeding

E F(Sp)).

as in the proof of Theorem

11.2 we arrive at

r~i-mA(Q). Then using the assumption

that

Q ~ Par2(F e)

we conclude

r I-~vPA(P) and then that

II

w

Deri~

in S e c t i o n

VPA(P)

II

E F

AND THE SPREAD

~,

Of the conditions

7.1-7.7

listed

7 the following one is the only one that remains to be

proven. 13.1

THEOREM.

For any sentence

S

of

]~

the f o l l o w i n g

two condi-

tions are equivalent:

(i)

Der~R(S )

VCCc~E;~(S E Fa).

(ii) PROOF.

Again the only interesting

case is

ter is proven with the help of the subfan (I)

SEA ~ >

(it) = >

~

of

(i)- and the lat~

such that

S ( r

(II),

(III)

Analogous

to (III) and

w

THE COMPLETENESS OF ~,

(IV) respectively,

of Lemma ii.i.

So far we have shown that for sen-

222

E.G.K.

tences

A

of

Leoez-Escobar,

W. V e l d m a n

I~:

14.1

Der]9(A) ~ >

Va~(A)

(see Theorem

14.2

Va~(A)

nerl~(A)

(see Corollary

However

=>

in order to have an honest

must show that it is plausible

14.3 where

completeness

"The sentence

A

~

theorem

for

~

we

Va~(A)

is an abbreviation of

8.3).

that

Valid~(A)--> "Valid(A)"

5.1)

for the

(informal)

statement

is logically valid from the inruitionistic

viewpoint" In order to avoid multitude

of realizations

the following 14.4

some of the problems associated

schematic

Given that then

~

for

~

with the

it is better to consider

14.3 in

form

is a r e a l i z a t i o n for

~

and that

Valid(A)

~I=A.

One way to show 14.4 would be to give the exact conditions under which:

a sentence

A

of our r e s t r i c t e d s e c o n d - o r d e r

language

i8 logically valid from the i n t u i t i o n i s t i c viewpoint.

Fortunately would Vali~

suffice

we do not need to know the exact conditions.

for our purposes

which would allow us to conclude

show that such properties In V a l i d ( A ) (2)

to specify

characterize

two important

Logical validity

The intuitionistic

viewpoint.

of

14.4, we do not need to ValidR(A).

concepts

and (~)

enough properties

are involved:

It

223

E.G.K. Lopez-Escobar, W. Veldman The e s s e n t i a l

(C1)

characteristics

of

(*) are that:

The validity of a compound sentence be reducible to the validity of simpler sentences,

(C2)

The validity of a sentence be independent of the interpretation of the non-logical symbols. On the o t h e r hand

to be in c o n f l i c t the t r a d i t i o n a l mathematical

with

view

"truth"

fied with

eventually

A possible

the

finding

compromise

as m e n t i o n e d

intuitionism

a proof

in the

is solely (and,

statement

of

(~)

concerned

in fact,

with

the intui-

is sometimes

identi-

of it).

is to satisfy

(**) as far as the

logical

consider

of an intuitionist.

approximation

is a sequence

(both by p r o d u c i n g The

seems

introduction,

In o r d e r to do the latter we must

world"

what he is doing).

characteristic

and t h e i r proofs

could be d e s c r i b e d

"There working

is that

are concerned.

As a first

for,

of a m a t h e m a t i c a l

"mathematical

tionist

(C2)

statements

tionistic

symbols

the e s s e n t i a l

the

"mathematical

world"

of an intui-

as follows: of m a t h e m a t i c a l

statements

new constructions

sequence

itself

on w h i c h he is

and by r e f l e c t i n g

can be thought

on

of as extend-

ing indefinitely". It w o u l d p r o b a b l y arranged

as an

flection

is an important

m-sequence

not a finitist) and

secondly,

experience m -seq u e n c e , person.

be a m i s t a k e

to c o n s i d e r

for two reasons:

part of i n t u i t i o n i s m

and as we all know h u m a n

even t h o u g h

of a given

it does not f o l l o w

Now we are

interested

that

may a p p e a r it w o u l d

in logical

sequence

Firstly,

because

to be re-

(the i n t u i t i o n i s t

reflection

it could be argued

intuitionist

the

that

is very erratic

the

subjective

to him as appear

validity,

is

(part of)

an

so to a n o t h e r that

is we wish

224

E.G.K.

characterize aZZ

those

sentences

intuitionists,

particular appears

creative

subjects

(i.e.,

are not

CI,

@

must

as true by

consider

proofs

any

the way

it

is progressing. for example:

(a) think

iff they

that

correctly,

do have

reduce @

and

Similar interest

both

considerations

assert

proofs

of

A,

struct

later on,

proofs)

the

(b) are and

(c)

@

ac-

of Divine

would

madness,

apply @

to

(AvB)

would

the c r e a t i v e

of

in the

[and

appear,

to us,

If we wish

but also

that he might

intuitionist

not as a

on w h i c h

sequence

(AnB).

subject,

iff

we

Of more

In view

of

see that he

of c o n v e r t i n g

the

that he might

con-

of an i n t u i t i o n i s t

statements

consider

he is w o r k i n g

to be m y s t i c i s m

include

should, c o n s i d e r

world

to u n d e r s t a n d

he a c t u a l l y

(linear)

3xA(x)].

or even those

of m a t h e m a t i c a l

statements

that we

Thus

B.

then we must

it is b e t t e r

accepted.

statements

assert

the m a t h e m a t i c a l

not only those those

was

be a c c e p t e d

in it.

into proofs

sequence

would

had also been

(A^B)

constructed

inspiration).

(apparent)

(A^B)

of m a t h e m a t i c a l

when

if we c o n s i d e r

actions

B

intuitionist

in view of a s s u m p t i o n

only when he had a m e t h o d

already

to be just the

and

concerning

(AnB)

(which

sentences).

see that

is to c o n s i d e r

Thus,

A

sequence

were

our i d e a l i z a t i o n s

then his

the

we w o u l d B

statements

to simpler

only when

was w o r k i n g A

h o w our p a r a d i g m a t i c a l

of c o m p o u n d

if we c o n s i d e r e d

would

intuitionist~

with

by

forgetful.

the truth

both

(i.e.,

that we imagine

world

as valid

too i n v o l v e d

idealizations,

c l a i m to have

Now we must cepts

It suffices

some

be r e c o g n i z e d

not become

to us that his m a t h e m a t i c a l to make

W. V e l d m a n

which w o u l d

so we should

intuitionist.

We do have

honest

Lopez-Escobar,

in his

considers later

on.

(or the result

the m e t h o d

in the

"mathematical

world"

at a given moment, Or in o t h e r words,

the m a t h e m a t i c a l

sequence

on,

but r a t h e r

world

of a

as a p a r t i a l

E.G.K. Lopez-Escobar,

W. Veldman

225

ordering. Our notion of r e a l i z a t i o n

for

called a "temporal" record of the

~

corresponds

to what might be

(possible) results of a creative

subject, w h e r e for simplicity we "record" only atomic acts or statements.

That is, suppose given

~

= .

corresponds to the structure of e v i d e n t i a l and e n v i s i o n e d by some creative subject. Dl(e) up

~;

D2(a)

Then given an

D2(a)

lection of rather simple species)

~EK,

objects e o n s t r u c t e d

is the c o l l e c t i o n of atomic

since species are properties,

situations e n c o u n t e r e d

gives us the c o l l e c t i o n of m a t h e m a t i c a l

to stage

Then

statements

(or

could be c o n s i d e r e d as a col-

c o n s i d e r e d up to stage

specifies those atomic statements v e r i f i e d by stage Now, granted such a reading for a r e a l i z a t i o n

a.

M(a)

a.

~

of our res-

tricted s e c o n d - o r d e r language, we obtain, by a simple induction on the logical c o m p l e x i t y of the sentences of

{A : A

is a sentence of

~

~,

and

that given

~EK:

~]=aA}

coincides with the c o l l e c t i o n of sentences c o n s i d e r e d as true sentences by the creative subject at stage In p a r t i c u l a r we obtain that ~I=A}

{A : A

~. is a sentence of

~

and

is the c o l l e c t i o n of sentences which are true for the given

creative subject at all stages of his m a t h e m a t i c a l world. Now we can return to 14.4. is a r e a l i z a t i o n of

~

Thus suppose that we are given that

and that V a l i d ( A ) .

Then

ered as true by one and by all of the intuitionist.

A

is consid-

Thus

appear in all the m a t h e m a t i c a l worlds of the intuitionist, A

is logically valid it would be in all the stages.

can be i n t e r p r e t e d as t h e ' ~ a t h e m a t i e a l world" then

A

would

and since

Thus if

~

of some i n t u i t i o n i s t

~I=A. Thus the truth of 14.4 is reduced to the question:

226

E.G.K.

Lopez-Escobar,

Can be an arbitrary r e a l i z a t i o n

W. V e l d m a n

~

of

~

be i n t e r p r e t e d as the

(possible) m a t h e m a t i c a l world of some i n t u i t i o n i s t ?

Actually,

in view

pleteness t h e o r e m tion.

answer

(?)

it suffices

Thus w h e t h e r

in fact

of Corollary

an honest

to c o n s i d e r

or not the

theorem

w

correctly

thinking

intuitionistic

restricted

second

realizations Furthermore of the

gives since

does

R

of

~

is

upon a p o s i t i v e

(see Section 8) be in-

the

intuitionists

and not forgetful) of them

(i.e.,

it seems

so as to have

AND KRIPKE MODELS,

predicate

order

logic

calculus ~,

us a (formal)

the notion

the r e a l i z a t i o n s

Kripke models

relationship for the

or not rests

shown

to be

not u n r e a s o n -

a positive

an-

(?).

R E A L I Z A T I O N S OF

of the

~

idealized

able to a l l o w our i d e a l i z a t i o n swer to

result we have

(possible) m a t h e m a t i c a l world of some i n t u i t i o n i s t ?

Since we have a l r e a d y honest,

realiza-

question:

Can the u n i v e r s a l r e a l i z a t i o n

terpreted as the

of the com-

just the u n i v e r s a l

completeness

completeness

to the f o l l o w i n g

8.3, for the p u r p o s e s

between

for

Since

has an a n a l o g u e

(formal)

of v a l i d i t y ~

specially

IPC via Kripke m o d e l s

leads

since

in the

for

~

vla

for the IPC.

are n a t u r a l

modifications

to c o n s i d e r

a completeness

to M a r k o v ' s

A

formula A~

validity

of IPC it may be of interest them;

every

principle

the

theorem and ours

not. It is now common

is e q u i v a l e n t "absurdity"

to s e c o n d - o r d e r

may be defined

that by further to all

knowledge

intents

restricting and purposes

that

second-order

intuitionistic

by

V(2)PP. ~2

minimal

logic

and that

What we have

we obtain

a conservative

logic

extension

in

observed

a calculus

~

~2 ~2 is

which

of IPC and

is in

E.G.K. w hich n e g a t i o n Because

tions even

(nor absurdity)

~

in view of our

of

~,

~J=l

verified)

ments

are

the v i e w p o i n t

15.1

such that

~ J=l.

treatment

The

(informal)

but r a t h e r

to the

considered

in

~

DEFINITIONS.

of

I

Or put

we obtain

appear

interpretation

for the r e a l i z a true

too few e l e m e n t a r y

in more

some

strange.

to the False being

fact that

~ .

227

rSle.

latter may

does not c o r r e s p o n d

from

W. Veldman

has no p r i v i l e g e d

of such n o n - p r e f e r e n t i a l

realizations However,

Lopez-Escobar,

picturesque

(or state-

terms,

is not very d i s c r i m i n a t i n g .

Let

~ =

be a r e a l i z a t i o n

and

e~K.

(i)

~

is a credulous

(2)

~

is a trivial r e a l i z a t i o n

iff every node

(3)

~

is a natural

iff there

for

Then node

of

realization

~

iff

~J=~ I. is credulous.

is a node

of

~

which

is

not credulous. (4)

is an ideal r e a l i z a t i o n

~

iff every node

of

~

is not credu-

lous.

The

ideal r e a l i z a t i o n s

that any

ideal r e a l i z a t i o n s

(as far as f i r s t - o r d e r versa.

15.2 (I)

tion

to Kripke

can be t r a n s f o r m e d

formulae

The t r a n s f o r m a t i o n s

are

concerned)

models

in the

sense

into an e q u i v a l e n t Kripke model

and vice

are as follows.

DEFINITIONS. Given

a realization

the Kripke m o d e l (2)

correspond

Given

a Kripke

predicate

let

Q

=

for

~

let

(~)i

be

. model

First

~

for

K = ~

obtained

Then define

(K) 2

be the r e a l i z a -

as follows:

be a new p r o p o s i t i o n a l

parameter).

let

parameter

for all

~(K:

(i.e.,

a

0-ary

228

E.G.K.

The r e m a r k

If

~

:

D(~)

D2(~)

=

{Q} U M(a).

the e q u i v a l e n c e

is an ideal r e a l i z a t i o n such that

K

for

is a Kripke

~

itf

model

A

A

iff

f

is a Kripke

model

15.6

If

~

is an ideal

realization

node

(i.e.,

if we simply then, Let

if

~

above

then

all the

anything

is a

of IPC

is an ideal

realization

((K)2) 1 : K.

for

and

~,

then

for any

A

a credulous

node

~ s 8

credulous

is left,

be the result

A

(~)i

of IPC

formula

is credulous

delete

provided Red(~]

first-order

every node

then

(K)21= ~ A*.

If

Because

~

(K) 2

15.5

essentially

ideal r e a l i z a t i o n s

~l=e A*.

then

and for any formula K~

for

for any formula

(~)iI= ~ A

If

between

as follows:

Kripke m o d e l

15.4

W. V e l d m a n

DI(~)

concerning

can now be stated

15.3

Lopez-Escobar,

nodes

we obtain

of d e l e t i n g

the

is also

then

8

a credulous is credulous)

of a r e a l i z a t i o n an ideal

realization.

credulous

nodes

of

~.

Thus

15.7

If

~

is a n a t u r a l

realization

then

Red(~)

is an ideal

realization.

It is easily if

~

natural tence

proven

is a credulous realization, A:

by induction

node

of

~,

on the c o m p l e x i t y

then

~ = ,

~ I= A.

we obtain

Then that

of if

A ~

for any

that is a sen-

E.G.K. Lopez-Escobar, W. Veldman 15.8

~ I=A = >

15.9

Red(~)l=A ~ >

229

Red(~) I=A,

Ve ( K ( 7 7 ~ I = a A ) .

In the case of the universal spread

~

: ,

Lemma 8.2

allows us to t r a n s f o r m 15.9 into:

15.10

Let

Red(e) l=A : >

MA

Ve (~ 7-13m(A ( F ( ~ m ) ) .

be an a b b r e v i a t i o n for the following:

Er(~m)) : >

MA : Va ( ~ 7 7 3 m ( A

Ve ( ~ 3 m ( A

E r(~m)).

Then from 15.10 and the p r o p e r t y of the u n i v e r s a l r e a l i z a t i o n we obtain:

MA =>

15.11

Since

Red(e)

15.3 - 1 5 . 6

Der~(A)).

is an ideal realization, we can apply the results

to conclude that for f i r s t - o r d e r sentences

MA, = >

(A

is valid in all Kripke models = >

Or in other words, recursive predicates

(~)

(Red(e)l=A = >

A

I--IPcA).

under the a s s u m p t i o n that for all p r i m i t i v e A(n):

V~ E~ u 7 3 n A ( a n )

~>

Va 6 ~ 3 n A ( ~ n )

we have r e c o v e r e d the completeness t h e o r e m for IPC w i t h respect to Kripke models which, as shown in Kreisel 1961, implies

Ve (B q 7 3 n A ( n , a )

=>

for primitive r e c u r s i v e predicates

V~ (B3nA(n,~).

A(n,~).

Since the nodes above a credulous node are also credulous~ we see that the r e a l i z a t i o n s up from ideal r e a l i z a t i o n s

for

~

can be c o n s i d e r e d as being built

(which c o r r e s p o n d to Kripke models

for

230

E.G.K.

Lopez-Escobar,

IPC) and trivial realizations

W. V e l d m a n

(in which every sentence

would appear that the reason why Markov's our completeness

theorem

a node in a realization

principle

is true).

is avoided

It

in

is because we do not have to decide w h e t h e r is credulous

or not.

Further evidence

to

this last remark is given by the following: 15.12

THEOREM.

If

~

is a natural realization for

=

and (D)

then for every sentence

S

of

l=S PROOF.

Let

complexity

K~ = {~K

iff

:7 ~ I =

Red(~)l=S.

I}.

Then we prove by induction

of the formula

(i)

for all

aEK*,

~ I = a A ~ Red(~)I: aA.

Let us consider the case when

A = (BnC).

Red(~)I= e

That is ~ I=~ (BnC).

(D), that for all sentences Va E K[~I=aS]

S iff

~I=@B.

and

we conclude

node of v B~K*.

(i) has been established

thus that

gives us that

more we are assuming ~I= BC].

BEK*

That ~l=a (BnC)

Suppose

be such that

hence,

Once

on the

Red(~)I= ~ If

B(K*

Red(~)l= BC

then and

that

~ I=BC.

If

and thus

~ I = BC.

Further-

Thus we have that

we obtain,

VB {

again with the help of

of Va ( K*[Red(~)I=~S].

E.G.K. w 16. HISTORICAL The above lings

theorem

his book "The Foundations can be compared

structed

in w

231

seems to confirm E.W. Beth's

the way in which his theorem

One gets this impression

there

W. Veldman

REMARK

completeness

concerning

Lopez-Escobar,

from reading Section of Mathematics".

with the spread

The semi-models

could be saved. 145, last paragraph,

(The semi-model

~ of explicit

theories,

theories,

occuring

was right in thinking that defining a fan of models, some inproper

points,

and then applying

in

M mentioned con-

in M which are not proper models

be compared with the overeomplete

taining

own fee-

can

in ~ ). So Beth necessarily

the fan theorem,

conwould

give the desired result. It is a pity that he did not carry out this program and distorted Brouwer's

argument

for the fan theorem.

seen the crucial rSle

of negation.

paper are a continuation

of Beth's

He also does not seem to have

Nevertheless,

the ideas in this

and it is a matter

of historical

justice to mention his name here. (We are indebted

to Prof.

Troelstra

for asking our attention

for this.)

232

E.G.K.

Lopez-Escobar,

W. Veldman

REFERENCES BETH, E,W, 1949 Semantical considerations on intuitionistie m~thematics, Math., vol. 9.

Indag.

1955

Semantic entailment and formal derivability, Mededelingen der

1956

Semantic construction of Intuitionistic Logic, ibid., vol. 19,

Kon. Ned. Akad. v. Wet., new series, vol.

18, no. 13.

no. ii.

DYSON, V,H, AND KREISEL, G, 1961 Analysis of Beth's semantic construction of Intuitionistic Logic, Technical Report No. 3, Applied Mathematics and Statistics Laboratories, Stanford. GIRARD, J-Y, 1971 Une extension de l'interpretation de G~del ~ l'analyse, et son application ~ i'elimination des coupures dans l'analyse et la theorie des types, Proceedings of the Second Scandinavian Logic Symposium, (Fenstad, Editor) pp. 63-92. HEYTING~ A, 1966 Intuitionism, An Introduction. Amsterdam.

North-Holland

Publishing Co.,

KREISEL, G, 1962 On weak completeness of intuitionistic predicate Journal of Symbolic Logic, vol. 27, pp. 139-158.

logic, The

KRIPKE} S, 1965 Semantical analysis of Intuitionistic Logic, Formal Systems and Recursive Functions, (Crossley and Dummett, Editors), pp. 92-129. PRAWITZ, D, 1965 Natural Deduction, A Proof Theoretical Wiksell, Stockholm. 1971

Study.

Almquist and

Ideas and results of proof theory, Proceedings of the Second Scandinavian Symposium,

(Fenstad,

Editor) pp. 235-308.

TROELSTRA, A,S, 1973 Metamathematieal Investigation of Intuitionistic Arithmetic and Analysis. Lecture Notes in Mathematics, vol. 344. E.G.K. L6pez-Escobar Department of Mathematics University of Maryland College Park, Maryland 20742

W. Veldman Math. Instituut Katholieke Univ. Nijmegen

THE REAL E L E M E N T S

IN A C O N S I S T E N C Y TYPE T H E O R Y

Dedicated

to Kurt

SchHtte

PROOF FOR SIMPLE

I

on the o c c a s i o n

of his 65 th b i r t h d a y

Horst

Luckhardt

Abstract

This

is the first of two papers

of simple tion,

type theory mean,

the s t r o n g e s t

question

recursive plus

type

theory

functionals

results

one c o m p r e h e n s i o n

method

today.

by i n t e r p r e t a -

Concerning

to a r i t h m e t i c

the q u a n t i f i e r f r e e

over

consistency

the

first

are proved.

can be r e d u c e d plus

What does

and hew can it be a c h i e v e d

constructive

the f o l l o w i n g

(I) Simple

on the questions:

a special

over

the p r i m i t i v e

rule of e x t e n s i o n a l i t y

A-property

on objects

of type

O.

(2) C o n s i s t e n c y cator", types

is fully d e s c r i b a b l e

a generalization

and e x t e n s i o n a l i t y .

(3) A n e c e s s a r y primitive

recursive

types O(Oe)

based

it rather

instances

ency proof

has

of c o n t i n u i t y

for c o n s i s t e n c y contains

indi-

with r e s p e c t

to

is that

the theory T of the

no c o n t i n u i t y

indicator

for

points.

gives

to the negations

and to c o n t i n u i t y

to make

"continuity

Especially:

on c o n t i n u i t y

leads

prehension

of the m o d u l u s

functionals

at d e f i n a b l e

The ~ - o p e r a t o r ening;

condition

by the n o t i o n

very

no p r o o f - t h e o r e t i c

strength-

of the above m e n t i o n e d indicators.

fine distinctions.

Therefore

com-

a consist-

234

H.

(4) w - r u l e s

for

to t h e o r i e s

types

greater

of c l a s s i c a l

strength.

Moreover

AemiVa.e

= a imply

recursive

constructive

Markov's

incompatible

with

higher

second

paper makes

question

by

and

By G ~ d e ~ s w e l l - k n o w n creasing

strength

consistency

concepts

} O are

the

this

it f o l l o w s

intuitionistically

functional

functionals

which

Significant

by p u r s u i n g

which

was

interpretation have

only

results

Hilbert's

developed

in a p r e v i o u s

using [33.

than on the

But

this

proof

more

this

on

of

a descripon the

fundamental

in f u l l

paper

for

justified

for a r i t h -

the b a s i s

ordinal

segments

and

intuitionistic

means

properties

to the b a r - r e c u r s i v e

functionals.

of t h e s e

is shown.

For

today

in the

concentrates

to a q u a n t i f i e r f r e e

functionals

concept.

we have

more

notions

there

of

calculus

is v i a

their

- in the c a s e step

on

constructive

functional

first

con-

one way

inter-

ordinal

o n the c o n s t r u c t i v e The

in-

inductions

f o r m of v a r i a b l e

second

analysis

is o n l y

So the o n l y

of

and relations

into

transfinite

of p r o o f s .

In the

systems

by an i n s i g h t that

good

for

abstract

not mean

analysis

This method

and more

proofs

does

is a v e r y

combinatorial

in a r e d u c t i o n

consistency

can only be

say b y f i x e d

- although

pretation

From

of a n o n -

survey

require

meaning.

to do this, them

of

obtained

results

them which

structive

the e x i s t e n c e

absurd.

type

of a c e r t a i n

and K r e i s e l - T r o e l s t r a ' s

that

- explicit.

the a u t h o r

analysis

consistently

interpretation.

Introduction

between

are

be a d d e d

: a.

failure

means

above

and analysis

of

and A~Va.~

the

cannot

(MP)

is n o t

objects

of t h e r e a l e l e m e n t s ,

functional

O.

principle

- even with

intuitionistic

concept metic

(MP)

comprehensions

tion by

zero

intuitionistic

function

fo~ lawlike

second

than

intuitionistically

that w-rules

The

and

Luckhardt

step

content consists

of a n a l y s i s ,

the c o m p u t a b i l i t y

the n e w a b s t r a c t

notions

H.

used

The

are of

first

mainly

principle

is an i n d u c t i o n

computation the author

t i o n of B r o u w e r ' s

The

second

tool

computation ciple

according

consistency

constructively

of

to r e a l i z e

matical bert's

real

vantage

and

that

it g i v e s

the q u e s t i o n

The

answer

no!

classically

directly method

Can

in t h e

and

gives

of

of

us

this

the

opinion

- although

connexion

it c o n c e r n s

with

which

notions

the

are

prin-

for the theorem;

which

domains

occasion method

to s i m p l e simple

enable

of m a t h e on H i l -

has

a constructive

the adcontent.

type

type

theory?

theory

- the higher

is

types

cannot

be g r a s p e d

forced

to set u p a n e w

analysis.

treatment

the

that we dispose

analysis

So h e r e w e

that

way.

fact

theorem

objects

says

is n e e d e d

at a n o t h e r

of

species.

underivability

be e x t e n d e d

the p r i n c i p l e s

The

is the a d d i t i o n a l

interpretation

is t h a t

manner.

from

which

and uniform

classical

its p r o o f - t h e o r e t i c a l

author's

on the

explained

idealized

up

but which

second

-

is the g e n e r a l i z a -

such fundamental

this m e t h o d

The reason

new

rests

abstract

elements,

in an e f f e c t i v e

which

analysis

ics.

is:

is:

a generalization

produce

proof

to e a c h

built

the m e t a t h e o r y

as a n a l y s i s .

this

in a c o n s t r u c t i v e

the a u t h o r

ideal

Now

only

As

strong

This

the s y s t e m

the c o m p u t a b i l i t y

activity.

types.

to G ~ d e l ' s

sufficient

makes

principle,

in all

directly

as

to s p r e a d s

is n o t w i t h i n

it c a n b e v i s u a l i z e d

us

works

which

for a t t a i n i n g

bar-induction

proof

the

- locally

introduced

procedure

consistency

theory

principle

is a u n i f o r m i z a t i o n

here which

In short,

235

two k i n d s :

tool

the

Luckhardt

in E33

fundamental

The

significance

is s t r e s s e d domain

of

because

of m a t h e m a t -

H.

236

The

aim of

these

will

look

for n e w

to us

a further

two p a p e r s

and

notations

direction

type

theory.

be t r a c e d

the

this

properties.

situation.

These

At

first

then w i l l

we

indicate

of r e s e a r c h .

axiom

theory

systems

over

the

considered

functional

here

for a r i t h m e t i c ,

language

as w e l l

as

the

used.

w 2 is d e v o t e d type

is to a n a l y s e

characteristic

In w I we d e s c r i b e analysis

Luckhardt

to the p r o o f - t h e o r e t i c

By the m e t h o d s

back

o~ G ~ d e l

to c o m p r e h e n s i o n s .

ducible

from

one

simple

Finally

also

extensionality

reduction and C o h e n

Further,

comprehension

and the

each

(C)~

axioms

of

a pure

of

choice

comprehension

of

can be e l i m i n a t e d

simplification

can

is de-

A-property.

by r e l a t i v i z a t i o n

as

in [3].

Because

~((C)~

sistency

of type

represents

a generalization and

theory

is e x p r e s s e d

of the

"modulus

extensionality.

theory

T of

indicator that

for

the

types

the a d d i t i o n

strengthening

of

and

functionals

based

because

distinctions.

w 4 it is p r o v e d to c l a s s i c a l

the

~-operators of

consistency

definition.)

that

w-rules

or i n t u i t i o n i s t i c

points.

respect is,

that

the

no c o n t i n u i t y

does

the

not

shown

alter

formation

the

of c o n t i hand

- is a p r o o f - t h e o r e t i c

the p r e c e d i n g

level

a consistency

~ 0 cannot

theories

to type

(On the o t h e r

assumed

types

-

- It is f u r t h e r

~((C)~

of

con-

indicator"

contains

allow

Therefore

for

with

on c o n t i n u i t y

(C) a, ~ ~ 0 - c o n s i s t e n c y

make

ently

Such

in w 3 the

for e x a m p l e

at d e f i n a b l e

the d e r i v a t i o n

by t r u t h

In

of c o n t i n u i t y " condition

of ~ - o p e r a t o r s

be p r o v e d fine

O(0~)

strength.

indicators

the a d d i t i o n

A necessary

continuity,

by a " c o n t i n u i t y

the p r i m i t i v e - r e c u r s i v e

proof-theoretic nuity

a certain

which

can

proof

has

be a d d e d

contain

the

then to

consist-

H.

primitive-recursive theorem

and w h i c h

Moreover tive

principle

compute

(MP)

O with

of the e x i s t e n c e

the failure

comprehensions

means

elements,

and analysis,

is studied

on the c o n s t r u c t i o n

are c o n c r e t e

m e n t of type

hints

theory

Functional

the n o t a t i o n s

there

in this

statements

indicating

Axioms

language

of type

which

treat-

to formulate

Notations.

the theory of simple

only e q u a l i t y the n o t i o n

types

of type o. Besides "type degree"

~: m a x ( g s l , . . . , g ~ m ) + 1 , the c o r r e s p o n d i n g

an e x t e n s i o n a l i t y

rule

(ER)-qf for q u a n t i f i e r - f r e e

to that in [33,

for f i n i t e l y m a n y e l , . . . , ~ m for gs > g6.

be realized.

proof-theoretic

type ~ can be coded

~ 6 is short =

re-

proceed.

of type theory.

the type O s l . . . ~ m ( m ~ O)

>

to the case of

can a c t u a l l y

Each

>

for arith-

characteristic

set hierarchy.

analogous

of

concept

in [43

Contrary

case,

might

in [33 here we still use

for

Then H i l b e r t ' s

how a natural

E3J using

g ( O ~ 1 . . . s m) denotes

are,

it is s u i t a b l e

in the f u n c t i o n a l

holds

objects

the

can only be describ-

by the author

for type theory.

by i n t e r p r e t a t i o n

language.

For our p u r p o s e s

a manner

this

interpretation

which

explicit.

w h i c h was r e a l i z e d

strictions

T plus

construc-

with M a r k o v ' s

= a. From

for lawlike

functionals

- is m a d e

and analysis,

the power

together

of the f u n c t i o n a l

- even with

arithmetic

w hich

recursively.

of a n o n r e c u r s i v e

As~Va.s

of e-rules

and the fan-

(MP) and A s ~ l Va.s = a follows.

of the real

I.

arithmetic

constants

intuitionistically

incompatibility

ed by i n t u i t i o n i s t i c

These

function

and K r e i s e l - T r o e l s t r a ' s

In the second part

metic

237

intuitionistic

all their

can be p r o v e d

intuitionistic

higher

functionals,

the n o n a b s u r d i t y

function

Luckhardt

pp. and

24-26 6 with

level

in each type

provided

6 within

formulas,

g6 > ge;

in

in

the same

g6 ~ m a x ( g s l , . . . , g S m ) .

238

H. L u c k h a r d t

E s t i m a t i o n s of p r o o f - t h e o r e t i c

strengths - by this we u n d e r s t a n d the

imitation of proofs of one system by proofs of another system in a fixed manner -

(The insight in such facts has its own p r o o f - t h e o r e t i c

are e x p r e s s e d by O.

In w 2

of

from which

as f o l l o w s :

Ax~

in

(AC) ~'~

and for

are

thus

we

by r e l a t i v i z a t i o n add

again

the

simple

obtain:

all simplified.

introduction

We do this

of h i g h e r

types

by f o l l o w increases

240

H.

the s t r e n g t h pressed:

situations

of h i g h e r

Theorem all A

o

of p r i n c i p l e s

Luckhardt

well-known

can be s i m p l i f i e d

in lower

types or o t h e r w i s e

in a u n i f o r m m a n n e r

with

ex-

the use

types.

1(a)

F o r all types

B, 6 i, ~ ~ B, u

L 6i

(i = I ..... n) and

:

. ~ A o ( ~ - l y ~ ' ~-I Y I ' ' ' ' ' A (C)~_[]ly ~ "'" []nZn

~ lyn)

(C)B-DIX~I ... [ 3 n X ~ A o ( X B , X I ..... x n) where

~, ~-I

The p r o o f

are c o d e s and t h e i r

is o n l y an e x e r c i s e

[3x6B[x] f o l l o w s

in coding.

the r i g h t

the left side by s u b s t i t u t i n g

Theorem

I (b)

Proof:

By t h e o r e m

~-(C)~ A

r

from w h i c h

one gets back

to

for x.

for all B >

I (a) w i t h ~ - B, n = I

= o-->

Icl~

h e r e can also be w r i t t e n

But this f o l l o w s

I(c)

Because DyYB[~-ly]

side,

(C)~

Icl~

Theorem

types.

= O D 1 X l . . . [ ] n X n A o (%-ly,xl ..... Xn)]

y by #x B y i e l d s

The p r e m i s e

of a p p r o p r i a t e

f r o m ~ - 1 ~ x = x the left side states

VzAya[zy Replacing

inverses

directly

from

F o r e a c h A there

(C)~

-->

as

= o nvB (IY'X(~-Iy))Yl (C) oe ---~I

= O.

(C)~

is an ~ such that for all

B >

(C)-A

A

Proof:

It s u f f i c e s

to p r o v e

the a s s e r t i o n

for p r e n e x

A ~ []iXl...~mXmAo[X I ,. . . , X m , X , U I ,. .. ,u n], w h e r e variables

of A. We use i n d u c t i o n

with respect

u I ,. ..,Un are all free

to m.

H.

I.

m=

Let

~ be

Luckhardt

241

O: the

characteristic

functional

of A

in T

([3],

p.

62) :

O

~ U l . . . U n u = O In t h i s

case

take

e H: 0 a n d

A o [ U , U I ..... u n] ~ U l . . . u n as

the

desired

comprehension

functional.

II.

m+

O:

Case

1:

A

E Ax] D2x2...DmXmAo[Xl

= By

induction

Ax'~

B [ x 1 , x , u I ..... u n]

hypothesis

(C)~

-->

..... X m , X , U I ..... u n]

there

VyAx,x]

is a 6 w i t h

{yxx I = O < - - >

B[Xl,X,Ul,...,Un]}

Thus (c)O6-A^(c)OY-A

-->

VyAX

{AxI.yxx I = 0

VYIAuOY

(+)

-->

namely

z = l x . y I (yx).

~-:

gives

~ > 6,y

and

(C)~

{zx = 0 < - - >

A X ~ ' U X I = O}

A[X]}

6

if

Y

otherwise

all

g6

> gy

B >

--> (C)~

,, (c)~

Theorem

(+)

--> (C)-A Case

2:

According

A

-= Vx] to c a s e

(C)~

A

Putting

{

for

VZAX

{yl u = 0 < - - >

A[X]}

B[Xl,X,u1,...,u ] there

n]

is e s u c h

Vzmx

{zx = O < - - >

-->

VzAx

{~(zx)

-->

VyAx

{yx

that ~A[x]}

= 0

= O

for

A[X]}

i[x]}

all

@ >

I (b)

H.

242

namely

y = Ix.s-g(zx).

Remark:

Similarly

For e a c h A there

one

theorem

paragraph

Theorem

I(c)

can be

prehension

can g i v e

is ~ such

(C)~

Using

Luckhardt

^^

(c)~

continued.

figure

is c a l l e d

for

all

-->

(C)-A.

there

reduced

of

Because

in a p r o o f

~ =^ ~r w h e r e

in a p r o o f

that

the r e d u c t i o n

instances

2

an i n t u i t i o n i s t i c

there

type

in the b e g i n n i n g

are o n l y

of A plus

is at m o s t

namely:

B >

~ given

~r H: A plus

reduction,

this

many

com-

(C) ~, we n o w h a v e

(C)~

one

finitely

of

with

(C)~

the r e s t r i c t i o n

that

axiom.

theory.

r

Remark:

From

equivalent

the n e g a t i v e

to its

"intuitionistic"

The

significance

the

impredicativity

meaningful the

special

asserts in our type. tivity

of this into

Thus

reduction two of

comprehension

(C)~

the the

normally

obstacle

considered

lies

in the the

the p r i m i t i v e which

- from we have

but

this

consequences

for

at once

that

~r is

version.

of a f u n c t i o n a l

zero-functional actual

it f o l l o w s

components:

impredicativity

the e x i s t e n c e case

translation

fact

natural

to o v e r c o m e

and

predicative

a fixed

the o t h e r

classically

functionals

formally

separating

it a n a l y s e s

and c o n s t r u c t i v e l y

recursive

looks

all

that

functional

objects

is not

accepted

the

of

the

and same

impredica-

separation

principle.

N o w we d i s c u s s

the

consistency,

which

can be e x p r e s s e d

H.

with

the use

of

Z

243

Luckhardt

as f o l l o w s :

r r

There

is an ~ w i t h :

~ v x ~176

Ay

{xy : O

Az-yz

= O}

A (Deduction

There

is a n e w i t h :

~-~ V x O(O~) A + (ER) In this w a y w e a continuity

see

~-~

Here

o n the r i g h t

described

3.

Ax

For

all

by

Definition:

of

Ay(xy

= O-->

a separation

~: ~ - ~ Ax~176 A + (ER)

Az.yz

principle

indicator,

Consider '''''

u 6 :

= O) }

involves

In g e n e r a l

the

continuity

such a situation

is

p-operator.

9n

%x is a n o t h e r

= O}.

of

^ yz#O)}

indicator".

8 ~ O8n...61

A x e6

Vy,z(xy=O

the u n d e r i v a b i l i t y

Vy ~ ~ . x y

a "continuity

'

In short:

the n e g a t i o n

side we have

{x~ = O -->

Continuity

the place

that

{xC~ = O ^

statement.

(~)

property

theorem)

(n ~ O).

is a c o n t i n u i t y {x(%x)~XU

argument

indicator

for

A % x ( ~ i x ) ... ( g n X ) ~

effectively

different

type

~6 a t

9 .. (~n x) }

from u with

the

same value.

The

"continuity

continuity".

indicator"

Every

modulus

is a g e n e r a l i z a t i o n

of

of

a continuity

continuity

gives

the

"modulus

of

indicator

244

H.

but not vice

versa.

Luckhardt

As an e x a m p l e

for

type

O(OO)

the m o d u l u s

of c o n t i n u -

ity X w i t h Ax ~ < • 1 7 6 1 7 6 1 7 6 1 7 6 1 7 6 gives

the

~ o,

following

B ~ o0,

Remark:

Of

indicator;

The

here

clarity

from

the

these

continuity

the p l a c e

the

above

of the n o t i o n

immediate

situations

insight

are

them

in g e n e r a l

[13,

71).

The

possible portant

to t r e a t example

N o w we r e t u r n indicator tained

r

in T,

"modulus into

continuity

intensional,

Ix~

of

~ (o (o~))

, 41

not

for

comes

there [23,

only

statements

be g i v e n

consistency

and

to a r b i t r a r y

continuity

into

the

continuity

constructively

of c o m p u t a t i o n s .

(see K r e i s e l

indicator"

this w i l l

to the

1 ~176~:

suffices.

of c o n t i n u i t y "

the

sequences

certain

(o (o~))

at p l a c e

incorporated

notion

extensional

from

for

u B can be

weaker

"continuity

lus of c o n t i n u i t y "

indicator

essential

to m a k e p.

uv s uw

Cu ~176176-.: i, X(u,I) , @i u ~: X(u,I)

B I ~ 0;

course

: w~176

is no h i n t p.

of h o w

154 and K l e e n e

generalizes

types,

However

the

but m a k e s

"moduit also

extensionally.

An

im-

below.

~ and

line

type O(O~)

(*).

If a c o n t i n u i t y

at the p l a c e

~o~

is con-

i.e. uO(~

(@u)

~ u~^

~U(@lU)

~ 0 ~ ~(@lU),

T then

for

be p r o v e d

this

~ the

continuity

statement

on the r i g h t

in A:

u~ = O--> -->

Consequently

u(~u)

= u~ = O ^

Vy,z(uy

Cu(r

: O A yz + O)

@ O

side

of

(*) c o u l d

245

H. L u c k h a r d t

Theorem (a)

3

Z ~+ ~

=>

There

for type O(O~) (b)

~r

~

is no c o n t i n u i t y

at the p l a c e ~o~

The e x i s t e n c e

at the p l a c e ~o~ form AxV~x,

(b) f o l l o w s equivalent VxAy

p l a c e ~o~. finable

of a c o n t i n u i t y

in A+(ER)

to

(*),

is, in A,

(ER), f i n a l l y

~ contains

afortiori

~o~ h e r e c h o s e n

no m o d u l u s

of c o n t i n u i t y

can be r e p l a c e d

at the

by any o t h e r de-

p l a c e of the same type.

o

(~I) u(l,~u)

~z o [u(i,z)

can be a d d e d

D-operator

(with l B -: lXnB" ...x~ 4 .I for

} ul

to a r i t h m e t i c ,

T and a n a l y s i s ,

the p r o o f - t h e o r e t i c

continuity

for type O(~0)

indicators

the f o l l o w i n g

T U BR c o n s i s t e n t l y

strength.

In these

can e a s i l y be e x h i b i t e d .

extensional

continuity

so

- : I,UU

u(@u)

o u(1,~u)

@U(@lU)

o

, @i u -: Wu

, further

So p p r o d u c e s

indicator

@i are a r b i t r a r y ,

= ul

= 1,~u(uu)

= s $ i = l(@lU)

(BI)

and

"inessential"

I: Cu o (ao)

B---OBI...B n)

by the a x i o m s

u(1,v)

changing

extensions

o ul]

extensional

o ul

v ~ < ~u-->

because

to

A z . y z = O}.

is c h a r a c t e r i z e d

without

(C)~

{xy = x ~ A z - y z = O) and, w i t h

_ The p l a c e

puO(~O)

(~2)

for type O(O~)

or in ~ in the l o g i c a l

(a) from the fact that

In the n e x t t h e o r e m we s h o w t h a t the f o l l o w i n g

which

indicator

~i x.

to V x A y ~

Thus a c o n s i s t e n t

%oe(o(o~)) , ~I~(~176

in T for all ~.

c a n n o t be p r o v e d

analogous

{xy = x ~ -->

indicator

at p l a c e

246

H.

In c o n n e c t i o n for

simple

ries

of

with

type

equal

theorem

theory

3

Luckhardt

(e ~ O)

requires

proof-theoretic

this

fine

shows

that

distinctions,

strength

with

a consistency

namely

respect

between

to their

proof theo-

continuity

properties.

Remark:

The

place;

fixed

the c h o i c e

Theorem

place of

i is t e c h n i c a l l y

p ,

arithmetic

T U BR = T U BR p l u s

the

can be r e p l a c e d

by any o t h e r

definable

motivated.

4(a)

T $ T plus

Proof:

I above

It s u f f i c e s

statements

for

Z

,

~ arithmetic analysis

to p r o v e

plus

= analysis

the a s s e r t i o n s

arithmetic

and

analysis

plus

for then

the

functional

follow

domains;

by the r e s u l t s

in [3].

The

computability

can be g i v e n treatment local

by

given

there.

(~

continuity

arithmetic

Theorem ~(C)~

Proof:

p of

(T U BR p l u s

~) of

[3],

X, X I I I

chapter

Formalizing

proof

(see [3],

this p.

a closed

as in [3],

137)

for

term

analogous chapter

T plus

p

of

type

to the

XIV

statements strong

over

do not

theory.

T plus

For

increase deductive

the c o m b i n a t o r i a l

a p)

consequences

strength

we c o n s i d e r

p.

4(b) has

p-

gives

(T U BR plus

O

^ = T U BR).

a sufficiently

point

the m e t h o d

consistency

A in A = T

Thus

in T p l u s

an i n t u i t i o n i s t i c

By t h e o r e m

1(b)

is the c o n t i n u i t y

proof

it s u f f i c e s indicator

in A+~.

to s h o w

previously

~(C)~176 formed

The

with

~.

starting-

of the

H.

u~176176 = O-->

1,Bu(uu)

Ax ~176176 {Xl = 0 - - >

~Vx

{xy = O

Hence

= 0 A Vz~

= 0 -->

Az.yz

ly~176176

Thus

Continuity

sions

(in the

consistently presence

Az.yz

trary

sential

~ I)}

= I)}

= I}

properties

form

of Z).

(C)).

And

does

to the

= ul = 0

Av.uv

= O} w i t h

~v~

u =:

I)-

on every

~(C)~

247

1 ^ u(1,Uu)

n V z ~ 1 7 6 1 7 6 ~176{zu = 0 < ~ >

x =:

of

vyOO(xy

{xl = 0 ^ A y ( x y

nVxAy

= O @

Luckhardt

Therefore

together

not

alter

with

imply

classical

constructive

situation

extension

constructively

type

functional theorem

negations

domain

4(a)

(C)~

as w e k n o w f r o m

is a d d e d theorem

I(c)

and

does

not work

not

that

strength; which

comprehen-

[e.g.

we have

the p r o o f - t h e o r e t i c

where

theory

of

in the

the addition

this

is c o n -

constitutes the

theory

a n es-

of

truth

definitions.

In c o n c l u s i o n

Theorem

the

"continuity

perspective"

c a n be

summarized

as f o l l o w s .

4 (c)

A

T = A plus

~

,

~(C)~

^

T U BR = ~plus All

systems

lar

they are

Proof:

~

, BR,

between

have

consistent

Arithmetic

~(C)~ the

same proof-theoretic

strength;

in p a r t i c u -

[3].

and analysis

are

treated

in p a r a l l e l .

A

T

(T U BR)

= A

(~

)

[3]

< A

(~

plus

BR)

plus

Z,

= A

(~

plus

BR)

plus

~

A

7 (c)Oe-A Theorem

4(b)

H.

248

4.

Invalidity

Also

T

(T U BR)

T

(T U BR)

of h i g h e r

connected

with

plus

Luckhardt

~

functional Theorem

observations

all

for

(total)

4[ u s ] taken

classically

(eR) ~ e x p r e s s e s "natural" also valid O(OO). ~

equals

initial the

0 or not.

segment

This

~

of

has

vy~176

functional

in c o n t r a d i c t i o n

VX O(OO)

follows

~-rules

f u n c t i o n a l c o n s t a n t s ~i

for

Take

case we - say of

length

n - which

so t h a t ~ ( ~ , n

Vy(xy

(~R) O(~

= 0 A Vz.yz

+ O)}

= 0 ~>

(C)~176

Az-yz

= O) }

whether

a finite

contains

all

* i) = 0 l i k e -

~ O)

c ~.

Is t h i s

~ of t y p e

steps

(~,n * l)n = I + 0

o(oo)

from

of

determine

to

immediately

constant

in ~:

= O ^ Vz~

{X~ = 0 ^ Ay(xy

and e v e r y

consistently.

number

can also

computation,

* i) = O ^

{x~ = 0-->

this rule

numbers,

in ~ a f u n c t i o n a l

expressed

constants

the n a t u r a l

in a f i n i t e

first

the

of

to a d m i t

the a r g u m e n t

needed

Ax O(OO)

which

In t h e

~(~,n

pO = 0 -->

for a l l

concept

types?

can be fully

= 0-->

are higher

(u v a r i a b l e )

it c a n be e s t a b l i s h e d

information

wise.

therefore

for h i g h e r

Then

4(a)

or c o n s t r u c t i v e l y .

a standard

theory

[33

e-rules

our previous

(~R) ~ A [ ~ O ] . A . ~ .I ] ,.

interpretation

now gives

H. L u c k h a r d t

249

Thus we have proved that an w-rule for type O(00)

cannot be added con-

sistently to theories over c o n s t r u c t i v e f u n c t i o n a l domains w h i c h contain i n t u i t i o n i s t i c logic and

(C)~176

This result can easily be extended to

all higher types because we have

T h e o r e m 5(a)

Proof:

(wR)~ ~ -- (wR) B T

Let AIr, I, A [ ~ ]

for 8
0(00)

to theories over con-

structive f u n c t i o n a l domains w h i c h contain T, i n t u i t i o n i s t i c

logic and

(C)~176

The case of n u m b e r - t h e o r e t i c functions

is not covered by this method.

But the result holds here too and is also valid for m u c h weaker theories.

T h e o r e m 5(c) w-rules for types d i f f e r e n t from zero cannot be added c o n s i s t e n t l y to theories in which all f u n c t i o n constants can be computed r e c u r s i v e l y and w h i c h contain functionals,

(relative to their language)

the p r i m i t i v e - r e c u r s i v e

i n t u i t i o n i s t i c a r i t h m e t i c and the fan-theorem.

For instance all

systems of i n t u i t i o n i s t i c

analysis

(with ~ i n

(wR) ~

250

ranging

over

(because

[I],

Proof:

By

leads

freely

the

Kleene

growing

fan-theorem p.

115)

theorem

tree w h i c h

all

Where

choice

objects)

come

5(a)

under

this

it s u f f i c e s This

([I],

to s h o w

for

p.

by

according

that

by u s i n g

the a d d i t i o n Kleene's

all r e c u r s i v e

W1(x~176

-: T1((X)o,X,y)

Az < Y ~ T 1 ( ( x )

, (u~

I are

the

R is d e c i d a b l e

projections

-: V t < x

and has

Vy ) , x ; x )

-->

Vt

rule

fan-theorem.

< I -->

{Ay.sy

the

the variable

As ~ { A y . s y

As

9 ~ R(z,x;x)}

interest

of

= a, p.

Ax

a s for

the premise

As ~ V a . s

be

,x;x)

(6).

intuitionistic

is n o t

using

which

W I (t,y) A ~ ( < m , t > ) : O ]

(t,y)

i t is p r o v e d

Aa OO

by

-->

(~R) s e x c e p t

stricted

which

{[~()=1

~ R(ly.~()

in c o n t r a d i c t i o n

placed

--< mVy )

(7)

Ax

as

Vt

Vx~

logic

and

Markov's

principle

H.

With

this

Theorem For

supplement

the a b o v e

proof

theories

in w h i c h

contain

functionals,

all

function

(relative

intuitionistic

incompatibility

holds

situation

the basic

thus

ideas.

Theorem

which

in f o r m of

(see K l e e n e

[O], Aa O O

(Ch T) O

p.

and

recursively

the p r i m i t i v e - r e c u r s i v e

the

fan-theorem

the

following

5(b)

(MP) ~

will

0 =

perhaps

is b a s e d

idea behind

become

clearer

o n the c o n t i n u i t y

theorem

the f o l l o w i n g

I

5(c), (d)

consequence

if w e r e v i e w of c o n s t r u c t i v e

is r e c u r s i v e n e s s

of C h u r c h ' s

thesis

281)

9 ar

with

(Ch T) ~ is c o n n e c t e d

with

~e~

~: V e A x

{~x=O

(~R) ~ 1 7 6in the f o l l o w i n g

VyT1(e,x,y)}

way.

5(e)

theories

contain

case.

c a n be c o m p u t e d

language)

arithmetic

explained

The basic

For

in this

for ~ ~ O:

functionals. enters

constants

to t h e i r

(~R) ~, As ~ 7 V a ( ~ = a),

Theorem

also works

5(d)

and which

The

253

Luckhardt

in w h i c h

the relevant

all function part

of T a n d

constants

are recursive

intuitionistic

logic

and which

the f o l l o w i n g

holds: (~R) ~

Proof:

A~ O O

By t h e o r e m

gether

with

within

the

From

~

this

5(a) :

theorem theory

9 ~e~

,

(~R) ~176 ~

(~R) OO ~

IV in K l e e n e

VeAx

the a s s e r t i o n

{px=O

[O],

follows

(~R) O p.

I

Aa O O

(~R) ~176~ 281

used

VyT1(e,x,y) } for

with

(~R) ~ 1 7 6resp.

9 ae~

(~R) O

(~R) O to-

informally every

gives

constant

(~R) ~176

oo

2~

H.

Remark: For

The

same

theories

which

necessarily tion

partial,

= {e}.

= {e} ~

A[{I}] ....

We n o w

system

tionistic the

with

we

arithmetic

and

AS

only

A[a]

to s h o w

(~R) ~

with

as far

Then

AaVe.a

the

first

=

thesis.

within

of T, part

form

AE{O}],

Church's

part

situa-

in the

as p o s s i b l e

the r e l e v a n t

fan-theorem.

thesis

-

now

to this

in p a r t i c u l a r

follows

5(a)

to c o n t a i n

the

(~R) ~176e x t e n d e d

A[~I] .... ; then

of t h e o r e m

ax = Uy}.

{i} of their,

(~R) ~ to C h u r c h ' s

we have

(~R) ~

suppose

(~R)~176

(9)

A[~o],

the p r o o f

which

over

{T1(e,x,y)^

enumeration

constants,

foregoing

and A [ { u ~

AaVeAxVy

a recursive

equivalent

Assume

formalize

(Ch T) :

function

By the

(~R) OO.

for

contain

is d e d u c t i v e l y

AaVe.a

the

holds

Luckhardt

intui(up to

gives

{~c~ ^

Ay-~y

< I -->

Vx~

Consequently

I

Ae.~c~-->

Ac

{Ay-~y ~

I -->

Vx~

Aa.ae~-->

Aa

{Ay.ay

< I -->

Vx~

(10)

The

second

part

(beginning

with

the a p p l i c a t i o n

of

the f a n - t h e o r e m )

becomes

(11)

As

{Ay.~y

N o w we

see

that

(I0),I

and

(11).

Applying

the

< I -->

theorem

additional

Vx~

5(c)

is a d i r e c t

argument

for

consequence

theorem

5(d)

to

of

theorem

(10).,2 and

5(e) ,

(11)

gives

(12)

Again

As n~ Va-~

theorem

5(d)

= a ,

follows

(MP)

~

~Aa~176

immediately

from

this w i t h

theorem

5(e).

H.

(12) of

can be i m p r o v e d

Luckhardt

by s t a r t i n g

255

a similar

argument

with

(11)

instead

(10) ,2:

~A~

77{Ay-~y

77V~

Together

~

{Ay.~y

with

(9)

I -->

Vx~

}

< I ^ ~Vx~

this

(11) , (MP)

}

implies

~V~o~ From

this

the n o n a b s u r d i t y

tive

function

of

the

existence

of a n o n r e c u r s i v e

construc-

7 7 Va-a#~

follows

with

Theorem

5(f)

For

theories

tionistic

As77Va'e

which

contain

arithmetic

(MP) ,

This

concludes

this

be g r a s p e d

constructive

part

= a

and

!

the p r i m i t i v e - r e c u r s i v e

intui-

the f a n - t h e o r e m :

A~77Va.~

I; p a r t

= a

II d e a l s

proof-theoretically

method

functions,

available

today?

~

77Va.a#C~

with

the p r o b l e m :

by i n t e r p r e t a t i o n ,

In w h a t the

way

can

strongest

256

H. Luckhardt

References

[03

Kleene,

S.C.:

Amsterdam [13

Kleene,

Introduction

S.C.

and Vesley,

Mathematics. [2]

Kreisel, logic.

[33

[43

Amsterdam

R.E.:

The F o u n d a t i o n s

Luckhardt,

logic 27

of intuitionistic

(1962),

H.: E x t e n s i o n a l

G~del Functional

Proof of Classical Analysis.

Lecture Notes

in Mathematics

Kreisel,

306,

H.: Uber Hilbert's

fur m a t h e m a t i s c h e

Annals math.

logic

Springer

Interpretation. 1973.

reale and ideale Elemente.

Logik und Grundlagenforschung,

G. und Troelstra,

of intuitionistic

predicate

139-158.

A Consistency

Luckhardt,

of Intuitionistic

1965.

G.: On weak completeness

J. symb.

Archiv [5]

to Metamathematics.

1962.

A.S.:

Formal

systems

to appear.

for some branches

analysis. I (1970),

229-387.

Postscript I If partial

functionals

are admitted

in w 4 then the connection between

the higher types and type O must be revised, 5(b), (c), (d) and Postscript

?

The m e t h o d

of w

(f) carry over under appropriate

also gives a nice f u n c t i o n a l

metical

(C) ~ : This reduces

pretable

via

p. 46, 74,

but our main theorems

(AC)O,O_Az o

88-91).

,

to

(C) ~ - Ax ~

(4 A 4)0

-

conditions.

interpretation

of a r i t h -

w h i c h is f u n c t i o n a l

VyOAz o

by

T u BR ~

(see

inter[3],

CHURCH ROSSER THEORE~ UNENDLICH Herrn Professor

iWOR A - K A L K U L E

MIT

LANGEN TER~EN Dr. Kurt SchGtte

seinem 65. Geburtstag

zu

gewidmet

W. Maa~

In dieser Arbeit wird mittels

Transfiniter

Theorem fdr einen typenfreien bewiesen.

Der Beweis

vorliegenden

l~Bt sich unmittelbar

~ -KalkGle

Induktion

mit unendlich

halten.

Wir geben am Schlu8 an, wie die auftretenden Anwendungen

und Schwichtenberg zahlen bewiesen Martin-LSf

zur Termbildung

dieser Art mit Typen hat Girard ~

~

an

angegeben. entstehenden

das Church Rosser (unver~ffentlicht).

der Terme

I)

0 , S

und die Variablen

2)

Sind

a

3)

Sind

ai

und

b

fGr alle

k-KalkG1

haben Barendregt

entwickelten

Methoden

i)

lob = IsL : J il :~

2)

l~xal

3)

ll

lal+1

,

sind Terme.

so sind auoh Terme,

der L~n~e eines Terms

=

KalkG1

9

(~xa)

so ist auch

:

labl = max(lal,lbl)+1

= sup(Jail+l)

der

Wit benutzen beim Beweis die von

Xl,X2,..

i ~ ~

bei

in [I] einen Beweis mit

F~ir den durch Weglassen

:

Terme,

ent-

Ordinalzahlen

[~ ).

Definition

Definition

und Reduktion

Theorem mit Hilfe von Ordinal-

und Tait fur den endlichen

(siehe Stenlund

auf die meisten

genGgend klein gehalten werden kSnnen.

Hilfe von Fundierungspr~dikaten Reduktionsregel

langen Termen

(mit oder ohne

die noch zus~tzliche

Ftir A -KalkGle

Regeln

ausdehnen

langen Termen

Typen),

beweistheoretischen

das Church Rosser

l-Kalktil mit unendlich

und

(ab)

Terme.

ein Term.

W. IVIaaB

258

Mitteilun~szeichen

:

i,j,k,m,n fur natGrliche Zahlen) zahlen; a,b,c,d,e fGr Terme; n mit n-maligem Auftreten yon

a,~,~,6 ffir abzihlbare Ordinalfir Terme der Gestalt (S(S..(SO)..)

S 9

Unser Ziel ist, das Church Rosser Theorem fir den folgenden Reduktionskalk~l ~ zu beweisen :

I)

a~

a

2)

(Ixa) b ~

3)

~

4)

( b) o ~

5)

a ~

6)

ai ~

7)

a ~

ax[bU

~

an

a'

,

a!l b

,

b

b ~

b'

=>

ab ~

fir alle

i e ~

b ~

=>

a'

a'b'

=>

a ~

, ~xa

~

~ Xxa,

a'

Wir geben einen zu diesem Kalkil iquivalenten ReduktionskalkG1 an, bei dem den einzelnen Reduktionen Ordinalzahlen als "Reduktionsordnungen" zugeordnet sind. Das Church Rosser Theorem fir den KalkG1 list sich dann dutch Induktion iber diese Reduktionsordnungen beweisen.

Reduktionen mit Reduktionsordnun~en (wir schreiben

~

anstatt

~ a,1

(I)

a

~

a

fir alle

a

(2)

a

~

a'

und

~

(3)

~

(4)

~

( b) c (5)

a

~

a'

(6)

a

~

a'

=> ,

~ ,

=>

b

: )

b'

-nb

~

b'

=>

(~xa) b

~ ,

~

b'

~xa

~

=>

Xxa'

ab

a'x[b']

a'n c

~

c'

Maa~

W.

(7)

ai

(8)

a

>

fGr alle

a!1

~

b

259

i e ~

=>

nach elner der R e g e l n

~

(I),..,(7)

und

at

b ~,n

mit (9)

=>

~


c

~

c'

f~ir

~ ~,n

c'

g >~

a und

~ a,n

d

~xa'

~

=>

a

=>

mit

~ a,n

~ < a

C

=>

[~

C'

a'

ai

>

a!1

C

8~

c'

ffir alle

i E

Beweis: I.

C

I~

C

>

2.

c

8~

d

=>

Dann gilt nach

I.

=>

C' c

J~

e

e

c'

~ ~ ,m

d

mit

j < 8

mit

8 := max(~,N)

und < a

~ < ~ . und

k c

8,k =>

c

i--

~

>

e

3.,4.

c'

Induktion nach

Lemma 2 : 0rdinalzahl

=>

c

8>

c'

6,k

G.

a

~ a

a

~m+n

a

mit einer a b z ~ h l b a r e n

260

W.

Beweis:

"=>"

Zur B e h a n d l u n g benutzt ai

~

Induktion

nach

der Regel

6)

(Gber Lemma a~

I. I.)

fGr alle

Maa~

der D e f i n i t i o n wird

von

die Regel

a

(8)

~

a'

des KalkGls

:

i e ~

=>

(I.V.)

a~

ai

mit abz~hlbare

ai 0rdinalzahlen

~i

fGr alle

i E ~

=>

a~

ai

fGr

a

mit

a a > ai

fGr alle

" A

upwards

obtained

F => a

with the

in

a sequent

~

any

(b)-rule, (b)-rule

is to be a top sequent

and

In other F => &

above

we apply

nor any

in

then we apply

the same form as

the sequent(s)

is no such

If n e i t h e r

semi-

by a l t e r n a t i v e l y

of an (a)-rule,

(a)-rules

F => A

the line

instead

(a)-rule

in the final

the

is

tree.

(b)-rules (b2)

~,A,F

=>

A

E,F

=>

4,mA

=>

F

~,A,A

"IA,F =>

(a3)

E,A

(b3) E,A,B,F

=> A

E,AAB,F

=> i

F

=>

=,A,A F

(a4)

=>

1~

=> E,B,A

E,AAB,A

(b4) E,At,r,YxAx E,YxAx,r

=> A

(taken in some fixed antecedent

in some

tl, t2,.., 4.2.

order)

sequent

The m i n i m a l T = UD. i I

a (minimal) be g e n e r a t e d V

is a

t

is to be the first

such that below

by

and

~

.

of

over of)

generated

occur in the

@

F0 => AO '

Let

containing

the tree.

containing

(~,~)

over

In (b4),

|

As is easily

is any s e m i - v a l u a t i o n V'

does not

of the s e m i - v a l u a t i o n

F = ~Ai

(the branch over

At

...

term in

the one to be constructed.

semi-valuations.

of a b r a n c h

semi-valuation

seml-valuations if

of (a4),

are to be all the terms

be the sequents and let

F => ~,At I,A 1~ => ~ , A t 2 , A r => E , Y x A x , A

=>

In an a p p l i c a t i o n

there

The

of sequents

the line has

(a2)

i.e.

of sentences

below as far as possible.

stage have

above

sets

~ U ~ .

the sentences

is c o n s t r u c t e d

sequent

by

is the tree

the top of the tree by the a p p l i c a t i o n the

be finite

(i.e. we take

which

if we at a certain

~

determined

~ = (|

as origin

fixed

applying words,

tree @ => ~

in some

Let

be the set of terms

e

tree

seen, (~,~)

Furthermore,

by the s e m i - v a l u a t i o n

=> AI' (@,~,~)

(T,F)

is then

"''

and is said to all m i n i m a l

are g e n e r a t e d containing

s

over

this way;

(~,i)

tree over

, then

(~,~,$)

299

D. P r a w i t z

such that

V' ~ V

4.3.

.

The s i m p l i f i e d

tree c o n s t r u c t e d

semi-valuation

tree

in the same w a y as in 4.1

over

except

(|

is the

that rule

(b4)

is

r e p l a c e d by: (b4') r => ~,Aa,A r => ~ x A x , where

a

is the first

A

parameter

ai

in

|

that does not

o c c u r in

s e q u e n t s b e l o w the one to be c o n s t r u c t e d . It is e a s i l y seen that if the s e m i - v a l u a t i o n V2

tree over

V1

(~,~,~)

g e n e r a t e d by the s i m p l i f i e d

such that

VI

cance

|

V2

branches

never

by some

for the c o n s t a n t s

of the s w i t c h to s i m p l i f i e d split in m o r e

g e n e r a t e d by

, then there is a s e m i - v a l u a t i o n

semi-valuation

is o b t a i n e d f r o m

tion of terms in

is a s e m i - v a l u e d

as,

trees

tree

over

(|

(simultaneous) a2,

...

The s i g n i f i -

is of course

than two b r a n c h e s

substitu-

that their

at one and the same

point. 4.4.

Consistent

semi-valuations.

It is e a s i l y

the s e m i - v a l u a t i o n g e n e r a t e d by the b r a n c h valuation where

tree is i n c o n s i s t e n t ,

some a t o m i c

succedent.

sentence

semi-valuations.

semi-valuation truncated

closed.

semi-valuation

ends in a s e q u e n t s

If all the b r a n c h e s

4.5. over

said above

for f i n i t e

only if the t r u n c a t e d

to g e n e r a t e

of the

exists

sets

@

(simplified)

and

A branch

of a t r u n c a t e d

tree are closed,

also

and f r o m w h a t

conclude:

a consistent ~

(simplified)

I shall speak about a

W i t h this t e r m i n o l o g y

There

and the

in q u e s t i o n is said to be

of a t r u n c a t e d

in this s e c t i o n we may

C l o s e d trees.

(e,~,~)

tree.

of the k i n d

the tree is said to be closed. has b e e n

if we only w a n t

in this way,

semi-

a sequent

of a b r a n c h w h e n we

W h e n the c o n s t r u c t i o n

tree is m o d i f i e d

(simplified)

tree w h i c h

of this kind,

contains

in the a n t e c e d e n t

We can b r e a k off the c o n s t r u c t i o n

have r e a c h e d a s e q u e n t consistent

t h e n the b r a n c h

occurs b o t h

seen that if

of a ( s i m p l i f i e d )

where

semi-valuation

semi-valuation

e = ~0~

if and

tree over

(~,~,*)

is not closed.

4.6. base

Semi-valuations

(~,~,~)

c o n s i s t e n t w i t h a base

I shall say that a s e m i - v a l u a t i o n

~.

Let

~

be a

tree is t r u n c a t e d

S00

D. P r a w i t z

with respect to

~

when

is m o d i f i e d by b r e a k i n g a sequent to

$

F => a

or some

the c o n s t r u c t i o n

is r e a c h e d w h e r e

either

belongs

to

~

said to be c l o s e d w i t h r e s p e c t

to

~

branch

A E a

is stopped

The g e n e r a l

Calculi

the f o r m u l a s

of f o r m u l a s , remarked

was

these

completeness

F

belongs tree is of e a c h

of s e q u ~ o t ~

in the i n f e r e n c e

important

sequents make

of the i n d u c t i v e

As a l r e a d y

to r e p r e s e n t

valuations

constructive

thus

or s e q u e n t s

inventions.

it p o s s i b l e

rules,

the

constructively

approximation

of the c l a s s i c a l

of truth.

Let a c o n d i t i o n or

in

in the d e r i v a t i o n s by s e q u e n c e s

and thus gives us a b e t t e r notion

A

w h e n the c o n s t r u c t i o n

side-formulas

one of G e n t z e n ' s

in 1.3.4,

classical

some

A semi-valuation

idea of s i d e - f o r m u l a s

The idea to i n t r o d u c e replacing

.

tree

of a b r a n c h as soon as

in that way.

II.

I.

of the s e m i - v a l u a t i o n

off the c o n s t r u c t i o n

A E F .

on

V = (T, F)

in the d e f i n i t i o n I.I.2 clauses

(2) - ( 4 )

(2a')

If e i t h e r

then e i t h e r

~A

side-formulas

of i n d u c t i v e v a l u a t i o n s

A E T

can then be e f f e c t e d by r e p l a c i n g

the

in the f o l l o w i n g way:

~ F

A ~ T or

An so on for the other

V

on the scope

or

V

satisfies

the c o n d i t i o n

X

,

satisfies

clauses.

From a constructive depends

be a c o n d i t i o n of the form

The idea to i n t r o d u c e

point

of the

of view,

(informal)

the i m p o r t a n c e quantifier

of this change

in (4a').

This

clause n o w reads: (4a')

If for each

the c o n d i t i o n Given

•

that for each

n o w c o n c l u d e by YxAx

t E @

, then e i t h e r

(4b')

t E |

, either YxAx

At E T

E T

or

V

, either

At

E T

that for e a c h

E F ,

from which

f o l l o w s by

VxAx

E F

Furthermore

get

YxAx ^ ~ YxAx E F , which

when

the i n d u c t i v e v a l u a t i o n s were

t E 8

(4a')

or

V

satisfies

satisfies or

, either

that e i t h e r

by (2a') and two a p p l i c a t i o n s

At At

E F E T

~xAx of

X

E T

, we can or or

(3b'), we

could not be c o n c l u d e d c o n s t r u c t i v e l y d e f i n e d as in s e c t i o n I (cf.I.3.3

and 1.3.4).

2.

The n o t a t i o n

of s e q u e n t s and the i n f i n i t e

The new c l a u s e s

calculi

(2') - (4') o b t a i n e d by i n t r o d u c i n g

side-formula8

D. P r a w i t z

301

in the d e f i n i t i o n of i n d u c t i v e v a l u a t i o n s rules

in a s e m i - f o r m a l

read c o n s t r u c t i v e l y , occurring

is p o i n t l e s s

elements

of this s e m i - f o r m a l

understood

sentences

A

and the s e n t e n c e s

occurring

in a s e q u e n c e

as in s e c t i o n

ence

F

~=

1.4.

But

is false (e,~,~)

(R I) of

~

of s i d e - f o r m u l a s

B

A E F

i.e.

understood

obtains.

of the form

in c o n t r a s t

S

A 6 F

the r u l e s

in

A

the

in a seof the form

as a s e q u e n t

to the s i t u a t i o n there,

(with a c l a s s i c a l

sequences as a s s e r t -

If we c o l l e c t

o c c u r r i n g in c o n d i t i o n s

or some s e n t e n c e

F => A this

"or"):

e i t h e r some sentI is true.

of the s e m i - f o r m a l

system with a

become:

For all

or some

of c o n d i t i o n s ,

and

A , we can r e p r e s e n t

In this n o t a t i o n , base

sequences A E T

in c o n d i t i o n s

is now to be r e a d

in

the "or"

disjunction;

s y s t e m can now be taken to

one of these c o n d i t i o n s

quence

sequent

tension between

( 2 ' ) - (4') and c o n s t r u c t i v e

of the form

ing that at least

B E T

a strange

definition

(see s e c t i o n 3 below).

be " d i s j u n c t i v e l y "

F

taken as i n f e r e n c e

point of v i e w the i n t r o d u c t i o n

The e x p r e s s i o n s

with

is b e t t e r

U n d e r s t o o d as an i n d u c t i v e

there a r i s e s

in the c l a u s e s

and f r o m a c l a s s i c a l

S

system.

F, A

B E A

such that e i t h e r some

is e l e m e n t

of

~

A 6 F

, the sequent

is e l e m e n t F => A

is to

be an axiom.

(R 2a)

r => ~,A

(R2b)

A, r =>

-I A , F => A (R 3a)

F => A,A

F => &, -IA

F => A, B

(R3b)

A, B, F => A

F => A, A A B

(R ~a)

F => A,At I

AAB,

F => A, At~

(R 4 b )

...

At,

F => A, Y x A x

to d i f f e r e n t

in the a n t e c e d e n t

the ones u s e d in 1.4.1

I.

Alternatively,

the i n f e r e n c e r u l e s s h o w n by $chGtte. main

idea m o r e

orderings

and succedent.

to operate

As seen,

the rules

that we pay

are the same as

semi-valuation

sequents

on c e r t a i n parts

of the

of s e q u e n t s

F => A

of the f o r m u l a s

of i n t r o d u c i n g

Since the n o t a t i o n

clearly,

the c o n v e n t i o n

or r e p e t i t i o n s

for c o n s t r u c t i n g

instead

F => A

YxAx,

The rules are to be u n d e r s t o o d w i t h no a t t e n t i o n

F => A

trees except

one may a l l o w sentences

as

seems to show the

I shall use this n o t a t i o n here.

302

D. Prawitz

that we there the risk these

prescribed

of a c e r t a i n

different

rules

coincide,

The calculi w i t h

the rules

calculus

of sequents

sequent

S

calculus

determined

is provable differences) 1951

3.1

F =7 A B

in

~

When

I shall write base

the infinite

= (| ~

infinite

in L o r e n z e n

between

the inductive

~S

.

is (except induction

the

The for some

introduced

1951.

calculi

A

belongs

valuations

and the

of sequents:

to

some

A in

r

belongs

to

F~

T~ .

is obtained

immediately

by an i n d u c t i o n

over the

of derivations.

Thus, calculus

from a s t r i c t l y

of sequents

inductive

valuation

3.2. sequents

induced

determined

above:

point ~

of view,

yields

new above

the

~.

The Hauptsatz for the ~

either

, or both

for some A E T@

by 1.3.2,

infinite

is a c c o r d i n g l y

~9 F => A , A

is e x c l u d e d

the infinite

nothing

and

calculus

a triviality

~& A, F =7 A ,

B E r , B E F@

and

A E F~ .

we have

of

or for

Since

the

again by the result

~& r => A .

3.3.

Restrictions

derivations

on the rule

in the infinite

are to be e f f e c t i v e l y complete

by

If

above,

B E A , B E T~

last p o s s i b i l i t y

by

by a c o n s i s t e n t

of view:

then by the result

classical

determined

The Hauptsatz.

from this point some

, I shall call

contained

if and only if either

This result length

system,

the system with

The e q u i v a l e n c e

or some

(For

the fact that

result

infinite ~

(R I)- (R4)

in this

and also

the formulas.

concerning

by the base

by the a r i t h m e t i c a l

by SchGtte

Classical

order b e t w e e n

see 6.3).

determined

notational

3.

a certain

oversimplification

calculus

described,

bases ~ = ( @ , ~ , ~ )

(R 4 a ) .

with

If we require

of sequents

we obtain

determined

for c o n s i s t e n t

denumerable

|

that

the

by

and atomically

and d e c i d a b l e

~

and

the result: If

A E T~

by the f o l l o w i n g (|

],[A})

scribed,

~

=7 A

observations.

truncated

The

semi-valuation

tree

over

with respect

to

~

can be e f f e c t i v e l y

and if closed w i t h r e s p e c t

to

~

, it is a d e r i v a t i o n

In the c a l c u l u s respect

, then

to

determined

~ ) is not

by

~

.

closed with

If the tree respect

to

(truncated @

deof

--~A

with

, the tree g e n e r a t e s

D. Prawitz a seml-valuation and

$

V'

with an atomic

are disjoint

atomically

complete

and

~'

base,

and

then

V'

, A

cannot

(using 1.3.2). of theorems

4.

and

effectively,

obtain two notions

" ~

is an

A

is false

is consistent

of the fact that the set that the derivations

are to

1959.

pointed

=> A"

the interest

out above:

definition

and

" ~

the equivalence

to left,

the questions in 1.3. have

3.1 holds

about inductive

The answers

T~

base)

F ~ , we

that constitute

than obtained

valuations

by

a

T ~ and

P~.

only from right

raised

in 1.2 and

anew for the infinite

(first given by SchGtte

is the arithmetical

and

constructively

to be considered

of the present

By the introduction

of

A =7"

of truth and falsity

answered ~

~

proved by Shoenfield

in the inductive

better approximation

when

~'

if ~

~ . Hence by 1.3.1.b 3ince

provided

point of view,

is the fact already

of side-formulas

of sequente.

V~

by requiring

first

such that Hence

results

From a constructive

Since

~'~

V' ~ V~ .

This gives a simple proof

Constructive

approach

(@,~',~')

are disjoint.

@'~

then be true in

is not affected

be described

part

~

and the lemma in the proof of 1.3.5, in

303

1951

follow the general

calculi

for the case pattern

of 1.3

with some slight modifications. 4.1. rules

Inversion

(R2),

miss(es). provable,

principle.

If the conclusion

(R3) and (R4b) is provable, If the conclusion

~xAx,

r => A

then there exists a sequence

Atl,r I => At; r',r => A,A,

At2,r 2 =7 A2;

...

can be obtained

r',r 2 =7 A2,A';

of any of the

then so is (are) of the rule

of provable

the pre(R4a)

such that a derivation

from derivations

of

is

sequents of

r',r I => AI,A';

...

The proof is immediate

by induction

over the length

of deriva-

tions. 4.2. ~

Hauptsatz.

The Hauptsatz result

yields

1.3.2 and follows

principle

~

r => A,A

and

~A,

F => A , then

and is a generalization like this result

now using induction

is a negation ~

If

r => A .

r => A ~

~ B , then if

A

~

directly

over the complexity B,r => A

is a conjunction

and

~

of the consistency from the inversion of formulas:

F =7 A,B

B ^ C, then

~

If

and hence

r =7 A,B

and

A

304 ~

D. P r a w i t z F => A,C

and

~

B,C,F => A

is a d e r i v e d

rule and)

~

If

F => A .

for every and ~

t

~Ai} i

A

is a u n i v e r s a l

and

~

...

Constructively, that either section

5.

A

that

~

A => A

are true

but

introduced

(i)

complete

,

F,F i => Ai,A;

If

~

is complete,

basis

indicated

in

Since

for

not to describe

the

truths of sequents valuation

induced by some

truths,

i.e.

valuations

induced

by c o n s i s t e n t

purpose,

different

the sentences

which

and

A,F

=> A,A

individual not

changes

section: about

the base

is its

are axioms.

terms now have

occurring

of a term

two obvious

(R I) by:

given a d e r i v a t i o n

is a p a r a m e t e r F => A,At

thing known

we replace

sequents

substitution

there are

(R I)- (R4) of the last

in the axioms,

t

for

for every

t .

(R4b) is now e q u i v a l e n t

(R4b')

then it holds

the logical

this latter

(RI') All

rule

~

for complete

But as a l r e a d y

Since the only positive

of

F => A,Bt

bases.

in the rules

a

prove

.

in the inductive

completeness,

(ii)

~

[ti]i,~Fi)i

F =~ A .

in g e n e r a l

his calculus

to generate

When we have to be made

thinning hypothesis

.

in all inductive

atomically

Hence

A =>

of the logical

and f a l s i t i e s ~

~

~

then

sequence

in 4.1.

also

that

we have:

The g e n e r a t i o n

truths

or

T e r t i u m non datur.

Gentzen base

and hence

VxBx,

for some

stated

we cannot

=> A

I above,

4.3. every

~

(by the fact

of the i n d u c t i o n

sentence

B t i , F i => A i

with the p r o p e r t y

F,F 2 = > A 2 , ~ ;

and hence

by two a p p l i c a t i o n s

in

of

the same

F => A,Aa r

or

status

, where

A , we can by

a , obtain d e r i v a t i o n s In other words,

to the finite

the infinite

rule:

F ~-> A,Aa F --~-> A,VxAx

where 6.

Completeness 6.1.

logically

PFoof true

a

does not

occur

of the calculus of c o m p l e t e n e s s .

if and only if

in

F

or

A .

of sequents The proof

~ => A

of the fact that

is now immediate

A

from the

is

D. Prawit z

equivalences simplified of

=> A

1.3.6 and 1.4.5 and the fact that a closed truncated

semi-valuation

tree over

(|

in the calculus of sequents.

sequents

305

in general

~ },~A))

is a derivation

The same proof holds for

if we define logical

truth for them in the

obvious way. 6.2.

Remarks.

predicate plete.

There is nothing

calculus which makes

In contrast,

sequents,

truth I.

this calculus generate

one expect

that the calculus

from the very construction

it is immediately

to logical

in the usual formulation

obvious

the first order logical

of a system intended to

truths. of construction

culus of sequents which makes the calculus

(i)

of

that it is complete with respect

is the natural formulation

to logical

is com-

of the calculus

One seems thus to be justified in saying that

To state in summary this principle respect

of

obviously

of the cal-

complete with

truths, we may recall the following

facts:

Studying an inductively defined notion of truth, we saw that the problem of finding a total valuation a sentence

A

is true is equivalent

sistent semi-valuation

in which

that the non-existence

of a consistent

which

A

is false,

A

is equivalent

in which

to finding a conis true, and hence semi-valuation

to logical

in

truth of

A

(section 1.3). (ii)

Furthermore,

we found a construction

semi-valuations consistent itself

that generates

all

in such a way that the non-existence

semi-valuation

in which

A

of

is false shows

in the fact that the construction becomes

closed

in a certain way (section 1.4). (iii)

Hence,

we just take these closed constructions

as deriva-

tions and are sure to derive exactly all the logical 6.3. calculus

I.

Additional of sequents

remark.

Although

is sufficient

truths.

this way of describing the

to account for its completeness,

This point has also been stressed by Kreisel and I am grate-

ful to him for much stimulating See also his contribution

of the theme treated h e r e . _

tc the present volume which became known

to me only after I had completed manuscript.

discussions

the present revision of my lecture

306

D. Prawitz

it does not explain why the inference the converses just the rules side-formulas

of inductive valuations

after the introduction after all,

existence

of certain semi-valuations, sentences

of those defining

the (a)-rules

in the construction

of the (a)-clauses

defining

of sequents;

valuations.

semi-valuations of these

are the

On the contrary,

of the semi-valuation

trees applied

satisfy the converses

the inductive valuations

coincide with the generalization side-formulas,

may here be appro-

the semi-valuations

the inductive

in order to make the generated

introducing

induced

does not simply depend on the defi-

fact that the clauses defining

converses

the truth

valuations

complete bases.

The colncidence mentioned

nitional

In other

(simplified)

but also as asserting

in all inductive

A warning against a certain oversimplification priate:

of

trees can be looked upon not only as stating the non-

and falsity of certain by atomically

are

the calculus

in the latter way.

it should be explained why the closed truncated

semi-valuation

i.e.

the semi-valuations,

and some obvious modifications;

of sequents was first described above words,

rules of the calculus,

of the rules for generating

(a)-clauses

i.e. with the (a)-rules

do not at all obtained by

of the calculus

instead they coincide with the g e n e r a l i z a t i o n

of the

(b)-clauses. It is to be recalled are interpreted valuation

that the sequents

trees.

When the upwards

tree is broken off because read downwards

in the calculus

as just the negation of the sequents construction

of inconsistencies

instead with the opposite

of sequents

used in the semi-

of the semi-valuation

in all branches and is

interpretation

of the se-

quents, we are in effect replacing

the semi-valuation

clauses by the

transpositions

replacing

and

by

" EF"

and

of their converses, " E T"

.

Thus,

wanted to explain depends (with the replacement

the coincidence

on the essential

just described)

defining the inductive valuations (b)-clause

Infinite

The notions and results sentential

in question

. ~ F" that we

fact that the transposition

of the converse of an (a)-clause

is identical

to the corresponding

and vice versa.

~!~

to infinite

" ~ T"

sentential parameters,

logic.

sentential

of sections

I and II are easily extended

Given an infinite

we consider sentences

of negation and conjunction

logic

~ Ai iEI

denumerable

set of

formed by the operations

of sentences

~Ai)iE I

with a

D. Prawitz

denumerable

index

set

I ; when

modifications

are necessary.

I.

valuations

Inductive Leaving

the clauses

The

has a h i g h e r

out the set of c o n s t a n t s

from the bases,

(3) - (4) in the d e f i n i t i o n

of i n d u c t i v e

we now replace

Ai 6 T

for all

i E I , then

~ Ai 6 T . iEI

(3b')

If

Ai E F

for some i E I , then

~ Ai A F . iEI

other n o t i o n s

of section

and the r e s u l t s

are then defined

in s e c t i o n

in the same way

1.3 then i m m e d i a t e l y

extend

to

case.

Generation

of s e m i - v a l u a t i o n s

In the c o n s t r u c t i o n for finite

I.I

some

v a l u a t i o n by

If

the present

conjunction

of s e m i - v a l u a t i o n

and u n i v e r s a l

trees,

we replace

quantification

the rules

by the rules

(b3')

(a3') ~,Aj,r, ~ A i => A iEI

r => ~,A 1,A

In the a p p l i c a t i o n s that

Aj does not occur

to be constructed,

At, A2,

...

trees,

containing

valuation

tree

over

semi-valuation determined

~

r => A,A I

.

below

are g e n e r a t e d

of a c o n s i s t e n t

to the t r u n c a t e d

closed.

the

of (b3'),

by semi-

semi-

But we now make no use of

trees.

as in s e c t i o n

we may now i n t r o d u c e

m i n e d by bases

sequent

such

[Ai)iE I .

semi-valuations

is e q u i v a l e n t being

j E I

by a base

For the same r e a s o n s way as there,

of

and the n o n - e x i s t e n c e

(~,~) (~,~)

of some

in the a p p l i c a t i o n s

I, all m i n i m a l

valuation

(R3a')

and

are to be all the s e n t e n c e s

As in section

Calculi

is to be the first

in the a n t e c e d e n t

sequent

simplified

Aj

of (a3'),

the s e m i - v a l u a t i o n

r => ~,A2,A

r => ~, ~ Ai,A iEI

~, ~ A i , F => A iEI

3.

cardinality,

(3a')

as there

2.

I

807

In place

of the rules

r => A,A 2 ...

r => A, ~ A. iEI i

II and in the same general

infinite

calculi

of sequents

(R3)-(R4), (R3b')

Aj,

deter-

we now have r => A

~ Ai,r=> iEI

A

308

D. Prawitz

where and

AI, A2, j

...

in (R3a') are to be all the sentences

in (R3b') is to belong

The results

Calculus

to generate

To generate

sentential

extend to

logic.

the logical t r u t h s

the logically

logic, we replace

~Ai}iE I

I

of section II.3 and II.4 now immediately

these calculi for infinite 4.

to

of

true sentences

the axioms in the calculi

in infinite

sentential

determined by a base

by the axioms

(El') as in first order logic but leave the other rules

(R2a),

(R3a'),

remains

(R2b),

infinite.

and (R3b')

as they are.

Except for notational

The calculus

differences,

thus

this calculus

is the one studied by Tait 1968. Since the rules of the calculus in the construction

that a closed truncated tion of logical

F => A

are the same as the ones used

of the semi-valuation semi-valuation

in the calculus,

truth is immediate

IV.

tree over

(r,A)

is a deriva-

the completeness with respect

in the same way as in section III.6

that we now make use of semi-valuation semi-valuation

trees and it is thus clear

trees instead

to (except

of simplified

trees).

Second

order valuations

and related notions

The notion of truth for second order sentences

that we could

hope to approach by extending the notions and results I and II is the notion of truth in generalized

of sections

second order models

in the sense of Henkin. Let a domain sequence be a sequence D0

is a non-empty

empty set of in

~

set of individuals

n-ary relations

of the descriptive

language,

in

~0

and "

constants

~

= ~0' ~1' ~ 2 '

~n'

n > 0 t

and parameters

individual variables variables

over

~n

"

order domain sequence

of formulas

range over

T

in

(~,I)

(~,I)

and the n-ary ~

to ~ n

(il,i2,...,in)

such that

I'

except for assigning

is like

I

by recur-

(n > 0)

predicate

is said to be a (normal)

if for each second order term

belongs

I

of a second order

G

~ x l x 2 . . . X n A ( X l , X 2 , . . . , X n ) and for each interpretation tion of

is a non-

in the usual way, letting the

~0

The sequence

where

Given an interpretation

we can then define the notion of truth in

sion over the complexity

"'~

' (i.e.

A(al,a2,...,an) ij

of the form I, the denota-

the set of all n-tuples

is true in to

second

aj

(9,I')

belongs

where

to ~ n )

9

D. P r a w i t z

It is truth second

in second

order d o m a i n

in all such m o d e l s

I.

sequence

(~,I)

and logical

where

~

is a (normal)

truth in the sense

that shall be c o n s i d e r e d

of truth

here.

Definitions 1.1.

Second

is u n d e r s t o o d 80' ~I' 82' that

order m o d e l s

309

order b i p a r t i t i o n s .

a triple

"'"

(8,q0,$)

such that

By a second

where

80

|

is a sequence

dicate

symbols

constants

of second to

The logical also

to

order)

80

'

constants,

over

case

, i.e.

are s u p p o s e d quantifier

order v a r i a b l e s

the term is atomic,

formula

at most

containing

case

the term is molecular.

and

G

is an

obtained

n-ary

second

by s u b s t i t u t i n g

and then,

If order

G

~

to use

if the term was m o l e c u l a r ,

or c o n s t a n t s and

now being a l l o w e d

A(G)

eliminating

(second

in

8n ,

is a second free,

is a second

then

as

of the form

..., x n

occurrences

u

to bind

n-ary

is either a symbol

x I, x2,

term,

two sets

4, ^, An

pre-

individual

parameters

A(Xl,X2,...,Xn)

for free

n-ary

are

whose

(or xn)~

~ x n A ( x n)

terms

and p a r a m e t e r s

and

or an e x p r e s s i o n

where

e

X

8 of ranges

Xxl,x2...XnA(Xl,X2,...,Xn ) over

@

sentences

n-ary predicate

the u n i v e r s a l

second

constants

n > 0 , is a set of

and where 8

sentences

term over a sequence

in w h i c h

for

and whose

8 n " second order

(n-ary)

Cn

and parameters,

order s e n t e n c e s

terms b e l o n g belong

and

of ranges

is the set of all i n d i v i d u a l

can be built up from some i n d i v i d u a l

and f u n c t i o n

order b i p a r t i t i o n

order

in w h i c h

order sentence

is the sentence of

Xn

the

in

A ( X n)

X-symbols

in

the usual way by conversion. The sequence of s e n t e n c e s such that and

en

s

~0

of ranges d e t e r m i n e d written

or

and the p r e d i c a t e

or in s e n t e n c e s

of

The t e r m i n o l o g y also used for second 1.2. order base

The ~=

(4) by

9s

bE a sentence

of the

terms n-ary

parameters

or by a set 80' ~I' 82'

determined predicate

and c o n s t a n t s

by

A

"'"

or

s

parameters occurring

in

A

s , respectively. introduced

for b i p a r t i t i o n s

in section

I.I.1

is

order b i p a r t i t i o n s .

(second

order)

(| | )

A

is the sequence

is the set of i n d i v i d u a l

is the set c o n s i s t i n g

P~, P~,...

clauses

~A

inductive

is defined with

valuation

as in I.I.2

the a d d i t i o n a l

induced by a second

(replacing

clauses:

|

in the

310

D. Prawitz

(5a) If

A(G) E T

for all n-ary terms

G

over

0, then

YX~A(X n) E T.

(5b) If

A(G) E F

for some n-ary terms G

over

|

yxnA(x n) 6 P.

1.3.

Quasi-valuations.

then

I shall also consider the quasi-valuation

induced by a second order base

~

, which is the pair

as in second order inductive valuations

except

(T,F)

defined

that the clauses

(5)

are replaced by: (5a') If

A(P)6 T

for all predicates

P

in

~n

'

then

yXnA(xn) 6 T.

(5b') If

A(P) 6 F

for some predicate

P

in

|

'

then

y X n A ( x n ) 6 F.

1.4.

Semi-valuations

order semi-valuations

and

order inductive valuations corresponding

(total)

in a way analogous (T,F)

over

|

We define

valuations

second

from second

to the one in which the

first order notions were defined.

sider semi-quasi-valuations verses

(total) valuations.

and second order

In addition,

we con-

that satisfy the con-

of the clauses defining the quasi-valuations,

i.e.

(2)- (4)

and (5'). 2.

Remarks

and further definitions

The notions

of truth and falsity in second

all the properties showing

defining the second

that these valuations

can be generated

the one obtained for first order logic thus have an approach similar

and the consistency

satisfy

in a way analogous

(result I.I.3.4),

for first order sentences.

we find that the inversion

Investiga-

principle

3.1.a

3.2 in section I are proved in the second order

valuations

3.1.b and in particular

valuations

3.3 now fail, also when classical

valuation

the completeness

of semi-

of inductive

reasoning

is accepted.

it is easily seen that no second order inductive

induced by an atomic base

showing e.g.

to

one would

case in the same way as in section I, but that the embedding

Indeed,

By

to the notion of truth of second order sentences

to the one established

ting this possibility,

order models

order total valuations.

that

is total;

VX I~ (xlt A ~ X ~ )

belongs

Any derivation to

T

or

F

already have to contain such a derivation as a proper part.

woul~ It can

be shown that only a quite special kind of second order sentences get a value in second order inductive that these valuations for second

valuations.

cannot be used to represent

order formulas

It is thus clear the notion of truth

that we are concerned with here.

In the case of quasi-valuatlons ever, all the basic results

and semi-quasi-valuations,

of section 1.3.

how-

- i.e. 3 . 1 - 3.3 - imme-

D. Prawitz diately

carry over without

valuation converse

change.

311

But it is clear that a quasi-

is not n e c e s s a r i l y a valuation of clause

since clause

(5a) in 1.1 will not be satisfied

(5b) and the in the general

case. We want the second order variables finable

to range

by second order terms as expressed

definition

of inductive

one hand, we cannot

valuations,

in the inductive

definition

valuations

of quanti-

because

the exten-

sions of the second order terms may depend on the meaning

of quanti-

fication

of the

(a fact formally reflected

inductive

valuations),

de-

(5) in the

but the dilemma is that on the

take this as an inductive

fication as attempted

over the relations

in the clauses

in the incompleteness

and on the other hand,

the quasi-valuations,

which are inductively defined and are total when the base is atomically complete,

give the variables

with our original

a range that is too small to accord

intention.

Any straightforward

extension

of the Gentzen-like

procedures

of first order logic to second order logic is therefore However,

by paying attention

be valuations,

to the quasi-valuations

we can get some solution

with in the end of section 1.3: tions and that of embedding In fact,

that happen to

of the two problems

that of generating

given semi-valuations

dealt

the total valuain total valuations.

given a total valuation V, it is easily seen that by an

appropriate

choice of an atomic base

quasi-valuation

induced by

~ .

also a given semi-valuation end, I make 2.1. and let

the following

be an G

~

,

V

can be embedded

Less easily,

can be embedded

in this way.

Let

~

n-tuples

To this

be a second order base

n-ary second order term over

relative

in the

it can be seen that

definitions.

Possible values. G

value of of all

excluded.

to

~

is a partition

(t1,T2,...,tn)

~

.

A possible

R = (RI,R 2)

of terms in

e0

(e,~,~)

of the set

such that

(1)

if

Gtlt2...t n E ~ , then

(tl,t2,...,t n) E R I ; and

(il)

if

Gtlt2...t n E ~ , then

(tl,t2,...,t n) E R 2 9

2.2.

By a representation

= (e,~,~)

is understood

for each molecular

n-ary

and for each possible unique contain

predicate

a sequence (n > 0)

value

symbol

of possible values relative

R

of

PG,R E e*n

|

= ~,

~* e2,

to

... such that

second order term

G

G

there is one

relative

to

and such that

Just these symbols and no others.

~

@~' |

over @

"'"

e ,

312

D. Prawitz 2.3.

Atomic

closure

of a bipartition.

Let

05

...

be a r e p r e s e n t a t i o n

* 82,

order b i p a r t i t i o n

(~,s

and let

|

of possible

relative

to

By the atomic

usin~

values

~*

is understood

i)

@0 = |

ii)

|

the atomic

and

|

(t 1,t 2 ,. .~ ~'

(using

A second

the atomic some

in

second

if the b i p a r t i t i o n ~

is closed

of

(~,v)

2.5.

order

and

where

written

~5 = (|

of possible

then already

order base

(|

over

of the form

as in 2.3,

in

~ = (8,%o,~)

where

V

, in other words,

atomic

values

occur

and

R = (R I,R2).

is closed

is a consistent

|

sentences

sentences

relative

05

of

to

~

,

| is said to be normal

is the q u a s i - v a l u a t i o n if

if

closure

is an atomic

induced

closure

and total,

term relative

symbol

that when

there to

68 , and

n-ary

P E 8n

a bipartition

is exactly term

~ G

~

one possible is then over

@

= (e,T,F) value

closed there

if and

Gtlt2...t n E T ,

then

Ptlt2...t n E T ; and

(ii)

if

Gtlt2...t n E F ,

then

Ptlt2...t n E F .

is consistent

possible

the atomic

closure

but not

total,

values

of a second

of

may a c c o r d i n g l y

~

there may be n o n - d e n u m e r -

order

term relative

have

record

the immediate

results

to

~

and

to be non-denumerable.

Results I first

n-ary

such that

if

~

of a

is an

(i)

ably many

~0

(tl,t2,...,t n) E R 2 ; |

~

It is to be noted

When

3.

in

of

only if to each m o l e c u l a r predicate

in

.

is consistent second

all atomic

order b i p a r t i t i o n part

such that

sentences

PG,Rtlt2"''tn

and all

where

of which must

An atomic by

~

representation

the symbols

all atomic

is the set containing

are the symbols

2.4. already

of

E R I ; and

PG,Rtlt2...t n PG,R

closure

~3' = (~',~0',~')

0 O*n ;

of the form

n)

that are not

here

= |

base

is the set containing

all sentences

lii)

~.

be a second

mentioned

above.

D. Prawit z

3.1.a and 3.2. results order"

Inversion

principle

3.1.a and 3.2 in section before

"inductive

3.1'-3.3'.

for q u a s i - v a l u a t i o n s .

as in section

3.1.b. valuation

Embedding

logic,

a semi-valuation

the second

order

trivially

V

by the 3.2

valuation,

(a)

Every

consistent

semi-

I fails

for second

order

e

if

to an i n d u c t i v e

base

V

that

can of course

(@,T,F)

V'

valuation

valuation .

Since

is and by 3.1.a

V'

since

induced

furthermore

V'

is a v a l u a t i o n

also in

by

is always

if

a semiI is consistent.

V

Total v a l u a t i o n s . The q u a s i - v a l u a t i o n base

i n d u c e d by a c o n s i s t e n t

is a total v a l u a t i o n

the d e f i n i t i o n (b)

over

in the i n d u c t i v e

non-atomic)

it follows

3.4.

in section

V = (T,F)

case be e x t e n d e d

is c o n s i s t e n t

- 3.3

to a v a l u a t i o n . 3.1.b

is i n c l u d e d

(possibly

V'

3.1

" i n d u c t i v e valuation" by by " s e m i - q u a s i - v a l u a t i o n " .

of s e m i - v a l u a t i o n s .

the result

The results

I.

can be e x t e n d e d

Although

The "second

and " s e m i - v a l u a t l"o n " .

in section I hold also when we r e p l a c e " q u a s i - v a l u a tlon " and " s e m i - v a l u a t i o n " Proofs

and consistency.

I hold also w h e n we insert

valuation"

Results

313

A closed

1.1

of inductive

quasi-valuation

quasi-valuation

if it s a t i s f i e s

and a complete

clause

(5b)

in

valuation.

is a total valuation.

Hence

the

induced by a normal

atomic

base

is a total

be a total v a l u a t i o n

over

~ .

Then

valuation. (c)

Let

V = (T,F)

included closure Hence,

in the q u a s i - v a l u a t i o n of

if

(~,T,F) (@,T,F)

quasi-valuation Proof. a consistent complete, tion

1.2 if it s a t i s f i e s

I. there

satisfy

3.1.b

complete

is also a s s e r t e d

is i n s u f f i c i e n t ;

i n d u c e d by an atomic

then

V

is i d e n t i c a l

(5b)

base

is itself

of clause

1960 but

to sect.

1.2.3.

of

to the (~,T,F).

i n d u c e d by

consistent

(5a)

and

in the d e f i n i -

in that definition.

by SchGtte

cf. f o o t n o t e

part

the q u a s i - v a l u a t i o n

the converse clause

V'

is

is also a total valuation.

i n d u c e d by the atomic

and 3.3'

and a t o m i c a l l y

V'

is closed,

V'

Since by 3.2'

it must

and

V

Hence, by

the p r o o f given

314

D. P r a w i t z

the d e f i n i t i o n

of total valuation,

To prove easily

Let

atomic base

Then

over

V = (T,F)

(@,@,$),

term over

~

assertion

(b), we note

proved by i n d u c t i o n

Lemma.

n-ary

the part

(a) follows.

the f o l l o w i n g

lemma,

P

be a p r e d i c a t e

such that for all

tl, t2,

induced

in

|

in

Gtlt2.~

n E T , then

P t l t 2 . . . t n E T , and

(ii)

if

Gtlt2.~

n E F , then

Ptlt2...t n E F .

for every

(ill)

if

A(G)

E T, then

A(P)

E T , and

(iv)

if

A(G)

E F, then

A(P)

E F .

To use

the lemma

quasi-valuation

there

P E |

lemma hold

(see s e c t i o n

inductive

because closed

The second

trivially

is a total v a l u a t i o n

V

Embedding

it follows

over

semi-valuation let

I.

3~

V = (T,F)

V'

3.5, we make use

second

order

logic

1960.

of

an

n-ary

in the c o n c l u s i o n 1.2 of

by part

case

(a).

of the next

from the first

one

that

is

(|

(|

and hence

V ~ V'

and that

V'

in total v a l u a t i o n s I.

can be extended

to a total valuation.

be a c o n s i s t e n t induced

1968.

by an atomic

(see V.2) with respect

lemma,

1967.

calculus

That

of

.

which

is proved

technique

used

the result

of sequents

to l o g i c a l

over

closure

V ~ V'

The e s s e n t i a l

in T a k a h a s h i

of the c u t - f r e e

semi-valuation

such that

of the f o l l o w i n g

is proved by P r a w i t z

the c o m p l e t e n e s s

by SchGtte

closure

is a total v a l u a t i o n

in the proof was also present implies

(iv)

~

(ii) of the

in the d e f i n i t i o n

that also

be the q u a s i - v a l u a t i o n

To prove

over

in (c) follows

of s e m i - v a l u a t i o n s

consistent

Then

is a closed

~ .

precisely, V'

G

V

(i) and

in (c) is only a special

Each

.

if

is a total v a l u a t i o n

assertion

More

(e,T,F)

term

Hence by (5a)

part is an atomic

by the first a s s e r t i o n

and let

that

V' ~ V; and by the a s s u m p t i o n

its atomic

3.5.

clause

Thus,

first a s s e r t i o n

3.5.

n-ary

2.5 above).

satisfies

valuation.

The result

(b) we note

such that the c o n d i t i o n s

V

an :

that

is to each

predicate

of the lemma,

A(X n)

G @O

if

it follows

by an

and

..., t n

(i)

to prove

is

A:

be the q u a s i - v a l u a t i o n

and let

which

for

truth was proved

D. Prawitz by induction over the length of Lemmao tion over

As in 3.5, let |

and let

by the atomic closure tion

8"

A :

V = (T,F)

be a consistent semi-valua-

V' = (T',F')

be the quasi-valuation induced

(~',~,$)

(8,T,F)

of

of possible values relative to

formula

A(XI,X2,...,Xn)

G I, G 2, ~

Gn

respectively, GI, G2,

315

,

n ~ 0 ,

using some representa-

(8,T,F)

~

of the same number of arguments as

and for all possible values

.~., G n

relative to

Then, for each

for all second order terms

(8,T,F)

XI, X2,

RI, R2,.o. , R n

..., X n,

of

it holds:

(i)

If

A ( G 1 , G 2 ~ . . , G n) E T, then

A(PGI,RI,PG2,R2,...,PGn,R n) E T';

(ii)

If

A(GI,G2,o..,G n) E F, then

A(PGI,R1,PG2,R2,...,PGn,Rn)E

When

n = 0, the lemma asserts that

To see that

V'

V ~ V' ~

is also a total valuation,

using the notation

of the lemma it suffices by (b) of 3.4 to show that closed, over

i.e. by the observation 2.5, that to each

8'

fled.

there is a

Let

R

occur in

m

(|

is

m-ary term

G

such that (i) and (li) of 2.5 is satis-

be the partition

([(t 1,t2,.,~ and let

P E |

F'.

Gtlt2...tm~ T'}, ((t I,t2, .... tm): G t l t 2 . . . t m E P'])

PGI,RI, PG2,R2,~

be the predicates from

8*

that

G , which therefore may be written G(PGI,RI'PG2,R2'~

Applying the lemma to

n)

G(Xi,X2,...,Xn)tlt2..~

A(XI,X2,~

n) , it follows that

G(GI,G2,~

n)

relative to

R

(8,T,F)

m

in place of

is a possible value to Hence, we can take the

predicate PG(G1,G2,...,Gn),R which belongs to 3~

8*m

and thus to

Logical truth.

~m

as the

P

required in 2.5~

By the results above, the following three

conditions are equivalent to logical truth in the sense of truth in all second order models:

316

D. P r a w i t z

(i)

A

is true

atomic

order base

(ii)

A

is true in all total

(iii)

A

is false

over

|

The e q u i v a l e n c e tional

fact

order

valuation second

struction

logic

(iii)

second

follows

follows

valuation

order

over

@A"

semi-valuation

from 3.4.c and 3.4.b. 3.5

(and the defini-

is a c o n s i s t e n t

semi-valuation).

of s e m i - v a l u a t i o n s (8,~,~)

@ U ~

,

from

sentences,

~

in s e c t i o n

1.4 is e x t e n d e d

In the d e f i n i t i o n

where

and where

@ ~

are now finite two rules

to

of a semi-

is now the sequence

and

we add the f o l l o w i n g

of ranges

sets of

for the con-

of the tree:

(a5)

E,

(ii)

straightforwardly.

over

by

order

order v a l u a t i o n s

of s e m i - v a l u a t i o n s

tree

determined

of (i) and

of (ii) and

The g e n e r a t i o n second

second

in no c o n s i s t e n t

that a total

Generation

i n d u c e d by any normal

(@A,@,~)

"

The e q u i v a l e n c e

4.

in the q u a s i - v a l u a t i o n

second

(b5)

VXnA(X n)

A(G), r,

VXnA(xn), r

~,

In a p p l i c a t i o n term over occur

~

=>

=> A

of (a5),

G

fixed

in some

of (b5),

order)

sequent

GI,G2,...

r

A

=>

~, A(G2),

E, y X n A ( x n ) ,

=>

is to be the first

(taken in some

In a p p l i c a t i o n over

r

a

in the a n t e c e d e n t

terms

r => ~ , A(GI),

n-ary

such that

below

a

A

second A(G)

order

does not

the one to be constructed.

are to be all

n-ary

second

order

~ .

As before,

all m i n i m a l

semi-valuations

are g e n e r a t e d

by such

trees. The s i m p l i f i e d 1.4.3,

semi-valuation

now also r e p l a c i n g

trees are defined

analogously

to

(b5) by

(b5 ' ) r => ~, A(P),

A

r => z, ~ X n A ( x n ) , in the a p p l i c a t i o n parameter

among

of w h i c h

PI' n p~,

one to be constructed.

..

P

a

is to be the first not

As before,

occurring

n-ary

predicate

in the sequents

the m i n i m a l

below

semi-valuations

can

the

D. Prawitz be obtained

from the ones generated

trees by substitutions, second

by simplified

now also substituting

the result

definition

second

Calculi

Infinite

and closed

of sequents

order case and the

trees need no change.

for second

order log!~

of the infinite

order logic

calculi

of sequents

is obtained by adding

(R5b)

F => A, A(GI)

F => A, A(G 2)

A(G),

r => A, ~XnA(X n) in (RSb)

G

are to be all the However,

is to be any n-ary

n-ary

term and in (R5a)

terms over the sequence

not only from a classical

II.3 still holds,

or false

~

=> A

or

in the second

upon classically). are never complete. (also when

~

A =>

Furthermore,

true sentences

point

valuation

also

~

complete

A => A

The finite

(looked

fails

in general

base). A, F = ,

would be provable

A,A

as axioms,

then

(as will be seen in

that are not logically

The finite

A

these valuations

in such a calculus

2.

of view,

induced by ~

IV.2,

but it seems that the set of provable

to warrant

...

in question.

The only sentences

the section below) interesting

GI~ G2,

point of view for which the

And as we saw in section

is an atomically

r => A

can hold are the ones that are true

order inductive

If we should add all the sequents all logically

of terms

but also from a constructive ~

F => A

yXnA(xn),

there seems to be no point in such calculi. for which

in section II

the two rules

(R5a)

result

order terms for

calculi

An extension to second

1.4.4 hold in the second

of truncated

V.

where

semi-valuation

order parameters.

Also

I.

317

sentences

true is not sufficiently

this kind of calculi.

calculus calculus

of sequents

for second

order logic is ob-

tained from the one for first order logic by adding rule the preceding section and the rule

(R5a') r => A, A(P) F => A, VXnA(X n)

(R5b)

of

318

D. P r a w i t z

where or

P

A .

is to be an The rules

truncated

the calculus. in the first is p r o v a b l e

predicate

of the c a l c u l u s

ones for c o n s t r u c t i n g a closed

n-ary

simplified

simplified

Hence

p a r a m e t e r not

are thus a g a i n

semi-valuation

semi-valuation

o c c u r r i n g in

identical

trees.

A

in the calculus.

is l o g i c a l l y

to the

In p a r t i c u l a r ,

tree is a d e r i v a t i o n

from IV.3.6 and IV.4, we i m m e d i a t e l y

order case:

r

in

o b t a i n as

true if and only if

=~ A

D. Prawitz Bibliographical

319

references

Beth 1955, E.W., Semantic entailment and formal derivability, Mededelingen der Kon. Nederlandes Akademie van Wetenschappen, Afd. letterkunde, n.s., 18, 309-542, Amsterdam. Gentzen 1934, Gerhard, Untersuchungen ~ber das logische Schliessen, Mathematische Zeitschrift, 39, 176-210. Hintlkka 1955, Jaakko, Form and content in quantification theory, Two papers in symbolic logic, Acta Philosophica ?ennica, no. 8, 7-55, Helsinki. Kanger,

1957, Stig,

Provability in logic, Stockholm.

Kreisel 1958, Georg, Review of Beth, La crise de la raison et la logique, J. Symbolic Logic, 23, 35-37. Lorenzen 1951, Paul, Algebraische und logische Untersuchungen Gber frei Verb~nde, J. Symbolic Logic, 16, 81-106. Prawitz 1965, Dag, Natural deduction, A proof-theoretical Stockholm.

study,

1968,

-

Hauptsatz for higher order logic, J. Symbolic Logic, 33, 452-457.

1971,

- Ideas and results in proof theory, in: Proceedings of the Second Scandinavian Logic Symposium (ed. J.E. Fenstad), 235-307, Amsterdam.

Sch~tte 1951, Kurt, Beweistheoretische Erfassung der unendlichen Indukticn in der Zahlentheorie, Mathematische Annalen 122, 369-389. 1956,

1960,

Shoenfield

-

-

Ein System des verknGpfenden Schliessens, Archiv fGr mathematische Logik und Grundlagenforschung, 2, 55-67. Syntactical and semantical properties of simple type theory, the Journal of Symbolic Logic, 25, 305-326.

1959, Joseph, On a restricted ~-rule, Bulletin de l~cademie Polonaise des Sciences, 7, 405-407.

Tait 1968, William, Normal derivability in classical logic, in: The syntax and semantics of Infinitary languages, Lecture notes in mathematics (ed. J. Barwise), 72, 204-236. Takahashi 1967, Moto-o, A proof of cut-elimlnation in simple type theory, Journal of the Mathematical Society of Japan, 19, 399-410.

BEMERIiUNGEN

ZU

B.

REGEL

UND

SCHEMA

Scarpellini

Einleitung In

dieser

f~lle

Arbeit

yon

(konsistente) zwei

mit

schaft

:

E)

t ein

Die

Frage

Ist

T zudem

T

(VX)

+

Wir und

setzen

durch

~ uns

der

An

: ~)

Fragen

haben

es

i)

allgemeine

als

deren Die

kann

2

wird +

S[tze

es

konsistent : 2)

~ B(x)

beantworten

durch

B(t)

.

?

Besitzt

?

wo

A(x)

sein, ) eine

befasse]

eine

positive

Frage

2)

zu

er-

konsistente,(eVtlo

?

nat~rlich

Teil

T ~

Theorien

Fall,

Primerweiterung

zum

)

fragen

zweckm~ssig

(yx)(A(x)

sind

gilt

intuitionistischen dem

B(x) Eigen-

so

Eige.schaften

) mit

A(x),

nur

die

sehr

zur

spezielle

Verf~gung

For-

stehende

wordeno Beispiele

nichttriviale Der Form

Grund

der

hat

gibt ist

S~tze

auch

Grundstock

igkeit

&

noch

B(x)

eine

zu (u.a.

ausser

ist,

die

den

S~tzen

2,

3 weggelassen,

versehiedene

Platzmangel yon

einem

zeigen,

dass

Formen

der,

dass

gewissen

yon

ob-

Refle-

es d o c h

Interesse

eher ist~

Anwendung.

Arbeit

gewissen

T

illustrierende

durehaus

man

T

folgender

gilt, ~

Sei und

mit

A(t)

Spezial-

lautet.

verf~gt,

(Vx)(A(x)

mit 1

und

T ~

so w i r d

disjunktive

- 3)

xionsprinzipien)o die

T +

Stellen

Besitzt

Terme

disjunktiven

Anhang

einigen

suggeriert

Wir

Ist

Methoden

folgt

Variablen,

den

ausschliesslich yon

zu b e w e i s e n d e n

Technik

f~r

) die

wie

konstante freien

Term,

B(x)

aufz~Lhlbare)

Die

~ber

: i)

beweistheoretischen typische

einziger

damn

Ausnahme

rekursiv

die als

mit

eine

intuitionistiseh,

werden

ist.

wir

denen

konstanter

lautet

Formel

wohl

x

(A(x)

(mit

men

yon

Theorie,

Formeln

Ist

behandeln

Fragen,

Resultate

an Hber

den

Zweck

zu

beweistheoretiseher die

Struktur

man,

Technik,

ausgehend mit

intuitionistischer

yon

relativer Theorien

einem Leicht-

erzielen

o 0hne

nern Formeln, dutch

Zweifel

. Hingegen n~mlich

lassen

sich

beschreiben die

Primer~veiterun~en

, dass

die

bier

sie

vermutlich

sich

erzwingen

die

bewiesenen eine

S~tze

disjunktiven

lassen

(Frage

stark

Eigent[imlichkeit Eigenschaften 3).

verallgemeipositivel schon

B.

I. S p e z i a l f ~ l l e , (a) Sei

Regel

und

in welchen

S ein k o n s i s t e n t e s , A, B zwei

dass

folgende

man

Sch~tte,[ o)

Dann

S

~

trivialerweise

S , A~B

Uber

Ferner

Funktionen

Funktionen. primitiv

Fall

S ~

seien

gibt

Sei n u n G d i e

lelchte

sich

Gehen wir

der Begriffe

aus

o) g e s n h l o s s e n

S klasslsch,

S ~A

Situation

und

so ist d i e

S ~B

weniger

(, d i e m i t

viele

ebenso

~i

folgen,

einfaoh,

wie

fol--

Zahlvariablen

' ~i

Konstanten

die

Formel

Insbesondere

zugehSri~en

' ... bezeich--

fLtr p r i m i t i v

re-

definierenden

fur n i c h t - p r i m l t i v - r e k u r s i v e Prim(T ) , d i e

ausdr~ckt:

ist darn% fttr j e d e n k o n s t a n t e n

~

ist

~h/nktor

~

Prim(F)

.

Formel

Rechnung

~

flndet

G ~ ~(~ ~ ) q P r l m ( ( )

ist also

ist,

die ~blichen

wen~

dass

(S~)(Prim(~)A-Prim(~))

offenbar

.

konsistent

in Z i + ~G

die

Rege~

gilt

~ (~)~Prlm(~)

,

z i + ~G

~

^P=i=(~)

aber yon der Theorie

Im Verlaufe

dieser

(3~)(~Prim(~)

Regel

zum

Schema

Uber,

Z.x + w G + G . Arbeit werden wir uns mit

Problem

besch~ftigen.

Gegeben

welches

d i e disju/iktive

ist

Eigenschaft

u n d hat t d a

Eigenschaften.

dlsjunktiven

Zi + nG

konsistente

.

man

Z i + IG

sofort~

2)

Ist

wUrden

Konstanten

Zi ~

~ibt

: Kann

?

verfUgt

(~$)qPrim(~)

Die Theorie

Fallp

B

ist

gen~gend

es eine

Zi

Harrop-Formel

(wegen

der

:

l)

Durch

oder klassisches es h H u f i g

Zahlentheorie t die nebst

vorhanden~

rekursiv.

F beweisbar

hat

Frage

ist d i e

aber keinerlei Dann

ist

zeigt.

Funktionsvariabeln

Glelchungen~

impliziert.

).

intuitionistische

net w e r d e n ) . kursive

, so

ja (, sonst

zu o)

Belspiel

auch

Schlussregel

konsistent

Im intuitionistischen

Zi die

Formeln.Dann

sich die naheliegende

Antwort

Sei

Schema

40 ) :

A

dass

im W i d e r s p r u c h

das

formales,intuitionistisches

zul~ssige

werden,

gendes

Regel

geschlossene

S S , pg.

wenn

stellt

die

Schema

System t

siehe

321

Scarpellini

er-

:

so ) .

so e r h a l t e n

Varianten

und

wit die

yon

ein intuitionistisches besitzt,

~ G eine Daraus

Formeln

in-

s

System A

~ B

S~ , fur

322

B.

welche

die Regel

dingungen

gilt

gefunden

: " wenn

werden,

ist u n d

die disjunktive

gewisse

einfache,

oretischen heit

mlt

] , ~S

3 und

Beispiel

IndlviduenDefinition

ist

Formel

2

Satz

1

: Seien ~(x

mit keinen

andern

schwach

positiv.

liebige

Terme

El)

eine

werden,dass

der beweisthe-

gewisse

Vertraut-

yon

positiv,

wenn

positiv,

A ~ V

, ~

M heisst

solchen

S kan~

enthalten.

schwach

vem~ge

Pr~dikatenkalkGl;

sie w e d e r

wenn

, V

7

sie aus

alleine

noch

aufgebaut

P r i m b a s i s t werLn sie n u r

enth~it.

Wir nennen

D

Primformeln ist. Prim-

M konslstent,

I ... x n k ) , B k ( X 1 ... X n k ) , k = 1 , 2 , . . . freien

Variabeln

als d e n

Sei M e i n e k o n s i s t e n t e

t I , ...

S~MvE

, tnk

gelte

endliche

~ ( t

S ~ ~ B k ( t

die

Es w i r d

F~lle

konslstent

ist.

ist E e i n e

I s t d a n n M'

soll gezeigt

triviale

intuitionistische

Formelmenge

konsistent

Es

es s o l l e n B e -

S + A mB

[7 ~vorausgesetzt.

heisst

heisst

Primformeln : Eine

;

dass

Pr~dikatenkalk~l

S der

t[nd N e g a t i o n e n

SuM

hat.

v~llig

L 6 ~oder

1 : Eine Formel

Eine

Definition formeln

nicht

und FunktionskonstaLnten

und negierten

wenn

garantieren,

Eigenschaft

aber doch

(b) D e r i n t u i t i o n i s t l s c h e

enth~it.

S ~ A ~ so S ~ B "

welche

Behandltuag zug~Lnglich sind.

~4

Im ersten

Scarpellini

angegebenen

Primbasis.

FUr

Formeln

| die ~'s

seien

Jedes k und be-

:

Primbasis,

I ...

t

) gilt

1 ...

t

) .

eine maximalkonsistente

sodass , d~n~

Primbasis,

gilt

auch

die M umfasst,

so ist

Theorie T = SuM,

u U (V ~)(Ak(~) ~Bk(~) ) k und hat die Ubllchen disjunktiven Eigenschaften.

konslstent Beweis:

Der Einfachheit

ger nk'S behandelt

man

halber analog.

theorie

intuitionlstischer

wlesen.

Wit

I ) S e i M'

nehmen

Primformel,

Sequenzenkalk~l

wie

SequenzenkalkUls

----~ p

~ falls

kUl nennen

wlr

; den Fall beliebi-

die Terminologie

fGr Details

Primbasis,

sel z.B.

auf

die M umfasst.

so p 9 M t o d e r ~ p e M ' . W i r

folgt:

schen

= 1 an

der Beweis[5]

ver-

in Schritten.

elne maximalkonsistente

Ist p e l n e

nk

Wir verwenden

Systeme;

fiihren d e n B e w e i s

wit

zu den Regeln

(GS) a d d i e r e n

wit

Gbertragen

und Axiomen fur jede

des

Wit bemerken: S~M

t in den

intuitlonisti-

Primformel

p das Axiom

p & Mttttnd ~p-----@ t f a l l s n p ~ M t . D e n r e s u l t l e r e n d e n G S M I . Zt~m K a l k ~ l

GSM'

addleren

wlr nun

alle Regeln

Kal-

B.

der

Scarpellini

Form

,

~(t),V WO

t eln b e l l e b i g e r

Formelfolge,

zu zelgen,

dass

den Theorien

Term

GST ~ Der

A

ist

Formel

bezelchnen

bzw. ---~A

und

also bewiesen,

Wit

GST ~

----* A

wit

disJunktiven

Wenn

GST~A

II)

AvB

9 so

Im f o l ~ e n d e n

diese

die

Ublichen

Konsistenzbeweis Begriffe:

usw~

Da nun ist,

noch,

f~r alle

k~nnen

eine H~he

wit

h(s)

H~hensprungs III)

eine

schlUsse

die

jeder

Sequenz

im E n d s t U c k

ordnen

wir

zu.

Schnitte) Ausnahmeo

~

Es b l e i b t

~ -Schlusses

~(S)

= ~(Sl)

ncch der Fall

setzen

: 0(S)

~d(~)

haben

=~d

(s

wir

die

Ordinalzahl

IV)

Fttr B e w e i s e

duktionsschritte

P aus

st~ck,

3)Elimination

SI,S 2 / S gleich

eines

Schlusses

B k ( t ) in d e r

Pr~mlsse~

gleich

0 ist~

eingeftihrt

worden

P aus

GST in bekannter

Weise

dann

auch der Begriff

des

werden.

S in P induktiv SchlUsse

sich alles

glelch

SI/S

' wo d = h ( S l ) Als

yon

und

oben nach

Struktur-

wie bei

Gentzen~

zu d i s k u % i e r e n .

- h(S)

0rdinalzahl

ist; ~ o ~(P)

yon

Wir

' @ ' P nehmen

SE yon P .

wir nun die bekannten

Gentzenschen

Re-

als d a sind

, 2) E l i m i n a t i o m

eines

in d e r E n d s e q u e n z ,

Primformel

eingeftthrt

der Endsequenz

GST kSnnen

i) V e r d ~ h l n u n ~ s r e d u k t i o n

die

eines

SI/S 2 ordnen wit jeder Konklusion S -I (statt 0(SI) ~ 1 w i e b e i G e n t z e n ) .

Bedeutung~

definieren

kann

zwei~en

also

Hauptformel

"Komplexit~t"

~-Schlusses

@ O(SI))

O(SE)

einer

fiir d e n

~ 2 zu

eines

die ~bllche

Formel

Sequenz

blelbt

:

ftihren 2qlr

Wir haben

Schnittes

F~r Axiome,logische

(inklusive

eines

jeder

GST konsistent

ein 9 d i e

slnd~

Hauptformel

S im B e w e i s

Insbesondere

f~Ir S c h n l t t e

0rdinalzahl

der

bzw.

als d a s i n d

GST und

Komplexit~t

Komplexit~t

A

usw.

c sines

der Begriff

hat,

im E n d s t ~ r

~

sind mit

GSM v ~

k~nnen t dass

Begriffe

solchen

die Komplexit~t dass

eine

schwierig

~quivalen% kurz

P im S y s t e m

Schluss

~ch~ittformel

zuordnen.

0rdinalzahl

Beweise

einer

auf eine kleine

Im Falle

GST~B

Kcmplexit~t

Sohl~sse

Als n ~ c h s t e s

unten

die

der

per Definition

Man beachte

Bild

ist d i e

~

.

eharakteristisch

kritiseher

Schlusses,

Wie ~blich,

der Komplexit~t ist

Gentzen

, und

Es ist n i c h t

schreiben

zeigen

beweistheoretischen

yon

EndstUek,

kritischen

wir

GST.

Eigenschaften

oder

betrachten

ist

GST vollkommen

Satz.

wenn

, Bk(X)

enth~It.

w l r mit

GSM Iund

Tim

ist u n d d i e ~ b l i c h e n GST ~

.o.

fiir x in ~ ( x )

eine

die Kalk~le

f~tr G S M t ~

Satz

frwi

Kalk~l

SuM'

k = 1,2,

~

die h~ohstens

Den resultlerenden

bls

323

logischen

logischer

Zeichens

Axiome

aus d e m E n d -

aus d e m E n d s t ~ c k .

324

B.

Reduktiensschritte

y o n d e r Art

Reduktionsschritte

bezeichnen.

Wir mUssen

nun noch

~-SchlGsse

aus d e m

Sei a l s o

ein kritischer

A)

EndstGck

P wie

wir kurz

einfUhren,

die

als v o r b e r e i t e n d e

es

uns g e s t a t t e n ~

zu e l i m i n i e r e n .

,~ in P ; s e i n e

sei

ein B e w e i s

~hldern w i r

2) w o l l e n

"~

~-Schluss

Voraussetzung

Es l i e g e

Dann

i),

Reduktionsschri~e

Bk(t),U Ak(t),r

Folgende

Scarpellini

Konklusion

liegt

also

im E n d s t U c k o

erf~llt:

Po y o n folgt

~ B k ( t ) im S y s t e m

ab

G S M ! vet.

:

p

9 o

__---~Bk(t)

,

Bk(t),

r

9

, Schnitt,

Verdiinnung

e

Wir

sagen,der

resultierende

Beweis

P'

folge

aus

P durch

einen

~-Reduk--

iogischer

Zeichen

wollen

tionsschritt. ~-Reduktionsschritte s~mmenfassend

als

haben

einen Beweis

schritte

Reduktionsschritte

folgende

P k~nnen

angewandt

2) v o r b e r e i t e n d e

Elimination

eigentliche

Reduktionsschritte i) A u f

und

nur

werden

fundamentale endlich

viele

wir

zu-

bezeichnen. Eigenschaften

:

vorbereitende

Reduktions-

,

Reduktionsschritte

vergr~ssern

die

Ordinalzahl

yon

P

nicht, 3)

eigentliche

Im F a l l e in

eines

~d(~O

eines

~-Schlusses

dies

Form

ersetzt

Po aus GSM'

einen ~

wird

; die

Beweis

oder

a.wendbar ( [ 6 ]

~7])

BL)

eine

Ist

folgt

die

Ordinalzahl

aus d e r T a t s a c h e , dureh

Ubrigen

die

F~lle

dass

y o n P. das

~o

Ordinalzahl

~ < ~o aus d e n U e b e r -

folgen

yon Gentzen.

y) W i r n e n n e n die

verkleinern

@ O(SI) ) jetzt

Beweises

legungen

Reduktionsschritte

A,r---*~

ein Beweis

P aus G S T N o r m a l b e w e i s ,

~ F

hat.

oberste

Po aus G S T y o n

---~A

wenn

Auf Normalbeweise

Sequenz

des

Endst~ckes

, fur w e l c h e n

seine

ist das

~(Po ) ~

yon

P,

~(p)

Endsequenz

Basislemma

so e x i s t i e r t gilt.

B.

VI)

Wir

beweisen

nun

durch

Scarpellini

transfinite

325

Induktion

Gber

O(P)

folgende

Be-

hauptung: B)

Sei

P ein

wo

F schwach

ein

Beweis

Ist

~(P) in

Beweis

aus

positivist P




Wegen

der

der

Hypothese

yon

~

~-Reduktionsschritt mit

aber

Reduktionssehritt

kritischer

~(t)

Pr~dikatenkalkUl

die

P1 yon

ergibt

P

o

gilt.

und

somit

. Das

logischer

(y)

~(P)

Pl y o n

Reduktionsschrit~

Beweis

9

Basislemma

Induktionsvoraussetzung. bis

kein ein

Hypothesen

loglscher einen

~

, ~

den O(Po)


sich wenn

wenn

f~r alle Belegungen

f,g

numerische

Terme~

System

der

WF-Konstanten

nur

Funktionale seien

intuitionistischen Zeichen

(und

enth~it.

zudem

Zahlen-

F~r

die Axiome ~

quantorenfreie jede

(k)

WF-Konstante

= ak

f~r

zu Z l a l l e w a h r e n P r i m f o r m e l n (im S i n n e d e s l e t z t e n A b s e h n i t t e s ) ~ so e r h ~ i t m a n d a s S y s t e m Z ; mit Z bezeichlI 12 n e t m a n d a s U n t e r s y s t e m y o n Z. , in w e l c h e m n u r r e k u r s i v e K o n s t a n t e n 11 beim Aufbau yon Termen und Funktoren verwendet werden. Uebertr> man die

Systeme

Zi,Zil,Zi2 dabei

Induktionsaxiome

delnd),

so e r h ~ i t

noch mit

Addiert

wahr,

Zahlentheorie

rekursive

...

vorhanden.

so l ~ s s t

,~,x) h e i s s e n

.

, ..o h e i s s e n

formale

den

primitiv

wo XI = ~ao,

k ~ n-i

,

t beteiligt,

= q(~

:

intuitionistischen

Mit

Axiome)

O'

,

vom

= q(f,g,~)

t(f)

Terme

Aufbau

t(~n,~,x) :

t(f,g,~)

yon ~

Scarpellini

man

man

in bekannter naeh

dem

Weise

Vorbild

Kalk~le

in den

yon Gentzen

GZi,GZiI,GZi2

einer Umsetzungsregel

Sequenzenkalk~l

versehen~

die

I l l als R e ~ e l

. Jeder es

( die

dieser

behan-

Kalk~le

ist

gestattet,numerisehe

T e r m e d u r c h a n d e r e y o n g l e i c h e m Weft zu e r s e t z e n (siehe ~ I , C ~ J )" F ~ r das F o l g e n d e b e n ~ t i g e n w i r e i n e n H i l f s s a t z f~r p o s i t i v e F o r m e l n : Hilfssatz

: F~r

A* i n p r ~ n e x e r ist,

angeben,

jede positive Normalform,

Formel

deren

A lisst

sich

effektiv Tell

quantorenfreier

eine

eine

Form~l

Primformel

sodass Z.

I-- A ~ A *

(k

= ~,1,2)

1k gilt.

Hinweis:

Man benutze,

~quivalent

ist

zu

dass

jede

(~x)(~)((x-i

Formel

A v

(~)B(~)

V A)A

(x%l ~ B ( ~ ) )

intuitionistisch

)

.

B.

(d)

Wahre

Im

pr~nexe

Fulgenden

@

Ist

~

und

"wahr"

ist

A

(~y)

,~,x,f,g

durch

@

) ist

wahr,

wer~n

"Stetlg

und

wahr"

oder

auch

definiert. so

heisst

wahr

wird~

A wahr,

A(~t~,~,x,y

wernq

) wahr

A

f~ir

jede

iSto

mit ahr,

@

(~)

A(~t~,~,x,~

dass

A(~

Lassen

wir

nur wahr"~ ist

Da

H

4 unten

unter

sieh

1 haben 4

Die

:

]

A(~u) ist

und

(

zu~

so

stetigen

stetigen

sprechen

wir

Furmktionale

von

vorhan-

Funktional-lnterpretation

d o c h m ~ s s e n wir die

1

ohne

freie V a r i a b l e n

f~r ~

(v) @ 0

den

= leere

Beweise

yon

H

lem-FurLktionen"~ , so

) pr~nex

, ~ elne

0( u 's verschieden Folge)

sagen

dann

konstruktive nur

e

sie erf~lle

Gegenstiicke eines

: Es

, H

3

deren lassen

als

existiert

Sei einer

e(v)

A(~u)

und ~

A(~u,v)

Zi2~- A.

eine

w a h r ist.

wahr.

A(~u,~,x

yon

Formel

, sodass

und A rekursiv wahr,so

Folge

sind

yon

und

WF-Konstanten,

alle

den

4

verlaufen

Existenz sich

eine

durch durch

A.

Mit

zu

H

Illustration

eine

die

unteren

Index

o

A(Cgu,~,x ) ist wahr, g e n a u d a n n w e n n A ( ~ u , ~ , n ) w ~ h r

kursiv

existiert,so-

so Z

eine p r ~ n e x e

ist

Darm

~

alle

zur

F

sind l e i c h t b e w e i s b a r ,

Stetigkeitsfunktion

wir

Sprache

aequivalent

Hilfss~tze

H ~ : Sei A(~u)

wir

Furmktoren

~- A . II : Sind alle K o n s t a n t e n in A r e k u r s i v ,

H 2

FgOgl~,~,x

aus Platzgr~inden w e g l a s s e n .

H i : Ist A wahr,

In

Funktor

sod ss

ist.

t und

unserer

exi,tiert,

].

Die n ~ c h s t e n Beweise

in

ein

) wahr Terme

"wahr"

yon Kreisel ~

Term

wahr,we~m

rekursive

"rekursiv sind~

) ist

,~,x,F[~u,~,x]

den

H

bis

aussagenlogisch

A(~i~,~,x,y

WF-Konstanten,Furaktions-

Furh E C~,

ta=Pk(tas,...,tan) , Typ (a)=T,0~and

[a]E=pk([a 11E,..t.Ian] ~)

VI (The Constant ~) a= 1,

4. he(g) 5.

scheme

where type ~i = I .

= }(X~.he1(a,~)) )

provided that for each x, he1(X) is an index for a functional with arguments ~ .

~8

H. Schwichtenberg,

S.S. Wainer

6.

he(s):~ he1(he2(g), 5)

7.

he(~)= he1(~' ) where ~' is some permutation of ~ . To be precise,

the above schemes should be interpreted as a

simultaneous inductive definition of a set of indices e, and for each index e a functional h

We believe however that the

e

intention is clear. w

The~-hierarchy. We now develop a recursion-theoretic hierarchy based on a

fixed but completely arbitrary type n+2 object ~, and prove that the functionals of type ~ n+1 appearing in the hierarchy are precisely those functionals definable in To(~) 9

The hierarchy is

just a generalization of [11] to higher types. Let lelF(~) , e < ~ , be a standard enumeration of all functionals (with arguments ~ of type ~ n) primitive recumsive in a type n+1 object F (in the sense of Kleene [5]).

We assume ~elF(~)= 0 if e

is not an index for a functional of the appropriate string of variables. We associate w i t h ~ a n ~(F)

()=

operator~defined

as follows

The ~-hierarchy is then obtained by iterating ~ o v e r a simultaneously generated set of ordinal notations.

Note however that the word

"hierarchy" is used in a rather broad sense here, since ~ m a y not be a jump operator in the usual sense (and a l t h o u g h ~ r a i s e s recursive degree" it need not raise "degree").

"primitive

As a result of this

our hierarchies will not in general have the uniqueness property. Definition.

I 1

and

for a c O ' a r e

inductively defined as

follows, where ~,# are variables of type n. will usually drop the superscript ~ )

(Since ~ i s

fixed we

H. Schwichtenberg, S . S . (1) I E 0 ,

"/(b ) )o and it remains to choose N so that N(i) is an index of this expression as a function of m and ~, primitive recumsive in FSasM(e)" Lemma ~. There are primitive recursive functions I and C such that if e is an index of a functional h e defined by schemes I,...,7 then for any b E 0 ,

C(e,b)g0,b>) )o Thus hel is also primitive recursive in FC(e,b) with an index primitive recursively computable from e,b and primitive recursive indices of I and C.

Hence h e is primitive recursive

in FC(e,b) by Kleene's scheme S&, with index I(e,b) given as a primitive recurslve function of I(e2,b), e , b , and primitive recurslve indices of I and C.

We give I and C the value 0 if none of the above cases applies. Inspection of the above cases shows that C(e,b) and I(e,b) are defined simultaneously from C(el,b) C(e2,b), I(el,b) I(e2,b),e,b and primitive recursive indices of C and I.

Since el,e 2 < e the

simultaneous definition is a primitive recursion on e.

Therefore

by the simultaneous primitive recursion theorem (e.g, Lemma 2.1 of [2]) we can indeed find primitive recurslve indices of C and I which satisfy this definition ~ This completes the proof.

354

H. Schwichtenberg,

S.S. Wainer

Next we show that every functional G(~) , with arguments ~ of pure types ~ n and with values of type O, which appears in the~-hierarehy, is definable by a term of To(~) 9 Lemma 6 There are primitive recursive functions p and Pl such that if the type n+1 functional F is defined by a term t c of To(~) thenle] F is defined by the term tp(c,e) of To(~) and x,~.

Ix~F(~) is defined by the term tp1(c) of To(~) .

proof We first define p by the primitive recursion theorem with cases corresponding

to the schemes 8o,...,$8 by which ~e~ F

is defined. In this proof and the next, u,v will be used to denote ~ariables of To(~) of the appropriate types ~ If ~e~ F is defined by $I,$2,$3 then [e~ F is Just a primitive recursive function of its numerical

arguments and

so p(c.e) is given explicitly as a function of e .

If ~elF=k~.~eIDF(le2~F(~),~) assume inductively that tp(c,el ) defines ~e2 ~F.

through S~ then we can defines le1~F~and tp(c,e2 )

Therefore ~e~ F is defined by the term

~ . tp(c,el ) (tp(c,e2)~)~ and we can clearly compute p(c,e) as a primitive recursive function of p(c,e I) , p(c,e 2) and e.

If ~el F is defined by $5 then lelF(0,~)= ~e1~F(~) and lelF(x+1,g)= le2~F(le~F(x,~),x,~) inductively that tp(c,el )

where again we can assume

defines ~e1~F and tp(c,e2 ) defines

le2 ~F . Now let r(O)=p(c,e I) and r(x+1)= the code for the term ~ .

tp(c,e2 ) (tr(x) ~) x ~ ~

Then for each x, tr(x)

H. Schwichtenberg,

S.S. Wainer

defines k~.~e~F(x,~) and therefore < t r ( x ~ x ~

355

defines le~ F .

But r is primitive recursive, with index i primitive recursively computable from p(c,el)

p(c,e2) and e.

Hence we can primitive

recursively compute from i, first a code for the term defining r, and then the code p(c,e) for the term < t r ( x ) > x E g

which defines ~e~ F.

The cases where ~e~ F is defined by S6 and $7, corresponding to permutation of arguments and function application, are trivial.

If lelF(g)=~i(k#.~e1~F(~,#))

through $8 then it is easy

to define p(c,e) primitive recursively from e and p(c,e 1) such that t p ( c , e ) = k ~ ,

ui(kV.tp(c,el)~V)

9 The case S0 is treated

similarly, replacing ~i by F and u i by t c 9 It is clear from the above cases that p is primitive recursive, as required.

To define Pl simply note that k x~. defined by the term x E g ,

Ix~F(~) can now be

whose code is given as

a primitive recursive function of c.

Lemma

7

There is a primitive recursive function q such that if a~ O ~ t h e n

q ( a ) E C ~ and tq(a) defines F ~ a

q

Proof Again by the primitive recurslon theorem. so that t q ( 1 ) = k t ~ O

.

Define q(1)

Now assume tq(a) defines F a.

Since x = < x , ~ > o (0) and ~ = < x , ~ > 1

there are terms tk and t$

356

H. Schwichtenberg, S.S. Wainer

which define the decoding functions k~.~o(O) and k~.a I 9 Fa P But F 2 a = k a . < l ~ o ( O ) ~ (~I,0 n),~(k#.I~o(O) ~ a(a1,#))> and so F2a is defined by the term ku.