نگره‌ی هنگرد

پیش‌نیازها نگره‌ی آسانگیرانه هنگرد

تاریخچه و فرگشت

نگره‌ی هنگرد

همچنین شناخته شده با: نظریه اصل موضوعی مجموعه‌ها نظریه مجموعه‌ها نگره هنگرد تسرملو-فرانکل نگره‌ی بنداشتی هنگردها

مینه

نگره‌‌ی هَنگَرد[=نظریه مجموعه‌ها] ، نگره‌‌ی انگارشی[=ریاضیاتی] گردایه‌های خوش‌آترمیده [=خوش‌تعریف]، که هنگرد‌ها نامیده می‌شوند، از براختهایی [=اشیایی] که هموند‌ها [=عضوها] یا بن‌پار‌های [=عنصرهای] هنگرد نامیده می‌شوند، است. نگره هنگرد ناب [=محض] تنها با هنگردها سر و کار دارد، براین‌پایه تنها هنگرد‌هایی بررسی می‌شوند که هموند‌های آنها نیز هنگرد‌ها اند.

1.∃𝐸 ∀𝑥(𝑥∉𝐸) ∃E ∀x(x∉E) forsome existsE forall x(x∉E)Axiom of Empty setaxiom✹

2.∀𝐴 ∀𝐵 [∀𝑥(𝑥∈𝐴⇔𝑥∈𝐵) ⇒𝐴=𝐵] ∀A ∀B [∀x(x∈A⇔x∈B) ⇒A=B] forall A forall B [forall x(x∈A⇔x∈B) ⇒A=B]Axiom of Extensionalityaxiom✹

3.∀𝐴 ∃𝐵 ∀𝑥(𝑥∈𝐵 ⇔ 𝑥∈𝐴 ∧ φ(𝑥)) ∀A ∃B ∀x(x∈B ⇔ x∈A ∧ φ(x)) forall A forsome existsB forall x(x∈B ⇔ x∈A ∧ φ(x))Axiom schema of separationaxiom✹

4.∀𝑆 ∃𝑃 ∀𝑥(𝑥∈𝑃 ⇔ 𝑥⊂𝑆) ∀S ∃P ∀x(x∈P ⇔ x⊂S) forall S forsome existsP forall x(x∈P ⇔ x⊂S)Axiom of the power setaxiom✹

5.∀𝐴 ∀𝐵 ∃𝐶 ∀𝑥(𝑥∈𝐶 ⇔ 𝑥=𝐴 ∨ 𝑥=𝐶) ∀A ∀B ∃C ∀x(x∈C ⇔ x=A ∨ x=C) forall A forall B forsome existsC forall x(x∈C ⇔ x=A ∨ x=C)Axiom of pairingaxiom✹

6.∀𝑆 ∃𝑈 ∀𝑥[𝑥∈𝑈 ⇔ ∃𝐴(𝑥∈𝐴 ∧ 𝐴∈𝑆)] ∀S ∃U ∀x[x∈U ⇔ ∃A(x∈A ∧ A∈S)] forall S forsome existsU forall x[x∈U ⇔ forsome existsA(x∈A ∧ A∈S)]Axiom of the unionaxiom✹

7.∀𝑆 [𝑆≠∅ ⇒ ∃𝑥(𝑥∈𝑆 ∧ 𝑥∩𝑆=∅)] ∀S [S≠∅ ⇒ ∃x(x∈S ∧ x∩S=∅)] forall S [S≠∅ ⇒ forsome existsx(x∈S ∧ x∩S=∅)]Axiom of Foundationaxiom✹

8.∀𝐴 ∃𝐵 ∀𝑦 [𝑦∈𝐵 ⇔ ∃𝑥 (𝑥∈𝐴 ∧ 𝑓(𝑥,𝑦))] ∀A ∃B ∀y [y∈B ⇔ ∃x (x∈A ∧ 𝑓(x,y))] forall A forsome existsB forall y [y∈B ⇔ forsome existsx (x∈A ∧ 𝑓(x,y))]Axiom of Replacementaxiom✹

9.∃𝐼 (∅∈𝐼 ∧ ∀𝑥 (𝑥∈𝐼 ⇒ 𝑥∪{𝑥}∈𝐼)) ∃I (∅∈I ∧ ∀x (x∈I ⇒ x∪{x}∈I)) forsome existsI (∅∈I ∧ forall x (x∈I ⇒ x∪{x}∈I))Axiom of infinityaxiom✹

10.∀𝑋 [∅∉𝑋 ⇒ ∃𝑓 :𝑋→⋃𝑋 ∀𝐴∈𝑋 (𝑓(𝐴)∈𝐴)] ∀X [∅∉X ⇒ ∃𝑓 :X→⋃X ∀A∈X (𝑓(A)∈A)] forall X [∅∉X ⇒ forsome exists𝑓 :X→⋃X forall A∈X (𝑓(A)∈A)] Axiom of choiceaxiom✹