Em matemática , uma relação bem fundada (também chamada de relação Noetheriana ou relação Artiniana ) é uma relação binária que satisfaz uma das duas seguintes condições, equivalente de acordo com o axioma da escolha dependente (uma versão fraca do axioma da escolha ):
Uma ordem bem fundada (também chamada de ordem Noetheriana ou ordem Artiniana ) é uma relação de ordem da qual a ordem estrita associada é uma relação bem fundada.
Qualquer relação bem fundada é estritamente acíclica , ou seja, seu fechamento transitivo é de ordem estrita. Uma relação R é bem fundada se seu fechamento transitivo for ele, ou se R for anti - reflexo e se seu fechamento reflexivo transitivo for uma ordem bem fundada.
Denotaremos por R −1 [ x ] o conjunto de R- antecedentes de x .
O teorema seguinte (em teoria dos conjuntos de Zermelo ) oferece tanto uma terceira definição equivalente da boa base e uma generalização da prova de princípio por indução transfinito (em uma boa ordem ou em um ordinal ), que se estende a axioma de Peano n o 5 ou o princípio da indução (correspondendo à ordem usual dos números naturais):
Teorema (bom fundamento e indução bem fundada) - Uma relação R em um conjunto E é bem fundada se e somente se, para uma parte de E ser igual a E como um todo, é suficiente que ela contenha cada elemento do qual ele contém todos os antecedentes R.
Formalmente: R é bem fundado se e somente se, para qualquer parte P de E ,se ∀ x ∈ E ( R -1 [ x ] ⊂ P ⇒ x ∈ P ), em seguida, P = E . DemonstraçãoAo passar para o complementar , a condição do enunciado é equivalente à implicação
para qualquer parte X de E , se ∀ x ∈ E ( R −1 [ x ] ∩ X = ∅ ⇒ x ∉ X ) então X = ∅ou novamente, em seu oposto :
para qualquer parte não vazia X de E , ∃ x ∈ X ( R −1 [ x ] ∩ X = ∅),que expressa bem como para tudo não vazio subconjunto X de E , existe um elemento x de X com nenhuma R -antécédent em X .
Da mesma forma, um segundo teorema (na teoria dos conjuntos de Zermelo-Fraenkel , portanto com substituição ) generaliza o princípio da definição por indução de uma sequência e, mais geralmente, da definição de uma função por recursão transfinita :
Teorema (função definida por recursão bem fundada) - Seja R uma relação bem fundada em um conjunto E e G uma classe funcional definida em qualquer lugar. Então, existe uma função f e apenas uma (no sentido: um único gráfico de função ), de domínio D f = E , tal que para todo x ∈ E , f ( x ) = G ( x , f | R - 1 [ x ] ), onde f | P indica a restrição de f a P .
DemonstraçãoDefina o predicado rec ( h ) por: h é uma função, do domínio D h ⊂ E , tal que para todo z ∈ D h , R −1 [ z ] ⊂ D h e h ( z ) = G ( z , h | R −1 [ z ] ), então o predicado F ( x , y ) por: ∃ h (rec ( h ) eh ( x ) = y ).
Por indução bem fundamentada, a classe F é funcional (o que já prova, por extensionalidade , que a possível função f anunciada no teorema é única), mas seu domínio está incluído no conjunto E portanto (de acordo com o diagrama de axiomas de substituição ) existe uma função f tal que F ( x , y ) ⇔ f ( x ) = y . Além disso, por construção, rec ( f ) é satisfeita.
Finalmente, D f = E , novamente por indução bem fundada: para todo x ∈ E tal que R −1 [ x ] ⊂ D f , o conjunto de pares h : = f ∪ {( x , G ( x , f | R −1 [ x ] ))} satisfaz rec ( h ) então x ∈ D f .
Esses dois teoremas se estendem a classes, como suas contrapartes no caso particular de recorrência transfinita . Mais precisamente: pode-se substituir, nessas duas afirmações, os conjuntos E , R e f por classes (relacional para R e funcional para f ), desde que para qualquer conjunto x , a classe R −1 [ x ] seja a junto ( no caso da indução transfinita, é inútil adicionar esta suposição porque ∈ −1 [ x ] = x ).
Num conjunto E dotado de uma relação bem fundada R , cada elemento x admite uma classificação ρ ( x ), que é um número ordinal . A função de classificação é definida em E por recursão bem fundada por:
ρ ( x ) = ∪ {α + 1 | α ∈ im (ρ | R −1 [ x ] ) } = ∪ {ρ ( y ) + 1 | y R x }(a união de um conjunto de ordinais é um ordinal). Assim, a classificação de x é o menor ordinal estritamente maior do que as classificações dos antecedentes de x .
O comprimento da relação R , frequentemente observada | R |, é o menor ordinal contendo todos os ρ ( x ).
Indução e recursão bem fundamentadas ( veja acima ) se aplicam a R , mas às vezes é mais conveniente aplicá-las ao recuo por ρ da ordem estrita no ordinal | R |, ou seja, à relação T definida por: xTy ⇔ ρ ( x ) <ρ ( y ).
A função de classificação torna possível organizar E de uma maneira óbvia em uma hierarquia, amplamente usada na teoria dos conjuntos com a relação de pertinência para R (cf. “ Classificação de um conjunto ”).
Um caso especial de recorrência bem fundada é a recorrência estrutural . Um algoritmo , quando constrói uma série de elementos ao mesmo tempo que garante que um elemento construído é estritamente inferior ao seu predecessor, também garante sua terminação , assim que a ordem estrita for bem fundamentada.
As estruturas usadas em algoritmos (tipos construídos) são frequentemente ordens estritas bem fundamentadas, portanto, temos um método muito geral para provar o término de um programa de computador .