Timeline for (Types of) induction on infinite chains
Current License: CC BY-SA 4.0
10 events
| when toggle format | what | by | license | comment | |
|---|---|---|---|---|---|
| Mar 23, 2019 at 9:02 | history | edited | Andrej Bauer | CC BY-SA 4.0 |
added 44 characters in body
|
| Mar 23, 2019 at 8:58 | comment | added | Andrej Bauer | @EmilJeřábek: You're absolutely right, I think constructive math has damaged my brain so it doesn't see that the double complement of a subset is the same set again. I changed the answer, thanks. | |
| Mar 22, 2019 at 17:59 | comment | added | Emil Jeřábek | Of course, I’m interpreting “infinite descending chain” to mean that the chain is defined as an infinite, i.e. $\omega$-indexed, sequence. The individual elements of the chain do not have to be distinct. They may even all be the same element. | |
| Mar 22, 2019 at 17:56 | comment | added | Emil Jeřábek | This is an absolutely elementary proof. 1 and 2 are really just contrapositive of each other. For 2->3, if $\dots<x_2<x_1<x_0$ is an $<$-chain, then $\{x_i:i\in\omega\}$ has no $<$-minimal element. For 3->2, assume that $X$ has no $<$-minimal element, and fix $x_0\in X$. Using dependent choices, find a sequence $\langle x_i:i<\omega\rangle$ of elements of $X$ such that $x_{i+1}<x_i$ for each $i$; that there is always a next element to choose from is precisely the statement that $X$ has no $<$-least element. You obtain a $<$-descending chain. | |
| Mar 22, 2019 at 17:26 | comment | added | Andrej Bauer | I am not aware of a proof that doesn't require transitivity. The one I have does. Do you have a reference? | |
| Mar 22, 2019 at 15:41 | comment | added | Emil Jeřábek | You don’t need transitivity or irreflexivity for the theorem. You do not need the reflexivization $\le$ either, if you simply state condition 2 so that $S$ has a $<$-minimal element. | |
| Mar 22, 2019 at 15:38 | history | edited | Andrej Bauer | CC BY-SA 4.0 |
added 104 characters in body
|
| Mar 22, 2019 at 15:36 | comment | added | Andrej Bauer | @EmilJeřábek: I did not require that a well-founded relation be transitive, so what are you talking about? Transitivity is needed for the theorem only, as stated. I will stress that the induction is the same thing as well-foundedness. | |
| Mar 22, 2019 at 13:03 | comment | added | Emil Jeřábek | Well-founded relations do not have to be transitive, transitivity does not enter well-founded induction in any way. Also, considering the original question, it might be worth stressing that this is a complete characterization: induction holds for a binary relation if and only if it is well founded. | |
| Mar 22, 2019 at 12:36 | history | answered | Andrej Bauer | CC BY-SA 4.0 |