Extensionality axiom je jedním z klíčových axiomů většiny nastavených teorií , zejména Zermelo a Zermelo-Fraenkel (ZF) teorie množin . V zásadě uvádí, že stačí ověřit, že dvě sady mají stejné prvky, aby se ukázalo, že tyto dvě sady jsou stejné , v tom smyslu, že mají stejné vlastnosti , žádná vlastnost neumožňuje odlišit jednu sadu od druhé. Přesněji řečeno, tvrdí, že ať už definujeme množinu jakkoli, záleží pouze na jejím rozšíření , prvcích, které k němu patří, a nikoli na způsobu, jakým byla definována.
Tento axiom se může zdát zřejmý intuitivnímu pojetí množiny, ale má důležité důsledky pro složitost rovnosti v teorii. K ověření rovnosti dvou množin je vedena jedna, například kvůli schématu axiomů porozumění , k ověření rovnocennosti mezi výroky libovolné složitosti, přičemž tato výroky samy mohou využívat rovnost mezi množinami (připomeňme, že jsou pouze sady v obvyklých teoriích sad).
Axiom je tedy úzce spjat s pojmem rovnosti dvou množin. Umožňuje ukázat jedinečnost množin charakterizovaných údaji jejich prvků, jako je prázdná množina , singletony , páry , množina částí množiny…
Rovnost lze do teorie množin zavést různými způsoby. V současné době je nejčastěji považován za primitivní vztah, axiomatizovaný na logické úrovni. Teorie množin je potom teorií uvedenou v jazyce počtu rovnostářských predikátů prvního řádu, postavená na jediném vztahu členství.
V tomto případě zní axiom roztažnosti takto:
∀ A ∀ B [∀ x ( x ∈ A ⇔ x ∈ B ) ⇒ A = B ] .To znamená, že: pokud je každý prvek množiny A také prvkem B a pokud každý prvek množiny B patří do množiny A , pak jsou dvě množiny A a B stejné.
Víme, že inkluze mezi dvěma množinami označenými A ⊂ B nebo A ⊆ B je definována:
A ⊂ B znamená ∀ x ( x ∈ A ⇒ x ∈ B )Dedukujeme proto další formulaci axiomu extenzionality, která je rovněž původní formulací Ernsta Zermela :
( ⊂ B a B ⊂ ) ⇒ = B .Tato poslední formulace ospravedlňuje současné využití dvojité začlenění ukazující kravatu mezi dvěma sadami: ukázat, že dvě sady a B jsou stejné, stačí ukázat, že je součástí B a B je uveden v A .
Konverze je obyčejná vlastnost rovnosti , platí pro jakýkoli binární vztah.
V počtu predikátů (rovnostářském) je základní vlastností rovnosti vlastnost substituce , která je vyjádřena ve formě schématu axiomů (nekonečno axiomů, jeden na vzorec sady počtu predikátů). Vlastnost substituce uvádí, že pokud jsou dva objekty stejné, jakákoli vlastnost kontrolovaná jedním je kontrolována druhým. Jedná se o vlastnosti vyjádřené v jazyce teorie a mohou záviset na možných parametrech a 1 … a p . Více formálně je schéma substitučních axiomů pro rovnost:
∀ a 1 … ∀ a p ∀ x ∀ y [ x = y ⇒ (P x a 1 … a p ⇒ P y a 1 … a p )] pro jakýkoli vzorec P, který neobsahuje jinou volnou proměnnou než x a 1 … A p .(toto schéma axiomů, ke kterým musíme přidat reflexivitu, ∀ x x = x , pak axiomatizuje rovnost, zejména odvodíme symetrii a tranzitivitu).
Vidíme tedy, že obrácení axiomu roztažnosti - pokud jsou dvě množiny stejné, pak mají stejné prvky - je obvyklou vlastností rovnosti, konkrétní případ schématu právě uvedl:
∀ A ∀ B [ A = B ⇒ ∀ x ( x ∈ A ⇔ x ∈ B )] .Axiomatizace rovnosti je formalizace logiky prvního řádu Leibnizovy definice rovnosti : dva objekty jsou si rovny, když mají stejné vlastnosti, řekněme kontraposem, dva objekty se liší, pokud jim vlastnost umožňuje rozlišovat.
Alternativou je zvážit teorii množin v počtu predikátů prvního řádu bez rovnosti a definovat druhou z členství pomocí extenzní rovnosti:
x = y znamená ∀ z ( z ∈ x ⇔ z ∈ y ) ( dvě sady jsou stejné, pokud mají stejné prvky ).Poté musíme uvést axiom, který umožňuje najít obvyklé vlastnosti rovnosti a který se v této souvislosti někdy nazývá axiom prodloužení:
∀ x ∀ y [∀ z ( z ∈ x ⇔ z ∈ y ) ⇒ ∀ u ( x ∈ u ⇔ y ∈ u )] ( pokud mají dvě množiny stejné prvky, pak patří do stejných množin )buď s rozšiřující definicí rovnosti:
∀ x ∀ y [ x = y ⇒ ∀ u ( x ∈ u ⇔ y ∈ u )] .Tento axiom se pak jeví jako konkrétní případ substituční vlastnosti pro rovnost předchozího odstavce, kde kde predikátem ve hře je členství v dané sadě. Definice rozšíření poskytuje další speciální případ:
∀ x ∀ y [ x = y ⇒ ∀ z ( z ∈ x ⇔ z ∈ y )] .Substituční vlastnost pro rovnost je poté prokázána pro jakýkoli predikát indukcí přes délku vzorce, který definuje tento predikát, přičemž dva předchozí konkrétní případy tvoří základní případ.
Axiom extenzionality zajišťuje jedinečnost množin definovaných predikátem, jako je prázdná množina, dvojice dvou daných množin, jejichž existence je přímo potvrzena některými dalšími axiomy nebo je z nich demonstrována.
Vzhledem k tomu, jakýkoli predikát P , jeden z jeho argumentů, který označíme rozlišením x , jsou ostatní, pokud existují, označeny jako 1 ... a p a slouží jako parametry, ne vždy existuje množina A definovaná jako množina objektů x, které splňují P , tj. takové, že pro všechna a 1 ... a p a pro všechna x ,
x ∈ A ⇔ P xa 1 … a str .Předpokládejme, že jsme prokázali existenci takového souboru A . V tomto případě je tato množina A jedinečnou množinou x splňující P : jedinečnost je bezprostředním důsledkem axiomu extenzity.
Potom zavedeme pro takové množiny nebo konstrukce množin určitý symbol, který jej bude označovat, například ∅ pro prázdnou množinu, { a } pro singleton sestavený z a , { a , b } pro dvojici tvořenou a a b . ..
Zavedení těchto nových symbolů ve skutečnosti nemění teorii v následujícím smyslu: věty (vyjádřené bez těchto symbolů) zůstávají stejné, jakýkoli výrok obsahující tyto nové symboly lze nahradit ekvivalentním výrokem, který je neobsahuje. To se ukazuje pomocí vlastností existence a jedinečnosti, díky nimž je bylo možné zavést.
Axiom extenzionality se objevuje v té či oné formě v axiomech teorie množin, což je nejčastěji teorie „extenzionálních množin“. Je však možné se alespoň předem zajímat o ne-extenzní teorie, které mají lepší vlastnosti v teorii důkazů, kvůli složitému „kvocientu“ vyvolanému extenzní rovností.
Axiom musí být přizpůsoben pro teorie množin s prvky ur , které nemají žádné prvky, ale liší se od prázdné množiny.