3 ms·
> It's the undecidability that's important to his result, not arbitrariness Undecidability is arbitrariness - to say that, for example, the axiom of choice is
by a1369209993 7y ago
> It's the undecidability that's important to his result, not arbitrariness
Undecidability is arbitrariness - to say that, for example, the axiom of choice is independent of ZF is the same thing as saying that there is a arbitrary choice[0] between ZF+C and ZF+!C. Similarly, the sequence[1] G(PA),G(PA+G(PA)),G(PA+G(PA)+G(PA+G(PA))),... requires (at least) one additional arbitrary bit per item.
0: not asserting anything about what makes that choice, though.
1: where G(X) is the Godel sentence, roughly "X cannot cannot prove G(X)"
- pron 7y agoWhat I meant was that Brouwer doesn't need lawless sequences; all the results are valid with lawful sequences only. He just didn't know that because he didn't know that lawful sequences can be undecidable. You can call it arbitrary, but it doesn't have to be random, it just needs to be unknowable, which is the case even if it's chosen by a computational rule. It is true that most of the sequences of the kind you presented are not computable, but I don't think any result of Brouwer's is affected.