V matematice je opodstatněný vztah (nazývaný také noetherovský vztah nebo artiniánský vztah ) binární vztah splňující jednu ze dvou následujících podmínek, ekvivalentní podle axiomu závislé volby (slabá verze axiomu volby ):
Opodstatněný řád (nazývaný také noetherovských řád nebo Artinian pořadí ), je pořadí vztah kterém spojená striktní pořadí je opodstatněný vztah.
Jakýkoli opodstatněný vztah je přísně acyklický , to znamená, že jeho přechodné uzavření je přísným řádem. Vztah R je opodstatněný, pokud jeho transitivní uzávěr je to, nebo pokud R je antireflexive a je-li jeho tranzitivní reflexivní uzávěr je opodstatněný pořadí.
Označíme R −1 [ x ] množinu R -antcedentů x .
Následující věta (v Zermelově teorii množin ) nabízí jak třetí ekvivalentní definici dobrého základu, tak zevšeobecnění důkazního principu transfinitní indukcí (na dobrém řádu nebo na ordinálním čísle ), která sama rozšiřuje axiom Peano n o 5 nebo princip indukce (odpovídá obvyklému pořadí na přirozených číslech):
Věta (dobrý základ a opodstatněná indukce ) - Relace R na množině E je opodstatněná právě tehdy, když pro část E rovnou E jako celku stačí, že obsahuje každý prvek, který obsahuje obsahuje všechny R -antancenty.
Formálně: R je opodstatněná pouze v případě, pro každou část P z E ,pokud ∀ x ∈ E ( R -1 [ x ] ⊂ P ⇒ x ∈ P ), pak P = E . DemonstracePředáním doplňku je podmínka příkazu ekvivalentní implikaci
pro jakoukoli část X z E , pokud ∀ x ∈ E ( R −1 [ x ] ∩ X = ∅ ⇒ x ∉ X ), pak X = ∅nebo opět v protikladu :
pro jakoukoli neprázdnou část X z E , ∃ x ∈ X ( R −1 [ x ] ∩ X = ∅),který vyjadřuje stejně jako pro všechny neprázdné podmnožiny X o E , existuje prvek x o X s žádný R -antécédent v X .
Podobně, druhá věta (v Zermelo-Fraenkel teorie množin , tedy s nahrazením ) zobecňuje zásadu definice indukcí části sekvence a obecněji definice funkce podle transfinitní rekurze :
Věta (funkce definována fundovanou rekurze ) - Nechť R je relace opodstatněný na množině E a G a funkční třídy definované všude. Pak existuje funkce f a pouze jedna (ve smyslu: jediný graf funkce ) z domény D f = E , taková, že pro všechna x ∈ E , f ( x ) = G ( x , f | R - 1 [ x ] ), kde f | P označuje omezení f k P .
DemonstraceDefinujte predikát rec ( h ) pomocí: h je funkce z domény D h ⊂ E , takže pro všechna z ∈ D h , R −1 [ z ] ⊂ D h a h ( z ) = G ( z , h | R −1 [ z ] ), pak predikát F ( x , y ) o: ∃ h (rec ( h ) a h ( x ) = y ).
Tím opodstatněné indukce, třída F je funkční (které již dokazuje, tím extensionality , že možné funkce f oznámeno ve větě je jedinečný), ale jeho doména je zahrnuta v nastavené E tedy (podle schématu náhradních axiomů ) existuje funkce f taková, že F ( x , y ) ⇔ f ( x ) = y . Navíc je konstrukčně splněn bod ( f ).
Nakonec D f = E , opět podloženou indukcí: pro všechna x ∈ E taková, že R −1 [ x ] ⊂ D f , množina párů h : = f ∪ {( x , G ( x , f | R −1 [ x ] ))} splňuje rec ( h ), takže x ∈ D f .
Tyto dvě věty se rozšiřují na třídy, jako jejich protějšky v konkrétním případě transfinitního opakování . Přesněji: v těchto dvou příkazech lze nahradit množiny E , R a f třídami (relačními pro R a funkčními pro f ), za předpokladu, že pro libovolnou množinu x je třída R −1 [ x ] spolu ( v případě transfinitní indukce je zbytečné tento předpoklad přidávat, protože ∈ −1 [ x ] = x ).
V množině E opatřené opodstatněnou relací R každý prvek x připouští hodnost ρ ( x ), což je pořadové číslo . Funkce hodnocení je na E definována opodstatněnou rekurzí pomocí:
ρ ( x ) = ∪ {α + 1 | α ∈ im (ρ | R −1 [ x ] ) } = ∪ {ρ ( y ) + 1 | y R x }(sjednocení sady ordinálů je ordinální). Pořadí x je tedy nejmenší ordinál, přísně větší než řady předchůdců x .
Délka této relace R , často poznamenal | R |, je nejmenší pořadové číslo obsahující všechny ρ ( x ).
Opodstatněná indukce a rekurze ( viz výše ) se vztahují na R , ale je někdy vhodnější je aplikovat na zpětný ráz ρ přísného pořadí na ordinálu | R |, tj. Ke vztahu T definovanému: xTy ⇔ ρ ( x ) <ρ ( y ).
Funkce pořadí umožňuje zřetelným způsobem uspořádat E do hierarchie, široce používané v teorii množin s členským vztahem pro R (srov. „ Hodnost množiny “).
Zvláštní případ opodstatněného opakování je strukturální opakování . Algoritmus , když se konstruuje soubor prvků, při současném zajištění, že početně prvek je přísně nižší než jeho předchůdce, také zajišťuje jeho ukončení , jakmile striktní pořadí je opodstatněný.
Struktury používané v algoritmických (konstruovaných typech) jsou často opodstatněné přísné objednávky, máme tedy velmi obecnou metodu k prokázání ukončení počítačového programu .