Quando a hipótese de coindução pode ser usada?

Question

Podemos usar a hipótese de indução quando provamos uma propriedade para uma estrutura bem ordenada.Estou ciente de que há uma prova disso.

Quando se trata de coindução, estou confuso.

Uma das respostas para outra pergunta "O que é coindução?"menciona que existe uma noção de uma definição correcursiva que deve ser bem formada.

Muitas coisas que (tento) ler relacionadas à coindução falam principalmente sobre bissimulação e equivalência.Mas, até onde sei, eles estão tentando provar alguma relação entre duas estruturas de dados coindutivas.Por exemplo, eles provam que dois fluxos são equivalentes.E a hipótese coindutiva é de alguma forma derivada de uma das hipóteses da bissimulação.Mesmo assim, acho que ainda estou perdido nos requisitos do que constitui uma boa formação no mundo coindutivo.

De alguma forma, posso ver que a hipótese de coindução funciona ao provar esses tipos de proposições, mas ainda não estou claro quando elas podem ser usadas para provar proposições mais gerais, como a mencionada em O que é coindução?.Nesse link, a proposição afirma que “algo é infinito”.Esta parece ser uma forma mais genérica de afirmação que alguém estaria interessado em provar.

Uma questão possivelmente relacionada é se qualquer proposição pode ser convertida e reafirmada como uma proposição de equivalência ou não.

Existe algum raciocínio informal simples que explica por que a co-indução funciona para algum requisito de boa formação?

Espero uma explicação como, se possível: https://math.stackexchange.com/questions/432293/well-ordering-and-mathematical-induction/432302#432302.

Answer 1

Primeiro, deixe-me lembrar os mínimos e os maiores pontos fixos para $\subseteq$.Estamos trabalhando em relação a algum conjunto $U$, o universo.No caso de definições (co)indutivas, $U$ é o conjunto de todos os termos.Uma função $f:2^U o2^U$ (de subconjuntos de $U$ para subconjuntos de $U$) é monótono, se $A\subseteq B$ sempre implica $f(A)\subseteq f(B)$.A ponto fixo de $f$ é um conjunto $A$ de tal modo que $f(A)=A$.

Para monótono $f$ sempre existe um ponto mínimo fixo $\mu f$, ou seja, a interseção de todos $A\subseteq U$ de tal modo que $f(A)\subseteq A$. Ao menos significa que para pontos fixos arbitrários $F$ nós sempre temos $\mu f\subseteq F$.

Por exemplo, deixe $f_{ tnat}$ ser definido por $f_{ t nat}(A)=\{0\}\cup\{n+1\mid n\in A\}$.A função $f_{ tnat}$ é a função de fechamento de uma etapa sob os construtores $0$ e $+1$.A condição $f_{ t nat}(A)\subseteq A$ significa que $A$ está fechado sob os construtores $0$ e $+1$.A intersecção significa que $\mu f_{ t nat}$ contém apenas os elementos que estão em todos os conjuntos fechados pelos construtores.Acontece que esses são os números naturais.O exemplo mostra como a definição indutiva de números naturais é o ponto de fechamento menos fixo nos construtores dos números naturais.Geralmente, conjuntos definidos indutivamente são pontos de fechamento menos fixos nos construtores.

Duplamente, para monótono $f$ também existe um maior ponto fixo $ f$, ou seja, a união de todos $A\subseteq U$, de tal modo que $f(A)\supsetq A$. O melhor significa que para pontos fixos arbitrários $F$ nós sempre temos $ u f\supsetq F$.Para completar a dualidade, notemos que a intersecção é o $\subseteq$-ínfimo e união o $\subseteq$-supremo e, portanto, o $\supsetq$-ínfimo.Então, de fato, os maiores pontos fixos para $\subseteq$ são apenas pontos menos fixos para $\supsetq$ e vice versa.(Além disso, observe que o requisito de monotonicidade é o mesmo para $\subseteq$ quanto a $\supsetq$.)

Agora, para técnicas de prova.Comecemos com o exemplo da indução em números naturais.Para mostrar que alguma propriedade $P$ vale para todos os números naturais, mostramos que $P(0)$ e essa $P(n)$ implica $P(n+1)$.Visualizando $P$ como um subconjunto de $U$ (o conjunto de todos os elementos onde a propriedade é válida), a obrigação de prova para a indução natural é que $P$ está fechado sob $f_{ tnat}$.A correção da técnica de prova da indução natural segue então da definição do ponto mínimo fixo:Se $f_{ t nat}(P)\subseteq P$, então $P$ faz parte da intersecção que forma $\mu f_{ t nat}$, então a propriedade se mantém por toda parte $\mu f_{ t nat}$, aquilo é $\mu f_{ t nat}\subseteq P$.

A indução é apenas a generalização do parágrafo anterior para um tom monótono arbitrário. $f$ em vez de $f_{ tnat}$.Coindução é o dual da indução:A obrigação de prova é $f(P)\supsetq P$.Isto significa que se $P$ segura em algum elemento $x$, então $x$ é construído usando apenas elementos de base sobre os quais $P$ também se mantém.Assim, em vez de mostrar que a propriedade sobrevive à aplicação de construtores, temos que mostrar que ela sobrevive à desconstrução.Uma vez satisfeita a obrigação de prova, obtemos $ u f\supsetq P$.

Que bom é a conclusão $ u f\supsetq P$?Vamos reconsiderar $P$ não como uma propriedade, mas como um subconjunto de $U$.A conclusão da coindução estabelece que todos os elementos da $P$ são membros bem formados do conjunto definido coindutivamente $ f$.Isto é o que acontece no exemplo em O que é coindução? mostrando forall n, Infinite (from n).Aqui, $f$ é o fechamento sob os construtores de Infinite (não de colist!) e $P$ é o conjunto de todos os termos da forma from n para alguns n.