Die axiomatische Mengenlehre ist eine Axiomatisierung der Mengenlehre, die die bekannten Antinomien der naiven Mengenlehre vermeidet. Insbesondere wird der Begriff auch für die Zermelo-Fraenkel-Mengenlehre mit Auswahlaxiom benutzt, die in der Mathematik ganz überwiegend gewählte Axiomatisierung.
Bertrand Russell selbst formulierte erstmals 1903 seine Typentheorie, die auf einer Stratifikation des Mengenbegriffs beruht, um die Russellsche Antinomie zu vermeiden. Auch die Principia Mathematica benutzt dieses System.
Der einflussreichste Versuch der Axiomatisierung stammt vom Ernst Zermelo aus dem Jahr 1907, diese Zermelo-Mengenlehre ist sowohl die Grundlage der Zermelo-Fraenkel-Mengenlehre als auch alternativer Axiomensysteme.
Ergänzt um Ersetzungsaxiom, Fundierungsaxiom und Auswahlaxiom ergibt sich das System ZFC (für engl. Zermelo-Fraenkel with Choice), nur mit den beiden ersteren ZF.
Die Neumann-Bernays-Gödel-Mengenlehre ist ein Erweiterung von ZFC um den Begriff der Klasse mit dem Vorteil einer endlichen Zahl von Axiomen, während ZFC Axiomenschemata benötigt.
Die bekanntesten Axiomatisierungen, die nicht eine Erweiterung oder Einschränkung von ZFC sind stammen von Ackermann, die Ackermann-Mengenlehre, und Quine. Quines System ist heute unter New Foundations („Neue Grundlagen“) bekannt, nach dem ursprünglichen Aufsatz von 1937 unter dem Titel New Foundations for Mathematical Logic („Neue Grundlagen der mathematischen Logik“).