ในทฤษฎีเซตเชิงสัจพจน์สัจพจน์ของเซตว่าง [ ^{1 ] [ 2 ]}หรือที่เรียกว่า^{สัจพจน์}ของเซตศูนย์^{[ 3 ]}และสัจพจน์ของการมีอยู่ [ ^{4 ] [ 5 ]}เป็นข้อความที่ยืนยันการมีอยู่ของเซตที่ไม่มีสมาชิก^{[ 3 ]}เป็นสัจพจน์ของทฤษฎีเซต Kripke–Platekและรูปแบบหนึ่งของทฤษฎีเซตทั่วไปที่ Burgess (2005) เรียกว่า "ST" และเป็นความจริงที่พิสูจน์ได้ในทฤษฎีเซต Zermeloและ^{ทฤษฎี}เซต Zermelo–Fraenkel ไม่ว่าจะ ^มีหรือไม่มีสัจพจน์ของการเลือก [ ^{6 ]}

ในภาษาที่เป็นทางการของสัจพจน์ Zermelo–Fraenkelสัจพจน์นั้นมีดังนี้:

${\displaystyle \exists A\,\forall x\,(x\notin A)}$[ ^{1 ] [ 2 ] [ 5 ]​}

หรืออีกทางเลือกหนึ่งคือ. ^{[ 7 ]}${\displaystyle \exists x\,\lnot \exists y\,(y\in x)}$

กล่าวคือ:

มีเซตหนึ่งซึ่งไม่มีสมาชิกใดอยู่ในเซตนั้น

เราสามารถใช้สัจพจน์ของความเท่าเทียมเพื่อแสดงว่ามีเซตว่างเพียงเซตเดียวเท่านั้น เนื่องจากมีเพียงเซตเดียว เราจึงสามารถตั้งชื่อมันได้เซตว่าง (เขียนแทนด้วย { } หรือ ∅) สัจพจน์นี้ เมื่อกล่าวในภาษาธรรมชาติ มีใจความโดยสรุปดังนี้:

เซตว่างมีอยู่จริง

สูตรนี้เป็นทฤษฎีบทและถือว่าเป็นจริงในทฤษฎีเซตทุกเวอร์ชัน^{[ 8 ]}ข้อโต้แย้งเพียงอย่างเดียวคือวิธีการพิสูจน์: โดยการทำให้เป็นสัจพจน์; โดยการอนุมานจากสัจพจน์การมีอยู่ของเซต (หรือตรรกะ) และสัจพจน์การแยก; โดยการอนุมานจากสัจพจน์ของอนันต์; หรือวิธีการอื่นใด

ในบางรูปแบบของสัจพจน์ ZF นั้น สัจพจน์ของเซตว่างจะถูกกล่าวซ้ำในสัจพจน์ของอนันต์อย่างไรก็ตาม ยังมีรูปแบบอื่นๆ ของสัจพจน์นั้นที่ไม่จำเป็นต้องมีเซตว่าง นอกจากนี้ สัจพจน์ ZF ยังสามารถเขียนได้โดยใช้สัญลักษณ์คงที่แทนเซตว่าง ในกรณีนี้ สัจพจน์ของอนันต์จะใช้สัญลักษณ์นี้โดยไม่จำเป็นต้องให้เซตนั้นว่าง ในขณะที่สัจพจน์ของเซตว่างนั้นจำเป็นต้องใช้เพื่อระบุว่าเซตนั้นว่างจริง

นอกจากนี้ บางครั้งเราอาจพิจารณาทฤษฎีเซตที่ไม่มีเซตอนันต์ และในกรณีนั้นอาจยังคงต้องใช้สัจพจน์ของเซตว่างอยู่ อย่างไรก็ตาม สัจพจน์ใดๆ ของทฤษฎีเซตหรือตรรกศาสตร์ที่บ่งชี้ถึงการมีอยู่ของเซตใดๆ ก็จะบ่งชี้ถึงการมีอยู่ของเซตว่างด้วย หากเรามีแบบแผนสัจพจน์ของการแยกออกจากกันซึ่งเป็นความจริง เนื่องจากเซตว่างเป็นเซตย่อยของเซตใดๆ ที่ประกอบด้วยสมาชิกที่สอดคล้องกับสูตรที่ขัดแย้งกัน ตัวอย่างเช่น ${\displaystyle \varnothing =\{u\in w\mid u\neq u\}}$

ในการกำหนดตรรกศาสตร์ภาคแสดงลำดับที่หนึ่งหลายๆ รูปแบบ การมีอยู่ของวัตถุอย่างน้อยหนึ่งชิ้นนั้นรับประกันได้เสมอ หากการกำหนดสัจพจน์ของทฤษฎีเซตถูกกำหนดขึ้นในระบบตรรกศาสตร์ ดังกล่าว โดยใช้แบบแผนสัจพจน์ของการแยกเป็นสัจพจน์ และหากทฤษฎีนั้นไม่แยกความแตกต่างระหว่างเซตกับวัตถุประเภทอื่นๆ (ซึ่งใช้ได้กับ ZF, KP และทฤษฎีที่คล้ายกัน) แล้วการมีอยู่ของเซตว่างก็เป็นทฤษฎีบทหนึ่ง

หากการแยกไม่ได้ถูกกำหนดเป็นโครงร่างสัจพจน์ แต่ได้มาจากการอนุมานเป็นโครงร่างทฤษฎีบทจากโครงร่างการแทนที่ (ดังเช่นที่บางครั้งทำกัน) สถานการณ์จะซับซ้อนมากขึ้นและขึ้นอยู่กับสูตรที่แน่นอนของโครงร่างการแทนที่ สูตรที่ใช้ใน บทความ เกี่ยวกับโครงร่างสัจพจน์ของการแทนที่อนุญาตให้สร้างภาพF [ a ] ได้ก็ต่อเมื่อaอยู่ในโดเมนของฟังก์ชันคลาสFเท่านั้น ในกรณีนั้น การอนุมานการแยกต้องใช้สัจพจน์ของเซตว่าง ในทางกลับกัน ข้อจำกัดของความเป็นทั้งหมดของFมักถูกละทิ้งจากโครงร่างการแทนที่ ซึ่งในกรณีนี้จะหมายถึงโครงร่างการแยกโดยไม่ต้องใช้สัจพจน์ของเซตว่าง (หรือสัจพจน์อื่นใดก็ตาม)