Das ist keine Logik höherer Ordnung, sondern erster Stufe. Man benützt ja bekanntlich oft Definitionen zur Vereinfachung von Axiomensystem, ich könnte in der Literatur massenhaft Beispiele gegeben. Auch die ZF-Formalisierung hier tut das: Sie benützt das definierte Durchschnitt-Symbol oder den definierten Eindeutigkeitsquantor. Insofern kann das ZF-Axiomensystem auch als per =Definition vereinfacht notiertes Axiomensystem in einer Prädikatenlogik ohne Gleichheit verstanden werden. Ich habe daher die Definition als Zusatzmöglichkeit hintangestellt. Ich denke das ist angemessener.-- Wilfried Neumaier 22:20, 15. Jan. 2008 (CET)