正則性公理とかラッセルのパラドクスを排除してるようにしか見えないもんな
実際は内包性公理を大幅に制限することで矛盾となる演繹をできないようにしたんだけど