On matematiikka , joka on hyvin perusteltu suhde (kutsutaan myös Noetherian suhteessa tai Artinian suhde ) on binaarinen suhde täyttävät toisen seuraavista kahdesta ehdosta, joka vastaa mukaan selviö riippuvan valinnan (heikko versio selviö valinta ):
Hyvin perusteltu järjestyksessä (kutsutaan myös Noetherian järjestyksessä tai Artinian järjestyksessä ) on järjestyksessä suhde , jotka liittyvät tiukat järjestys on hyvin perusteltu suhde.
Kaikki perustellut suhteet ovat tiukasti asyklisiä , toisin sanoen sen transitiivinen sulkeminen on tiukka järjestys. Suhde voidaan R on perusteltu, jos sen transitiivista sulkemisesta on se, tai jos R on antireflexive ja jos sen transitiivista refleksiivinen sulkeminen on perusteltu järjestyksessä.
Merkitään R -1 [ X ] joukon R -antecedents on X .
Seuraava lause ( Zermelon joukko-teoriassa ) tarjoaa sekä kolmannen ekvivalentin määritelmän hyvälle perustukselle että yleistämisen todistusperiaatteelle transfiniittisen induktion avulla ( hyvässä järjestyksessä tai järjestyksessä ), joka itse laajentaa Peano n o 5: n aksiomia. tai induktioperiaate (vastaa tavallista luonnollisten lukujen järjestystä):
Lause (hyvä perusta ja perusteltu induktio ) - Suhde R joukolla E on perusteltu vain ja vain, jos osalle E on yhtä suuri kuin E kokonaisuutena, riittää, että se sisältää jokaisen elementin, josta se on sisältää kaikki R- edeltäjät.
Muodollisesti: R on perusteltu, jos ja vain jos jonakin P ja E ,jos ∀ x ∈ E ( R -1 [ x ] ⊂ P ⇒ x ∈ P ) jälkeen P = E . EsittelySiirtymällä komplementaariseen lausekkeen ehto vastaa implikaatiota
tahansa osa X on E , jos ∀ x ∈ E ( R -1 [ x ] ∩ X = ∅ ⇒ x ∉ X ), sitten X = ∅tai taas päinvastoin :
mistä tahansa ei-tyhjän osan X ja E , ∃ x ∈ X ( R -1 [ x ] ∩ X = ∅),joka ilmentää sekä kaikista nonempty osajoukko X ja E , on olemassa elementti x on X , jossa ei ole R -antécédent on X .
Samoin, toinen lause (in Zermelo-Fraenkel teoria sarjaa , siis jossa vaihto ) yleistää periaatetta määritelmän induktiolla on sekvenssin ja yleisemmin määrittely toiminto transfinite rekursio :
Lause (määritetty toiminto perusteltu rekursio ) - Olkoon R on relaation hyvin perusteltu on joukko E ja G toiminnallinen luokka on määritelty kaikkialla. Tällöin on olemassa funktio f ja vain yksi (siinä mielessä: yksi funktion graafi ), toimialue D f = E , siten että kaikille x ∈ E : lle f ( x ) = G ( x , f | R - 1 [ x ] ), missä f | P tarkoittaa rajoittaminen f ja P .
EsittelyMääritetään predikaatti rec ( h ) seuraavasti: h on toimialueen D h ⊂ E funktio siten, että kaikille z ∈ D h , R −1 [ z ] ⊂ D h ja h ( z ) = G ( z , h | R −1 [ z ] ), sitten predikaatti F ( x , y ) seuraavasti: ∃ h (rec ( h ) ja h ( x ) = y ).
Hyvin perustellulla induktiolla luokka F on toiminnallinen (mikä todistaa jo ekstensionaliteetilla , että lauseessa ilmoitettu mahdollinen funktio f on ainutlaatuinen), mutta sen toimialue kuuluu siis sarjaan E ( korvaavien aksiomien kaavion mukaan) ) on olemassa funktio f siten, että F ( x , y ) ⇔ f ( x ) = y . Lisäksi rakenteen perusteella kappale ( f ) täyttyy.
Lopuksi, D f = E , jälleen perustellulla induktiolla: kaikille x ∈ E siten, että R −1 [ x ] ⊂ D f , parien joukko h : = f ∪ {( x , G ( x , f | R −1 [ x ] ))} täyttää kohdan rec ( h ), joten x ∈ D f .
Nämä kaksi lausetta ulottuvat luokkiin, kuten niiden vastineet transfinite-toistumisen erityistapauksessa . Tarkemmin sanottuna: joukot E , R ja f voidaan korvata näissä kahdessa lauseessa luokilla (relaatio R: lle ja funktionaalinen f: lle ), edellyttäen, että minkä tahansa joukon x osalta luokka R −1 [ x ] on yhdessä ( transfiniittisen induktion tapauksessa on turha lisätä tätä oletusta, koska ∈ −1 [ x ] = x ).
Joukossa E , joka on varustettu perustellulla suhteella R , jokainen elementti x myöntää arvon ρ ( x ), joka on järjestysluku . Sijoitusfunktio määritetään E : ssä perustellulla rekursiolla:
ρ ( x ) = ∪ {α + 1 | α ∈ im (ρ | R −1 [ x ] ) } = ∪ {ρ ( y ) + 1 | y R x }(joukko asetuksia on järjestys). Siten x: n sijoitus on pienin järjestysaste, joka on ehdottomasti suurempi kuin x: n edeltäjien rivejä .
Pituus on suhteessa R , havaitaan usein | R | on pienin järjestys, joka sisältää kaikki ρ ( x ).
Hyvin perusteltu induktio ja rekursio ( ks. Edellä ) koskevat R: tä , mutta joskus on helpompaa soveltaa niitä järjestysnumeron tiukan järjestyksen vetoon ρ | R | eli suhteeseen T, jonka määrittelee: xTy ⇔ ρ ( x ) <ρ ( y ).
Sijoitusfunktio mahdollistaa E : n organisoimisen ilmeisellä tavalla hierarkiaksi, jota käytetään laajalti joukko- teoriassa R- jäsenyydensuhteen kanssa (vrt. ” Joukon sijoitus ”).
Erityinen perustellun toistumisen tapaus on rakenteellinen toistuminen . Algoritmi , kun se rakentaa useista tekijöistä samalla kun varmistetaan, että rakennettu elementti on tiukasti huonompi sen edeltäjä, myös varmistaa sen päättäminen , kun tiukat järjestys on hyvin perusteltu.
Algoritmeissa käytetyt rakenteet (rakennetut tyypit) ovat usein perusteltuja tiukkoja tilauksia, joten meillä on hyvin yleinen menetelmä todistaa tietokoneohjelman päättyminen .