は、ツェルメロ＝フレンケル集合論などの集合論の公理系を構成する公理の一つであり、空集合（元をもたない集合）の存在を定める。ただし、この公理を採用しないZF公理系の定式化も存在する ケネス・キューネン『集合論 独立性証明への案内』藤田博司訳、日本評論社、2008年、ISBN 978-4-535-78382-9。
定義 集合論の言語 を用いて、空集合の公理は下記のように定義される。
定義の解釈 自然言語を用いて、空集合の公理は次で解釈される。
「元をもたない集合が存在する。」
性質
外延性の公理との連言により、元をもたない集合は一意に定まる。この集合を空集合と呼ぶ。数式上では、 や と表記する。
空集合を表す定数記号を予め用意してZFを記述することもある。その流儀では、無限公理の 相当の元は、単に何らかの集合を表すだけのただの記号に置き換わり、空集合の公理によってはじめてそれが空集合であると保証される。
この公理の主張自体は明白なものと考えられているが、一階述語論理と置換公理から導くことが可能なためProof Explorer, Theorem axnul、公理に加えないこともある。
脚注・出典
参考文献