ทฤษฎีเซตเชิงสร้างสรรค์แบบสัจพจน์เป็นแนวทางหนึ่งของลัทธิสร้างสรรค์ทางคณิตศาสตร์ที่ดำเนินตามแบบแผนของทฤษฎีเซตแบบสัจพจน์ โดยทั่วไปจะใช้ ภาษาลำดับที่หนึ่งแบบเดียวกัน กับ " " และ " " ของทฤษฎีเซตแบบคลาสสิก ดังนั้นจึงไม่ควรสับสนกับ แนวทาง ประเภทเชิงสร้างสรรค์ ในทางกลับกัน ทฤษฎีเชิงสร้างสรรค์บางทฤษฎีได้รับแรงบันดาลใจจากความสามารถใน การ ตีความในทฤษฎีประเภท${\displaystyle =}$${\displaystyle \in }$

นอกจากจะปฏิเสธหลักการของส่วนกลางที่ถูกกีดกัน ( ) แล้ว ทฤษฎีเซตเชิงสร้างสรรค์มักต้องการให้ตัวบ่งปริมาณเชิงตรรกะบางตัวในสัจพจน์มีขอบเขตจำกัดซึ่งได้รับแรงบันดาลใจจากผลลัพธ์ที่เกี่ยวข้องกับความไม่แน่นอน ${\displaystyle {\mathrm {PEM} }}$

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

ในทฤษฎีเซต ข้อจำกัดในการตีความเชิงสร้างสรรค์ของการมีอยู่โดยปริยาย นำไปสู่ข้อกำหนดที่เข้มงวดมากขึ้นเกี่ยวกับลักษณะเฉพาะของเซตที่เกี่ยวข้องกับกลุ่มที่ไม่จำกัดขอบเขต ซึ่งประกอบเป็นฟังก์ชัน (ทางคณิตศาสตร์ และดังนั้นจึงหมายถึง ฟังก์ชัน ทั้งหมด เสมอ ) มักเป็นเพราะเงื่อนไขในนิยามที่เป็นไปได้ในแต่ละกรณีอาจไม่สามารถตัดสินได้ โดยการนำนิยามมาตรฐานของความเท่าเทียมกันของเซตผ่านการขยายขอบเขตมาใช้ สัจพจน์ แห่งการเลือก ( Axiom of Choice) ฉบับสมบูรณ์ จึงเป็นหลักการที่ไม่สร้างสรรค์ ซึ่งบ่งชี้ถึงสูตรที่อนุญาตในแผนผังการแยก (Separation schema) ที่นำมาใช้ โดยทฤษฎีบทของ Diaconescuผลลัพธ์ที่คล้ายกันนี้ใช้ได้กับ การอ้างสิทธิ์การมีอยู่ของ สัจพจน์แห่งความสม่ำเสมอ (Axiom of Regularity)ดังแสดงด้านล่าง ซึ่งมี ตัวแทน อุปนัย ที่เทียบเท่ากันในทางคลาสสิก ดังนั้น การพัฒนาทฤษฎีเซตแบบสัญชาตญาณนิยมอย่างแท้จริงจึงต้องมีการปรับเปลี่ยนถ้อยคำของสัจพจน์มาตรฐานบางข้อให้เทียบเท่ากันในทางคลาสสิก นอกเหนือจากความต้องการความสามารถในการคำนวณและข้อสงวนเกี่ยวกับความไม่สามารถคาดเดาได้^{[ 1 ]}คำถามทางเทคนิคเกี่ยวกับสัจพจน์ที่ไม่ใช่ตรรกะใดที่ขยายตรรกะพื้นฐานของทฤษฎีได้อย่างมีประสิทธิภาพ ถือเป็นหัวข้อวิจัยอีกเรื่องหนึ่งเช่นกัน ${\displaystyle f\subset X\times Y}$${\displaystyle {\mathrm {PEM} }}$

ด้วยข้อเสนอที่ไม่สามารถตัดสินได้ด้วยการคำนวณซึ่งเกิดขึ้นแล้วในเลขคณิตของโรบินสันแม้แต่การแยกเชิงทำนาย เพียงอย่างเดียว ก็ทำให้สามารถกำหนดเซตย่อยที่เข้าใจยากได้อย่างง่ายดาย ในทางตรงกันข้ามกับกรอบงานแบบคลาสสิก ทฤษฎีเซตเชิงสร้างสรรค์อาจปิดได้ภายใต้กฎที่ว่าคุณสมบัติใด ๆ ที่สามารถตัดสินได้สำหรับทุกเซตนั้นเทียบเท่ากับคุณสมบัติที่ไม่สำคัญอย่างใดอย่างหนึ่งหรือนอกจากนี้ เส้นจำนวนจริงอาจถือได้ว่าไม่สามารถแยกส่วนได้ในความหมายนี้ ความไม่สามารถตัดสินได้ของการเชื่อมโยงแบบเลือกยังส่งผลต่อข้ออ้างเกี่ยวกับลำดับทั้งหมด เช่น ลำดับของจำนวนเชิงอันดับ ทั้งหมด ซึ่งแสดงโดยความสามารถในการพิสูจน์และการปฏิเสธของข้อความในลำดับที่กำหนดการเชื่อมโยงแบบเลือกสิ่งนี้จะกำหนดว่าความสัมพันธ์นั้นเป็นแบบไตรภาคหรือไม่ ทฤษฎีของจำนวนเชิงอันดับที่อ่อนแอลงจะส่งผลต่อความแข็งแกร่งทางทฤษฎีการพิสูจน์ที่กำหนดไว้ในการวิเคราะห์เชิงอันดับ ${\displaystyle \top }$${\displaystyle \bot }$${\displaystyle (\alpha \in \beta )\lor (\alpha =\beta )\lor (\beta \in \alpha )}$

ในทางกลับกัน ทฤษฎีเซตเชิงสร้างสรรค์สามารถแสดงคุณสมบัติการแยกและการมีอยู่ที่ น่าสนใจได้ ดังที่คุ้นเคยจากการศึกษาทฤษฎีเลขคณิตเชิงสร้างสรรค์ คุณสมบัติเหล่านี้เป็นคุณลักษณะของทฤษฎีคงที่ซึ่งเชื่อมโยงการตัดสินของข้อเสนอที่พิสูจน์ได้ในทฤษฎีโดยเชิงอภิปรัชญา โดยเฉพาะอย่างยิ่ง คุณลักษณะดังกล่าวได้รับการศึกษาอย่างดี ซึ่งสามารถแสดงได้ในเลขคณิตของ Heytingด้วยตัวบ่งปริมาณเหนือตัวเลข และซึ่งมักจะสามารถรับรู้ได้ด้วยตัวเลข ตามที่เป็นทางการในทฤษฎีการพิสูจน์โดยเฉพาะอย่างยิ่ง คุณสมบัติการมีอยู่เชิงตัวเลขและคุณสมบัติการแยกที่เกี่ยวข้องอย่างใกล้ชิด ตลอดจนการปิดภายใต้กฎของ Churchซึ่งเป็นพยานว่าฟังก์ชันที่กำหนดใด ๆ สามารถคำนวณได้^{[ 2 ]}

ทฤษฎีเซตไม่ได้แสดงเพียงทฤษฎีบทเกี่ยวกับจำนวนเท่านั้น ดังนั้นจึงอาจพิจารณาคุณสมบัติการมีอยู่แบบเข้มแข็ง (strong existence property) ที่ทั่วไปกว่า ซึ่งหาได้ยากกว่า ดังที่จะได้กล่าวถึงต่อไป ทฤษฎีจะมีคุณสมบัตินี้ได้ก็ต่อเมื่อสามารถพิสูจน์ได้ดังต่อไปนี้: สำหรับคุณสมบัติใดๆถ้าทฤษฎีพิสูจน์ได้ว่ามีเซตที่มีคุณสมบัตินั้นอยู่ กล่าวคือ ถ้าทฤษฎีอ้างถึงข้อความการมีอยู่ ก็จะมีคุณสมบัติที่อธิบายเซตดังกล่าวได้อย่างเฉพาะ เจาะจงด้วย กล่าวอย่างเป็นทางการมากขึ้น สำหรับ述语 (predicate) ใดๆ ก็ จะมี述语 (predicate) ที่ทำให้ ${\displaystyle \phi }$${\displaystyle \psi }$${\displaystyle \phi }$${\displaystyle \psi }$

${\displaystyle {\mathsf {T}}\vdash \exists x.\phi (x)\implies {\mathsf {T}}\vdash \exists !x.\phi (x)\land \psi (x)}$

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

ทฤษฎีบางทฤษฎีที่มีการตีความการดำรงอยู่แบบคลาสสิกนั้น ในความเป็นจริงแล้วสามารถถูกจำกัดเพื่อให้แสดงคุณสมบัติการดำรงอยู่แบบเข้มแข็งได้เช่นกัน ในทฤษฎีเซตของ Zermelo–Fraenkelซึ่งเซตทั้งหมดถือว่าสามารถกำหนดได้ด้วยลำดับ (ordinal-definable)ซึ่งเป็นทฤษฎีที่ใช้สัญลักษณ์ไม่มีเซตใดที่ไม่มีคุณสมบัติการกำหนดได้เช่นนั้น คุณสมบัตินี้ยังได้รับการบังคับใช้ผ่าน สมมติฐาน เอกภพที่สร้างได้ในเพื่อเปรียบเทียบ ลองพิจารณาทฤษฎีที่กำหนดโดยบวกกับสัจพจน์เต็มรูปแบบของสมมติฐานการดำรงอยู่ของ การเลือก : โปรดจำไว้ว่าชุดของสัจพจน์นี้พิสูจน์ทฤษฎีบทการเรียงลำดับที่ดี (well-ordering theorem) ซึ่งหมายความว่าการเรียงลำดับที่ดีมีอยู่สำหรับเซตใดๆ โดยเฉพาะอย่างยิ่ง หมายความว่าความสัมพันธ์มีอยู่จริงในทางรูปแบบที่สร้างการเรียงลำดับที่ดีของ(กล่าวคือ ทฤษฎีอ้างว่ามีองค์ประกอบที่เล็กที่สุดสำหรับเซตย่อยทั้งหมดของโดยสัมพันธ์กับความสัมพันธ์เหล่านั้น) ทั้งนี้แม้ว่าความสามารถในการกำหนดลำดับดังกล่าวจะเป็น ที่ ทราบ กันดีว่าไม่ ขึ้นอยู่กับ ซึ่งหมายความว่าสำหรับสูตรเฉพาะใดๆในภาษาของทฤษฎี ทฤษฎีไม่ได้พิสูจน์ว่าเซตที่สอดคล้องกันเป็นความสัมพันธ์การเรียงลำดับที่ดีของจำนวนจริง ดังนั้น จึงเป็นการพิสูจน์อย่างเป็นทางการ ถึงการมีอยู่ ของเซตย่อยที่มีคุณสมบัติของการเป็นความสัมพันธ์แบบเรียงลำดับที่ดี แต่ในขณะเดียวกัน ก็ไม่สามารถกำหนดเซตเฉพาะใดๆ ที่สามารถตรวจสอบคุณสมบัติดังกล่าวได้ ${\displaystyle {\mathsf {ZF}}+({\mathrm {V} }={\mathrm {HOD} })}$${\displaystyle {\mathsf {ZF}}+({\mathrm {V} }={\mathrm {L} })}$${\displaystyle {\mathsf {ZFC}}}$${\displaystyle {\mathsf {ZF}}}$${\displaystyle W\subset {\mathbb {R} }\times {\mathbb {R} }}$${\displaystyle {\mathbb {R} }}$${\displaystyle {\mathbb {R} }}$${\displaystyle {\mathsf {ZFC}}}$${\displaystyle \psi }$${\displaystyle {\mathsf {ZFC}}}$${\displaystyle W\subset {\mathbb {R} }\times {\mathbb {R} }}$${\displaystyle W}$

ดังที่กล่าวมาข้างต้น ทฤษฎีเชิงสร้างสรรค์อาจแสดงคุณสมบัติการมีอยู่เชิงตัวเลขสำหรับจำนวนบางจำนวนและ โดยที่หมายถึงจำนวนที่สอดคล้องกันในทฤษฎีเชิงรูปธรรม ในที่นี้ต้องแยกแยะอย่างระมัดระวังระหว่างการบ่งชี้ที่พิสูจน์ได้ระหว่างสองประพจน์และคุณสมบัติของทฤษฎีในรูปแบบเมื่อใช้แบบแผนที่สร้างขึ้นทางอภิปรัชญาของประเภทหลังเป็นกฎการอนุมานของแคลคูลัสการพิสูจน์ และไม่สามารถพิสูจน์สิ่งใหม่ได้อีกต่อไป เราจะกล่าวว่าทฤษฎีนั้นปิดภายใต้กฎนั้น ${\displaystyle {\mathsf {T}}}$${\displaystyle {\mathsf {T}}\vdash \exists e.\psi (e)\implies {\mathsf {T}}\vdash \psi ({\underline {\mathrm {e} }})}$${\displaystyle {\mathrm {e} }}$${\displaystyle {\underline {\mathrm {e} }}}$${\displaystyle {\mathsf {T}}\vdash P\to Q}$${\displaystyle {\mathsf {T}}\vdash P\implies {\mathsf {T}}\vdash Q}$${\displaystyle {\mathsf {T}}}$

เราอาจพิจารณาเพิ่มกฎที่สอดคล้องกับคุณสมบัติเชิงอภิปรัชญาเป็นนัย (ในความหมายของ " ") ให้กับในรูปแบบของแผนผังสัจพจน์หรือในรูปแบบเชิงปริมาณ สถานการณ์ที่ศึกษากันโดยทั่วไปคือสถานการณ์ของค่าคงที่ที่แสดงคุณสมบัติเชิงอภิปรัชญาประเภทต่อไปนี้: สำหรับตัวอย่างจากชุดสูตรบางสูตรในรูปแบบเฉพาะ ซึ่งในที่นี้แสดงผ่านและเราได้พิสูจน์การมีอยู่ของจำนวนเพื่อให้ในที่นี้เราอาจตั้งสมมติฐานโดยที่ขอบเขตเป็นตัวแปรจำนวนในภาษาของทฤษฎี ตัวอย่างเช่น กฎของ Church เป็นกฎที่ยอมรับได้ในเลขคณิต Heyting อันดับแรกและยิ่งไปกว่านั้นหลักการวิทยานิพนธ์ของ Church ที่สอดคล้องกันสามารถนำมาใช้เป็นสัจพจน์ได้อย่างสอดคล้อง ทฤษฎีใหม่ที่มีหลักการนี้เพิ่มเข้ามานั้นเป็นแบบต่อต้านคลาสสิก เนื่องจากอาจไม่สอดคล้องกันอีกต่อไปที่จะนำ มาใช้ด้วย ในทำนอง เดียวกัน การนำหลักการตรงกลางที่ถูกยกเว้นไปผนวกเข้ากับทฤษฎีบางอย่างทฤษฎีที่ได้มานั้นอาจพิสูจน์ข้อความใหม่ที่เป็นแบบคลาสสิกอย่างเคร่งครัด และอาจทำให้คุณสมบัติเชิงอภิปรัชญาบางประการที่เคยได้รับการพิสูจน์ไว้ก่อนหน้านี้สำหรับ เสียไปในลักษณะเช่นนี้อาจไม่สามารถนำมาใช้ในซึ่งเรียกอีกอย่างว่าเลขคณิตของพีอาโน ${\displaystyle \to }$${\displaystyle {\mathsf {T}}}$${\displaystyle {\mathsf {T}}}$${\displaystyle \phi }$${\displaystyle \psi }$${\displaystyle {\mathrm {e} }}$${\displaystyle {\mathsf {T}}\vdash \phi \implies {\mathsf {T}}\vdash \psi ({\underline {\mathrm {e} }})}$${\displaystyle \phi \to \exists (e\in {\mathbb {N} }).\psi (e)}$${\displaystyle e}$${\displaystyle {\mathsf {HA}}}$${\displaystyle {\mathrm {CT} }_{0}}$${\displaystyle {\mathrm {PEM} }}$${\displaystyle {\mathrm {PEM} }}$${\displaystyle {\mathsf {T}}}$${\displaystyle {\mathsf {T}}}$${\displaystyle {\mathrm {CT} }_{0}}$${\displaystyle {\mathsf {HA}}+{\mathrm {PEM} }}$${\displaystyle {\mathsf {PA}}}$

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

${\displaystyle \forall (f\in {\mathbb {N} }^{\mathbb {N} }).\exists (e\in {\mathbb {N} }).{\Big (}\forall (n\in {\mathbb {N} }).\exists (w\in {\mathbb {N} }).T(e,n,w)\land U(w,f(n)){\Big )}}$

เงื่อนไข T ของ Kleeneร่วมกับการดึงผลลัพธ์แสดงให้เห็นว่าตัวเลขอินพุตใดๆที่ถูกแมปไปยังตัวเลขนั้นจะถูกพิสูจน์ได้ว่าเป็นการแมปที่คำนวณได้ ในที่นี้หมายถึงแบบจำลองทฤษฎีเซตของจำนวนธรรมชาติมาตรฐาน และคือดัชนีที่เกี่ยวข้องกับการแจงนับโปรแกรมที่กำหนดไว้ มีการใช้รูปแบบที่แข็งแกร่งกว่า ซึ่งขยายหลักการนี้ไปยังฟังก์ชันที่กำหนดบนโดเมนที่มีความซับซ้อนต่ำ หลักการนี้ปฏิเสธความสามารถในการตัดสินใจสำหรับเงื่อนไขที่กำหนดเป็น ซึ่งแสดงว่าคือดัชนีของฟังก์ชันที่คำนวณได้ซึ่งหยุดที่ดัชนีของตัวเอง อาจพิจารณารูปแบบที่อ่อนกว่าและมีการปฏิเสธสองครั้งของหลักการนี้ได้เช่นกัน ซึ่งไม่จำเป็นต้องมีการใช้งานแบบเรียกซ้ำสำหรับทุกแต่ยังคงทำให้หลักการที่อ้างว่ามีฟังก์ชันที่พิสูจน์ได้ว่าไม่มีการใช้งานแบบเรียกซ้ำนั้นไม่สอดคล้องกัน บางรูปแบบของวิทยานิพนธ์ของ Church ในฐานะหลักการนั้นสอดคล้องกับทฤษฎีเลขคณิตลำดับที่สอง แบบคลาสสิกที่อ่อนแอ ซึ่ง เป็นระบบย่อยของทฤษฎีลำดับแรกแบบสองประเภท ด้วย ซ้ำ ${\displaystyle n}$${\displaystyle f(n)}$${\displaystyle w}$${\displaystyle {\mathbb {N} }}$${\displaystyle e}$${\displaystyle f\in {\mathbb {N} }^{X}}$${\displaystyle X\subset {\mathbb {N} }}$${\displaystyle Q(e)}$${\displaystyle \exists (w\in {\mathbb {N} }).T(e,e,w)}$${\displaystyle e}$${\displaystyle f}$${\displaystyle {\mathsf {RCA}}_{0}}$${\displaystyle {\mathsf {Z}}_{2}}$

กลุ่มของฟังก์ชันที่คำนวณได้นั้นสามารถนับได้ ในระดับคลาสสิก ซึ่งในระดับคลาสสิกก็เหมือนกับการนับได้ แต่ทฤษฎีเซตแบบคลาสสิกโดยทั่วไปจะอ้างว่าสิ่งนี้ใช้ได้กับฟังก์ชันอื่นๆ นอกเหนือจากฟังก์ชันที่คำนวณได้ด้วย ตัวอย่างเช่น มีการพิสูจน์ว่าฟังก์ชันทั้งหมด (ในความหมายของทฤษฎีเซต) มีอยู่จริงที่ไม่สามารถจับได้ด้วยเครื่องจักรทัวริงหากพิจารณาโลกแห่งการคำนวณอย่างจริงจังในฐานะออนโทโลยี ตัวอย่างสำคัญของแนวคิดต่อต้านคลาสสิกที่เกี่ยวข้องกับสำนักมาร์โคเวียนคือการอนุญาตให้กลุ่มที่ไม่สามารถนับได้ต่างๆ สามารถนับได้ในระดับคลาสสิก เมื่อนำเอาการนับได้ในระดับคลาสสิกของกลุ่มลำดับที่ไม่มีที่สิ้นสุดของจำนวนธรรมชาติทั้งหมด ( ) มาใช้เป็นสัจพจน์ในทฤษฎีเชิงสร้างสรรค์ "ความเล็ก" (ในแง่คลาสสิก) ของกลุ่มนี้ ในการสร้างทฤษฎีเซตบางอย่าง ก็จะถูกทฤษฎีนั้นจับเอาไว้แล้ว ทฤษฎีเชิงสร้างสรรค์อาจไม่นำเอาสัจพจน์แบบคลาสสิกหรือต่อต้านคลาสสิกมาใช้ และจึงยังคงไม่เอนเอียงไปทางใดทางหนึ่ง ${\displaystyle {\mathbb {N} }^{\mathbb {N} }}$${\displaystyle {\mathsf {ZF}}}$${\displaystyle {\mathbb {N} }^{\mathbb {N} }}$

หลักการเชิงสร้างสรรค์ได้พิสูจน์แล้วสำหรับและดังนั้นสำหรับองค์ประกอบใดๆของข้อความตรงกลางที่ถูกยกเว้นที่สอดคล้องกันสำหรับข้อเสนอจะไม่สามารถถูกปฏิเสธได้ อันที่จริง สำหรับ ใดๆ ที่กำหนดโดยหลักการไม่ขัดแย้ง เป็นไปไม่ได้ที่จะตัดออกและตัดออกการปฏิเสธพร้อมกัน และกฎของเดอ มอร์แกนที่เกี่ยวข้องจะใช้ได้ดังที่กล่าวมาข้างต้น แต่ทฤษฎีอาจอนุญาตให้มีการอ้างการปฏิเสธได้ในบางกรณีการยอมรับสิ่งนี้ไม่จำเป็นต้องให้พยานเฉพาะเจาะจงที่แสดงถึงความล้มเหลวของข้อความตรงกลางที่ถูกยกเว้นสำหรับข้อเสนอเฉพาะเจาะจง กล่าว คือ พยานถึงความไม่สอดคล้องกันภาคแสดงบนโดเมนอนันต์สอดคล้องกับปัญหาการตัดสินใจด้วยแรงจูงใจจากปัญหาที่ไม่สามารถตัดสินได้ด้วยการคำนวณที่ พิสูจน์แล้ว เราอาจปฏิเสธความเป็นไปได้ของการตัดสินใจของภาคแสดงโดยไม่ต้องอ้างการมีอยู่ใดๆใน อีกตัวอย่างหนึ่ง สถานการณ์ดังกล่าวถูกบังคับใช้ใน การวิเคราะห์เชิงสัญชาตญาณ ของบราวเวอร์ในกรณีที่ตัวบ่งปริมาณครอบคลุมลำดับไบนารีที่ไม่มีที่ สิ้นสุดจำนวนอนันต์ และระบุว่าลำดับเป็นศูนย์ทุกที่ ในส่วนที่เกี่ยวกับคุณสมบัตินี้ ซึ่งได้รับการระบุอย่างแน่ชัดว่าเป็นลำดับที่คงที่ตลอดไป การนำหลักการความต่อเนื่องของ Brouwer มาใช้อย่างเคร่งครัดทำให้ไม่สามารถพิสูจน์ได้ว่าคุณสมบัตินี้สามารถตัดสินได้สำหรับลำดับทั้งหมด ${\displaystyle \forall (x\in X).\neg \neg {\big (}Q(x)\lor \neg Q(x){\big )}}$${\displaystyle Q}$${\displaystyle x}$${\displaystyle X}$${\displaystyle x}$${\displaystyle Q(x)}$${\displaystyle \neg \forall (x\in X).{\big (}Q(x)\lor \neg Q(x){\big )}}$${\displaystyle t\in X}$${\displaystyle Q(t)}$${\displaystyle \neg {\big (}Q(t)\lor \neg Q(t){\big )}}$${\displaystyle Q(x)}$${\displaystyle X}$${\displaystyle X}$${\displaystyle Q(x)}$${\displaystyle x}$

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

ในทางประวัติศาสตร์ หัวข้อของทฤษฎีเซตเชิงสร้างสรรค์ (มักเรียกอีกอย่างว่า " ") เริ่มต้นด้วยงานของJohn Myhill เกี่ยวกับทฤษฎีที่เรียก ว่าและ^{[ 3 ] [ 4 ] [ 5 ]} ในปี 1973 เขาได้เสนอทฤษฎีเซตเชิงสร้างสรรค์เป็นทฤษฎีเซตลำดับที่หนึ่งโดยอาศัยตรรกะเชิงสัญชาตญาณ โดยใช้พื้นฐานที่พบได้ทั่วไปและละทิ้งสัจพจน์ของการเลือก รวมถึงหลักการของสิ่งที่ไม่รวมอยู่ตรงกลาง โดยในตอนแรกยังคงทุกอย่างไว้เหมือนเดิม อย่างไรก็ตาม รูปแบบที่แตกต่างกันของสัจพจน์บางส่วนที่เทียบเท่ากันในบริบทแบบคลาสสิกนั้นไม่เทียบเท่ากันในบริบทเชิงสร้างสรรค์ และบางรูปแบบบ่งชี้ว่าดังที่จะแสดงให้เห็น ในกรณีเหล่านั้น จึงมีการนำสูตรที่อ่อนแอกว่าในเชิงสัญชาตญาณมาใช้ ระบบที่อนุรักษ์นิยมมากกว่ามากนี้ก็เป็นทฤษฎีลำดับที่หนึ่งเช่นกัน แต่มีหลายประเภทและมีการกำหนดปริมาณแบบจำกัด โดยมีเป้าหมายเพื่อให้เป็นพื้นฐานอย่างเป็นทางการสำหรับโครงการคณิตศาสตร์เชิงสร้างสรรค์ของ Errett Bishop${\displaystyle {\mathsf {CST}}}$${\displaystyle {\mathsf {IZF}}}$${\displaystyle {\mathsf {CST}}}$${\displaystyle {\mathsf {ZFC}}}$${\displaystyle {\mathsf {ZFC}}}$${\displaystyle {\mathrm {PEM} }}$${\displaystyle {\mathsf {CST}}}$

การอภิปรายหลักนำเสนอทฤษฎีลำดับในภาษาเดียวกันกับ ซึ่งนำไปสู่ทฤษฎีที่^ได้รับการศึกษาอย่างดีของPeter Aczel [ ^{6 ]}และอื่นๆ ผลลัพธ์สมัยใหม่หลายอย่างสืบย้อนไปถึง Rathjen และลูกศิษย์ของเขา ยังมีลักษณะเฉพาะด้วยคุณสมบัติสองประการที่มีอยู่ในทฤษฎีของ Myhill ด้วยเช่นกัน: ประการแรก มันใช้การแยกเชิงทำนายแทนที่จะใช้แผนผังการแยกแบบเต็มรูปแบบที่ไม่จำกัดขอบเขต ขอบเขตสามารถจัดการได้ในฐานะคุณสมบัติทางไวยากรณ์ หรืออีกทางหนึ่ง ทฤษฎีสามารถขยายได้แบบอนุรักษ์นิยมด้วยตัวบ่งชี้ขอบเขตที่สูงกว่าและสัจพจน์ของมัน ประการที่สองสัจพจน์ Powerset ที่ไม่สามารถ ทำนาย ได้ถูกละทิ้ง โดยทั่วไปแล้วจะใช้สัจพจน์ที่เกี่ยวข้องแต่มีความอ่อนแอกว่าแทน รูปแบบที่แข็งแกร่งถูกใช้อย่างไม่เป็นทางการในโทโพโลยีทั่วไป แบบคลาสสิก การเพิ่มเข้าไปในทฤษฎีที่อ่อนแอกว่าจะกู้คืนได้ดังรายละเอียดด้านล่าง^{[ 7 ]} ระบบซึ่งต่อมาเป็นที่รู้จักกันในชื่อทฤษฎีเซตแบบสัญชาตญาณของ Zermelo–Fraenkel ( ) เป็นทฤษฎีเซตที่แข็งแกร่งโดยไม่มีคล้ายกับแต่มีความอนุรักษ์นิยมหรือทำนาย ได้น้อยกว่า ทฤษฎีที่ระบุว่าเป็นเวอร์ชันเชิงสร้างสรรค์ของทฤษฎีเซต Kripke–Platekแบบคลาสสิกที่ไม่มีรูปแบบของ Powerset และแม้แต่สัจพจน์ของการรวบรวมก็มีขอบเขต ${\displaystyle {\mathsf {ZF}}}$${\displaystyle {\mathsf {CZF}}}$${\displaystyle {\mathsf {CZF}}}$${\displaystyle {\mathrm {PEM} }}$${\displaystyle {\mathsf {CZF}}}$${\displaystyle {\mathsf {ZF}}}$${\displaystyle {\mathsf {IZF}}}$${\displaystyle {\mathrm {PEM} }}$${\displaystyle {\mathsf {CZF}}}$${\displaystyle {\mathsf {IKP}}}$${\displaystyle {\mathsf {KP}}}$

ทฤษฎีจำนวนมากที่ศึกษาในทฤษฎีเซตเชิงสร้างสรรค์เป็นเพียงข้อจำกัดของทฤษฎีเซต Zermelo–Fraenkel ( )${\displaystyle {\mathsf {ZF}}}$ในแง่ของสัจพจน์และตรรกะพื้นฐาน ทฤษฎีเหล่านี้จึงสามารถตีความได้ในแบบจำลองใดๆของ ${\displaystyle {\mathsf {ZF}}}$

เมื่อเปรียบเทียบเลขคณิตกับทฤษฎีในภาษาของทฤษฎีเซตในด้านหนึ่งเลขคณิต Peano แบบคลาสสิก สามารถตีความได้สองทางกับทฤษฎีที่กำหนดโดยลบอนันต์และไม่มีเซตอนันต์ บวกกับการมีอยู่ของการปิดแบบทรานซิทีฟ ทั้งหมด (ข้อหลังนี้ยังบ่งบอกเป็นนัยหลังจากส่งเสริมความสม่ำเสมอให้กับแบบแผนการเหนี่ยวนำเซตซึ่งจะกล่าวถึงต่อไป) ในทำนองเดียวกัน เลขคณิตเชิงสร้างสรรค์ยังสามารถใช้เป็นข้อแก้ตัวสำหรับสัจพจน์ส่วนใหญ่ที่นำมาใช้ใน: เลขคณิต Heytingสามารถตีความได้สองทางกับทฤษฎีเซตเชิงสร้างสรรค์แบบอ่อน^{[ 8 ] [ 9 ]}ดังที่อธิบายไว้ในบทความเกี่ยวกับเราอาจกำหนดลักษณะความสัมพันธ์การเป็นสมาชิก " " ทางเลขคณิตและด้วยความสัมพันธ์นั้นพิสูจน์ได้ว่า - แทนที่จะเป็นการมีอยู่ของเซตของจำนวนธรรมชาติ - เซตทั้งหมดในทฤษฎีของมันอยู่ในการจับคู่แบบหนึ่งต่อหนึ่งกับจำนวน ธรรมชาติ von Neumann (จำกัด) ซึ่งเป็นหลักการที่แสดงด้วย บริบทนี้ยืนยันเพิ่มเติมถึงความเป็นส่วนขยาย การจับคู่ การรวมกัน การตัดกันแบบไบนารี (ซึ่งเกี่ยวข้องกับแผนผังสัจพจน์ของการแยกเชิงทำนาย ) และแผนผังการเหนี่ยวนำเซต เมื่อนำมาใช้เป็นสัจพจน์ หลักการดังกล่าวข้างต้นประกอบกันเป็นทฤษฎีเซตที่เหมือนกับทฤษฎีที่กำหนดโดยลบการมีอยู่ของแต่บวกเป็นสัจพจน์ สัจพจน์ทั้งหมดเหล่านั้นจะได้รับการอธิบายโดยละเอียดด้านล่าง ในทำนองเดียวกันยังพิสูจน์ได้ว่าเซตจำกัดแบบสืบทอด นั้น เป็นไปตามสัจพจน์ก่อนหน้านี้ทั้งหมด ผลลัพธ์นี้ยังคงอยู่เมื่อส่งต่อไปยังและลบอนันต์ ในทางกลับกันบวกการแยกอย่างสมบูรณ์นั้นไม่ได้แข็งแกร่งกว่าเลขคณิตอันดับสองแบบคลาสสิก ${\displaystyle {\mathsf {PA}}}$${\displaystyle {\mathsf {ZF}}}$${\displaystyle {\mathsf {CZF}}}$${\displaystyle {\mathsf {HA}}}$${\displaystyle {\mathsf {HA}}}$${\displaystyle \in }$${\displaystyle \omega }$${\displaystyle {\mathrm {V} }={\mathrm {Fin} }}$${\displaystyle {\mathsf {CZF}}}$${\displaystyle \omega }$${\displaystyle {\mathrm {V} }={\mathrm {Fin} }}$${\displaystyle {\mathsf {CZF}}}$${\displaystyle {\mathsf {PA}}}$${\displaystyle {\mathsf {ZF}}}$${\displaystyle {\mathsf {CZF}}}$

ในส่วนของการสร้างความจริงเชิงสร้างสรรค์นั้น มี ทฤษฎี การสร้างความ จริงที่เกี่ยวข้องอยู่ ในทำนองเดียวกัน ทฤษฎีการสร้างความจริงเชิงสร้างสรรค์ของ Aczel หรือ Zermelo-Fraenkel ได้รับการตีความในทฤษฎีประเภท Martin-Löfดังที่ได้กล่าวไว้ในส่วนเกี่ยวกับเรื่องนี้ด้วยวิธีนี้ ทฤษฎีบทที่พิสูจน์ได้ในทฤษฎีเซตนี้และทฤษฎีเซตที่อ่อนกว่า จึงเป็นตัวเลือกสำหรับการนำไปใช้ในคอมพิวเตอร์ ${\displaystyle {\mathsf {CZF}}}$${\displaystyle {\mathsf {CZF}}}$

แบบจำลอง พรีชีฟสำหรับทฤษฎีเซตเชิงสร้างสรรค์ได้รับการแนะนำแล้วเช่นกัน แบบจำลองเหล่านี้คล้ายคลึงกับแบบจำลองพรีชีฟสำหรับทฤษฎีเซตเชิงสัญชาตญาณที่พัฒนาโดยDana Scottในช่วงทศวรรษ 1980 ^{[ 10 ] [ 11 ]}แบบจำลองการทำให้เป็นจริงภายในโทโพสที่มีประสิทธิภาพได้รับการระบุ ซึ่งตรวจสอบความถูกต้องของการแยกอย่างสมบูรณ์ การเลือกแบบพึ่งพาที่สัมพันธ์กัน ความเป็นอิสระ ของข้อสมมติสำหรับเซต แต่ยังรวมถึงความสามารถในการนับย่อยของเซตทั้งหมด หลักการของ Markov และวิทยานิพนธ์ของ Church ในการกำหนดสูตรสำหรับภาคแสดงทั้งหมดด้วย^{[ 12 ]}${\displaystyle {\mathsf {CZF}}}$${\displaystyle {\mathrm {RDC} }}$${\displaystyle {\mathrm {IP} }}$${\displaystyle {\mathrm {MP} }}$${\displaystyle {\mathrm {CT} _{0}}}$

ด้านล่างนี้ จะนำเสนอชุดของสัจพจน์ที่คุ้นเคย หรือการปรับเปลี่ยนเล็กน้อยที่เกี่ยวข้อง เน้นย้ำว่าการไม่มีอยู่ในตรรกศาสตร์ส่งผลต่อสิ่งที่พิสูจน์ได้อย่างไร สัจพจน์ที่กล่าวถึงจะสร้างขึ้นไปสู่ก่อนต่อมาจะเน้นให้เห็นว่าสัจพจน์ที่ไม่ใช่แบบคลาสสิกใดบ้างที่สอดคล้องกัน ${\displaystyle {\mathrm {PEM} }}$${\displaystyle {\mathsf {ECST}}}$

ในทฤษฎีเซตทฤษฎีเซตเชิงสร้างสรรค์ขั้นพื้นฐาน (Elementary Constructive Set Theory) เป็นทฤษฎีย่อยเชิงสร้างสรรค์ของทฤษฎีเซต Zermelo–Fraenkel โดยใช้ การแยกแบบมีขอบเขตเท่านั้น ทฤษฎีนี้ได้รับการออกแบบอย่างรอบคอบเพื่อให้สามารถพิจารณาได้ว่าเป็น ทฤษฎี เชิงทำนายด้วย${\displaystyle {\mathsf {ECST}}}$${\displaystyle {\mathsf {ZF}}}$

${\displaystyle {\mathsf {ECST}}}$ทฤษฎี นี้อนุญาตให้ดำเนินการพื้นฐานของการรวมเซตและการตัดกันของเซตได้ แตกต่างจากทฤษฎีเซตของ Kripke-Platek ตรง ที่ใช้สัจพจน์ของการแทนที่แต่ไม่ใช้การเหนี่ยวนำเอปซิลอนมีกลไกทั่วไปในการกำหนดและวิเคราะห์ฟังก์ชัน และบทความนี้ขยายความว่าคณิตศาสตร์ในทฤษฎีเซตเชิงสร้างสรรค์โดยทั่วไปแตกต่างจากคณิตศาสตร์ในตรรกศาสตร์แบบคลาสสิกอย่างไรมีเซตอนันต์ โดยเฉพาะอย่างยิ่งเซตของจำนวนธรรมชาติแต่ไม่มีเซตที่นับไม่ได้แบบคลาสสิก ทฤษฎีนี้ยังไม่สามารถจำลองการดำเนินการของเลขคณิต Heytingได้ เนื้อหาในส่วนนี้สรุปโดยอธิบายรายละเอียดความสัมพันธ์ของหลักการทางทฤษฎีเซตเพิ่มเติมกับการเรียกซ้ำแบบดั้งเดิม ${\displaystyle {\mathsf {ECST}}}$${\displaystyle \omega }$

ในตรรกศาสตร์เชิงสัญชาตญาณตรรกศาสตร์คลาสสิกสามารถอธิบายได้ด้วยสัจพจน์ของทฤษฎีเซตบวกกับสัจพจน์ของเซตกำลังเมื่อเพิ่มการรวมกันแบบคลาสสิกอย่างเคร่งครัดของการแยกอย่างสมบูรณ์และสัจพจน์ของความสม่ำเสมอเข้าไป ด้วย${\displaystyle {\mathsf {ZF}}}$${\displaystyle {\mathsf {ECST}}}$

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

ส่วนนี้จะแนะนำภาษาของวัตถุและแนวคิดเสริมที่ใช้ในการทำให้เป็นรูปธรรมนี้

สัญลักษณ์เชื่อมประโยคที่ใช้ในการสร้างสูตรทางไวยากรณ์เป็นมาตรฐาน สัจพจน์ของทฤษฎีเซตให้วิธีการพิสูจน์ความเท่าเทียมกัน " " ของเซต และสัญลักษณ์นั้นอาจถูกนำไปใช้กับคลาสได้โดยการใช้สัญลักษณ์อย่างไม่ถูกต้องเซตที่สามารถตัดสินความเท่าเทียมกันได้เรียกว่าเซตแบบไม่ต่อเนื่องการปฏิเสธ " " ของความเท่าเทียมกันบางครั้งเรียกว่าการปฏิเสธความเท่าเทียมกัน และมักเขียนว่า " " อย่างไรก็ตาม ในบริบทที่มีความสัมพันธ์แบบแยกจากกันเช่น เมื่อจัดการกับลำดับ สัญลักษณ์หลังนี้บางครั้งก็ถูกใช้เพื่อสิ่งอื่นที่แตกต่างออกไป ${\displaystyle =}$${\displaystyle \neg }$${\displaystyle \neq }$

วิธีการทั่วไปที่ใช้กันในที่นี้ก็คือการขยายตรรกะพื้นฐานออกไปโดยใช้ตัวบ่งชี้ทวิภาคดั้งเดิมของทฤษฎีเซตเพียงตัวเดียวเท่านั้นเช่นเดียวกับความเท่าเทียมกัน การปฏิเสธความเป็นองค์ประกอบมักจะเขียนว่า ${\displaystyle \in }$${\displaystyle \in }$${\displaystyle \notin }$

ด้านล่างอักษรกรีกหมายถึงประพจน์หรือตัวแปรภาคแสดงในแบบแผนสัจพจน์และหรือใช้สำหรับภาคแสดงเฉพาะดังกล่าว คำว่า "ภาคแสดง" บางครั้งก็ใช้แทนกันได้กับคำว่า "สูตร" แม้แต่ในกรณีเอกภาคก็ตาม ${\displaystyle \phi }$${\displaystyle P}$${\displaystyle Q}$

ตัวบ่งปริมาณจะใช้กับเซตเท่านั้น และจะใช้ตัวอักษรพิมพ์เล็กแทน โดยทั่วไปแล้ว อาจใช้เครื่องหมายวงเล็บเพื่อแสดงภาคแสดง เพื่อเน้นตัวแปรอิสระบางตัวในนิพจน์ทางไวยากรณ์ เช่น " " การมีอยู่เพียงหนึ่งเดียวในที่นี้หมายถึง. ${\displaystyle Q(z)}$${\displaystyle \exists !x.Q(x)}$${\displaystyle \exists x.\forall y.{\big (}y=x\leftrightarrow Q(y){\big )}}$

โดยทั่วไปแล้ว เรามักใช้สัญกรณ์การสร้างเซตสำหรับคลาสซึ่งในบริบทส่วนใหญ่ไม่ได้เป็นส่วนหนึ่งของภาษาวัตถุ แต่ใช้เพื่อการอธิบายที่กระชับ โดยเฉพาะอย่างยิ่ง เราอาจแนะนำการประกาศสัญกรณ์ของคลาสที่เกี่ยวข้องผ่าน " " เพื่อแสดงสิ่งใด ๆในรูป. สามารถใช้述语ที่เทียบเท่าทางตรรกะเพื่อแนะนำคลาสเดียวกันได้ นอกจากนี้ยังเขียนเป็นตัวย่อสำหรับ ตัวอย่างเช่น เราอาจพิจารณาและสิ่งนี้ก็ถูกแสดงด้วย เช่นกัน ${\displaystyle A=\{z\mid Q(z)\}}$${\displaystyle Q(a)}$${\displaystyle a\in A}$${\displaystyle \{z\in B\mid Q(z)\}}$${\displaystyle \{z\mid z\in B\land Q(z)\}}$${\displaystyle \{z\in B\mid z\notin C\}}$${\displaystyle B\setminus C}$

เราย่อ คำว่า by และby แนวคิดทางไวยากรณ์ของการกำหนดปริมาณแบบจำกัดในความหมายนี้สามารถมีบทบาทในการกำหนดแบบแผนสัจพจน์ ดังที่เห็นได้จากการอธิบายสัจพจน์ด้านล่าง แสดงการอ้างสิทธิ์ของคลาสย่อยเช่นโดยสำหรับภาคแสดงโดย ปริยาย และดังนั้นจึงสรุปได้ว่าแนวคิดของตัวกำหนดปริมาณแบบจำกัดเซตย่อย ดังเช่นใน ได้ถูกนำมาใช้ในการศึกษาทฤษฎีเซตเช่นกัน แต่จะไม่กล่าวถึงเพิ่มเติมในที่นี้ ${\displaystyle \forall z.{\big (}z\in A\to Q(z){\big )}}$${\displaystyle \forall (z\in A).Q(z)}$${\displaystyle \exists z.{\big (}z\in A\land Q(z){\big )}}$${\displaystyle \exists (z\in A).Q(z)}$${\displaystyle \forall (z\in A).z\in B}$${\displaystyle \forall z.(z\in A\to z\in B)}$${\displaystyle A\subset B}$${\displaystyle Q}$${\displaystyle \forall z.{\big (}(z\in B\land Q(z))\to z\in B{\big )}}$${\displaystyle \{z\in B\mid Q(z)\}\subset B}$${\displaystyle \forall (z\subset A).z\in B}$

ถ้าพิสูจน์ได้ว่ามีเซตอยู่ภายในคลาสนั่นหมายความว่า เราจะเรียกคลาสนั้นว่า " มีสมาชิกอยู่ " เราอาจใช้การกำหนดปริมาณในเพื่อแสดงสิ่งนี้ได้เป็นคลาสนั้นจะพิสูจน์ได้ว่าไม่ใช่เซตว่าง ซึ่งจะกล่าวถึงต่อไป แม้ว่าในทางคลาสสิกจะเทียบเท่ากัน แต่ " ไม่ว่าง ในเชิงสร้างสรรค์ " เป็นแนวคิดที่อ่อนกว่า มีการปฏิเสธสองครั้ง และควรเรียกว่า " ไม่มีสมาชิกอยู่ " น่าเสียดายที่คำที่ใช้เรียกแนวคิดที่มีประโยชน์มากกว่าอย่าง "มีสมาชิกอยู่" นั้นไม่ค่อยได้ใช้ในคณิตศาสตร์คลาสสิก ${\displaystyle \exists z.(z\in A)}$${\displaystyle A}$${\displaystyle \exists (z\in A).(z=z)}$${\displaystyle A}$

มีสองวิธีในการแสดงว่าคลาสต่างๆแยกจากกันซึ่งสามารถรวบรวมกฎการปฏิเสธที่ถูกต้องตามสัญชาตญาณได้หลายข้อ: โดยใช้สัญลักษณ์ข้างต้น นี่คือความสมมูลเชิงตรรกะล้วนๆ และในบทความนี้ ข้อเสนอจะสามารถแสดงได้ใน รูป อีกด้วย${\displaystyle {\big (}\forall (x\in A).x\notin B{\big )}\leftrightarrow \neg \exists (x\in A).x\in B}$${\displaystyle A\cap B=\{\}}$

เรียกว่าคลาสย่อยสามารถแยกออกจาก คลาสหลักได้ หากเงื่อนไขการเป็นสมาชิกแบบสัมพัทธ์สามารถตัดสินได้ กล่าวคือ ถ้าเงื่อนไขนั้นเป็นจริง นอกจากนี้ยังเรียกว่าคลาสย่อยสามารถตัดสินได้ หากคลาสหลักมีความชัดเจนจากบริบท ซึ่งมักจะเป็นเซตของจำนวนธรรมชาติ ${\displaystyle A\subset B}$${\displaystyle B}$${\displaystyle \forall (x\in B).x\in A\lor x\notin A}$

ใช้สัญลักษณ์ เพื่อแสดงว่าสองคลาสมีสมาชิกเหมือนกันทุกประการ กล่าวคือหรือเทียบเท่ากับ ซึ่งไม่ควรสับสนกับแนวคิดเรื่องจำนวนสมาชิกที่ เท่า กันซึ่งจะกล่าวถึงต่อไป ${\displaystyle A\simeq B}$${\displaystyle \forall z.(z\in A\leftrightarrow z\in B)}$${\displaystyle (A\subset B)\land (B\subset A)}$

โดยใช้สัญลักษณ์แทนความสัมพันธ์ที่สะดวกระหว่างและสัจพจน์ในรูปแบบจะตั้งสมมติฐานว่ากลุ่มของเซตทั้งหมดที่เป็นจริงนั้น ก่อให้เกิดเซตในรูปแบบที่ไม่เป็นทางการมากนัก อาจแสดงได้เป็น ในทำนองเดียวกัน ข้อเสนอสื่อถึง " เมื่ออยู่ในกลุ่มเซตของทฤษฎี" สำหรับกรณีที่เป็นตัวบ่งชี้ที่ผิดอย่างเห็นได้ชัด ข้อเสนอจะเทียบเท่ากับการปฏิเสธข้ออ้างการมีอยู่ก่อนหน้านี้ ซึ่งแสดงถึงการไม่มีอยู่ของในฐานะเซต ${\displaystyle A}$${\displaystyle \{z\mid Q(z)\}}$${\displaystyle x\in A}$${\displaystyle Q(x)}$${\displaystyle \exists a.\forall z.{\big (}z\in a\leftrightarrow Q(z){\big )}}$${\displaystyle Q}$${\displaystyle \exists a.a\simeq A}$${\displaystyle \forall a.(a\simeq A)\to P(a)}$${\displaystyle P(A)}$${\displaystyle A}$${\displaystyle P}$${\displaystyle A}$

นอกจากนี้ ยังมีการขยายแนวคิดเรื่องความเข้าใจในชั้นเรียนเพิ่มเติมดังที่กล่าวมาข้างต้น ซึ่งใช้กันทั่วไปในทฤษฎีเซต โดยให้ความหมายแก่ข้อความต่างๆ เช่น " " และอื่นๆ ${\displaystyle \{f(z)\mid Q(z)\}\simeq \{\langle x,y,z\rangle \mid T(x,y,z)\}}$

ในทางไวยากรณ์แล้ว เซต อาจถูกกำหนดลักษณะโดยใช้述语 2-ary อีกรูปแบบหนึ่งได้เช่นกันโดยที่ด้านขวามืออาจขึ้นอยู่กับตัวแปรจริงและอาจขึ้นอยู่กับการเป็นสมาชิกในตัวมันเองด้วย ${\displaystyle w}$${\displaystyle R}$${\displaystyle \forall x.x\in w\leftrightarrow R(x,w)}$${\displaystyle w}$${\displaystyle w}$

ตรรกศาสตร์ของทฤษฎีเซตที่กล่าวถึงในที่นี้เป็นแบบสร้างสรรค์ กล่าวคือ มันปฏิเสธหลักการของสิ่งที่ไม่รวมอยู่ตรงกลาง (excluded middle ) กล่าว คือการเชื่อมแบบ " หรือ" (disjunction) นั้น เป็นจริงโดยอัตโนมัติสำหรับทุกประพจน์ สิ่งนี้มักถูกเรียกว่า กฎ ของสิ่งที่ไม่รวมอยู่ตรงกลาง ( law of excluded middle ) ในบริบทที่ถือว่าเป็นเช่นนั้น โดยทั่วไปแล้ว ในเชิงสร้างสรรค์ เพื่อพิสูจน์สิ่งที่ไม่รวมอยู่ตรงกลางสำหรับประพจน์ กล่าวคือ เพื่อพิสูจน์การเชื่อมแบบ " หรือ" นั้น จำเป็นต้องพิสูจน์อย่าง ใดอย่างหนึ่งอย่างชัดเจน เมื่อมีการพิสูจน์อย่างใดอย่างหนึ่งแล้ว เราจะกล่าวว่าประพจน์นั้นสามารถตัดสินได้ (decidable) และสิ่งนี้จะหมายความโดยตรรกะว่าการเชื่อมแบบ "หรือ" นั้นเป็นจริง ในทำนองเดียวกันและพบได้บ่อยกว่านั้น ตัวบ่งชี้สำหรับในโดเมนจะกล่าวได้ว่าสามารถตัดสินได้เมื่อข้อความที่ซับซ้อนกว่านั้นสามารถพิสูจน์ได้ สัจพจน์ที่ไม่ใช่แบบสร้างสรรค์อาจทำให้การพิสูจน์ที่อ้างถึงความสามารถในการตัดสินของ(และ/หรือ) ดังกล่าวอย่างเป็นทางการ ในแง่ที่ว่ามันพิสูจน์สิ่งที่ไม่รวมอยู่ตรงกลางสำหรับ(หรือข้อความที่ใช้ตัวบ่งปริมาณข้างต้น) โดยไม่ต้องแสดงความจริงของด้านใดด้านหนึ่งของการเชื่อมแบบ "หรือ" กรณีนี้มักเกิดขึ้นในตรรกศาสตร์คลาสสิก ในทางตรงกันข้าม ทฤษฎีสัจพจน์ที่ถือว่าเป็นการสร้างสรรค์มักจะไม่ยอมให้มีการพิสูจน์แบบคลาสสิกหลายข้อเกี่ยวกับข้อความที่มีคุณสมบัติซึ่งพิสูจน์ได้ว่าไม่สามารถ ตัดสินได้ด้วยวิธีการ คำนวณ ${\displaystyle {\mathrm {PEM} }}$${\displaystyle \phi \lor \neg \phi }$${\displaystyle \phi }$${\displaystyle {\mathrm {LEM} }}$${\displaystyle P}$${\displaystyle P\lor \neg P}$${\displaystyle P}$${\displaystyle \neg P}$${\displaystyle Q(x)}$${\displaystyle x}$${\displaystyle X}$${\displaystyle \forall (x\in X).{\big (}Q(x)\lor \neg Q(x){\big )}}$${\displaystyle P}$${\displaystyle Q}$${\displaystyle P}$

กฎแห่งความไม่ขัดแย้งเป็นกรณีพิเศษของรูปแบบประพจน์ของmodus ponensการใช้กฎดังกล่าวกับข้อความปฏิเสธใดๆ ทำให้ กฎของเดอ มอร์แกนที่ถูกต้องข้อหนึ่งปรากฏขึ้นแล้วในตรรกะขั้นต่ำ ที่อนุรักษ์นิยมกว่า กล่าวคือตรรกะแบบสัญชาตญาณนิยมยังคงตั้งสมมติฐานว่า เป็นไปไม่ได้ที่จะตัดประพจน์และตัดการปฏิเสธของประพจน์นั้นออกไปพร้อมกัน ดังนั้นการปฏิเสธข้อความตรงกลางที่ถูกยกเว้นสำหรับประพจน์แต่ละข้อจึงไม่สอดคล้องกัน ในที่นี้ การปฏิเสธซ้ำซ้อนแสดงให้เห็นว่าข้อความการแยกที่พิสูจน์แล้วในขณะนี้ไม่สามารถตัดออกหรือปฏิเสธได้เลย แม้ในกรณีที่การแยกนั้นอาจพิสูจน์ไม่ได้ (ตัวอย่างเช่น โดยการแสดงให้เห็นหนึ่งในส่วนประกอบของการแยก ดังนั้นจึงตัดสินใจ) จากสัจพจน์ที่สมมติขึ้น ${\displaystyle \neg P}$${\displaystyle \neg \neg (P\lor \neg P)}$${\displaystyle P}$

ตรรกศาสตร์เชิงสัญชาตญาณที่อยู่เบื้องหลังทฤษฎีเซตที่กล่าวถึงในที่นี้ แตกต่างจากตรรกศาสตร์ขั้นต่ำตรงที่ยังคงอนุญาตให้มีการกำจัดการปฏิเสธซ้ำซ้อนสำหรับประพจน์แต่ละประพจน์ซึ่งหลักการยกเว้นตรงกลางเป็นจริง ในทางกลับกัน การกำหนดทฤษฎีบทเกี่ยวกับวัตถุจำกัดมักจะไม่แตกต่างจากแบบคลาสสิก เมื่อกำหนดแบบจำลองของจำนวนธรรมชาติทั้งหมดแล้ว สิ่งที่เทียบเท่าสำหรับภาคแสดง นั่นคือหลักการของมาร์คอฟจะไม่เป็นจริงโดยอัตโนมัติ แต่สามารถพิจารณาได้ว่าเป็นหลักการเพิ่มเติม ${\displaystyle P}$

ในโดเมนที่มีผู้คนอาศัยอยู่และใช้การระเบิด การเชื่อมโยงแบบ "หรือ" บ่งบอกถึงข้ออ้างการมีอยู่ซึ่งในทางกลับกันก็บ่งบอกถึงในทางคลาสสิก การบ่งชี้เหล่านี้สามารถย้อนกลับได้เสมอ หากข้อใดข้อหนึ่งก่อนหน้านี้ถูกต้องในทางคลาสสิก ก็อาจคุ้มค่าที่จะพยายามพิสูจน์มันในรูปแบบหลัง สำหรับกรณีพิเศษที่ถูกปฏิเสธ เราจะจัดการกับข้ออ้างการมีอยู่ของตัวอย่างค้านซึ่งโดยทั่วไปแล้วมีความแข็งแกร่งกว่าข้ออ้างการปฏิเสธในเชิงสร้างสรรค์การยกตัวอย่างที่ขัดแย้งกัน แน่นอนว่าหมายความว่าไม่ใช่กรณีที่เป็นจริงสำหรับทุก ที่เป็นไปได้แต่เรายังสามารถแสดงให้เห็นได้ว่าการเป็นจริงสำหรับทุกจะนำไปสู่ความขัดแย้งทางตรรกะโดยไม่ต้องอาศัยตัวอย่างค้านเฉพาะ และแม้กระทั่งในขณะที่ไม่สามารถสร้างตัวอย่างค้านได้ ในกรณีหลังนี้ ในเชิงสร้างสรรค์ เราไม่ได้กำหนดข้ออ้างการมีอยู่ ${\displaystyle P\lor \exists (x\in X).\neg Q(x)}$${\displaystyle \exists (x\in X).(Q(x)\to P)}$${\displaystyle {\big (}\forall (x\in X).Q(x){\big )}\to P}$${\displaystyle P}$${\displaystyle \exists (x\in X).\neg Q(x)}$${\displaystyle \neg \forall (x\in X).Q(x)}$${\displaystyle t}$${\displaystyle Q(t)}$${\displaystyle Q}$${\displaystyle x}$${\displaystyle Q}$${\displaystyle x}$

โดยใช้สัญลักษณ์ที่แนะนำข้างต้น สัจพจน์ต่อไปนี้ให้วิธีการพิสูจน์ความเท่าเทียมกัน " " ของเซต สองเซต โดยที่เมื่อแทนค่าแล้ว ตัวบ่งชี้ใดๆ เกี่ยวกับจะแปลงเป็นตัวบ่งชี้ใดๆ ของ ได้ด้วยคุณสมบัติทางตรรกะของความเท่าเทียมกัน ทิศทางตรงกันข้ามของการบ่งชี้ที่สมมติขึ้นจึงเป็นจริงโดยอัตโนมัติ ${\displaystyle =}$${\displaystyle x}$${\displaystyle y}$

ในการตีความเชิงสร้างสรรค์ องค์ประกอบของกลุ่มย่อยของอาจมีข้อมูลมากกว่าองค์ประกอบของในแง่ที่ว่า การสามารถตัดสินได้ก็คือการสามารถตัดสินได้และ (เว้นแต่ว่าการเชื่อมโยงแบบเลือกทั้งหมดจะมาจากสัจพจน์) ในการตีความของ Brouwer–Heyting–Kolmogorovนี่หมายถึงการพิสูจน์หรือการปฏิเสธ เนื่องจากอาจไม่สามารถแยกออกจาก ได้กล่าวคืออาจไม่สามารถตัดสินได้สำหรับองค์ประกอบทั้งหมดในดังนั้น สองกลุ่มและจะต้องถูกแยกแยะออกจากกันโดยหลักการเบื้องต้น ${\displaystyle A=\{z\in B\mid Q(z)\lor \neg Q(z)\}}$${\displaystyle B}$${\displaystyle B}$${\displaystyle b\in A}$${\displaystyle Q(b)\lor \neg Q(b)}$${\displaystyle Q(b)}$${\displaystyle \{z\in B\mid Q(z)\}}$${\displaystyle B}$${\displaystyle Q}$${\displaystyle B}$${\displaystyle A}$${\displaystyle B}$

พิจารณาเงื่อนไขที่พิสูจน์ได้ว่าเป็นจริงสำหรับทุกองค์ประกอบของเซตโดยที่และสมมติว่าคลาสทางด้านขวามือได้รับการพิสูจน์แล้วว่าเป็นเซต โปรดสังเกตว่า แม้ว่าเซตทางด้านขวามือนี้จะเชื่อมโยงกับข้อมูลที่เกี่ยวข้องกับการพิสูจน์ความถูกต้องของเงื่อนไขสำหรับทุกองค์ประกอบอย่างไม่เป็นทางการก็ตาม แต่สัจพจน์ความเท่าเทียม (Extensionality axiom) กำหนดว่า ในทฤษฎีเซตของเรา เซตทางด้านขวามือจะถูกตัดสินว่าเท่ากับเซตทางด้านซ้ายมือ ${\displaystyle Q}$${\displaystyle y}$${\displaystyle y\simeq \{z\in y\mid Q(z)\}}$${\displaystyle Q}$

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

โปรดทราบว่าการใช้ " " เป็นสัญลักษณ์ในทฤษฎีตรรกศาสตร์ภาคแสดง ทำให้ความเท่าเทียมกันของสองพจน์เป็นนิพจน์ที่ไม่ต้องใช้ตัวบ่งปริมาณ ${\displaystyle =}$

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

ทฤษฎีประเภทสมัยใหม่อาจมุ่งเน้นไปที่การกำหนดความเท่าเทียมกันที่ต้องการ " " ในแง่ของฟังก์ชัน ดังเช่นที่เห็นได้ในเรื่องความเท่าเทียมกันของประเภท แนวคิดที่เกี่ยวข้องอย่างเรื่อง ขอบเขตของฟังก์ชันมักไม่ถูกนำมาใช้ในทฤษฎีประเภท ${\displaystyle \simeq }$

กรอบแนวคิดอื่นๆ สำหรับคณิตศาสตร์เชิงสร้างสรรค์อาจเรียกร้องกฎเฉพาะสำหรับการเท่ากันหรือการแยกออกจากกันสำหรับองค์ประกอบของแต่ละเซตที่กล่าวถึง แต่ในแนวทางที่เน้นการแยกออกจากกันของเซต อาจใช้คำจำกัดความข้างต้นในแง่ของเซตย่อยเพื่ออธิบายแนวคิดเรื่องความเท่ากันของเซตย่อยเหล่านั้นได้เช่นกัน ในทำนองเดียวกัน แนวคิดอย่างหลวมๆ ของการเติมเต็มของเซตย่อยสองเซตและเกิดขึ้นเมื่อสมาชิกสองตัวใดๆและสามารถพิสูจน์ได้ว่าแยกออกจากกัน ชุดของคู่ที่เติมเต็มกันนั้นมีพฤติกรรมที่ดี ทางพีชคณิต${\displaystyle z\in x}$${\displaystyle x}$${\displaystyle \simeq }$${\displaystyle u\subset x}$${\displaystyle v\subset x}$${\displaystyle s\in u}$${\displaystyle t\in v}$${\displaystyle \langle u,v\rangle }$

กำหนดสัญลักษณ์แสดงความสัมพันธ์ของการจับคู่ขององค์ประกอบที่กำหนดจำนวนหนึ่งโดยใช้การเชื่อมแบบ "หรือ" ตัวอย่างเช่นคือประโยคที่ไม่มีตัวบ่งปริมาณและในทำนองเดียวกันคือประโยคและอื่นๆ ${\displaystyle z\in \{a,b\}}$${\displaystyle (z=a)\lor (z=b)}$${\displaystyle z\in \{a,b,c\}}$${\displaystyle (z=a)\lor (z=b)\lor (z=c)}$

ข้อสมมติฐานพื้นฐานเกี่ยวกับการดำรงอยู่เพิ่มเติมอีกสองข้อที่กำหนดให้กับเซตอื่นๆ มีดังต่อไปนี้ ประการแรก

จากนิยามข้างต้นจะขยายเป็นดังนั้นนี่จึงเป็นการใช้ความเท่าเทียมกันและการเชื่อมแบบ "หรือ" สัจพจน์กล่าวว่า สำหรับเซตสองเซตใดๆและจะมีอย่างน้อยหนึ่งเซตซึ่งประกอบด้วยเซตทั้งสองนั้นอย่าง น้อยหนึ่งเซต${\displaystyle \{x,y\}\subset p}$${\displaystyle \forall z.(z=x\lor z=y)\to z\in p}$${\displaystyle x}$${\displaystyle y}$${\displaystyle p}$

ด้วยการแยกขอบเขตด้านล่าง คลาสนี้จึงมีอยู่จริงในฐานะเซต กำหนดให้เป็นแบบจำลองคู่ลำดับมาตรฐานดังนั้น เช่น จึงหมายถึงสูตรที่มีขอบเขตอีกสูตรหนึ่งในภาษาเชิงทฤษฎีอย่างเป็นทางการ ${\displaystyle \{x,y\}}$${\displaystyle \langle x,y\rangle }$${\displaystyle \{\{x\},\{x,y\}\}}$${\displaystyle q=\langle x,y\rangle }$

จากนั้น โดยใช้การระบุปริมาณเชิงการมีอยู่และการเชื่อมโยง

กล่าวคือ สำหรับเซตใดๆ ก็ตามจะมีอย่างน้อยหนึ่งเซตที่ประกอบด้วยสมาชิกทั้งหมดของเซตนั้นเซตที่เล็กที่สุดดังกล่าวคือยูเนียน ของเซต นั้น ${\displaystyle x}$${\displaystyle u}$${\displaystyle z}$${\displaystyle x}$${\displaystyle y}$

โดยทั่วไปแล้ว สัจพจน์ทั้งสองมักถูกกำหนดให้เข้มงวดมากขึ้น โดยใช้ " " แทนที่จะเป็นเพียง " " แม้ว่าในทางเทคนิคแล้วจะซ้ำซ้อนในบริบทของ: เนื่องจากสัจพจน์การแยกด้านล่างถูกกำหนดด้วย " " ดังนั้นสำหรับข้อความต่างๆความเท่าเทียมกันสามารถอนุมานได้ โดยที่ทฤษฎีอนุญาตให้แยกโดยใช้ในกรณีที่เป็นข้อความแสดงการมีอยู่ เช่นในสัจพจน์การรวมกันนี้ ยังมีการกำหนดรูปแบบอื่นโดยใช้ตัวบ่งปริมาณสากล อีกด้วย${\displaystyle \leftrightarrow }$${\displaystyle \to }$${\displaystyle {\mathsf {BCST}}}$${\displaystyle \leftrightarrow }$${\displaystyle \exists t.\forall z.\phi (z)\to z\in t}$${\displaystyle \phi }$${\displaystyle \phi }$

นอกจากนี้ การใช้การแยกขอบเขต (bounded Separation) สัจพจน์ทั้งสองที่กล่าวมาข้างต้นรวมกันบ่งบอกถึงการมีอยู่ของการรวมกันแบบไบนารีของสองคลาสและเมื่อคลาสเหล่านั้นได้รับการพิสูจน์แล้วว่าเป็นเซต ซึ่งแทนด้วยหรือ สำหรับ เซตที่กำหนดไว้เพื่อตรวจสอบการเป็นสมาชิกในการรวมกันของสองเซตที่กำหนดและจำเป็นต้องตรวจสอบส่วนหนึ่งของสัจพจน์ ซึ่งสามารถทำได้โดยการตรวจสอบการเชื่อมโยงแบบเลือก (disjunction) ของตัวบ่งชี้ที่กำหนดเซตและสำหรับในแง่ของเซตที่เกี่ยวข้อง จะทำได้โดยการตรวจสอบการเชื่อมโยงแบบเลือก (disjunction ) ${\displaystyle a}$${\displaystyle b}$${\displaystyle \bigcup \{a,b\}}$${\displaystyle a\cup b}$${\displaystyle z}$${\displaystyle z\in a\cup b}$${\displaystyle y=a}$${\displaystyle y=b}$${\displaystyle z\in y}$${\displaystyle a}$${\displaystyle b}$${\displaystyle z}$${\displaystyle z\in a\lor z\in b}$

สัญลักษณ์การรวมและสัญลักษณ์การสร้างเซตอื่นๆ ยังใช้สำหรับคลาสด้วย ตัวอย่างเช่น ประโยคเสนอเขียนได้ว่า ให้ ตอนนี้ เมื่อกำหนดความสามารถในการตัดสินใจของการเป็นสมาชิกใน กล่าวคือ ข้อความที่อาจเป็นอิสระสามารถแสดงได้เป็นแต่เช่นเดียวกับข้อความตรงกลางที่ถูกยกเว้นใดๆ การปฏิเสธซ้ำซ้อนของข้อความหลังนั้นเป็นจริง: การรวมนั้นไม่ได้ถูกครอบครองโดยสิ่งนี้แสดงให้เห็นว่าการแบ่งส่วนเป็นแนวคิดที่ซับซ้อนกว่านั้นในเชิงสร้างสรรค์ด้วย ${\displaystyle z\in A\land z\notin C}$${\displaystyle z\in A\setminus C}$${\displaystyle B\subset A}$${\displaystyle z\in A}$${\displaystyle B}$${\displaystyle z\in B\lor z\notin B}$${\displaystyle z\in B\cup (A\setminus B)}$${\displaystyle z}$

คุณสมบัติที่เป็นเท็จสำหรับเซตใดๆ สอดคล้องกับ ชั้น ว่างซึ่งแสดงด้วยหรือศูนย์ การที่ชั้นว่างเป็นเซตนั้นสามารถอนุมานได้ง่ายจากสัจพจน์การมีอยู่ของสิ่งอื่นๆ เช่น สัจพจน์อนันต์ด้านล่าง แต่ถ้าหากเราสนใจที่จะไม่รวมเซตอนันต์ในการศึกษาของเราอย่างชัดเจน เราอาจใช้ ณ จุดนี้ ${\displaystyle \{\}}$${\displaystyle 0}$

การนำสัญลักษณ์(เพื่อใช้เป็นสัญลักษณ์ย่อสำหรับนิพจน์ที่เกี่ยวข้องกับคุณสมบัติเฉพาะ) มาใช้ถือว่าสมเหตุสมผล เนื่องจากสามารถพิสูจน์ได้ว่าเซตนี้มีเพียงหนึ่งเดียว เนื่องจากเป็นเท็จสำหรับทุก ๆ ดังนั้น สัจพจน์จึงเป็นดังนี้ ${\displaystyle \{\}}$${\displaystyle y\in \{\}}$${\displaystyle y}$${\displaystyle \exists x.x\simeq \{\}}$

ทฤษฎีย่อยของไม่มีองค์ประกอบพื้นฐาน (urelement)กล่าวคือ อะตอมที่แยกแยะได้ซึ่งสามารถเป็นสมาชิกของเซตได้ แต่ก็ไม่มีสมาชิกใดๆ อยู่ในตัวมันเองด้วย ในทฤษฎีเซตที่มีองค์ประกอบพื้นฐาน ความเท่าเทียมกันไม่ได้เทียบเท่ากับ อย่างง่ายๆดังที่ระบุไว้ในสัจพจน์ความขยายข้างต้น ${\displaystyle {\mathsf {ZF}}}$${\displaystyle x=y}$${\displaystyle x\simeq y}$

เขียนแทนซึ่งเท่ากับนั่นคือในทำนองเดียวกัน เขียนแทนซึ่งเท่ากับนั่นคือดังนั้น ข้อเสนอที่เรียบง่ายและพิสูจน์แล้วว่าผิดก็คือ ตัวอย่างเช่น ซึ่งสอดคล้องกับในแบบจำลองเลขคณิตมาตรฐาน อีกครั้ง ในที่นี้ สัญลักษณ์เช่นถูกมองว่าเป็นสัญลักษณ์ที่สะดวก และข้อเสนอใดๆ ก็ตามจะถูกแปลงเป็นนิพจน์โดยใช้เพียง " " และสัญลักษณ์เชิงตรรกะ รวมถึงตัวบ่งปริมาณ พร้อมกับการวิเคราะห์เชิงอภิคณิตศาสตร์ที่แสดงให้เห็นว่าความสามารถของทฤษฎีใหม่นั้นเทียบเท่ากันอย่างมีประสิทธิภาพการขยายอย่างเป็นทางการโดยใช้สัญลักษณ์เช่น ก็อาจได้รับการพิจารณาเช่นกัน ${\displaystyle 1}$${\displaystyle S0}$${\displaystyle \{\{\}\}}$${\displaystyle \{0\}}$${\displaystyle 2}$${\displaystyle S1}$${\displaystyle \{\{\},\{\{\}\}\}}$${\displaystyle \{0,1\}}$${\displaystyle \{\}\in \{\}}$${\displaystyle 0<0}$${\displaystyle \{\}}$${\displaystyle \in }$${\displaystyle 0}$

โดยทั่วไปแล้ว สำหรับเซตหนึ่งให้กำหนดเซตผู้สืบทอดเป็นการทำงานร่วมกันของการดำเนินการผู้สืบทอดกับความสัมพันธ์การเป็นสมาชิกมีข้อความเวียนเกิด ในแง่ที่ว่าโดยสมบัติการสะท้อนกลับของความเท่าเทียมกันและโดยเฉพาะอย่างยิ่งจะมีสมาชิกอยู่เสมอ ${\displaystyle x}$${\displaystyle Sx}$${\displaystyle x\cup \{x\}}$${\displaystyle (y\in Sx)\leftrightarrow (y\in x\lor y=x)}$${\displaystyle x\in Sx}$${\displaystyle Sx}$

ต่อไปนี้เป็นการใช้แบบแผนสัจพจน์ กล่าวคือ สัจพจน์สำหรับชุดของ述语บางชุด แบบแผนสัจพจน์บางส่วนที่กล่าวถึงจะอนุญาตให้มีชุดของพารามิเตอร์ใดๆ ก็ได้ (หมายถึงตัวแปรที่มีชื่อเฉพาะใดๆ ก็ได้) กล่าวคือ อนุญาตให้มีการสร้างอินสแตนซ์ของแบบแผนซึ่ง述语 (บางอย่างโดยเฉพาะ) ขึ้นอยู่กับตัวแปรชุดเพิ่มเติมจำนวนหนึ่ง และข้อความของสัจพจน์นั้นเข้าใจได้ด้วยการปิดแบบสากลภายนอกเพิ่มเติมที่สอดคล้องกัน (เช่นใน) ${\displaystyle v_{0},v_{1},\dots ,v_{n}}$${\displaystyle \phi }$${\displaystyle \forall v_{0}.\forall v_{1}.\cdots \forall v_{n}.}$

ทฤษฎีเซตเชิงสร้างสรรค์พื้นฐานประกอบด้วยสัจพจน์หลายข้อซึ่งเป็นส่วนหนึ่งของทฤษฎีเซตมาตรฐานเช่นกัน ยกเว้น สัจพจน์ การแยกแบบ "สมบูรณ์" ที่ถูกลดทอนลง นอกจากสัจพจน์ทั้งสี่ข้างต้นแล้ว ยังตั้งสมมติฐานเกี่ยวกับการแยกเชิงทำนาย (Predicative Separation) และแบบแผนการแทนที่ (Replacement schema) ด้วย ${\displaystyle {\mathsf {BCST}}}$

สัจพจน์นี้เทียบเท่ากับการตั้งสมมติฐานเกี่ยวกับการมีอยู่ของเซตที่ได้จากการตัดกันของเซตใดๆกับคลาสใดๆ ที่อธิบายด้วยคุณลักษณะสำหรับเซตใดๆที่พิสูจน์แล้วว่าเป็นเซต เมื่อคุณลักษณะถูกกำหนดเป็นเราจะได้การตัดกันแบบไบนารีของเซตและเขียนได้ว่าการตัดกันสอดคล้องกับการเชื่อมโยงในลักษณะที่คล้ายคลึงกับที่การรวมกันสอดคล้องกับการแยกออกจากกัน ${\displaystyle s}$${\displaystyle y}$${\displaystyle \{x\mid \phi (x)\}}$${\displaystyle z}$${\displaystyle \phi (x):=x\in z}$${\displaystyle s=y\cap z}$

เมื่อพิจารณาภาคแสดงเป็นการปฏิเสธจะได้หลักการความแตกต่าง ซึ่งรับรองการมีอยู่ของเซตใดๆ โปรดสังเกตว่าเซตเช่นหรือนั้นว่างเปล่าเสมอ ดังนั้น ดังที่กล่าวไว้ จากการแยกและการมีอยู่ของเซตอย่างน้อยหนึ่งเซต (เช่น อนันต์ด้านล่าง) จะนำไปสู่การมีอยู่ของเซตว่าง(หรือเขียนแทนด้วย) ภายในบริบทแบบอนุรักษ์นิยมนี้แผนผังการแยกเชิงภาคแสดงนั้นเทียบเท่ากับเซตว่างบวกกับการมีอยู่ของจุดตัดทวิภาคสำหรับเซตสองเซตใดๆ รูปแบบหลังของการกำหนดสัจพจน์ไม่ได้ใช้แผนผังสูตร ${\displaystyle \phi (x):=x\notin z}$${\displaystyle y\setminus z}$${\displaystyle y\setminus y}$${\displaystyle \{x\in y\mid \neg (x=x)\}}$${\displaystyle \{\}}$${\displaystyle 0}$${\displaystyle {\mathsf {BCST}}}$

การแยกเชิงทำนายเป็นแผนผังที่คำนึงถึงลักษณะทางไวยากรณ์ของตัวบ่งชี้ที่กำหนดเซต จนถึงความเท่าเทียมกันที่พิสูจน์ได้ สูตรที่อนุญาตจะถูกแสดงด้วย ซึ่งเป็นระดับต่ำสุดในลำดับชั้น Lévy ทางทฤษฎี เซต^{[ 13 ]} ตัวบ่งชี้ทั่วไปในทฤษฎีเซตไม่เคยถูกจำกัดทางไวยากรณ์ในลักษณะดังกล่าว ดังนั้นในทางปฏิบัติ คลาสย่อยทั่วไปของเซตจึงยังคงเป็นส่วนหนึ่งของภาษาคณิตศาสตร์ เนื่องจากขอบเขตของคลาสย่อยที่เป็นเซตที่พิสูจน์ได้นั้นมีความอ่อนไหวต่อเซตที่มีอยู่แล้ว ขอบเขตนี้จึงขยายออกไปเมื่อมีการเพิ่มสมมติฐานการมีอยู่ของเซตเพิ่มเติม ${\displaystyle \Delta _{0}}$

คลาสที่มีสมาชิกอย่างมากที่สุดหนึ่งตัวเรียกว่าซับซิงเกิลตัน สำหรับประพจน์แนวคิดที่เกิดขึ้นซ้ำๆ ในการวิเคราะห์เชิงสร้างสรรค์ของทฤษฎีเซตคือการมองภาคแสดงเป็นซับซิงเกิลตันซึ่งเป็นคลาสย่อยของลำดับที่สองถ้าพิสูจน์ได้ว่าหรือหรือแล้วจะมีสมาชิกอยู่ หรือว่างเปล่า (ไม่มีสมาชิก) หรือไม่ว่างเปล่า (ไม่มีสมาชิก) ตามลำดับ เห็นได้ชัดว่าเทียบเท่ากับประพจน์และ เช่นกันในทำนองเดียวกันเทียบเท่ากับและเทียบเท่ากับ ดังนั้นในที่นี้การที่แยกออกจาก ได้อย่างแม่นยำหมายความ ว่า ในแบบจำลองของจำนวนธรรมชาติ ถ้าเป็นจำนวนยังแสดงว่าเล็กกว่าการรวมกันที่เป็นส่วนหนึ่งของคำจำกัดความของการดำเนินการสืบทอดข้างต้นสามารถใช้เพื่อแสดงข้อความตรงกลางที่ถูกยกเว้นเป็น กล่าวคือสามารถตัดสินได้ก็ต่อเมื่อผู้สืบทอดของ มีค่ามากกว่าลำดับที่เล็กที่สุด ข้อเสนอแนะนี้ จะได้รับการตัดสินในทางใดทางหนึ่งโดยการกำหนด ว่ามีขนาดเล็กกว่า อย่างไร : โดยการมีขนาดเล็กกว่าอยู่แล้วหรือโดยการเป็นผู้มาก่อนโดยตรงของ อีกวิธีหนึ่งในการแสดงถึงส่วนกลางที่ถูกยกเว้นสำหรับคือการมีอยู่ของสมาชิกจำนวนน้อยที่สุดของคลาสที่มีสมาชิกอาศัยอยู่ ${\displaystyle P}$${\displaystyle x=0\land P}$${\displaystyle B:=\{x\in 1\mid P\}}$${\displaystyle 1:=S0=\{0\}}$${\displaystyle P}$${\displaystyle \neg P}$${\displaystyle \neg \neg P}$${\displaystyle B}$${\displaystyle P}$${\displaystyle 0\in B}$${\displaystyle B=1}$${\displaystyle \neg P}$${\displaystyle B=0}$${\displaystyle \neg (0\in B)}$${\displaystyle B}$${\displaystyle 1}$${\displaystyle P\lor \neg P}$${\displaystyle B}$${\displaystyle 0\in B}$${\displaystyle 0}$${\displaystyle B}$${\displaystyle 0\in SB}$${\displaystyle P}$${\displaystyle B}$${\displaystyle 0}$${\displaystyle P}$${\displaystyle 0}$${\displaystyle 0}$${\displaystyle B}$${\displaystyle 0}$${\displaystyle SB}$${\displaystyle P}$${\displaystyle b:=B\cup \{1\}}$

ถ้าสัจพจน์การแยกอนุญาตให้แยกได้ด้วยแล้ว จะเป็นเซตย่อยซึ่งอาจเรียกว่าค่าความจริงที่เกี่ยวข้องกับ ค่า ความจริงสองค่าสามารถพิสูจน์ได้ว่าเท่ากันในฐานะเซต โดยการพิสูจน์ความสมมูล ในแง่ของศัพท์เฉพาะนี้ ชุดของค่าการพิสูจน์สามารถเข้าใจได้ล่วงหน้าว่ามีความหลากหลาย ไม่น่าแปลกใจที่ประพจน์ที่ตัดสินได้จะมีค่าความจริงหนึ่งในเซตไบนารี การแยกแบบตรงกลางที่ถูกยกเว้นสำหรับ นั้นก็ถูกบ่งชี้โดยนัยจากข้อความโดยรวมด้วย ${\displaystyle P}$${\displaystyle B}$${\displaystyle P}$${\displaystyle P}$${\displaystyle \forall b.(0\in b)\lor (0\notin b)}$

เมื่อใช้คำศัพท์ที่ไม่เป็นทางการเกี่ยวกับกลุ่ม เซตใดๆ ก็ถือว่าเป็นกลุ่มเช่นกัน ในขณะเดียวกัน ก็มีสิ่งที่เรียกว่า กลุ่ม ที่แท้จริงซึ่งไม่สามารถขยายไปเป็นเซตได้ เมื่อในทฤษฎีมีการพิสูจน์ว่าแล้ว ก็ต้องเป็นกลุ่มที่แท้จริงด้วย (เมื่อพิจารณาจากมุมมองของเซต ซึ่งเป็นทฤษฎีที่มีการแยกอย่างสมบูรณ์ กลุ่มที่แท้จริงโดยทั่วไปมักถูกมองว่าเป็นกลุ่มที่มีขนาด "ใหญ่เกินไป" ที่จะเป็นเซต ในทางเทคนิคแล้ว พวกมันเป็นคลาสย่อยของลำดับชั้นสะสมที่ขยายออกไปเกินขอบเขตเชิงลำดับใดๆ) ${\displaystyle \neg \exists x.A\subset x}$${\displaystyle A}$${\displaystyle {\mathsf {ZF}}}$

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

ข้อความต่อไปนี้ใช้ได้กับความสัมพันธ์ใดๆ ก็ตามมันให้เงื่อนไขเชิงตรรกะล้วนๆ ที่ว่า สองพจน์และไม่สามารถมีความสัมพันธ์กันได้ ${\displaystyle E}$${\displaystyle s}$${\displaystyle y}$${\displaystyle E}$

${\displaystyle {\big (}\forall x.xEs\leftrightarrow (xEy\land \neg xEx){\big )}\to \neg (yEs\lor sEs\lor sEy)}$

สิ่งที่สำคัญที่สุดในที่นี้คือการปฏิเสธส่วนแยกสุดท้าย. นิพจน์นี้ไม่เกี่ยวข้องกับการกำหนดปริมาณแบบไม่จำกัด และจึงได้รับอนุญาตในทฤษฎีการแยกการสร้างของรัสเซลแสดงให้เห็นว่า. ดังนั้นสำหรับเซตใดๆการแยกเชิงทำนายเพียงอย่างเดียวบ่งชี้ว่ามีเซต ซึ่งไม่ใช่สมาชิกของ. โดยเฉพาะอย่างยิ่ง ไม่มีเซตสากลใดๆที่สามารถมีอยู่ได้ในทฤษฎีนี้ ${\displaystyle \neg sEy}$${\displaystyle \neg (x\in x)}$${\displaystyle \{x\in y\mid x\notin x\}\notin y}$${\displaystyle y}$${\displaystyle y}$

ในทฤษฎีที่นำเอาสัจพจน์ของความสม่ำเสมอ มาใช้เพิ่มเติม เช่นพิสูจน์ได้ว่าไม่จริงสำหรับเซตใดๆดังนั้นจึงหมายความว่าเซตย่อยเท่ากับตัวมันเอง และคลาสคือเซตว่าง ${\displaystyle {\mathsf {ZF}}}$${\displaystyle x\in x}$${\displaystyle x}$${\displaystyle \{x\in y\mid x\notin x\}}$${\displaystyle y}$${\displaystyle \{x\mid x\in x\}}$

สำหรับค่าใดๆ ของและกรณีพิเศษในสูตรข้างต้นจะให้ผลลัพธ์ดังนี้ ${\displaystyle E}$${\displaystyle y}$${\displaystyle s=y}$

${\displaystyle \neg {\big (}\forall x.xEy\leftrightarrow \neg xEx{\big )}}$

สิ่งนี้หมายความอยู่แล้วว่าไม่มีเซตใดเท่ากับซับคลาสของคลาสสากล กล่าวคือ ซับคลาสนั้นเป็นซับคลาสที่แท้จริงด้วย แต่ถึงแม้จะไม่มีความสม่ำเสมอ ก็ยังสอดคล้องที่จะมีคลาสที่แท้จริงของสมาชิกเอกพจน์ซึ่งแต่ละสมาชิกนั้นประกอบด้วยตัวมันเองอย่างสมบูรณ์ ${\displaystyle y}$${\displaystyle \{x\mid x\notin x\}}$${\displaystyle {\mathsf {ZF}}}$

อนึ่ง ในทฤษฎีที่มีการแบ่งชั้นอย่างเช่นIntuitionistic New Foundationsนั้น การแสดงออกทางไวยากรณ์อาจไม่ได้รับอนุญาตในเรื่องการแยกส่วน ดังนั้น การพิสูจน์การปฏิเสธการมีอยู่ของเซตสากลข้างต้นจึงไม่สามารถทำได้ในทฤษฎีนั้น ${\displaystyle x\in x}$

โครงสร้างสัจพจน์ของการแยกเชิงทำนาย (Predicative Separation) เรียกอีกอย่างว่าการแยก (Separation) หรือ การแยกแบบมีขอบเขต (Bounded Separation) เช่น การแยกสำหรับตัวบ่งปริมาณที่มีขอบเขต ของเซต เท่านั้น (หมายเหตุเตือน: ระบบการตั้งชื่อลำดับชั้นของ Lévy นั้นคล้ายคลึงกับ ลำดับชั้น ทางคณิตศาสตร์แม้ว่าการเปรียบเทียบอาจมีความละเอียดอ่อน: การจัดประเภททางคณิตศาสตร์บางครั้งไม่ได้แสดงออกมาในเชิงไวยากรณ์ แต่แสดงออกมาในแง่ของกลุ่มย่อยของจำนวนธรรมชาติ นอกจากนี้ ระดับล่างสุดของลำดับชั้นทางคณิตศาสตร์มีคำจำกัดความทั่วไปหลายอย่าง ซึ่งบางอย่างไม่อนุญาตให้ใช้ฟังก์ชันทั้งหมดบางอย่าง ความแตกต่างที่คล้ายกันนี้ไม่เกี่ยวข้องในระดับที่สูงกว่า สุดท้ายนี้ โปรดทราบว่าการจัดประเภทของสูตรอาจแสดงออกมาได้ถึงความเท่าเทียมกันในทฤษฎี) ${\displaystyle \Delta _{0}}$${\displaystyle \Delta _{0}^{0}}$${\displaystyle \Sigma _{1}^{0}}$${\displaystyle \Delta _{0}}$

โครงสร้างดังกล่าวเป็นวิธีการที่Mac Lane ใช้ใน การลดทอนระบบที่ใกล้เคียงกับทฤษฎีเซตของ Zermelo สำหรับรากฐานทางคณิตศาสตร์ที่เกี่ยวข้องกับทฤษฎีโทโพสนอกจากนี้ยังใช้ในการศึกษาเรื่องความแน่นอนและเป็นส่วนหนึ่งของการกำหนดทฤษฎีเซตของ Kripke-Platekด้วย ${\displaystyle {\mathsf {Z}}}$

ข้อจำกัดในสัจพจน์ยังทำหน้าที่เป็นผู้เฝ้ารักษา คำจำกัดความ ที่ไม่สามารถระบุได้อย่างชัดเจน กล่าวคือ ไม่ควรกล่าวอ้างถึงการมีอยู่ของวัตถุที่ไม่สามารถอธิบายได้อย่างชัดเจน หรือวัตถุที่มีคำจำกัดความเกี่ยวข้องกับตัวมันเองหรือการอ้างอิงถึงคลาสที่เหมาะสม เช่น เมื่อคุณสมบัติที่จะตรวจสอบเกี่ยวข้องกับตัวบ่งปริมาณสากล ดังนั้นในทฤษฎีเชิงสร้างสรรค์ที่ไม่มีสัจพจน์ของเซตกำลังเมื่อหมายถึงภาคแสดง 2-ary บางอย่าง โดยทั่วไปแล้วไม่ควรคาดหวังว่าคลาสย่อยของจะเป็นเซต ในกรณีที่มันถูกกำหนดไว้ เช่น ใน ${\displaystyle R}$${\displaystyle s}$${\displaystyle y}$

${\displaystyle \{x\in y\mid \forall t.{\big (}(t\subset y)\to R(x,t){\big )}\}}$,

หรือผ่านคำจำกัดความที่คล้ายกันซึ่งเกี่ยวข้องกับการหาปริมาณเหนือเซตต่างๆโปรดทราบว่าหากคลาสย่อยนี้ได้รับการพิสูจน์แล้วว่าเป็นเซต เซตย่อยนี้เองก็จะอยู่ในขอบเขตที่ไม่จำกัดของตัวแปรเซตด้วยกล่าวอีกนัยหนึ่ง เนื่องจากคุณสมบัติของคลาสย่อยนั้นเป็นไปตามเงื่อนไข เซตที่แน่นอนนี้ซึ่งกำหนดโดยใช้การแสดงออกจะมีบทบาทในการกำหนดลักษณะเฉพาะของตัวมันเอง ${\displaystyle t\subset y}$${\displaystyle s}$${\displaystyle y}$${\displaystyle t}$${\displaystyle s\subset y}$${\displaystyle s}$${\displaystyle R(x,s)}$

แม้ว่าการแยกเชิงทำนายจะนำไปสู่จำนวนนิยามของคลาสที่กำหนดให้เป็นเซตที่น้อยลง แต่ก็ควรเน้นย้ำว่านิยามของคลาสจำนวนมากที่เทียบเท่ากันในเชิงคลาสสิกนั้นไม่เทียบเท่ากันเมื่อจำกัดตัวเองอยู่กับตรรกะที่อ่อนกว่า เนื่องจากความไม่สามารถตัดสินได้ของภาคแสดงทั่วไป แนวคิดของเซตย่อยและคลาสย่อยจึงมีความซับซ้อนมากขึ้นโดยอัตโนมัติในทฤษฎีเซตเชิงสร้างสรรค์มากกว่าในทฤษฎีคลาสสิก ดังนั้นด้วยวิธีนี้จึงได้ทฤษฎีที่กว้างขึ้น สิ่งนี้ยังคงเป็นจริงหากใช้การแยกอย่างสมบูรณ์ เช่นในทฤษฎีซึ่งอย่างไรก็ตามทำให้คุณสมบัติการมีอยู่และการตีความเชิงทฤษฎีประเภทมาตรฐานเสียไป และด้วยวิธีนี้จึงทำให้มุมมองจากล่างขึ้นบนของเซตเชิงสร้างสรรค์เสียไป นอกจากนี้ เนื่องจากsubtypingไม่ใช่คุณสมบัติที่จำเป็นของทฤษฎีประเภทเชิงสร้างสรรค์จึงกล่าวได้ว่าทฤษฎีเซตเชิงสร้างสรรค์แตกต่างจากกรอบงานนั้นมาก ${\displaystyle {\mathsf {IZF}}}$

ต่อไปให้พิจารณา

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

โดยผ่านการแทนที่ การมีอยู่ของคู่ใดๆก็ตามย่อมเป็นผลมาจากการมีอยู่ของคู่อื่นๆ ที่เฉพาะเจาะจงเช่นกัน เช่นแต่เนื่องจากการรวมแบบไบนารีที่ใช้ในได้ใช้สัจพจน์การจับคู่ไปแล้ว วิธีการนี้จึงจำเป็นต้องตั้งสมมติฐานการมีอยู่ของมากกว่า การมีอยู่ ของ ในทฤษฎีที่มีสัจพจน์เซตกำลังที่ไม่สามารถทำนายได้ การมีอยู่ของก็สามารถพิสูจน์ได้โดยใช้การแยก ${\displaystyle \{x,y\}}$${\displaystyle \{0,1\}=2=SS0}$${\displaystyle S}$${\displaystyle 2}$${\displaystyle 0}$${\displaystyle 2\subset {\mathcal {P}}{\mathcal {P}}0}$

ด้วยแผนผังการแทนที่ ทฤษฎีที่กล่าวมาข้างต้นพิสูจน์ได้ว่าชั้นสมมูลหรือผลรวมดัชนีเป็นเซต โดยเฉพาะอย่างยิ่งผลคูณคาร์ทีเซียนซึ่งเก็บคู่ขององค์ประกอบทั้งหมดของสองเซต เป็นเซต ในทางกลับกัน สำหรับจำนวนคงที่ใดๆ (ในอภิทฤษฎี) นิพจน์ผลคูณที่สอดคล้องกัน เช่นสามารถสร้างเป็นเซตได้ ข้อกำหนดเชิงสัจพจน์สำหรับเซตที่กำหนดแบบเวียนซ้ำในภาษาจะกล่าวถึงเพิ่มเติมด้านล่าง เซตเป็นเซตแบบไม่ต่อเนื่อง กล่าวคือ ความเท่าเทียมกันขององค์ประกอบภายในเซตสามารถตัดสินได้ หากความสัมพันธ์ที่สอดคล้องกันในฐานะเซตย่อยของสามารถตัดสินได้ ${\displaystyle x\times x\times x\times x}$${\displaystyle x}$${\displaystyle x}$${\displaystyle x\times x}$

การแทนที่มีความเกี่ยวข้องกับการทำความเข้าใจฟังก์ชันและสามารถมองได้ว่าเป็นรูปแบบหนึ่งของการทำความเข้าใจโดยทั่วไปเฉพาะเมื่อมีการสมมติ เท่านั้น การแทนที่จึงจะหมายถึงการแยกอย่างสมบูรณ์ ในกรณีนี้การแทนที่มีความสำคัญอย่างยิ่งในการพิสูจน์การมีอยู่ของเซตที่มีอันดับ สูง กล่าวคือ ผ่านตัวอย่างของแบบแผนสัจพจน์ที่เชื่อมโยงเซตขนาดเล็กกับเซตขนาดใหญ่ ${\displaystyle {\mathrm {PEM} }}$${\displaystyle {\mathsf {ZF}}}$${\displaystyle \phi (x,y)}$${\displaystyle x}$${\displaystyle y}$

ทฤษฎีเซตเชิงสร้างสรรค์มักมีโครงร่างสัจพจน์แบบการแทนที่ ซึ่งบางครั้งอาจจำกัดอยู่เฉพาะสูตรที่มีขอบเขต อย่างไรก็ตาม เมื่อมีการละทิ้งสัจพจน์อื่นๆ โครงร่างนี้มักจะได้รับการเสริมความแข็งแกร่งขึ้น ไม่ใช่เกินกว่า แต่เพียงเพื่อเรียกความแข็งแกร่งในการพิสูจน์กลับคืนมา สัจพจน์ที่แข็งแกร่งกว่านั้นก็มีอยู่เช่นกัน ซึ่งจะไม่ทำลาย คุณสมบัติการมีอยู่จริงที่แข็งแกร่งของทฤษฎี ดังที่จะกล่าวถึงต่อไป ${\displaystyle {\mathsf {ZF}}}$

ถ้าพิสูจน์ได้ว่า เป็นฟังก์ชันบนและมีโคโดเมน(ซึ่งจะกล่าวถึงโดยละเอียดด้านล่าง) แล้วภาพของจะเป็นเซตย่อยของในแนวทางอื่นๆ เกี่ยวกับแนวคิดของเซต แนวคิดของเซตย่อยจะถูกกำหนดในแง่ของ "การดำเนินการ" ในลักษณะนี้ ${\displaystyle i_{X}}$${\displaystyle X}$${\displaystyle Y}$${\displaystyle i_{X}}$${\displaystyle Y}$

ส่วนประกอบของเซตจำกัดที่สืบทอดได้นั้น สามารถนำไปใช้ในภาษาโปรแกรมทั่วไปใดๆ ก็ได้ สัจพจน์ที่กล่าวถึงข้างต้นนั้นเป็นนามธรรมจากการดำเนินการทั่วไปบนชนิดข้อมูลเซต : การจับคู่และการรวมเกี่ยวข้องกับการซ้อนและการทำให้แบนราบหรือเมื่อรวมกันก็คือการเชื่อมต่อ การแทนที่เกี่ยวข้องกับการทำความเข้าใจและการแยกเกี่ยวข้องกับการกรอง ซึ่งมักจะง่ายกว่า การแทนที่ร่วมกับการเหนี่ยวนำเซต (ที่จะกล่าวถึงต่อไป) เพียงพอที่จะสร้างสัจพจน์ได้อย่างสร้างสรรค์ และทฤษฎีนั้นก็ได้รับการศึกษาโดยไม่ต้องใช้ค่าอนันต์ด้วย ${\displaystyle H_{\aleph _{0}}}$${\displaystyle H_{\aleph _{0}}}$

การผสมผสานระหว่างการจับคู่และการรวมกัน สัจพจน์ที่เกี่ยวข้องกับผู้สืบทอดได้ง่ายกว่าคือสัจพจน์ของการเชื่อมโยง [ ^{14 ] [ 15 ] หลักการ}ดังกล่าวมีความเกี่ยวข้องกับการสร้างแบบจำลองมาตรฐานของลำดับ Neumann แต่ละ รายการ นอกจากนี้ยังมีสูตรสัจพจน์ที่จับคู่การรวมและการแทนที่เข้าด้วยกัน แม้ว่าการตั้งสมมติฐานการแทนที่จะไม่ใช่สิ่งจำเป็นในการออกแบบทฤษฎีเซตเชิงสร้างสรรค์ที่อ่อนแอซึ่งสามารถตีความได้สองทางด้วยเลขคณิต Heyting แต่การเหนี่ยวนำบางรูปแบบนั้นจำเป็น เพื่อเปรียบเทียบ ลองพิจารณาทฤษฎีคลาสสิกที่อ่อนแอมากที่เรียกว่าทฤษฎีเซตทั่วไปซึ่งตีความคลาสของจำนวนธรรมชาติและเลขคณิตของพวกมันผ่านเพียงแค่การขยาย การเชื่อมโยง และการแยกอย่างสมบูรณ์ ${\displaystyle {\mathsf {HA}}}$

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

สำหรับเงื่อนไขคงที่และเซตหนึ่งข้อความนี้แสดงว่าเป็นเซตที่เล็กที่สุด (ในความหมายของ " ") ในบรรดาเซตทั้งหมดที่เงื่อนไขดังกล่าวเป็นจริง และเป็นเซตย่อยของ เสมอ จุดมุ่งหมายของสัจพจน์อนันต์คือการได้มา ซึ่ง เซตอุปนัยที่เล็กที่สุดเพียงหนึ่งเดียวในที่สุด${\displaystyle I}$${\displaystyle a}$${\displaystyle I(a)\land {\big (}\forall y.I(y)\to a\subset y{\big )}}$${\displaystyle a}$${\displaystyle \subset }$${\displaystyle y}$${\displaystyle I(y)}$${\displaystyle y}$

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

${\displaystyle {\big (}\exists z.z\in A{\big )}\land \forall (x\in A).\exists (s\in A).x\in s}$.

กล่าวโดยละเอียด ให้แสดงด้วยคุณสมบัติอุปนัย ${\displaystyle \mathrm {Ind} _{A}}$

${\displaystyle (0\in A)\land \forall (x\in A).Sx\in A}$.

ในแง่ของ述语ที่อยู่เบื้องหลังคลาส ดังนั้น ซึ่งในภายหลังจะแปลเป็น ${\displaystyle Q}$${\displaystyle \forall x.(x\in A)\leftrightarrow Q(x)}$${\displaystyle Q(0)\land \forall x.{\big (}Q(x)\to Q(Sx){\big )}}$

เขียนสำหรับจุดตัดทั่วไป(อาจพิจารณารูปแบบอื่นของคำจำกัดความนี้ซึ่งต้องการแต่เราใช้แนวคิดนี้เฉพาะสำหรับคำจำกัดความเสริมต่อไปนี้เท่านั้น) ${\displaystyle \bigcap B}$${\displaystyle \{x\mid \forall (y\in B).x\in y\}}$${\displaystyle \cap B\subset \cup B}$

โดยทั่วไปแล้ว เราจะกำหนดคลาสซึ่งเป็นจุดตัดของเซตอุปนัยทั้งหมด (อาจมีการใช้สูตรที่ขึ้นอยู่กับพารามิเตอร์ของเซตเพื่อให้) คลาส นี้จะ ประกอบด้วยเซตทั้งหมดที่ตรง ตาม คุณสมบัติที่ไม่จำกัดขอบเขตจุดประสงค์คือ หากเซตอุปนัยมีอยู่จริง คลาสนี้จะมีจำนวนธรรมชาติร่วมกันกับเซตเหล่านั้น และจากนิยามของ " " จะบ่งชี้ว่าเป็นจริงสำหรับจำนวนธรรมชาติเหล่านี้แต่ละตัว แม้ว่าการแยกแบบมีขอบเขตจะไม่เพียงพอที่จะพิสูจน์ว่า เป็นเซตที่ต้องการ แต่ภาษาในที่นี้เป็นพื้นฐานสำหรับสัจพจน์ต่อไปนี้ ซึ่งรับรองการอุปนัยของจำนวนธรรมชาติสำหรับภาคแสดงที่ประกอบเป็นเซต ${\displaystyle \omega =\bigcap \{y\mid \mathrm {Ind} _{y}\}}$${\displaystyle w}$${\displaystyle \omega \subset w}$${\displaystyle \omega }$${\displaystyle x}$${\displaystyle \forall y.\mathrm {Ind} _{y}\to x\in y}$${\displaystyle \omega }$${\displaystyle \omega \subset A}$${\displaystyle \subset }$${\displaystyle Q}$${\displaystyle \omega }$

ทฤษฎีเซตเชิงสร้างสรรค์ขั้นพื้นฐานมีสัจพจน์และสมมติฐาน ${\displaystyle {\mathsf {ECST}}}$${\displaystyle {\mathsf {BCST}}}$

ต่อไป เราจะใช้สัญลักษณ์เพื่อแทนเซตอุปนัยที่เล็กที่สุดที่ไม่ซ้ำกันในปัจจุบัน ซึ่งเป็นลำดับฟอนนอยมันน์ ที่ไม่จำกัดขอบเขต เซตนี้ประกอบด้วยเซตว่าง และสำหรับแต่ละเซตใน จะมี อีกเซตหนึ่งในที่มีสมาชิกเพิ่มขึ้นอีกหนึ่งตัว ${\displaystyle \omega }$${\displaystyle \omega }$${\displaystyle \omega }$

สัญลักษณ์ที่เรียกว่าศูนย์และตัวสืบทอดอยู่ในลายเซ็นของทฤษฎีของPeanoในที่นี้ตัวสืบทอดที่กำหนดไว้ข้างต้นของจำนวนใดๆ ซึ่งอยู่ในคลาสเดียวกันนั้นเป็นผลโดยตรงจากการกำหนดลักษณะของจำนวนธรรมชาติโดยแบบจำลอง von Neumann ของเรา เนื่องจากตัวสืบทอดของเซตดังกล่าวมีตัวมันเองอยู่ด้วย จึงพบว่าไม่มีตัวสืบทอดใดเท่ากับศูนย์ ดังนั้น สองในสัจพจน์ของ Peanoเกี่ยวกับสัญลักษณ์ศูนย์และสัจพจน์เกี่ยวกับความปิดของ จึงได้มาอย่างง่ายดาย ประการที่สี่ ในที่ซึ่งเป็นเซตสามารถพิสูจน์ได้ว่า บน เป็นการดำเนินการแบบหนึ่ง ต่อ หนึ่ง${\displaystyle {\mathsf {BCST}}}$${\displaystyle \omega }$${\displaystyle S}$${\displaystyle {\mathsf {ECST}}}$${\displaystyle \omega }$${\displaystyle S}$${\displaystyle \omega }$

สำหรับเงื่อนไขบางประการของเซตข้อความที่กล่าวอ้างนั้นใช้ได้กับเซตย่อยทั้งหมดของเซตของจำนวนธรรมชาติ และสัจพจน์นี้พิสูจน์ได้ว่าเซตดังกล่าวมีอยู่จริง การกำหนดปริมาณเช่นนี้ยังสามารถทำได้ในเลขคณิต อันดับสอง ด้วย${\displaystyle P}$${\displaystyle \forall S.(S\subset \omega \to P(S))}$${\displaystyle P}$

ลำดับคู่ " " บนจำนวนธรรมชาติถูกจับโดยความสัมพันธ์การเป็นสมาชิก " " ทฤษฎีนี้พิสูจน์ว่าลำดับและความสัมพันธ์ความเท่าเทียมกันบนเซตนี้สามารถตัดสินได้ ไม่เพียงแต่ไม่มีจำนวนใดเล็กกว่าแต่การอุปมานยังบ่งชี้ว่าในบรรดาเซตย่อยของเซตว่างคือเซตที่ไม่มีสมาชิกที่เล็กที่สุด ข้อความแย้งของสิ่งนี้พิสูจน์การมีอยู่ของจำนวนที่เล็กที่สุด ที่ถูกปฏิเสธสองครั้ง สำหรับเซตย่อยที่ไม่ว่างทั้งหมดของหลักการที่ถูกต้องอีกประการหนึ่งซึ่งเทียบเท่ากับหลักการคลาสสิกคือการมีอยู่ของจำนวนที่เล็กที่สุดสำหรับเซตย่อยที่แยกได้ทั้งหมดที่มีสมาชิกอาศัยอยู่ กล่าวคือ การอ้างการมีอยู่ของเซตย่อยที่มีสมาชิกอาศัยอยู่ของเทียบเท่ากับการยกเว้นตรงกลางสำหรับและทฤษฎีเชิงสร้างสรรค์จึงจะไม่พิสูจน์ว่ามีลำดับที่ดี ${\displaystyle <}$${\displaystyle \in }$${\displaystyle 0}$${\displaystyle \omega }$${\displaystyle \omega }$${\displaystyle b:=\{z\in 1\mid P\}\cup \{1\}}$${\displaystyle \omega }$${\displaystyle P}$${\displaystyle \omega }$

หากต้องการแรงจูงใจ ความสะดวกในการตั้งสมมติฐานเกี่ยวกับเซตของจำนวนที่ไม่จำกัดในความสัมพันธ์กับคุณสมบัติเชิงอุปนัยอื่นๆ จะปรากฏชัดเจนในการอภิปรายเรื่องเลขคณิตในทฤษฎีเซตในส่วนถัดไป แต่ดังที่คุ้นเคยจากทฤษฎีเซตแบบคลาสสิก รูปแบบที่อ่อนแอของอนันต์ก็สามารถกำหนดได้เช่นกัน ตัวอย่างเช่น เราอาจตั้งสมมติฐานเกี่ยวกับการมีอยู่ของเซตเชิงอุปนัยบางอย่างซึ่งสมมติฐานการมีอยู่ดังกล่าวก็เพียงพอแล้ว เมื่อสามารถใช้การแยกอย่างสมบูรณ์เพื่อแยกเซตย่อยเชิงอุปนัยของจำนวนธรรมชาติ ซึ่งเป็นเซตย่อยร่วมของคลาสเชิงอุปนัยทั้งหมด หรืออาจใช้สมมติฐานการมีอยู่เฉพาะเจาะจงมากขึ้นก็ได้ ไม่ว่าจะด้วยวิธีใด เซตเชิงอุปนัยก็จะตรงตามคุณสมบัติการมีอยู่ก่อนหน้าต่อไปนี้ในความหมายของแบบจำลองของฟอน นอยมันน์ : ${\displaystyle \exists y.\mathrm {Ind} _{y}}$${\displaystyle w}$${\displaystyle \Delta _{0}}$

${\displaystyle \forall m.(m\in w)\leftrightarrow {\big (}m=0\lor \exists (p\in w).Sp=m{\big )}}$

หากไม่ใช้สัญลักษณ์สำหรับสัญลักษณ์ผู้สืบทอดที่กำหนดไว้ก่อนหน้านี้ ความเท่าเทียมกันเชิงขยายกับผู้สืบทอดจะถูกแสดงด้วยซึ่งแสดงว่าองค์ประกอบทั้งหมดเท่ากับหรือมีเซตผู้สืบทอดซึ่งมีสมาชิกอื่น ๆ ร่วมกันกับ ${\displaystyle Sp=m}$${\displaystyle \forall n.(n\in m)\leftrightarrow (n=p\lor n\in p)}$${\displaystyle m}$${\displaystyle 0}$${\displaystyle p\in w}$${\displaystyle m}$

สังเกตว่าจากนิพจน์ " " ทางด้านขวามือ คุณสมบัติที่บ่งบอกลักษณะเฉพาะของสมาชิกในที่นี้ทางไวยากรณ์นั้นประกอบด้วยสัญลักษณ์นั้นเอง เนื่องจากลักษณะจากล่างขึ้นบนของจำนวนธรรมชาติ สิ่งนี้จึงไม่รุนแรงในที่นี้ สมมติว่ามีการอุปนัยเซตบนไม่มีเซตสองเซตใดที่มีคุณสมบัตินี้ นอกจากนี้ โปรดสังเกตว่ายังมีสูตรที่ยาวกว่าของคุณสมบัตินี้ โดยหลีกเลี่ยง " " และใช้ตัวบ่งปริมาณที่ไม่จำกัดแทน ${\displaystyle \exists (p\in w)}$${\displaystyle w}$${\displaystyle m}$${\displaystyle w}$${\displaystyle \Delta _{0}}$${\displaystyle {\mathsf {ECST}}}$${\displaystyle \exists (p\in w)}$

โดย การนำสัจพจน์อนันต์มาใช้ การกำหนดปริมาณแบบจำกัดเซตที่ถูกต้องตามกฎหมายใน述语ที่ใช้ใน-Separation จะอนุญาตให้ใช้ตัวกำหนดปริมาณที่ไม่จำกัดเชิงตัวเลขได้อย่างชัดเจน - ความหมายทั้งสองของคำว่า "จำกัด" ไม่ควรสับสนกัน โดยถือว่ากลุ่มของตัวเลขนั้นจำกัดหากข้อความ การมีอยู่ ต่อไปนี้เป็นจริง${\displaystyle \Delta _{0}}$${\displaystyle \omega }$${\displaystyle I\subset \omega }$

${\displaystyle \exists (m\in \omega ).\forall (n\in \omega ).(n\in I\to n<m)}$