Tarski-Grothendieck küme teorisi - Tarski–Grothendieck set theory

Tarski-Grothendieck küme teorisi ( TG , matematikçiler Alfred Tarski ve Alexander Grothendieck'in adını almıştır ) bir aksiyomatik küme teorisidir . Bu bir olan olmayan muhafazakar uzatma ait Zermelo-Fraenkel küme kuramı (ZFC) ve eklenmesine diğer aksiyomatik seti teorilerden ayırt edilir Tarski aksiyomuna her set için bir olduğu devletler Grothendieck evren (aşağıya bakınız) ait olduğu. Tarski'nin aksiyomu, erişilemeyen kardinallerin varlığını ima eder ve ZFC gibi geleneksel küme teorilerinden daha zengin bir ontoloji sağlar . Örneğin, bu aksiyomun eklenmesi kategori teorisini destekler .

Mizar sistemi ve Metamath için kullanılması Tarski-Grothendieck küme teorisi delillerinden biçimsel doğrulama .

Aksiyomlar

Tarski-Grothendieck küme teorisi, geleneksel Zermelo-Fraenkel küme teorisi ile başlar ve ardından "Tarski'nin aksiyomunu" ekler. Biz kullanacağız aksiyomlar , tanımlar tarif etmek Mizar ve notasyonu. Mizar'ın temel nesneleri ve süreçleri tamamen resmidir ; aşağıda gayri resmi olarak açıklanmıştır. Önce şunu varsayalım:

• Herhangi bir set verildiğinde , singleton mevcuttur. ${\ displaystyle A}$${\ displaystyle \ {A \}}$
• Herhangi iki küme verildiğinde, bunların sırasız ve sıralı çiftleri mevcuttur.
• Herhangi bir set kümesi verildiğinde, birliği vardır.

TG , aynı zamanda ZFC'nin bir parçası oldukları için geleneksel olan aşağıdaki aksiyomları içerir :

• Aksiyomu ayarla: Ölçülen değişkenler tek başına kümeler üzerinden değişir; her şey bir dizi (aynı ontoloji olarak ZFC ).
• Genişlemenin aksiyomu : Aynı üyelere sahiplerse iki küme aynıdır.
• Düzenlilik aksiyomu : Hiçbir set kendisinin bir üyesi değildir ve döngüsel üyelik zincirleri imkansızdır.
• Değiştirme Axiom şema : Let alanı içinde sınıf fonksiyonu seti olmak . Sonra aralığı içinde (değerleriyle tüm üyeleri için bir ) aynı zamanda bir set. ${\ displaystyle F}$${\ displaystyle A}$${\ displaystyle F}$${\ displaystyle F (x)}$${\ displaystyle x}$${\ displaystyle A}$

Bu ayıran Tarski aksiyomu olan TG diğer aksiyomatik seti teorilerden. Tarski'nin aksiyomu aynı zamanda sonsuzluk , seçim ve güç setinin aksiyomlarını da ima eder . Ayrıca , TG'nin ontolojisinin ZFC gibi geleneksel küme teorilerinden çok daha zengin olması sayesinde erişilemez kardinallerin varlığını da ima eder .

• Tarski'nin aksiyomu (Tarski 1939'dan uyarlanmıştır). Her set için , üyeleri aşağıdakileri içeren bir set vardır : ${\ displaystyle x}$${\ displaystyle y}$

- kendisi; ${\ displaystyle x}$

- her üyenin her alt kümesi ; ${\ displaystyle y}$

- her üyenin güç seti ; ${\ displaystyle y}$

- Her alt kümesi içinde kardinalitesi az daha . ${\ displaystyle y}$${\ displaystyle y}$

Daha resmi:

${\ displaystyle \ forall x \ y [x \ y \ wedge \ forall z \ y ({\ mathcal {P}} (z) \ subseteq y \ wedge {\ mathcal {P}} (z) \ içinde var y) \ wedge \ forall z \ in {\ mathcal {P}} (y) (\ neg (z \ yaklaşık y) \ - z \ y içinde)]}$

" " x'in güç sınıfını ve " " eşit sayılmayı belirtir . Tarski'nin aksiyomunun belirttiği şey (yerelde), her küme için ait olduğu bir Grothendieck evreni olduğudur . ${\ displaystyle {\ mathcal {P}} (x)}$${\ displaystyle \ yaklaşık}$${\ displaystyle x}$

Bu , “evrensel bir set” e çok benziyor - sadece üye olarak güç kümesine ve tüm alt kümelerine sahip olmakla kalmaz, aynı zamanda bu güç kümesinin güç kümesine de sahiptir - üyeleri, güç kümesi alma veya alma işlemleri altında kapalıdır. bir alt küme. Bu, elbette kendisinin bir üyesi olmaması ve tüm kümelerin bir kümesi olmaması dışında "evrensel bir küme" gibidir. Bu, ait olduğu garantili Grothendieck evreni . Ve sonra böyle herhangi birinin kendisi daha da büyük bir “neredeyse evrensel kümenin” bir üyesidir vb. Normalde var olduğunu varsaydığından çok daha fazla seti garanti eden güçlü kardinalite aksiyomlarından biridir. ${\ displaystyle y}$${\ displaystyle x}$${\ displaystyle x}$${\ displaystyle x}$${\ displaystyle y}$

Mizar sisteminde uygulama

TG uygulamasının altında yatan ve mantıksal sözdizimini sağlayan Mizar dili yazılır ve türlerin boş olmadığı varsayılır. Bu nedenle, teorinin üstü kapalı olarak boş olmadığı kabul edilir . Varoluş aksiyomları, örneğin sırasız çiftin varlığı, terim kurucularının tanımıyla dolaylı olarak da uygulanır.

Sistem eşitlik, üyelik koşulu ve aşağıdaki standart tanımları içerir:

• Singleton : Tek üyeli bir set;
• Sırasız çift : İki farklı üyeye sahip bir set. ; ${\ displaystyle \ {a, b \} = \ {b, a \}}$
• Sıralı çift : Küme ; ${\ displaystyle \ {\ {a, b \}, \ {a \} \} = (a, b) \ neq (b, a)}$
• Alt küme : Tüm üyeleri başka bir kümenin üyesi olan bir küme;
• Sendika setlerinin bir dizi : herhangi bir üyesi tüm üyeleri kümesi . ${\ displaystyle Y}$${\ displaystyle Y}$

Metamath'ta Uygulama

Metamath sistemi keyfi yüksek dereceli mantıkları destekler, ancak tipik olarak aksiyomların "set.mm" tanımlarıyla kullanılır. Ax-Groth aksiyomu aşağıdaki gibi Metamath tanımlanır Tarski aksiyomu, ekler:

⊢ ∃y (x ∈ y ∧ ∀z ∈ y (∀w (w ⊆ z → w ∈ y) ∧ ∃w ∈ y ∀v (v ⊆ z → v ∈ w)) ∧ ∀z (z ⊆ y → ( z ≈ y ∨ z ∈ y)))

Ayrıca bakınız

• Boyut sınırlaması aksiyomu

Notlar

Referanslar

• Andreas Blass , IM Dimitriou ve Benedikt Löwe (2007) " Seçme Aksiyomu Olmadan Erişilemeyen Kardinaller ," Fundamenta Mathematicae 194: 179-89.
• Bourbaki Nicolas (1972). "Univers" . In Michael Artin ; Alexandre Grothendieck ; Jean-Louis Verdier (editörler). Séminaire de Géométrie Algébrique du Bois Marie - 1963-64 - Théorie des topos et cohomologie étale des schémas - (SGA 4) - cilt. 1 (Matematik Ders Notları 269 ) (Fransızca). Berlin; New York: Springer-Verlag . s. 185–217. 2003-08-26 tarihinde orjinalinden arşivlendi .
• Patrick Suppes (1960) Aksiyomatik Küme Teorisi . Van Nostrand. Dover yeniden basımı, 1972.
• Tarski, Alfred (1938). "Über unerreichbare Kardinalzahlen" (PDF) . Fundamenta Mathematicae . 30 : 68–89.
• Tarski, Alfred (1939). "Herhangi bir kümenin iyi sıralı alt kümelerinde" (PDF) . Fundamenta Mathematicae . 32 : 176–183.

Dış bağlantılar

• Trybulec, Andrzej, 1989, " Tarski – Grothendieck Küme Teorisi ", Journal of Formalized Mathematics .
• Metamath : " Proof Explorer Ana Sayfası. " Aşağı kaydırarak "Grothendieck'in Aksiyomu" na gidin.
• PlanetMath : " Tarski'nin Aksiyomu "