Es gibt übrigens eine wirklich 100%ig prädikatenlogische Formulierung der ZF-Axiome (die einzige mir bekannte)und zwar bei: Oberschelp, Allgemeine Mengenlehre, 1994, S. 262. Sie benützt nur wirklich sauber definierte prädikatenlogische Zeichen und nutzt u.a. den Eindeutigkeitsquantor aus, um die problematischen Funktionen zu eliminieren. Der Eindeutigkeitsquantor ist in der Prädikatenlogik mit Gleichheitsprädikat definiert (und wird auch schon im Auswahlaxiom benutzt). Man sollte diese Form der Prädikatenlogik als Voraussetzung angeben, und zwar ganz am Anfang, und möglichst darauf hinweisen, welche Zeichen dort definiert sind. Die Oberschelp-Mengenlehre ist m. E. die einzige, die auch klar sagt, dass man in der Prädikatenlogik keine Mengenterme benützen kann (!), weil sie sich nicht exakt definieren lassen (S. 263). Sie arbeitet selbst in einer Klassenlogik, in der beliebige Klassenterme zur Verfügung stehen. Deshalb findet sich dort eine Seite vorher (S. 261) eine sehr viel einfachere Version von ZF, die Klassenterme gut ausnützt. Historisch ist die prädikatenlogische Version so oder so nicht. Die alten Logiker wie Zermelo und Fraenkel benützten sie noch nicht. Von Skolem stammt die erste Formalisierung, aber nicht in der heutigen Form der Prädikatenlogik. Auch sie muss deswegen übersetzt werden. Dr. W. Neumaier