Von Neumann – Bernays – Gödel teorie množin - Von Neumann–Bernays–Gödel set theory

V základech matematiky , von Neumann-Bernays-Gödel teorie množin ( NBG ) je samozřejmé, teorie množin , která je konzervativní rozšíření z Zermelo-Fraenkel-Choice teorie množin (ZFC). NBG zavádí pojem z třídy , což je sbírka sad definovaných pomocí vzorce , jehož quantifiers pohybovat pouze po sadách. NBG může definovat třídy, které jsou větší než sady, jako je třída všech sad a třída všech pořadových čísel . Morse – Kelleyova teorie množin (MK) umožňuje definovat třídy pomocí vzorců, jejichž kvantifikátory se pohybují nad třídami. NBG je konečně axiomatizovatelný, zatímco ZFC a MK nikoli.

Klíčovou větou NBG je věta o existenci třídy, která uvádí, že pro každý vzorec, jehož kvantifikátory se pohybují pouze nad množinami, existuje třída skládající se z množin splňujících vzorec. Tato třída je vytvořena zrcadlením postupné konstrukce vzorce pomocí tříd. Vzhledem k tomu, že všechny teoretické vzorce jsou konstruovány ze dvou druhů atomových vzorců ( členství a rovnost ) a nakonec mnoha logických symbolů , je k vytvoření tříd, které je uspokojují, zapotřebí pouze konečný počet axiomů . To je důvod, proč je NBG konečně axiomatizovatelný. Třídy se také používají pro jiné konstrukce, pro zpracování paradoxů set-teoretiky a pro vyjádření axiomu globální volby , který je silnější než axiom výběru ZFC .

John von Neumann zavedl třídy do teorie množin v roce 1925. Primitivní pojmy jeho teorie byly funkce a argument . Pomocí těchto pojmů definoval třídu a množinu. Paul Bernays přeformuloval von Neumannovu teorii tím, že vzal třídu a nastavil ji jako primitivní pojmy. Kurt Gödel zjednodušil Bernaysovu teorii pro svůj důkaz relativní konzistence axiomu volby a zobecněné hypotézy kontinua .

Třídy v teorii množin

Využití tříd

Třídy mají v NBG několik použití:

• Produkují konečnou axiomatizaci teorie množin.
• Používají se k vyjádření „velmi silné formy axiomu volby “ - konkrétně axiomu globální volby : Existuje funkce globální volby definovaná pro třídu všech neprázdných množin tak, že pro každou neprázdnou množinu je to silnější než u ZFC axiom volby: Pro každou sadu neprázdných množin existuje funkce výběru definovaná tak, že pro všechny${\ displaystyle G}$${\ Displaystyle G (x) \ in x}$${\ displaystyle x.}$${\ displaystyle s}$ ${\ displaystyle f}$${\ displaystyle s}$${\ Displaystyle f (x) \ in x}$${\ Displaystyle x \ in s.}$
• Tyto set-teoretický paradoxy jsou zpracovány tím, že uznává, že některé třídy nemůže být soubory. Předpokládejme například, že třída všech pořadových čísel je sada. Pak je tranzitivní množina dobře objednal by . Podle definice je tedy pořadové číslo. Proto, což je v rozporu s dobrým uspořádáním Proto, není sada. Protože třída, která není množinou, se nazývá správná třída , je správná třída.${\ Displaystyle Ord}$${\ Displaystyle Ord}$${\ displaystyle \ in}$${\ Displaystyle Ord}$${\ Displaystyle Ord \ in Ord}$${\ displaystyle \ in}$${\ Displaystyle Obj.}$${\ Displaystyle Ord}$${\ Displaystyle Ord}$
• Správné třídy jsou užitečné v konstrukcích. Ve svém důkazu relativní konzistence axiomu globální volby a zobecněné hypotézy kontinua použil Gödel k vybudování konstruovatelného vesmíru správné třídy . Zkonstruoval funkci ve třídě všech řadových řad, která pro každý řadový díl sestaví konstruovatelnou množinu aplikací operace sestavování sestav na dříve sestrojené množiny. Konstruovatelný vesmír je obrazem této funkce.

Axioma schéma versus věta o existenci třídy

Jakmile jsou třídy přidány do jazyka ZFC, je snadné transformovat ZFC do teorie množin pomocí tříd. Nejprve je přidáno schéma axiomu porozumění třídy. Toto schéma axiomu uvádí: Pro každý vzorec, který kvantifikuje pouze přes množiny, existuje třída skládající se z - řazených n -tic splňujících vzorec - to znamená, že pak je schéma nahrazení axiomu nahrazeno jediným axiomem, který používá třídu. Nakonec je axiom extenzionality ZFC upraven tak, aby zpracovával třídy: Pokud mají dvě třídy stejné prvky, pak jsou totožné. Ostatní axiomy ZFC se nemění. ${\ Displaystyle \ phi (x_ {1}, \ ldots, x_ {n})}$${\ displaystyle A}$${\ displaystyle n}$${\ Displaystyle \ forall x_ {1} \ cdots \, \ forall x_ {n} [(x_ {1}, \ ldots, x_ {n}) \ in A \ iff \ phi (x_ {1}, \ ldots, x_ {n})].}$

Tato teorie není definitivně axiomatizována. Náhradní schéma ZFC bylo nahrazeno jediným axiomem, ale bylo zavedeno axiomové schéma třídního porozumění.

Aby byla vytvořena teorie s konečným počtem axiomů, je schéma axiomu třídního porozumění nejprve nahrazeno konečným počtem axiomů existence třídy . Pak jsou tyto axiomy použity k prokázání věty o existenci třídy, která implikuje každou instanci schématu axiomu. Důkaz této věty vyžaduje pouze sedm třída existenční axiomy, které se používají k převedení konstrukci formule do výstavby třídy splňující vzorec.

Axiomatizace NBG

Třídy a sady

NBG má dva typy objektů: třídy a sady. Intuitivně je každá sada také třídou. Existují dva způsoby, jak to axiomatizovat. Bernays používal logiku s mnoha třídami se dvěma druhy: třídami a sadami. Gödel se vyhnul třídám zavedením primitivních predikátů: pro „ je třída“ a pro „ je množina“ (v němčině je „množina“ Menge ). Rovněž zavedl axiomy, které říkaly, že každá sada je třída a že pokud je třída členem třídy, pak je množinou. Použití predikátů je standardní způsob eliminace řazení. Elliott Mendelson upravil Gödelův přístup tím, že všechno mělo být třída a definoval nastavený predikát jako Tato modifikace eliminuje Gödelův třídní predikát a jeho dva axiomy. ${\ displaystyle {\ mathfrak {Cls}} (A)}$${\ displaystyle A}$${\ displaystyle {\ mathfrak {M}} (A)}$${\ displaystyle A}$${\ displaystyle A}$${\ displaystyle A}$${\ displaystyle M (A)}$${\ displaystyle \ existuje C (A \ in C).}$

Bernaysův dvouřadý přístup se může na první pohled zdát přirozenější, ale vytváří složitější teorii. V Bernaysově teorii má každá sada dvě reprezentace: jednu jako množinu a druhou jako třídu. Existují také dva členské vztahy : první, označený „∈“, je mezi dvěma množinami; druhý, označený „η“, je mezi množinou a třídou. Tato redundance je vyžadována logikou s mnoha třídami, protože proměnné různých druhů se pohybují nad disjunktními subdoménami domény diskurzu .

Rozdíly mezi těmito dvěma přístupy neovlivňují to, co lze dokázat, ale ovlivňují způsob psaní prohlášení. V Gödelově přístupu, kde a jsou třídy, je platné tvrzení. V Bernaysově přístupu toto prohlášení nemá žádný význam. Pokud je však množina, existuje ekvivalentní příkaz: Definujte „sada představuje třídu “, pokud mají stejné sady jako členové - tj. Příkaz, kde množina představuje třídu, je ekvivalentní Gödelovu${\ displaystyle A \ in C}$${\ displaystyle A}$${\ displaystyle C}$${\ displaystyle A}$${\ displaystyle a}$${\ displaystyle A}$${\ Displaystyle \ forall x (x \ in a \ iff x \; \ eta \; A).}$${\ Displaystyle a \; \ eta \; C}$${\ displaystyle a}$${\ displaystyle A}$${\ Displaystyle A \ v C.}$

Přístup přijatý v tomto článku je přístup Gödela s Mendelsonovou modifikací. To znamená, že NBG je axiomatický systém v predikátové logice prvního řádu s rovností a jeho jediné primitivní pojmy jsou třída a vztah členství.

Definice a axiomy extenze a párování

Sada je třída, která patří alespoň do jedné třídy: je sada, pokud a pouze pokud . Třída, která není množinou, se nazývá řádná třída: je správná třída právě tehdy . Proto je každá třída buď množinou, nebo řádnou třídou, a žádná třída není obojí (pokud je teorie konzistentní ). ${\ displaystyle A}$${\ displaystyle \ existuje C (A \ v C)}$${\ displaystyle A}$${\ displaystyle \ forall C (A \ notin C)}$

Gödel představil konvenci, že proměnné velkých písmen se pohybují nad třídami, zatímco proměnné malých písmen se pohybují nad sadami. Gödel také použil názvy, které začínají velkými písmeny, k označení konkrétních tříd, včetně funkcí a vztahů definovaných pro třídu všech sad. V tomto článku je použita Gödelova konvence. Umožňuje nám napsat:

K prokázání věty o existenci třídy jsou zapotřebí následující axiomy a definice.

Axiom extenze.  Pokud mají dvě třídy stejné prvky, pak jsou totožné.

${\ Displaystyle \ forall A \, \ forall B \, [\ forall x (x \ in A \ iff x \ in B) \ implikuje A = B]}$ 

Tento axiom zobecňuje axiom extenze ZFC na třídy.

Axiom párování .  Pokudajsou sady, pak existuje sada,jejíž jedinými členy jsoua. ${\ displaystyle x}$${\ displaystyle y}$${\ displaystyle p}$${\ displaystyle x}$${\ displaystyle y}$

${\ Displaystyle \ forall x \, \ forall y \, \ existuje p \, \ forall z \, [z \ in p \ iff (z = x \, \ lor \, z = y)]}$ 

Stejně jako v ZFC, axiom extenze implikuje jedinečnost množiny , což nám umožňuje zavést notaci${\ displaystyle p}$${\ displaystyle \ {x, y \}.}$

Objednané páry jsou definovány:

${\ Displaystyle (x, y) = \ {\ {x \}, \ {x, y \} \}}$

N -tice jsou definovány indukčně pomocí uspořádaných párů:

${\ displaystyle (x_ {1}) = x_ {1},}$

${\ Displaystyle {\ text {For}} n> 1 \! :( x_ {1}, \ ldots, x_ {n-1}, x_ {n}) = ((x_ {1}, \ ldots, x_ { n-1}), x_ {n}).}$

Axiomy existence třídy a axiom pravidelnosti

K prokázání věty o existenci třídy budou použity axiomy existence třídy: Pro každý vzorec ve proměnných volných množin, který kvantifikuje pouze přes množiny, existuje třída -tuplů, které ji splňují. Následující příklad začíná dvěma třídami, které jsou funkcemi, a vytváří složenou funkci . Tento příklad ilustruje techniky, které jsou potřebné k prokázání věty o existenci třídy, které vedou k potřebným axiomům existence třídy. ${\ displaystyle n}$ ${\ displaystyle n}$

Příklad 1:  Pokud jsou třídy a jsou funkce, pak je složená funkce definována vzorcem: Protože tento vzorec má dvě volné množinové proměnné a věta o existenci třídy sestrojí třídu uspořádaných dvojic:${\ displaystyle F}$${\ displaystyle G}$${\ Displaystyle G \ circ F}$${\ Displaystyle \ existuje t [(x, t) \ in F \, \ land \, (t, y) \ in G].}$${\ displaystyle x}$${\ displaystyle y,}$${\ Displaystyle G \ circ F \, = \, \ {(x, y): \ existuje t [(x, t) \ in F \, \ land \, (t, y) \ in G] \}. }$ Protože je tento vzorec postaven na jednodušších vzorcích využívajících konjunkturu a existenciální kvantifikaci , jsou zapotřebí operace třídy , které berou třídy představující jednodušší vzorce a vytvářejí třídy představující vzorce pomocí a . K vytvoření třídy představující vzorec s , průnik používaný od K vytvoření třídy představující vzorec s se doména používá od${\ Displaystyle \ land}$ ${\ displaystyle \ existuje}$${\ Displaystyle \ land}$${\ displaystyle \ existuje}$${\ Displaystyle \ land}$${\ Displaystyle x \ in A \ cap B \ iff x \ in A \ land x \ in B.}$${\ displaystyle \ existuje}$${\ Displaystyle x \ v Dom (A) \ iff \ existuje t [(x, t) \ v A].}$ Před přijetím křižovatky n -tice a potřeba další komponenty, aby měly stejné proměnné. Komponenta se přidá k n -ticím n -tic a přidá se k n -ticím n -tic : ${\ displaystyle F}$${\ displaystyle G}$${\ displaystyle y}$${\ displaystyle F}$${\ displaystyle x}$${\ displaystyle G}$ ${\ Displaystyle F '= \ {(x, t, y) :( x, t) \ v F \} \,}$ a ${\ Displaystyle \, G '= \ {(t, y, x) :( t, y) \ v G \}}$ V definici proměnné není příkazem omezeno, takže se pohybuje nad třídou všech sad. Podobně v definici rozsahů proměnných nad So je zapotřebí axiom, který přidá další komponentu (jejíž hodnoty se pohybují nad ) do n -tic dané třídy. ${\ displaystyle F ',}$${\ displaystyle y}$${\ displaystyle (x, t) \ v F,}$${\ displaystyle y}$${\ displaystyle V}$${\ displaystyle G ',}$${\ displaystyle x}$${\ Displaystyle V.}$${\ displaystyle V}$ Dále jsou proměnné umístěny ve stejném pořadí, aby se připravily na křižovatku: ${\ Displaystyle F '' = \ {(x, y, t) :( x, t) \ v F \} \,}$ a ${\ Displaystyle \, G '' = \ {(x, y, t) :( t, y) \ v G \}}$ Chcete-li přejít od do az do vyžaduje dvě různé obměny , tak axiómy že je třeba podpora permutace n-tic prvků. ${\ displaystyle F '}$${\ displaystyle F ''}$${\ displaystyle G '}$${\ displaystyle G ''}$ Křižovatka a úchyty : ${\ displaystyle F ''}$${\ displaystyle G ''}$${\ Displaystyle \ land}$ ${\ Displaystyle F '' \ cap G '' = \ {(x, y, t) :( x, t) \ in F \, \ land \, (y, t) \ in G \}}$ Vzhledem k tomu, že je definován jako , přičemž doména zpracovává a produkuje složenou funkci: ${\ Displaystyle (x, y, t)}$${\ displaystyle ((x, y), t)}$${\ displaystyle F '' \ cap G ''}$${\ displaystyle \ existuje t}$ ${\ Displaystyle G \ circ F = Dom (F '' \ cap G '') = \ {(x, y): \ existuje t ((x, t) \ v F \, \ země \, (t, y ) \ v G) \}}$ Axiomy průniku a domény jsou tedy potřeba.

Axiomy existence třídy jsou rozděleny do dvou skupin: axiomy zpracovávající jazyková primitiva a axiomy zpracovávající n -tice. V první skupině jsou čtyři axiomy a ve druhé skupině tři axiomy.

Axiomy pro zpracování jazykových primitiv:

Členství.  Existuje třída obsahující všechny uspořádané páry, jejichž první složka je členem druhé složky. ${\ displaystyle E}$

${\ Displaystyle \ existuje E \, \ forall x \, \ forall y \, [(x, y) \ in E \ iff x \ in y] \!}$ 

Křižovatka (konjunkce).  Pro jakékoli dvě třídy a existuje třída skládající se přesně ze sad, které patří do obou a . ${\ displaystyle A}$${\ displaystyle B}$${\ displaystyle C}$${\ displaystyle A}$${\ displaystyle B}$

${\ Displaystyle \ forall A \, \ forall B \, \ existuje C \, \ forall x \, [x \ in C \ iff (x \ in A \, \ land \, x \ in B)]}$ 

Doplněk (negace).  Pro jakoukoli tříduexistuje třídaskládající se přesně ze sad, do kterých nepatří. ${\ displaystyle A}$${\ displaystyle B}$${\ displaystyle A}$

${\ Displaystyle \ forall A \, \ existuje B \, \ forall x \, [x \ in B \ iff \ neg (x \ in A)]}$ 

Doména (existenciální kvantifikátor).  Pro jakoukoli třídu existuje třída skládající se přesně z prvních komponent uspořádaných dvojic . ${\ displaystyle A}$${\ displaystyle B}$${\ displaystyle A}$

${\ Displaystyle \ forall A \, \ existuje B \, \ forall x \, [x \ in B \ iff \ existuje y ((x, y) \ in A)]}$ 

Axiomem extenze je třída v průsečíkovém axiomu a třída v axiomech komplementu a domény jedinečná. Budou označeny: a . Na druhou stranu, extenčnost není použitelná v axiomu členství, protože určuje pouze ty sady, které jsou uspořádanými páry. ${\ displaystyle C}$${\ displaystyle B}$${\ displaystyle A \ cap B,}$ ${\ displaystyle \plement A,}$${\ displaystyle Dom (A),}$${\ displaystyle E}$${\ displaystyle E}$

První tři axiomy naznačují existenci prázdné třídy a třídy všech množin: Axiom členství implikuje existenci třídy Průsečíky a komplementární axiomy znamenají existenci prázdné třídy. Axiom extenze je tato třída jedinečná; označuje se Doplněk je třída všech množin, která je také jedinečná rozšířením. Nastavený predikát , který byl definován jako , je nyní předefinován, aby se zabránilo kvantifikaci nad třídami. ${\ Displaystyle E.}$${\ Displaystyle E \ cap \plement E}$${\ Displaystyle \ emptyset.}$${\ displaystyle \ emptyset}$${\ displaystyle V}$${\ displaystyle M (A)}$${\ displaystyle \ existuje C (A \ v C)}$${\ displaystyle A \ in V}$

Axiomy pro manipulaci s n -ticemi:

Produkt od . ${\ displaystyle V}$ Pro jakoukoli tříduexistuje třídaskládající se z uspořádaných dvojic, do nichž patří první složka. ${\ displaystyle A}$${\ displaystyle B}$${\ displaystyle A}$

${\ Displaystyle \ forall A \, \ existuje B \, \ forall u \, [u \ v B \ iff \ existuje x \, \ existuje y \, (u = (x, y) \ land x \ v A) ]}$

Kruhová permutace .  Pro jakoukoli tříduexistuje třída,jejíž 3 -tice jsou získány použitím kruhové permutacena 3 -tice. ${\ displaystyle A}$${\ displaystyle B}$${\ Displaystyle (y, z, x) \ mapsto (x, y, z)}$${\ displaystyle A}$

${\ Displaystyle \ forall A \, \ existuje B \, \ forall x \, \ forall y \, \ forall z \, [(x, y, z) \ in B \ iff (y, z, x) \ in A]}$

Transpozice .  Pro jakoukoli tříduexistuje třída,jejíž 3 -tice jsou získány transpozicí posledních dvou složek 3 -tic dvojice. ${\ displaystyle A}$${\ displaystyle B}$${\ displaystyle A}$

${\ Displaystyle \ forall A \, \ existuje B \, \ forall x \, \ forall y \, \ forall z \, [(x, y, z) \ in B \ iff (x, z, y) \ in A]}$

Extensionalitou součin podle axiomu znamená existenci jedinečné třídy, která je označena tímto. Tento axiom se používá k definování třídy všech -tuples : a If je -li třída, extenzialita znamená, že je jedinečnou třídou skládající se z -tuples o například členství axiom vytváří třídu , která může obsahovat prvky, které nejsou uspořádaných dvojic, zatímco průnik obsahuje pouze objednané páry . ${\ displaystyle V}$${\ displaystyle A \ times V.}$${\ displaystyle V^{n}}$${\ displaystyle n}$${\ displaystyle V^{1} = V}$${\ Displaystyle V^{n+1} = V^{n} \ krát V. \,}$${\ displaystyle A}$${\ Displaystyle A \ cap V^{n}}$${\ displaystyle n}$${\ displaystyle A.}$${\ displaystyle E}$${\ Displaystyle E \ cap V^{2}}$${\ displaystyle E}$

Kruhové permutační a transpoziční axiomy neimplikují existenci unikátních tříd, protože specifikují pouze 3 – tice -n -tice třídy Tím, že zadají 3 -tice, také určují -tuple pro od: Axiomy pro zpracování n -tic a doménový axiom naznačují následující lemma, které se používá v důkazu věty o existenci třídy. ${\ Displaystyle B.}$${\ displaystyle n}$${\ Displaystyle n \ geq 4}$${\ Displaystyle (x_ {1}, \ ldots, x_ {n-2}, x_ {n-1}, x_ {n}) = ((x_ {1}, \ ldots, x_ {n-2}), x_ {n-1}, x_ {n}).}$

Tuple lemma.

1. ${\ Displaystyle \, \ forall A \, \ existuje B_ {1} \, \ forall x \, \ forall y \, \ forall z \, [(z, x, y) \ in B_ {1} \ iff ( x, y) \ v A]}$
2. ${\ Displaystyle \, \ forall A \, \ existuje B_ {2} \, \ forall x \, \ forall y \, \ forall z \, [(x, z, y) \ in B_ {2} \ iff ( x, y) \ v A]}$
3. ${\ Displaystyle \, \ forall A \, \ existuje B_ {3} \, \ forall x \, \ forall y \, \ forall z \, [(x, y, z) \ in B_ {3} \ iff ( x, y) \ v A]}$
4. ${\ Displaystyle \, \ forall A \, \ existuje B_ {4} \, \ forall x \, \ forall y \, \ forall z \, [(y, x) \ in B_ {4} \ iff (x, y) \ v A]}$

Důkaz:   Třída : Aplikovat produkt podle na produkovat Třída : Použít transpozici na produkovat Třída : Použít kruhovou permutaci na vytvořit Třída : Použít kruhovou permutaci na , poté použít doménu pro produkci${\ displaystyle B_ {3}}$${\ displaystyle V}$${\ displaystyle A}$${\ displaystyle B_ {3}.}$
            ${\ displaystyle B_ {2}}$${\ displaystyle B_ {3}}$${\ displaystyle B_ {2}.}$
            ${\ displaystyle B_ {1}}$${\ displaystyle B_ {3}}$${\ displaystyle B_ {1}.}$
            ${\ displaystyle B_ {4}}$${\ displaystyle B_ {2}}$${\ displaystyle B_ {4}.}$

K prokázání věty o existenci třídy je zapotřebí ještě jeden axiom: axiom pravidelnosti . Protože byla prokázána existence prázdné třídy, je uvedeno obvyklé tvrzení tohoto axiomu.

Axiom pravidelnosti .  Každá neprázdná množina má alespoň jeden prvek, se kterým nemá žádný společný prvek.

${\ Displaystyle \ forall a \, [a \ neq \ emptyset \ implikuje \ existuje u (u \ in a \ land u \ cap a = \ emptyset)].}$

Tento axiom znamená, že soubor nemůže patřit k sobě: Předpokládejme, že a nechť Pak neboť to je v rozporu axiom pravidelnosti, protože je jediným prvkem proto Axiom pravidelnosti rovněž zakazuje nekonečné sestupné členské sekvence sestav:${\ displaystyle x \ in x}$${\ displaystyle a = \ {x \}.}$${\ Displaystyle x \ cap a \ neq \ emptyset}$${\ Displaystyle x \ in x \ cap a.}$${\ displaystyle x}$${\ displaystyle a.}$${\ displaystyle x \ notin x.}$${\ Displaystyle \; \; \ cdots \ in x_ {n+1} \ in x_ {n} \ in \ cdots \ in x_ {1} \ in x_ {0}.}$

Gödel ve své monografii z roku 1940, která vycházela z přednášek z roku 1938., uvedl pravidelnost spíše pro třídy než pro sady. V roce 1939 dokázal, že pravidelnost pro sady znamená pravidelnost pro třídy.

Věta o existenci třídy

Věta o existenci třídy.  Nechť je vzorec, který kvantifikuje pouze v sadách a neobsahuje žádné volné proměnné kromě (ne nutně všech těchto). Potom všem , existuje jedinečná třída z -tuples taková, že: Třída je označen${\ Displaystyle \ phi (x_ {1}, \ dots, x_ {n}, Y_ {1}, \ dots, Y_ {m})}$${\ Displaystyle x_ {1}, \ tečky, x_ {n}, Y_ {1}, \ tečky, Y_ {m}}$${\ displaystyle Y_ {1}, \ tečky, Y_ {m}}$${\ displaystyle A}$${\ displaystyle n}$${\ Displaystyle \ forall x_ {1} \ cdots \, \ forall x_ {n} [(x_ {1}, \ dots, x_ {n}) \ in A \ iff \ phi (x_ {1}, \ dots, x_ {n}, Y_ {1}, \ tečky, Y_ {m})].}$${\ displaystyle A}$${\ Displaystyle \ {(x_ {1}, \ dots, x_ {n}): \ phi (x_ {1}, \ dots, x_ {n}, Y_ {1}, \ dots, Y_ {m}) \ }.}$

Důkaz věty bude proveden ve dvou krocích:

1. Transformační pravidla se používají k transformaci daného vzorce na ekvivalentní vzorec, který zjednodušuje indukční část důkazu. Například, pouze logické symboly v transformovaných vzorci jsou , , a , takže indukční zpracovává logické symboly s jen ve třech případech.${\ displaystyle \ phi}$${\ Displaystyle \ neg}$${\ Displaystyle \ land}$${\ displaystyle \ existuje}$
2. Věta o existenci třídy je u transformovaných vzorců prokázána induktivně. Axiomy existence třídy, které se řídí strukturou transformovaného vzorce, se používají k vytvoření jedinečné třídy -tuples splňující vzorec.${\ displaystyle n}$

Transformační pravidla.  V pravidlech 1 a 2 níže, a pozadím označují množina nebo třída proměnných. Tato dvě pravidla eliminují všechny výskyty třídních proměnných před a všechny výskyty rovnosti. Při každém použití pravidla 1 nebo 2 na podformuli je zvoleno tak, aby se lišilo od ostatních proměnných v aktuálním vzorci. Tři pravidla se opakují, dokud neexistují žádné podformuly, na které by je bylo možné použít. Tím se vytvoří vzorec, který je postaven pouze s , , , , nastavit proměnné a proměnné třídy , kde není než bude vypadat . ${\ displaystyle \ Delta}$${\ displaystyle \ Gamma}$${\ displaystyle \ in}$${\ displaystyle i}$${\ displaystyle z_ {i}}$${\ Displaystyle \ neg}$${\ Displaystyle \ land}$${\ displaystyle \ existuje}$${\ displaystyle \ in}$${\ displaystyle Y_ {k}}$${\ displaystyle Y_ {k}}$${\ displaystyle \ in}$

1. ${\ displaystyle \, Y_ {k} \ in \ Gamma}$ je přeměněna na ${\ Displaystyle \ existuje z_ {i} (z_ {i} = Y_ {k} \, \ land \, z_ {i} \ in \ Gamma).}$
2. Rozšíření se používá k transformaci do${\ displaystyle \ Delta = \ Gamma}$${\ Displaystyle \ forall z_ {i} (z_ {i} \ in \ Delta \ iff z_ {i} \ in \ Gamma).}$
3. Logické identity se používají k transformaci subformul obsahujících a k subformulám, které používají pouze a${\ Displaystyle \ lor, \ implikuje, \ iff,}$${\ displaystyle \ forall}$${\ Displaystyle \ neg, \ land,}$${\ displaystyle \ existuje.}$

Transformační pravidla: vázané proměnné .  Uvažujme vzorec složené funkce z příkladu 1 s jeho proměnnými volných množin nahrazenými a : Indukční důkaz odstraní , čímž vznikne vzorec. Protože je však pro indexované proměnné uvedena věta o existenci třídy, tento vzorec nemá formu očekávanou indukční hypotéza . Tento problém je vyřešen tím, že nahradí proměnnou s Vázané proměnné ve vnořených quantifiers jsou zpracovány zvýšením dolní index jednou za každý následující kvantifikátorem. To vede k pravidlu 4, které musí být aplikováno za ostatními pravidly, protože pravidla 1 a 2 produkují kvantifikované proměnné. ${\ displaystyle x_ {1}}$${\ displaystyle x_ {2}}$${\ Displaystyle \ existuje t [(x_ {1}, t) \ in F \, \ land \, (t, x_ {2}) \ v G].}$${\ displaystyle \ existuje t}$${\ Displaystyle (x_ {1}, t) \ in F \ land (t, x_ {2}) \ v G.}$${\ displaystyle t}$${\ displaystyle x_ {3}.}$

4. Pokud vzorec neobsahuje žádné jiné volné sady proměnných, než jsou pak nahrazeny vázané proměnné, které jsou vnořené do kvantifikátorů . Tyto proměnné mají (kvantifikátor) vnořovací hloubku .${\ Displaystyle x_ {1}, \ tečky, x_ {n},}$${\ displaystyle q}$${\ displaystyle x_ {n+q}}$ ${\ displaystyle q}$

Příklad 2:   Pravidlo 4 je aplikováno na vzorec, který definuje třídu skládající se ze všech množin tvaru , tj. Množin, které obsahují alespoň a množiny obsahující - například kde a jsou množiny. ${\ displaystyle \ phi (x_ {1})}$${\ Displaystyle \ {\ emptyset, \ {\ emptyset, \ dots \}, \ dots \}.}$${\ displaystyle \ emptyset}$${\ displaystyle \ emptyset}$${\ Displaystyle \ {\ emptyset, \ {\ emptyset, a, b, c \}, d, e \}}$${\ Displaystyle a, b, c, d,}$${\ displaystyle e}$ ${\ Displaystyle {\ begin {aligned} \ phi (x_ {1}) \, & = \, \ existuje u \; \, [\, u \ v x_ {1} \, \ land \, \ neg \ existuje v \; \, (\; v \, \ in \, u \,)] \, \ land \, \, \ existuje w \; {\ bigl (} w \ v x_ {1} \, \ land \ , \ existuje y \; \, [(\; y \, \ in w \; \ land \; \ neg \ existuje z \; \, (\; z \, \ in \, y \,)] {\ bigr)} \\\ phi _ {r} (x_ {1}) \, & = \, \ existuje x_ {2} [x_ {2} \! \ in \! x_ {1} \, \ land \, \ neg \ existuje x_ {3} (x_ {3} \! \ in \! x_ {2})] \, \ land \, \, \ existuje x_ {2} {\ bigl (} x_ {2} \! \ in \! x_ {1} \, \ land \, \ existuje x_ {3} [(x_ {3} \! \ in \! x_ {2} \, \ land \, \ neg \ existuje x_ {4} (x_ {4} \! \ in \! x_ {3})] {\ bigr)} \ end {aligned}}}$ Protože je jedinou volnou proměnnou, kvantifikovaná proměnná se objeví dvakrát v hloubce vnoření 2. Její dolní index je 3, protože Pokud jsou dva rozsahy kvantifikátorů ve stejné hloubce vnoření, jsou buď totožné, nebo disjunktní. Tyto dva výskyty jsou v nesouvislých oborech kvantifikátorů, takže mezi sebou vzájemně neinteragují. ${\ displaystyle x_ {1}}$${\ Displaystyle n = 1.}$${\ displaystyle x_ {3}}$${\ displaystyle x_ {3} \ v x_ {2}}$${\ Displaystyle n+q = 1+2 = 3.}$${\ displaystyle x_ {3}}$

Důkaz věty o existenci třídy.  Důkaz začíná aplikací transformačních pravidel na daný vzorec k vytvoření transformovaného vzorce. Protože tento vzorec je ekvivalentní danému vzorci, důkaz je dokončen prokázáním věty o existenci třídy pro transformované vzorce.

Důkaz věty o existenci třídy pro transformované vzorce

V důkazu je použito následující lemma. ${\ displaystyle {\ mathsf {Expansion \; lemma.}} \,}$Nechť a nechť být třída obsahuje všechny objednané páry , který by splňoval To znamená, pak může být rozšířena do jedinečného třídy z -tuples splňujících . To znamená,${\ Displaystyle 1 \ leq i <j \ leq n,}$${\ displaystyle P}$${\ displaystyle (x_ {i}, x_ {j})}$${\ displaystyle R (x_ {i}, x_ {j}).}$${\ Displaystyle P \ supseteq \ {(x_ {i}, x_ {j}): R (x_ {i}, x_ {j}) \}.}$${\ displaystyle P}$${\ displaystyle Q}$${\ displaystyle n}$${\ displaystyle R (x_ {i}, x_ {j})}$${\ Displaystyle Q = \ {(x_ {1}, \ ldots, x_ {n}): R (x_ {i}, x_ {j}) \}.}$ ${\ displaystyle {\ mathsf {Proof \ !:}}}$ ${\ Displaystyle {\ mathsf {Class \; existence \; věta \; pro \; transformované \; vzorce.}} \,}$ Budiž vzorec, který: ${\ Displaystyle \ phi (x_ {1}, \ ldots, x_ {n}, Y_ {1}, \ ldots, Y_ {m})}$ Potom všem , existuje jedinečná třída z -tuples taková, že: ${\ displaystyle Y_ {1}, \ tečky, Y_ {m}}$${\ displaystyle A}$${\ displaystyle n}$ ${\ Displaystyle \ forall x_ {1} \ cdots \, \ forall x_ {n} [(x_ {1}, \ ldots, x_ {n}) \ in A \ iff \ phi (x_ {1}, \ ldots, x_ {n}, Y_ {1}, \ ldots, Y_ {m})].}$ ${\ displaystyle {\ mathsf {Proof \!: \, Basis \; krok.}} \,}$ ${\ displaystyle \ phi}$má 0 logických symbolů. Hypotéza věty naznačuje, že jde o atomový vzorec formy nebo${\ displaystyle \ phi}$${\ displaystyle x_ {i} \ v x_ {j}}$${\ Displaystyle x_ {i} \ v Y_ {k}.}$ ${\ Displaystyle {\ mathsf {Inductive \; step.}} \; \ phi}$má logické symboly kde . Předpokládejme indukční hypotézu, že věta platí pro všechny s méně než logickými symboly. Nyní dokážeme větu pro pomocí logických symbolů. V tomto důkazu je seznam třídních proměnných zkrácen na , takže vzorec - například - může být zapsán jako${\ displaystyle k}$${\ displaystyle k> 0}$${\ Displaystyle \ psi}$${\ displaystyle k}$${\ displaystyle \ phi}$${\ displaystyle k}$${\ displaystyle Y_ {1}, \ tečky, Y_ {m}}$${\ displaystyle {\ vec {Y}}}$${\ Displaystyle \ phi (x_ {1}, \ dots, x_ {n}, Y_ {1}, \ dots, Y_ {m})}$${\ Displaystyle \ phi (x_ {1}, \ dots, x_ {n}, {\ vec {Y}}).}$

Gödel poukázal na to , že věta o existenci třídy „je metatheorem , tedy teorém o systému [NBG], nikoli v systému…“ Je to věta o NBG, protože je v metateorii prokázána indukcí na vzorcích NBG. Jeho důkaz - namísto vyvolání konečného počtu axiomů NBG - indukčně popisuje, jak použít axiomy NBG k sestavení třídy splňující daný vzorec. Pro každý vzorec lze tento popis proměnit v konstruktivní důkaz existence, který je v NBG. Proto tento metatheorem může generovat důkazy NBG, které nahrazují použití věty o existenci třídy NBG.

Rekurzivní počítačový program stručně zachycuje konstrukci třídy z daného vzorce. Definice tohoto programu nezávisí na důkazu věty o existenci třídy. Je však zapotřebí důkaz, který prokáže, že třída vytvořená programem splňuje daný vzorec a je vytvořena pomocí axiomů. Tento program je napsán v pseudokódu, který používá příkaz Case ve stylu Pascal .

${\ Displaystyle \ mathbf {funkce} \; {\ text {Class}} (\ phi, \, n)}$
${\ Displaystyle {\ begin {aligned} \ mathbf {input} \!: \; \, & \ phi {\ text {je transformovaný vzorec formuláře}} \ phi (x_ {1}, \ ldots, x_ { n}, Y_ {1}, \ ldots, Y_ {m}); \\ & n {\ text {určuje, že se vrátí třída}} n {\ text {-tuples.}} \\\; \; \ ; \; \ mathbf {output} \!: \; \, & {\ text {class}} A {\ text {of}} n {\ text {-tuples uspokojující}} \\ & \, \ forall x_ { 1} \ cdots \, \ forall x_ {n} [(x_ {1}, \ ldots, x_ {n}) \ in A \ iff \ phi (x_ {1}, \ ldots, x_ {n}, Y_ { 1}, \ ldots, Y_ {m})]. \ End {aligned}}}$

${\ displaystyle \ mathbf {begin}}$

${\ Displaystyle \ mathbf {case} \; \ phi \; \ mathbf {of}}$

${\ displaystyle {\ begin {alignedat} {2} x_ {i} \ in x_ {j}: \; \; & \ mathbf {return} \; \, E_ {i, j, n}; && {\ text {//}} E_ {i, j, n} \; \, = \ {(x_ {1}, \ dots, x_ {n}): x_ {i} \ in x_ {j} \} \\ x_ {i} \ in Y_ {k}: \; \; & \ mathbf {return} \; \, E_ {i, Y_ {k}, n}; && {\ text {//}} E_ {i, Y_ {k}, n} = \ {(x_ {1}, \ tečky, x_ {n}): x_ {i} \ v Y_ {k} \} \\ \ neg \ psi: \; \; & \ mathbf {return} \; \, \plement _ {V^{n}} {\ text {Class}} (\ psi, \, n); && {\ text {//}} \plement _ {V^{n }} {\ text {Class}} (\ psi, \, n) = V^{n} \ setminus {\ text {Class}} (\ psi, \, n) \\\ psi _ {1} \ land \ psi _ {2}: \; \; & \ mathbf {return} \; \, {\ text {Class}} (\ psi _ {1}, \, n) \ cap {\ text {Class}} ( \ psi _ {2}, \, n); && \\\; \; \; \; \, \ existuje x_ {n+1} (\ psi): \; \; & \ mathbf {return} \; \, Dom ({\ text {Class}} (\ psi, \, n+1)); && {\ text {//}} x_ {n+1} {\ text {je zdarma v}} \ psi; {\ text {Class}} (\ psi, \, n+1) \\ & \ && {\ text {// vrací třídu}} (n+1) {\ text {-tuples}} \ end { alignedat}}}$

${\ displaystyle \ mathbf {end}}$

${\ displaystyle \ mathbf {end}}$

Nechť je vzorec příkladu 2 . Volání funkce generuje třídu, která je níže porovnána s To ukazuje, že konstrukce třídy zrcadlí konstrukci jejího definujícího vzorce${\ displaystyle \ phi}$${\ Displaystyle A = Třída (\ phi, 1)}$${\ displaystyle A,}$${\ Displaystyle \ phi.}$${\ displaystyle A}$${\ Displaystyle \ phi.}$

${\ Displaystyle {\ begin {alignedat} {2} & \ phi \; && = \; \; \ existuje x_ {2} \, (x_ {2} \! \ in \! x_ {1} \ land \; \; \ neg \; \; \; \; \ existuje x_ {3} \; (x_ {3} \! \ in \! x_ {2})) \, \ land \; \; \, \ existuje x_ {2} \, (x_ {2} \! \ In \! X_ {1} \ land \; \; \, \ existuje x_ {3} \, (x_ {3} \! \ In \! X_ {2 } \, \ land \; \; \ neg \; \; \; \; \ existuje x_ {4} \; (x_ {4} \! \ in \! x_ {3}))) \\ & A \; && = Dom \, (\; E_ {2,1,2} \; \ cap \; \ doplněk _ {V^{2}} \, Dom \, (\; E_ {3,2,3} \; )) \, \ cap \, Dom \, (\; E_ {2,1,2} \; \ cap \, Dom \, (\; \, E_ {3,2,3} \; \ cap \; \plement _ {V^{3}} \, Dom \, (\; E_ {4,3,4} \;))) \ end {alignedat}}}$

Rozšíření věty o existenci třídy

Gödel rozšířil větu o existenci třídy na vzorce obsahující vztahy přes třídy (například a unární relace ), speciální třídy (jako například ) a operace (jako a ). Aby byla věta o existenci třídy rozšířena, musí vzorce definující vztahy, speciální třídy a operace kvantifikovat pouze přes sady. Poté lze transformovat do ekvivalentního vzorce splňujícího hypotézu o teorémě existence třídy . ${\ displaystyle \ phi}$${\ displaystyle Y_ {1} \ subseteq Y_ {2}}$ ${\ displaystyle M (Y_ {1})}$${\ Displaystyle Ord}$ ${\ displaystyle (x_ {1}, x_ {2})}$${\ displaystyle x_ {1} \ cap Y_ {1}}$${\ displaystyle \ phi}$

Následující definice určují, jak vzorce definují vztahy, speciální třídy a operace:

1. Vztah je definován:${\ displaystyle R}$${\ Displaystyle R (Z_ {1}, \ dots, Z_ {k}) \ iff \ psi _ {R} (Z_ {1}, \ dots, Z_ {k}).}$
2. Speciální třídu definuje:${\ displaystyle C}$${\ Displaystyle u \ in C \ iff \ psi _ {C} (u).}$
3. Operace je definována:${\ displaystyle P}$${\ Displaystyle u \ in P (Z_ {1}, \ dots, Z_ {k}) \ iff \ psi _ {P} (u, Z_ {1}, \ dots, Z_ {k}).}$

Pojem je definován:

1. Proměnné a speciální třídy jsou termíny.
2. Pokud je operace s argumenty a jsou termíny, pak je termín.${\ displaystyle P}$${\ displaystyle k}$${\ Displaystyle \ Gamma _ {1}, \ tečky, \ Gamma _ {k}}$${\ Displaystyle P (\ Gamma _ {1}, \ dots, \ Gamma _ {k})}$

Následující pravidla transformace eliminují vztahy, speciální třídy a operace. Pokaždé, když se na podformuli použije pravidlo 2b, 3b nebo 4, je vybráno tak, aby se lišilo od ostatních proměnných v aktuálním vzorci. Pravidla se opakují, dokud neexistují žádné podformuly, na které by je bylo možné použít. a označují podmínky. ${\ displaystyle i}$${\ displaystyle z_ {i}}$${\ Displaystyle \, \ Gamma _ {1}, \ dots, \ Gamma _ {k}, \ Gamma,}$${\ displaystyle \ Delta}$

Příklad 3:  Transformace${\ displaystyle Y_ {1} \ subseteq Y_ {2}.}$ ${\ Displaystyle Y_ {1} \ subseteq Y_ {2} \ iff \ forall z_ {1} (z_ {1} \ v Y_ {1} \ implikuje z_ {1} \ v Y_ {2}) \ quad {\ text {(pravidlo 1)}}}$

Příklad 4:  Transformace${\ Displaystyle x_ {1} \ cap Y_ {1} \ in x_ {2}.}$ ${\ Displaystyle {\ begin {alignedat} {2} x_ {1} \ cap Y_ {1} \ in x_ {2} & \ iff \ existuje z_ {1} [z_ {1} = x_ {1} \ cap Y_ {1} \, \ land \, z_ {1} \ in x_ {2}] && {\ text {(pravidlo 3b)}} \\ & \ iff \ existuje z_ {1} [\ forall z_ {2} ( z_ {2} \ in z_ {1} \ iff z_ {2} \ in x_ {1} \ cap Y_ {1}) \, \ land \, z_ {1} \ in x_ {2}] && {\ text {(pravidlo 4)}} \\ & \ iff \ existuje z_ {1} [\ forall z_ {2} (z_ {2} \ in z_ {1} \ iff z_ {2} \ in x_ {1} \ land z_ {2} \ in Y_ {1}) \, \ land \, z_ {1} \ in x_ {2}] \ quad && {\ text {(pravidlo 3a)}}} \\\ end {alignedat}}}$ Tento příklad ukazuje, jak spolupracují pravidla transformace při eliminaci operace.

Věta o existenci třídy (rozšířená verze).  Nechť je vzorec, který kvantifikuje pouze přes množiny, neobsahuje žádné volné proměnné kromě a může obsahovat vztahy, speciální třídy a operace definované vzorci, které kvantifikují pouze přes sady. Pak pro všechny existuje jedinečná třída z -tuples taková, že${\ Displaystyle \ phi (x_ {1}, \ dots, x_ {n}, Y_ {1}, \ dots, Y_ {m})}$${\ Displaystyle x_ {1}, \ tečky, x_ {n}, Y_ {1}, \ tečky, Y_ {m}}$${\ displaystyle Y_ {1}, \ tečky, Y_ {m},}$${\ displaystyle A}$${\ displaystyle n}$${\ Displaystyle \ forall x_ {1} \ cdots \, \ forall x_ {n} [(x_ {1}, \ dots, x_ {n}) \ in A \ iff \ phi (x_ {1}, \ dots, x_ {n}, Y_ {1}, \ tečky, Y_ {m})].}$

Důkaz: Pomocí  transformačních pravidel vytvořte ekvivalentní vzorec, který neobsahuje žádné vztahy, speciální třídy ani operace. Tento vzorec splňuje hypotézu o větě o existenci třídy. Proto je pro všechny je zde jedinečná třída of -tuples , který by splňoval${\ displaystyle \ phi}$${\ displaystyle Y_ {1}, \ tečky, Y_ {m},}$${\ displaystyle A}$${\ displaystyle n}$${\ Displaystyle \ forall x_ {1} \ cdots \, \ forall x_ {n} [(x_ {1}, \ dots, x_ {n}) \ in A \ iff \ phi (x_ {1}, \ dots, x_ {n}, Y_ {1}, \ tečky, Y_ {m})].}$

Nastavte axiomy

Axiomy párování a pravidelnosti, které byly potřebné pro důkaz věty o existenci třídy, byly uvedeny výše. NBG obsahuje další čtyři sady axiomů. Tři z těchto axiomů se zabývají operacemi třídy aplikovanými na sady.

Definice.   je funkce, pokud${\ displaystyle F}$${\ Displaystyle F \ subseteq V^{2} \ land \ forall x \, \ forall y \, \ forall z \, [(x, y) \ in F \, \ land \, (x, z) \ in F \ implikuje y = z].}$

V teorii množin definice funkce nevyžaduje zadání domény nebo codomény funkce (viz Funkce (teorie množin) ). Definice funkce NBG generalizuje definici ZFC ze sady uspořádaných párů na třídu uspořádaných párů.

Definice ZFC nastavených operací image , union a power set jsou také zobecněny na operace třídy. Obraz třídy pod funkcí je Tato definice nevyžaduje, aby Sjednocení třídy bylo Mocenská třída je Rozšířená verze věty o existenci třídy předpokládá existenci těchto tříd. Axiomy nahrazení, spojení a energetické sady naznačují, že když jsou tyto operace aplikovány na sady, vytvářejí sady. ${\ displaystyle A}$${\ displaystyle F}$${\ Displaystyle F [A] = \ {y: \ existuje x (x \ in A \, \ land \, (x, y) \ in F) \}.}$${\ displaystyle A \ subseteq Dom (F).}$${\ displaystyle A}$${\ Displaystyle \ cup A = \ {x: \ existuje y (x \ in y \, \, \ land \, y \ in A) \}.}$${\ displaystyle A}$${\ displaystyle {\ mathcal {P}} (A) = \ {x: x \ subseteq A \}.}$

Axiom nahrazení.  Pokud je funkce, a je soubor, pak se obraz z nedostatečně , je množina. ${\ displaystyle F}$${\ displaystyle a}$${\ displaystyle F [a]}$${\ displaystyle a}$${\ displaystyle F}$

${\ Displaystyle \ forall F \, \ forall a \, [F {\ text {is a function}} \ \ implies \ neexistuje b \, \ forall y \, (y \ in b \ iff \ existuje x (x \ in a \, \ land \, (x, y) \ in F))].}$

Nemít požadavek v definici produkuje silnější axiom nahrazení, který je použit v následujícím důkazu. ${\ displaystyle A \ subseteq Dom (F)}$${\ displaystyle F [A]}$

Věta ( axiom separace NBG ).  If is a set and is a subclass of then is a set. Důkaz: Třída Existence teorém konstruuje omezení na funkce identity na : Vzhledem k tomu, obraz nedostatečně je , axióm náhrady znamená, že je soubor. Tento důkaz závisí na definici obrázku, který nemá požadavek, protože spíše než${\ displaystyle a}$${\ displaystyle B}$${\ displaystyle a,}$${\ displaystyle B}$
 ${\ displaystyle B}$${\ Displaystyle I {\ upharpoonright _ {B}} = \ {(x_ {1}, x_ {2}): x_ {1} \ in B \ land x_ {2} = x_ {1} \}.}$${\ displaystyle a}$${\ displaystyle I {\ upharpoonright _ {B}}}$${\ displaystyle B}$${\ displaystyle B}$${\ displaystyle a \ subseteq Dom (F)}$${\ displaystyle Dom (I {\ upharpoonright _ {B}}) = B \ subseteq a}$${\ Displaystyle a \ subseteq Dom (I {\ upharpoonright _ {B}}).}$

Axiom spojení.  Pokud je to sada, pak existuje sada obsahující${\ displaystyle a}$${\ Displaystyle \ cup a.}$

${\ Displaystyle \ forall a \, \ existuje b \, \ forall x \, [\, \ existuje y (x \ in y \, \, \ land \, y \ in a) \ implikuje x \ in b \, ].}$

Sada axiomů síly.  Pokud je to sada, pak existuje sada obsahující${\ displaystyle a}$${\ displaystyle {\ mathcal {P}} (a).}$

${\ Displaystyle \ forall a \, \ existuje b \, \ forall x \, (x \ subseteq a \ implies x \ in b).}$

Teorém.  Pokud je množina, pak a jsou sady. Důkaz: Axiom unie uvádí, že je podtřídou množiny , takže axiom oddělení znamená, že je množina. Stejně tak axiom mocenské množiny uvádí, že je podtřídou množiny , takže z axiomu separace vyplývá, že jde o množinu. ${\ displaystyle a}$${\ Displaystyle \ cup a}$${\ displaystyle {\ mathcal {P}} (a)}$
 ${\ Displaystyle \ cup a}$${\ displaystyle b}$${\ Displaystyle \ cup a}$${\ displaystyle {\ mathcal {P}} (a)}$${\ displaystyle b}$${\ displaystyle {\ mathcal {P}} (a)}$

Axiom nekonečna.  Existuje neprázdná množina taková, že pro všechny oblasti , existuje v takové, že je vlastní podmnožina . ${\ displaystyle a}$${\ displaystyle x}$${\ displaystyle a}$${\ displaystyle y}$${\ displaystyle a}$${\ displaystyle x}$${\ displaystyle y}$

${\ Displaystyle \ existuje a \, [\ neexistuje podmnožina y))].}$

Axiomy nekonečna a nahrazení dokazují existenci prázdné množiny . V diskusi o axiomech existence třídy byla prokázána existence prázdné třídy . Nyní dokážeme, že jde o sadu. Nechť funkce a nechť je množina daná axiómem nekonečna. Nahrazením je obraz pod , který se rovná , množinou. ${\ displaystyle \ emptyset}$${\ displaystyle \ emptyset}$${\ Displaystyle F = \ emptyset}$${\ displaystyle a}$${\ displaystyle a}$${\ displaystyle F}$${\ displaystyle \ emptyset}$

NBG je axiom nekonečna je naznačeno ZFC je axiom nekonečna : První konjunkci ZFC je axiom, implikuje první konjunkci s NBG je axiom. Druhé spojení axiomu ZFC , znamená druhé spojení axiomu NBG, protože k prokázání axiomu nekonečna ZFC z axiomu nekonečna NBG je zapotřebí některých dalších axiomů NBG (viz Slabý axiom nekonečna ). ${\ Displaystyle \, \ existuje a \, [\ emptyset \ in a \, \ land \, \ forall x (x \ in a \ implies x \ cup \ {x \} \ in a)]. \,}$${\ displaystyle \ emptyset \ in a}$${\ Displaystyle \ forall x (x \ in a \ implies x \ cup \ {x \} \ in a)}$${\ Displaystyle x \ subset x \ cup \ {x \}.}$

Axiom globální volby

Koncept třídy umožňuje NBG mít silnější axiom volby než ZFC. Volba funkce je funkce definovaná na množině všech neprázdných množin taková, že pro všechny ZFC je axiom výběru států, které existuje volba funkce pro každou sadu neprázdných sad. Funkce globální volby je funkce definovaná pro třídu všech neprázdných množin tak, že pro každou neprázdnou množinu Axiom globální volby uvádí, že existuje funkce globální volby. Tento axiom znamená, ZFC je axiom výběru, protože pro každou sadu z neprázdných sad, (dále jen omezení z k ) je funkce, volba v roce 1964, William B. Easton ukázala, že globální volba je silnější než axiomu výběru pomocí nutí k výstavbě model, který splňuje axiom volby a všechny axiomy NBG kromě axiomu globální volby. Axiom globální volby je ekvivalentní každé třídě s dobře uspořádaným, zatímco axiom volby ZFC je ekvivalentní každé sadě s dobře uspořádaným. ${\ displaystyle f}$${\ displaystyle s}$${\ Displaystyle f (x) \ in x}$${\ Displaystyle x \ in s.}$${\ displaystyle G}$${\ Displaystyle G (x) \ in x}$${\ displaystyle x.}$${\ displaystyle s}$${\ displaystyle G \ vert _ {s}}$${\ displaystyle G}$${\ displaystyle s}$${\ Displaystyle s.}$

Axiom globální volby.  Existuje funkce, která vybírá prvek z každé neprázdné sady.

${\ Displaystyle \ existuje G \, [G {\ text {is a function}} \, \ land \ forall x (x \ neq \ emptyset \ implises \ existence y (y \ in x \ land (x, y) \ v G))].}$

Dějiny

Von Neumannův systém axiomu z roku 1925

Von Neumann publikoval úvodní článek o svém systému axiomů v roce 1925. V roce 1928 poskytl podrobné zpracování svého systému. Von Neumann založil svůj systém axiomu na dvou doménách primitivních objektů: funkcích a argumentech. Tyto domény se překrývají-objekty, které jsou v obou doménách, se nazývají argumentové funkce. Funkce odpovídají třídám v NBG a funkce argumentů odpovídají množinám. Von Neumannova primitivní operace je aplikace funkcí , označovaná spíše [ a ,  x ] než a ( x ), kde a je funkce a x je argument. Tato operace vytváří argument. Von Neumann je definováno tříd i sestav s využitím funkce a argumentů-funkce, které berou pouze dvě hodnoty, A a B . Ten je definován x  ∈  pokud [ ,  x ] ≠  .

Von Neumannova práce v teorii množin byla ovlivněna články Georga Cantora , axiomy Ernsta Zermela z roku 1908 pro teorii množin a kritikou Zermelovy teorie množin z roku 1922, které byly dány nezávisle Abrahamem Fraenkelem a Thoralfem Skolemem . Oba Fraenkel a Skolem poukázal na to, že Zermelo axiomy nemohou prokázat existenci množiny { Z ₀ ,  Z ₁ ,  Z ₂ , ...}, kde Z ₀ je množina přirozených čísel a Z _{n +1} je k napájení sadu z Z _n . Poté zavedli axiom nahrazení, který by zaručoval existenci takovýchto sad. Oni se zdráhali přijmout tento axiom: Fraenkel prohlásil, „že nahrazení bylo příliš silným axiomem pro„ obecnou teorii množin ““, zatímco „Skolem pouze napsal, že“ můžeme zavést „nahrazení“.

Von Neumann pracoval na problémech teorie množin Zermelo a poskytl řešení pro některé z nich:

• Teorie ordinals
  • Problém: Cantorovu teorii pořadových čísel nelze v teorii množin Zermelo rozvíjet, protože postrádá axiom nahrazení.
  • Řešení: Von Neumann obnovil Cantorovu teorii definováním řadových řad pomocí množin, které jsou dobře uspořádány vztahem ∈, a pomocí axiomu nahrazení k prokázání klíčových vět o řadových řadách, jako je každá dobře uspořádaná množina řádově izomorfní s ordinálem. Na rozdíl od Fraenkela a Skolema von Neumann zdůraznil, jak důležitý je náhradní axiom pro teorii množin: „Ve skutečnosti se domnívám, že bez tohoto axiomu není vůbec možná žádná teorie pořadových čísel.“
• Kritérium identifikující třídy, které jsou příliš velké na to, aby mohly být nastaveny
  • Problém: Zermelo takové kritérium neposkytlo. Jeho teorie množin se vyhýbá velkým třídám, které vedou k paradoxům , ale vynechává mnoho množin, například tu, kterou zmiňují Fraenkel a Skolem.
  • Řešení: Von Neumann zavedl kritérium: Třída je příliš velká na to, aby byla množinou, a to pouze tehdy, pokud ji lze namapovat na třídu V všech sad. Von Neumann si uvědomil, že set-teoretickým paradoxům lze zabránit tím, že nedovolíme, aby tak velké třídy byly členy jakékoli třídy. Kombinací tohoto omezení s jeho kritéria, získal svůj axiom omezené velikosti : A třída C není členem žádné skupiny tehdy a jen tehdy, pokud C mohou být mapovány do V. .
• Konečná axiomatizace
  • Problém: Zermelo použil ve svém axiomu oddělení nepřesný koncept „určité výrokové funkce “ .
  • Řešení: Skolem představil axiomové schéma separace, které bylo později použito v ZFC, a Fraenkel představil ekvivalentní řešení. Zermelo však oba přístupy odmítl „zejména proto, že implicitně zahrnují koncept přirozeného čísla, který by podle Zermelova názoru měl být založen na teorii množin“. Von Neumann se vyhnul schématům axiomu formalizací konceptu „určité výrokové funkce“ svými funkcemi, jejichž konstrukce vyžaduje jen konečný počet axiomů. To vedlo k tomu, že jeho teorie množin měla konečně mnoho axiomů. V roce 1961 Richard Montague dokázal, že ZFC nelze definitivně axiomatizovat.
• Axiom pravidelnosti
  • Problém: Teorie množin Zermelo začíná prázdnou sadou a nekonečnou sadou a iteruje axiomy párování, sjednocení, sady sil, separace a možnosti generování nových sad. Neomezuje však sady na tyto. Umožňuje například sady, které nejsou podložené , například množina x vyhovující x  ∈  x .
  • Řešení: Fraenkel zavedl axiom k vyloučení těchto sad. Von Neumann analyzoval Fraenkelův axiom a uvedl, že nebyl „přesně formulován“, ale přibližně by řekl: „Kromě množin ... jejichž existenci axiomy absolutně vyžadují, neexistují žádné další množiny.“ Von Neumann navrhl axiom pravidelnosti jako způsob, jak vyloučit nepodložené množiny, ale nezahrnul jej do svého systému axiomů. V roce 1930 se Zermelo stal prvním, kdo publikoval systém axiomů, který zahrnoval pravidelnost.

Von Neumannův systém axiomu z roku 1929

V roce 1929 publikoval von Neumann článek obsahující axiomy, které by vedly k NBG. Tento článek byl motivován jeho obavou o konzistentnost axiomu omezení velikosti. Uvedl, že tento axiom „dělá hodně, vlastně příliš mnoho“. Kromě implikování axiomů separace a nahrazení a dobře uspořádané věty také znamená, že každá třída, jejíž mohutnost je menší než V, je množina. Von Neumann si myslel, že tato poslední implikace přesahuje kantorskou teorii množin, a dospěl k závěru: „Musíme tedy diskutovat o tom, zda její konzistence [axiomu] není ještě problematičtější než axiomatizace teorie množin, která nepřekračuje nezbytný kantorský rámec.“

Von Neumann zahájil vyšetřování konzistence zavedením svého axiomatického systému z roku 1929, který obsahuje všechny axiomy jeho axiomového systému z roku 1925 kromě axiomu omezení velikosti. Tento axiom nahradil dvěma jeho důsledky, axiomem nahrazení a axiomem volby. Von Neumannův axiom výběru uvádí: „Každý vztah R má podtřídu, která je funkcí se stejnou doménou jako R. “

Nechť S je von Neumannův systém axiomu z roku 1929. Von Neumann představil systém axiomu S + pravidelnost (který se skládá ze S a axiomu pravidelnosti), aby prokázal, že jeho systém z roku 1925 je ve srovnání s S konzistentní . Dokázal:

1. Pokud je S konzistentní, pak je S + pravidelnost konzistentní.
2. S + Pravidelnost znamená axiom omezení velikosti. Protože toto je jediný axiom jeho systému axiomu 1925, který S + pravidelnost nemá, S + pravidelnost implikuje všechny axiomy jeho systému 1925.

Tyto výsledky naznačují: Je -li S konzistentní, pak von Neumannův systém axiomu z roku 1925 je konzistentní. Důkaz: Pokud je S konzistentní, pak je S + pravidelnost konzistentní (výsledek 1). Pomocí důkazu rozporem předpokládejme, že systém axiomu 1925 je nekonzistentní nebo ekvivalentně: systém axiomu 1925 implikuje rozpor. Protože S + pravidelnost implikuje axiomy systému 1925 (výsledek 2), S + pravidelnost také znamená rozpor. To však odporuje konzistenci pravidelnosti S +. Pokud je tedy S konzistentní, pak von Neumannův axiový systém z roku 1925 je konzistentní.

Protože S je jeho systém axiomu 1929, von Neumannův systém axiomu 1925 je konzistentní vzhledem k jeho systému axiomu 1929, který je bližší kantorské teorii množin. Hlavní rozdíly mezi kantorskou teorií množin a systémem axiomu 1929 jsou třídy a von Neumannův axiom. Axiomový systém S + Pravidelnost upravili Bernays a Gödel, aby vytvořil ekvivalentní axiomatický systém NBG.

Bernayův axiový systém

V roce 1929 Paul Bernays začal upravovat von Neumannův nový axiomový systém tím, že třídy a množiny bral jako primitivy. Své dílo publikoval v sérii článků z let 1937 až 1954. Bernays uvedl, že:

Účelem úpravy systému von Neumann je zůstat blíže struktuře původního systému Zermelo a současně využívat některé ze set-teoretických konceptů Schröderovy logiky a Principia Mathematica, které se logikům staly známými. Jak bude zřejmé, z tohoto uspořádání vyplývá značné zjednodušení.

Bernays zpracovával sady a třídy logikou se dvěma třídami a zavedl dvě primitiva členství: jedno pro členství v sadách a jedno pro členství ve třídách. Těmito primitivy přepsal a zjednodušil von Neumannovy axiomy z roku 1929. Bernays také zahrnoval axiom pravidelnosti do svého systému axiomů.

Gödelův axiový systém (NBG)

V roce 1931 poslal Bernays Kurtovi Gödelovi dopis obsahující jeho teorii množin . Gödel Bernaysovu teorii zjednodušil tím, že z každé sady udělal třídu, což mu umožnilo použít pouze jeden druh a jedno primitivum členství. Oslabil také některé Bernaysovy axiomy a nahradil von Neumannův axiom výběru ekvivalentním axiomem globální volby. Gödel použil své axiomy ve své monografii z roku 1940 o relativní konzistenci globální volby a zobecněné hypotéze kontinua.

Pro Gödela bylo pro jeho monografii uvedeno několik důvodů:

• Gödel uvedl matematický důvod - globální volba NBG vytváří silnější teorii konzistence: „Tato silnější forma axiomu [volby], pokud je v souladu s ostatními axiomy, samozřejmě znamená, že slabší forma je také konzistentní.“
• Robert Solovay usoudil: „Hádám, že si [Gödel] přál vyhnout se diskusi o technikách zapojených do vývoje základů modelové teorie v rámci axiomatické teorie množin.“
• Kenneth Kunen uvedl důvod, proč se Gödel této diskusi vyhnul: „Existuje také mnohem kombinatoričtější přístup k L [ konstruktivnímu vesmíru ], který vyvinul ... [Gödel ve své monografii z roku 1940] ve snaze vysvětlit svou práci ne- logici ... Tento přístup má zásluhu na odstranění všech zbytků logiky z léčby L. “
• Charles Parsons poskytl filozofický důvod pro Gödelovu volbu: „Tento pohled [že‚ vlastnost množiny ‘je primitivem teorie množin] se může odrazit v Gödelově volbě teorie s třídními proměnnými jako rámcem pro ... [jeho monografie] . "

Gödelův úspěch spolu s podrobnostmi jeho prezentace vedl k výtečnosti, které by se NBG těšilo po další dvě desetiletí. V roce 1963 Paul Cohen prokázal své důkazy nezávislosti pro ZF pomocí některých nástrojů, které Gödel vyvinul pro své důkazy relativní konzistence pro NBG. Později se ZFC stalo populárnějším než NBG. To bylo způsobeno několika faktory, včetně dodatečné práce potřebné k zvládnutí nucení v NBG, Cohenova prezentace nucení z roku 1966, která používala ZF, a důkaz, že NBG je konzervativní rozšíření ZFC.

NBG, ZFC a MK

NBG není logicky ekvivalentní ZFC, protože jeho jazyk je výraznější: může vytvářet prohlášení o třídách, které v ZFC nelze dělat. NBG a ZFC však znamenají stejná prohlášení o sadách. Proto je NBG konzervativní rozšíření ZFC. NBG implikuje věty, které ZFC neznamená, ale protože NBG je konzervativní rozšíření, tyto věty musí zahrnovat správné třídy. Například, to je teorém NBG, že globální axiom výběru znamená, že pořádná třída V může být dobře-objednal a že každá pořádná třída může být uveden do one-to-one korespondence s V. .

Jedním důsledkem konzervativního rozšíření je, že ZFC a NBG jsou ekvikonzistentní . Dokazování toho využívá princip exploze : z rozporu je vše prokazatelné. Předpokládejme, že ZFC nebo NBG jsou nekonzistentní. Pak nekonzistentní teorie implikuje protichůdná tvrzení ∅ = ∅ a ∅ ≠ ∅, což jsou tvrzení o množinách. Podle konzervativní vlastnosti extenze tato teorie implikuje i další teorie. Proto je také nekonzistentní. Přestože je NBG výraznější, je v souladu se ZFC. Tento výsledek spolu s von Neumannovým důkazem relativní konzistence z roku 1929 naznačuje, že jeho axiomový systém z roku 1925 s axiómem omezení velikosti je v souladu s ZFC. To zcela vyřeší von Neumannovo znepokojení nad relativní konzistencí tohoto mocného axiomu, protože ZFC je v kantorském rámci.

I když je NBG konzervativní rozšíření ZFC, věta může mít v NBG kratší a elegantnější důkaz než v ZFC (nebo naopak). Přehled známých výsledků této povahy viz Pudlák 1998 .

Morse – Kelleyova teorie množin má axiomatické schéma třídního porozumění, které zahrnuje vzorce, jejichž kvantifikátory se pohybují nad třídami. MK je silnější teorie než NBG, protože MK dokazuje konzistenci NBG, zatímco Gödelova druhá věta o neúplnosti naznačuje, že NBG nemůže prokázat konzistenci NBG.

Diskuse o některých ontologických a dalších filozofických problémech, které NBG představuje, zvláště v kontrastu se ZFC a MK, najdete v příloze C Potter 2004 .

Modely

ZFC, NBG a MK mají modely popsatelné z hlediska kumulativní hierarchie V _α  a konstruovatelné hierarchie L _α  . Nechť V hotelu je nedosažitelný kardinál mítK, ať X ⊆ V _κ , a nechat Def ( X ) označuje třídu prvního řádu definovatelných podmnožiny z X s parametry. V symbolech, kde " " označuje model s doménou a vztahem , a " " označuje vztah spokojenosti : ${\ displaystyle (X, \ in)}$ ${\ displaystyle X}$${\ displaystyle \ in}$${\ displaystyle \ models}$

${\ displaystyle \ operatorname {Def} (X): = {\ Bigl \ {} \ {x \ mid x \ in X {\ text {and}} (X, \ in) \ models \ phi (x, y_ { 1}, \ ldots, y_ {n}) \}: \ phi {\ text {je vzorec prvního řádu a}} y_ {1}, \ ldots, y_ {n} \ v X {\ Bigr \}} .}$

Pak:

• ( V _κ , ∈) a ( L _κ , ∈) jsou modely ZFC .
• ( V _κ ,  V _κ+1 , ∈) je model MK, kde V _{κ se} skládá ze sad modelu a V _{κ+1 se} skládá z tříd modelu. Protože model MK je modelem NBG, je tento model také modelem NBG.
• ( V _κ , Def ( V _κ ), ∈) je model Mendelsonovy verze NBG, který nahrazuje axiom globální volby NBG za axiom volby ZFC. Axiomy ZFC jsou v tomto modelu pravdivé, protože ( V _κ , ∈) je model ZFC. Platí zejména axiom volby ZFC, ale globální volba NBG může selhat. Axiomy existence třídy NBG jsou v tomto modelu pravdivé, protože třídy, jejichž existenci tvrdí, mohou být definovány definicemi prvního řádu. Axiom členství například platí, protože třídu definuje:${\ displaystyle E}$

${\ Displaystyle E = \ {x \ in V _ {\ kappa} :( V _ {\ kappa}, \ in) \ models \ neexistuje u \ \ existuje v [x = (u, v) \ land u \ in v] \}.}$

• ( L _κ , L _{κ ⁺} , ∈), kde κ ⁺ je nástupnickým kardinálem κ, je modelem NBG. Axiomy existence třídy NBG jsou pravdivé v ( L _κ ,  L _{κ ⁺} , ∈). Axiom členství například platí, protože třídu definuje:${\ displaystyle E}$

${\ Displaystyle E = \ {x \ in L _ {\ kappa} :( L _ {\ kappa}, \ in) \ models \ neexistuje u \ \ existuje v [x = (u, v) \ land u \ in v] \}.}$

Takže E  ∈ 𝒫 ( L _κ ). Ve svém důkazu, že GCH je pravdivý v L , Gödel dokázal, že 𝒫 ( L _κ ) ⊆  L _{κ ⁺} . Proto E  ∈  L _{κ ⁺} , takže axiom členství platí v ( L _κ ,  L _{κ ⁺} , ∈). Podobně jsou pravdivé axiomy ostatních tříd. Axiom globální volby je pravda, protože L _κ je dobře nařízeno omezení z funkce Gödel (který mapuje třídu ordinals na constructible sad) na řadové méně než mítK. Proto ( L _κ ,  L _{κ ⁺} , ∈) je model NBG.

Teorie kategorie

Ontologie NBG poskytuje lešení pro mluvení o „velkých objektech“, aniž by riskoval paradox. Například v některých vývojech teorie kategorií je „ velká kategorie “ definována jako ta, jejíž předměty a morfismy tvoří správnou třídu. Na druhé straně „malá kategorie“ je kategorie, jejíž předměty a morfismy jsou členy množiny. Můžeme tedy hovořit o „ kategorii všech sad “ nebo „ kategorii všech malých kategorií “, aniž bychom riskovali paradox, protože NBG podporuje velké kategorie.

NBG však nepodporuje „kategorii všech kategorií“, protože členy by byly velké kategorie a NBG neumožňuje řádným třídám být členy čehokoli. Ontologickým rozšířením, které nám umožňuje formálně hovořit o takové „kategorii“, je konglomerát , což je soubor tříd. Poté je „kategorie všech kategorií“ definována jejími objekty: konglomerátem všech kategorií; a jeho morfismy: konglomerát všech morfismů od A do B, kde A a B jsou objekty. O tom, zda je ontologie zahrnující třídy a sady adekvátní pro teorii kategorií, viz Muller 2001 .

Poznámky

Reference

Bibliografie

• Adámek, Jiří; Herrlich, Horst; Strecker, George E. (1990), Abstrakt a konkrétní kategorie (Radost koček) (1. vyd.), New York: Wiley & Sons, ISBN 978-0-471-60922-3.
  • Adámek, Jiří; Herrlich, Horst; Strecker, George E. (2004) [1990], Abstrakt a konkrétní kategorie (Radost koček) (Dover ed.), New York: Dover Publications, ISBN 978-0-486-46934-8.
• Bernays, Paul (1937), „A System of Axiomatic Set Theory — Part I“, The Journal of Symbolic Logic , 2 (1): 65–77, doi : 10,2307/2268862 , JSTOR  2268862.
• Bernays, Paul (1941), „A System of Axiomatic Set Theory — Part II“, The Journal of Symbolic Logic , 6 (1): 1–17, doi : 10.2307/2267281 , JSTOR  2267281.
• Bernays, Paul (1991), Axiomatická teorie množin (2. přepracované vydání.), Dover Publications, ISBN 978-0-486-66637-2.
• Bourbaki, Nicolas (2004), Elements of Mathematics: Theory of Sets , Springer, ISBN 978-3-540-22525-6.
• Chuaqui, Rolando (1981), Axiomatická teorie množin: Impredikativní teorie tříd , Severní Holandsko, ISBN 0-444-86178-5.* Cohen, Paul (1963), „The Independence of the Continuum Hypothesis“, Proceedings of the National Academy of Sciences of the United States of America , 50 (6): 1143–1148, Bibcode : 1963PNAS ... 50.1143C , doi : 10,1073/pnas.50.6.1143 , PMC  221287 , PMID  16578557.
• Cohen, Paul (1966), Teorie množin a hypotéza kontinua , WA Benjamin.
  • Cohen, Paul (2008), Teorie množin a hypotéza kontinua , Dover Publications, ISBN 978-0-486-46921-8.
• Dawson, John W. (1997), Logical dilemmas: The life and work of Kurt Gödel , Wellesley, MA: AK Peters.
• Easton, William B. (1964), Powers of Regular Cardinals (disertační práce), Princeton University.
• Felgner, Ulrich (1971), „Srovnání axiomů místní a univerzální volby“ (PDF) , Fundamenta Mathematicae , 71 : 43–62 , doi : 10,4064/fm-71-1-43-62.
• Ferreirós, José (2007), Labyrint myšlenky: Historie teorie množin a její role v matematickém myšlení (2. přepracované vydání), Basilej, Švýcarsko: Birkhäuser, ISBN 978-3-7643-8349-7.
• Gödel, Kurt (1940), The Consistency of the Axiom of Choice and of the Generalalized Continuum Hypototh with the Axioms of Set Theory (Revised ed.), Princeton University Press, ISBN 978-0-691-07927-1.
  • Gödel, Kurt (2008), Konzistence axiomu volby a zobecněné hypotézy kontinua s axiomy teorie množin , s předmluvou Laver, Richard (Paperback ed.), Ishi Press, ISBN 978-0-923891-53-4.
• Gödel, Kurt (1986), Collected Works, Volume 1: Publications 1929–1936 , Oxford University Press, ISBN 978-0-19-514720-9.
• Gödel, Kurt (1990), Collected Works, Volume 2: Publications 1938-1974 , Oxford University Press, ISBN 978-0-19-514721-6.
• Gödel, Kurt (2003), Collected Works, Volume 4: Correspondence A – G , Oxford University Press, ISBN 978-0-19-850073-5.
• Gray, Robert (1991), "Počítačové programy a matematické důkazy", The Mathematical Intelligencer , 13 (4): 45–48, doi : 10.1007/BF03028342 , S2CID  121229549.
• Hallett, Michael (1984), kantorská teorie množin a omezení velikosti (vázaná ed.), Oxford: Clarendon Press, ISBN 978-0-19-853179-1.
  • Hallett, Michael (1986), kantorská teorie množin a omezení velikosti (brožovaná ed.), Oxford: Clarendon Press, ISBN 978-0-19-853283-5.
• Kanamori, Akihiro (2009b), The Higher Infinite: Large Cardinals in Set Theory from their Beginnings , Springer, ISBN 978-3-540-88867-3.
• Kanamori, Akihiro (2009), „Bernays and The Theory“ (PDF) , Bulletin of Symbolic Logic , 15 (1): 43–69, doi : 10,2178/bsl/1231081769 , JSTOR  25470304 , S2CID  15567244.
• Kanamori, Akihiro (2012), „In Praise of Replacement“ (PDF) , Bulletin of Symbolic Logic , 18 (1): 46–90, doi : 10.2178/bsl/1327328439 , JSTOR  41472440 , S2CID  18951854.
• Kunen, Kenneth (1980), The Set Theory: An Introduction to Independence Proofs (Hardcover ed.), North-Holland, ISBN 978-0-444-86839-8.
  • Kunen, Kenneth (2012), The Set Theory: An Introduction to Independence Proofs (Paperback ed.), North-Holland, ISBN 978-0-444-56402-3.
• Mendelson, Elliott (1997), An Introduction to Mathematical Logic (4th ed.), London: Chapman and Hall/CRC, ISBN 978-0-412-80830-2. - Pp. 225–86 obsahují klasické učebnicové zpracování NBG, které ukazuje, jak plní to, co od teorie množin očekáváme, a to pomocí uzemňovacích vztahů , teorie řádu , pořadových čísel , transfinitních čísel atd.
• Mirimanoff, Dmitry (1917), „Les antinomies de Russell et de Burali-Forti et le problème fundamentální de la théorie des ensembles“, L'Enseignement Mathématique , 19 : 37–52.
• Montague, Richard (1961), „Sémantické uzavření a nefinitní axiomatizovatelnost I“, in Buss, Samuel R. (ed.), Infinitistic Methods: Proceedings of the Symposium on Foundations of Mathematics , Pergamon Press, pp. 45–69.
• Mostowski, Andrzej (1950), „Některé impresivní definice v teorii axiomatických množin“ (PDF) , Fundamenta Mathematicae , 37 : 111–124, doi : 10,4064/fm-37-1-111-124.
• Muller, FA (1. září 2001), „Sady, třídy a kategorie“ (PDF) , British Journal for the Philosophy of Science , 52 (3): 539–73, doi : 10,1093/bjps/52.3.539.
• Müller, Gurt, ed. (1976), Sady a třídy: O díle Paula Bernayse , Studie logiky a základy matematiky Svazek 84, Amsterdam: Severní Holandsko, ISBN 978-0-7204-2284-9.
• Potter, Michael (2004), Teorie množin a její filozofie: Kritický úvod (vázaná ed.), Oxford University Press, ISBN 978-0-19-926973-0.
  • Potter, Michael (2004p), Teorie množin a její filozofie: Kritický úvod (brožovaná ed.), Oxford University Press, ISBN 978-0-19-927041-5.
• Pudlák, Pavel (1998), „The Longs of Proofs“ (PDF) , in Buss, Samuel R. (ed.), Handbook of Proof Theory , Elsevier, s. 547–637, ISBN 978-0-444-89840-1.
• Smullyan, Raymond M .; Fitting, Melvin (2010) [Upravené a opravené vydání: poprvé publikováno v roce 1996 nakladatelstvím Oxford University Press], The Set Theory and the Continuum Problem , Dover, ISBN 978-0-486-47484-7.
• Solovay, Robert M. (1990), „Úvod do roku 1938 , 1939 , 1939a a 1940 “, Kurt Gödel Collected Works, Volume 2: Publications 1938–1974 , Oxford University Press, s. 1–25, ISBN 978-0-19-514721-6.
• von Neumann, John (1923), „Zur Einführung der transfiniten Zahlen“ , Acta Litt. Akadem. Sc. Szeged X. , 1 : 199–208.
  • Anglický překlad: van Heijenoort, Jean (2002a) [1967], „O zavedení transfinitních čísel“ , From Frege to Gödel: A Source Book in Mathematical Logic, 1879-1931 (Fourth Printing ed.), Harvard University Press, pp . 346–354, ISBN 978-0-674-32449-7.
  • Anglický překlad: van Heijenoort, Jean (2002b) [1967], „An axiomatization of set theory“ , From Frege to Gödel: A Source Book in Mathematical Logic, 1879-1931 (Fourth Printing ed.), Harvard University Press, pp. 393–413, ISBN 978-0-674-32449-7.
• von Neumann, John (1925), „Eine Axiomatisierung der Mengenlehre“ , Journal für die Reine und Angewandte Mathematik , 154 : 219–240.
• von Neumann, John (1928), „Die Axiomatisierung der Mengenlehre“ , Mathematische Zeitschrift , 27 : 669–752, doi : 10,1007/bf01171122 , S2CID  123492324.
• von Neumann, John (1929), „Über eine Widerspruchsfreiheitsfrage in der axiomatischen Mengenlehre“ , Journal für die Reine und Angewandte Mathematik , 160 : 227–241.

externí odkazy

• „von Neumann-Bernays-Gödel teorie množin“ . PlanetMath .
• Szudzik, Matthew. „von Neumann-Bernays-Gödel Theory Setory“ . MathWorld .