동화 가설은 언제 사용될 수 있나요?

Question

잘 정돈된 구조의 속성을 증명할 때 귀납 가설을 사용할 수 있습니다.나는 이에 대한 증거가 있다는 것을 알고 있습니다.

동화에 관해서는 혼란 스럽습니다.

다른 질문에 대한 답변 중 하나 "코인덕션이란 무엇인가요?"에서는 정형화된 정의에 대한 개념이 존재한다고 언급합니다.

내가 (노력하는) 동전 유도와 관련하여 읽으려고 하는 많은 것들은 대부분 이중 시뮬레이션과 동등성에 대해 이야기합니다.그러나 내가 아는 한, 그것들은 두 개의 동시 데이터 구조에 대한 관계를 증명하려고 노력하고 있습니다.예를 들어, 두 스트림이 동일하다는 것을 증명합니다.그리고 상호작용 가설은 어떻게든 이중시뮬레이션 가설 중 하나에서 파생됩니다.그럼에도 불구하고, 나는 아직도 조화로운 세계에서 무엇이 잘 형성되어야 하는지에 대한 요구 사항을 놓치고 있는 것 같습니다.

나는 그런 종류의 명제를 증명할 때 합성 가설이 효과가 있다는 것을 어떻게든 알 수 있지만, 그것이 에서 언급된 것과 같은 더 일반적인 명제를 증명하는 데 언제 사용될 수 있는지는 여전히 불분명합니다. 코인덕션이란 무엇인가요?.해당 링크에서 명제는 "뭔가 무한하다"고 명시합니다.이는 증명에 관심이 있는 보다 일반적인 형태의 진술처럼 보입니다.

아마도 관련된 질문은 어떤 명제가 동등성 명제로 전환되고 재진술될 수 있는지 여부입니다.

공동 유도가 일부 잘 구성된 요구 사항에 대해 작동하는 이유를 설명하는 간단한 비공식적 추론이 있습니까?

가능하다면 다음과 같은 설명을 원합니다. https://math.stackexchange.com/questions/432293/well-ordering-and-mathematical-induction/432302#432302.

Answer 1

먼저, 최소 및 최대 고정점을 기억해 보겠습니다. $\subseteq$.우리는 일부 세트를 기준으로 작업 중입니다. $U$, 우주.(공)귀납적 정의의 경우, $U$ 모든 용어의 집합입니다.기능 $f:2^U o2^U$ (의 하위 집합에서 $U$ 하위 집합에 $U$) 이다 단조, 만약에 $A\하위 기술 B$ 항상 암시한다 $f(A)\하위 집합f(B)$.ㅏ 고정점 ~의 $f$ 세트이다 $A$ 그렇게 $f(A)=A$.

모노톤용 $f$ 항상 최소 고정점이 있다 $\mu f$, 즉 모든 것의 교차점 $A\subseteq U$ 그렇게 $f(A)\subseteq A$. 최소 임의의 고정 지점에 대해 의미합니다. $F$ 우리는 항상 $\mu f\subseteq F$.

예를 들어 $f_{ t nat}$ 에 의해 정의된다 $f_{ t nat}(A)=\{0\}\cup\{n+1\mid n\in A\}$.함수 $f_{ t nat}$ 생성자 아래의 1단계 클로저 함수입니다. $0$ 그리고 $+1$.조건 $f_{ t nat}(A)\subseteq A$ 의미하는 것은 $A$ 생성자 아래에서 닫힙니다. $0$ 그리고 $+1$.교차점은 다음을 의미합니다. $\mu f_{ t nat}$ 생성자 아래에 닫힌 모든 집합에 있는 요소만 포함합니다.이것은 자연수입니다.이 예는 자연수의 귀납적 정의가 어떻게 자연수의 생성자 아래에서 최소 고정 폐쇄 지점인지 보여줍니다.일반적으로 귀납적으로 정의된 집합은 생성자 아래에서 최소한으로 고정된 폐쇄 지점입니다.

이중적으로, 모노톤용 $f$ 가장 큰 고정점도 있다 $ u f$, 즉 모두의 연합 $A\subseteq U$, 그렇게 $f(A)\supseteq A$. 가장 위대한 임의의 고정 지점에 대해 의미합니다. $F$ 우리는 항상 $ u f\supseteq F$.이중성을 완전하게 만들기 위해 교차점은 다음과 같습니다. $\subseteq$-최하위와 결합 $\subseteq$-최고 그리고 따라서 $\supseteq$-최한.따라서 실제로 가장 큰 고정점은 $\subseteq$ 에 대한 최소 고정점입니다. $\supseteq$ 그 반대.(또한 단조성의 요구 사항은 다음과 같습니다. $\subseteq$ 에 관해서는 $\supseteq$.)

이제 증명 기술을 살펴보겠습니다.자연수에 대한 귀납법의 예부터 시작하겠습니다.어떤 재산이 있다는 것을 보여주기 위해 $P$ 모든 자연수에 대해 성립함을 보여줍니다. $P(0)$ 그리고 그 $P(n)$ 암시한다 $P(n+1)$.보기 $P$ 의 하위 집합으로 $U$ (특성이 보유하는 모든 요소의 집합) 자연 유도에 대한 증명 의무는 다음과 같습니다. $P$ 아래에 폐쇄되어 있습니다 $f_{ t nat}$.자연 유도의 증명 기술의 정확성은 최소 고정점의 정의를 따릅니다.만약에 $f_{ t nat}(P)\subseteq P$, 그 다음에 $P$ 다음을 형성하는 교차점의 일부입니다. $\mu f_{ t nat}$, 따라서 속성은 전체적으로 유지됩니다. $\mu f_{ t nat}$, 그건 $\mu f_{ t nat}\subseteq P$.

유도는 이전 단락을 임의의 모노톤으로 일반화한 것일 뿐입니다. $f$ 대신에 $f_{ t nat}$.Coinduction은 유도의 이중입니다.입증의무는 $f(P)\supseteq P$.이는 다음을 의미합니다. $P$ 어떤 요소를 보유 $x$, 그 다음에 $x$ 기본 요소만을 사용하여 구성됩니다. $P$ 또한 보유하고 있습니다.따라서 속성이 생성자를 적용해도 살아남는다는 것을 보여주는 대신, 해체 후에도 속성이 살아남는다는 것을 보여야 합니다.입증 의무가 충족되면 우리는 다음을 얻습니다. $ u f\supseteq P$.

결론이 무슨 소용이냐 $ u f\supseteq P$?다시 생각해보자 $P$ 속성이 아니라 하위 집합으로 $U$.동전 유도의 결론은 다음의 모든 요소를 ​​확립합니다. $P$ 공동으로 정의된 집합의 잘 구성된 구성원입니다. $ u f$.다음 예에서는 이런 일이 발생합니다. 코인덕션이란 무엇인가요? 전시 forall n, Infinite (from n).여기, $f$ 생성자 아래에 클로저가 있습니다. Infinite (아님 colist!) 그리고 $P$ 형식의 모든 항의 집합입니다. from n 일부 n.