Timeline for (Fictive) story of a time where people reasoned only up to isomorphism
Current License: CC BY-SA 4.0
14 events
| when toggle format | what | by | license | comment | |
|---|---|---|---|---|---|
| Nov 18 at 16:43 | history | edited | Paul Taylor | CC BY-SA 4.0 |
added 577 characters in body
|
| Nov 18 at 16:29 | comment | added | Paul Taylor | @SridharRamesh: your long sequence of Comments is a very similar argument to the one I had in mind, so maybe you could rewrite them as an Answer. | |
| Oct 16, 2017 at 0:59 | comment | added | Sridhar Ramesh | (Ah, but I realize this is essentially what the aforementioned Escardo argument surely works out to as well.) | |
| Oct 15, 2017 at 21:42 | comment | added | Sridhar Ramesh | But at this point, we realize the whole system of knocking pebbles off the row-end is completely independent from what names are written on them; regardless of what names are written on them, we do the same thing: knock off the end-pebble when a sheep returns. So we can forget the names altogether, and just do that. Knock off an end-pebble when a sheep returns. And we are assured, from above, that the row returns to nothing precisely when all the sheep have returned. Thus, we can count (a set of distinguishable) sheep with a row of (indistinguishable, apart from their position) pebbles. FIN. | |
| Oct 15, 2017 at 21:40 | comment | added | Sridhar Ramesh | After a while, we decide we're too lazy to be swapping these pebbles all the time, and instead of swapping physical pebbles, we just erase the names written on them and write the desired new names, to same effect. When a sheep returns, we erase and rewrite two pebble-names if need be, and then knock-off the end pebble. The row of pebbles still lists at any moment precisely which sheep haven't yet returned, and we are still assured that it will become empty precisely when all the sheep have returned. [cont] | |
| Oct 15, 2017 at 21:40 | comment | added | Sridhar Ramesh | Sheep may come back in some other order, any order they please. Still, we can handle this easily enough: if sheep A returns, but the end of the row is marked with the name for sheep B, we simply swap the row-end B-pebble with the mid-row A-pebble, and then knock off the A-pebble from the end of the row. The row of pebbles still lists at any moment precisely which sheep haven't yet returned, and we are still assured that it will become empty precisely when all the sheep have returned. [cont] | |
| Oct 15, 2017 at 21:39 | comment | added | Sridhar Ramesh | If the sheep were to return in precisely the opposite of the order in which they went out, then we could easily knock their corresponding pebble off the end of the row with each return; this would all play out in precise reverse of the build-up, and the row would return to its initial emptiness when, and precisely when, all the sheep had returned. BUT! [cont] | |
| Oct 15, 2017 at 21:39 | comment | added | Sridhar Ramesh | Another simple argument (though I cannot speak as to its historical plausibility) which avoids explicit consideration of "infinite descent" might be like so: The sheep go out in some order, one pebble marked with corresponding sheep's name tossed onto the end of a row for each one, building up a row yea long. [cont] | |
| Oct 15, 2017 at 20:21 | history | edited | Paul Taylor | CC BY-SA 3.0 |
deleted 58 characters in body
|
| Oct 15, 2017 at 19:14 | history | edited | Paul Taylor | CC BY-SA 3.0 |
added 20 characters in body
|
| Oct 15, 2017 at 18:58 | comment | added | Gerhard Paseman | This suggests to me using Boolean circuit (flowchart) analysis to restructure proofs to minimize certain component usage (for example, building a three inverter circuit using ands, ors, and just two inverters). Do you know of anyone who has diagrammed the proofs and done a similar kind of analysis on them? Gerhard "Computer-Aided Proof Optimization Through Clones!" Paseman, 2017.10.15. | |
| Oct 15, 2017 at 17:53 | comment | added | Paul Taylor | I see the temptation of permutation groups. Also, HoTT (Martin's setting) was partly motivated by (higher dimensional) groupoids. I think, however, Martin wanted to eliminate (as much as possible) the repeated use of induction in Giuseppe Peano's 1889 paper to prove things like commutativity, associativity and distributivity of $+$ and $\times$ in favour of (the more appropriate) primary-school set theory. (At least, Peano presumably used induction repeatedly: his treatment is extremely terse.) | |
| Oct 15, 2017 at 16:21 | comment | added | Gerhard Paseman | It seems that one could develop much of a theory of permutation groups before inventing the concept of number to ease the development. Does Martin Escardo's development resemble such a development of permutation groups? Gerhard "Who Needs These 'Numbers' Anyway?" Paseman, 2017.10.15. | |
| Oct 15, 2017 at 13:17 | history | answered | Paul Taylor | CC BY-SA 3.0 |