Comment by pron | Hacker News Reader

Comment by pron | Hacker News Reader

Parent Full thread

We need to separate Brouwer's construction of the choice sequences from his philosophical justification for them; in the transition between the two there were just things he couldn't have known. His entire conception of choice sequences was because the mathematician's mind is finite. He couldn't have based his choice sequences on computation because the notion didn't exist yet, but if it had, he wouldn't have needed "lawless sequences". There is just nothing that requires them either in his chosen axioms or in his philosophy -- their salient feature is that one cannot predict their behavior, something that, after Turing, we know is true even for "lawful sequences" but Brouwer didn't. I, therefore, do not think it is correct to say that he wasn't a finitist because he relied on randomness. As far as he knew, randomness was consistent with a finite mind, the finiteness is what mattered to him, and anyway, he cared about undecidability, not randomness, but didn't know the former can exist without the latter.

What is essential to his philosophy is that the only justification for the axioms can come from nature by way of empiricism, and is therefore finite. If you accept Russel's, Brouwer's and Hilbert's belief that mathematics contains Truth, and if you then accept Brouwer's belief that the only source of truth is nature by way of empiricism, you have no choice today but to reject both LEM and induction. It is perfectly fine to work in constructive mathematics, and, in the Turingian sense it is of value, but it is no longer justified by Brouwer's philosophy of mathematical truth. Brouwer would have had to reject today's constructive mathematics on the same grounds he rejected classical mathematics: its axioms are unjustified by nature and empirical observation, even in principle. In fact, I don't think there is any philosophy of mathematics that could distinguish between constructivism and classical mathematics on any reasonable philosophical grounds today.

I would say that Brouwer's philosophy is (with today's knowledge) constructivist and ultra-finitist. BTW, Brouwer was not opposed to formalism as much as he was to logicism, and he even tried to propose a way to reconcile the two ("Intuitionistic reflections on formalism", 1927).

In modern terms, you can identify sequences and automata: a sequence is a current state, plus a transition function giving you the next element of the sequence and the next state. However, if every function is tracked by a computable process, then the transition function must also tracked by a computable process, and so every infinite sequence must be generated by a computable process.

This identification is precisely what choice sequences are used to rule out. If a sequence is genuinely arbitrary, then you cannot describe it up front with a finite amount of data and a finite rule for updating that data. Instead, you have to imagine a mathematician adding a new axiom at each time step about the next element of a choice sequence, and requiring that any constructions they do works uniformly regardless of what axioms may be chosen in the future.

In this picture, the total amount of axiomatic data is actually going up over time, and this is actually important for the results Brouwer proved. In particular, without the axioms for choice sequences, you cannot derive the strong counterexamples, because you need classically-false axioms to prove classically-false theorems (like the continuity of all real-valued functions).

> This identification is precisely what choice sequences are used to rule out.

But you don't need to rule them out -- Brouwer certainly didn't. He just wanted to rule out decidable sequences. It's the undecidability that's important to his result, not arbitrariness, and that's perfectly compatible with automata. He just didn't know about computational undecidability and thought that undecidability requires lawlessness, but it doesn't. In any event, he didn't think randomness violates finitism. That only finite systems can be the source of axioms has been a constant refrain of his. I see that according to Wikipedia's definition of Finitism, he would be a "classical finitist."

> In particular, without the axioms for choice sequences, you cannot derive the strong counterexamples, because you need classically-false axioms to prove classically-false theorems (like the continuity of all real-valued functions).

The continuity of all real-valued functions can be proven with just computable sequences because of undecidability; you just can't do it if computational undecidability hasn't been discovered yet. In fact, it doesn't even become quite "classically false", but can be "embedded" in classical mathematics by restricting the "all": all computable real functions are continuous is a classical theorem. AFAIK, all constructive theorems can be embedded in classical mathematics by restricting them to computable entities. Do you have an example of any result that relies on uncomputable sequences?

> 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)"

What 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.

Reply on news.ycombinator.com