EINE ÄQUIVALENTE FORMALISIERUNG DER LOGIK VON FEFERMAN UND ACZEL

1. Xusgchcrid von einer beliebigen abzahlbaren Sprache dip des einsortigen Pradikatenkalkuls der ersten Stufe mit Identitat, hat S. PEFERMAN gemeinsam mit P. ACZEL in [ l ] eine verallgemeinerte Sprache 9* eingefuhrt. 9* unterscheidet sich von 9 u. i i . darin, daB neben der iiblichen Biimplikation t, ein neues binares Symbol E fur eine Aquivalenz zwischen Formeln hinzukommt und neue Axiomgruppen (1)-(4), die den Gebrauch von = regeln. ACZEL hat in [l] eine Variante von 9* vorgeschlagen, die wir mit 9' bezeichnen wollen. dip' unterscheidet sich von 9* nur in einem der Axiome der Gruppe (4). Das Hauptergebnis der Arbeit [l] besteht in dem Nach weis der Widerspruchsfreiheit des Abstraktionsprinzips