Comment by neel_k | Hacker News Reader

Comment by neel_k | Hacker News Reader

Parent Full thread

Brouwer was absolutely not a finitist! Indeed, he completely rejected the idea that you could use formal logic to bound what mathematics could talk about.

A better (but still not entirely accurate) description would be that Brouwer had an epistemic conception of mathematical truth: mathematicians become able to assert mathematical truths as they engage in the process of constructing mathematical objects. This is indeed a constructive process, but it isn't finitistic -- for Brouwer mathematical reasoning is open-ended rather than a closed set of rules.

So much like Goedel (who disagreed with Brouwer in many other respects), Brouwer was totally committed to the idea that mathematical statements actually mean things. And because they carry meaning, the mathematical process and the properties of the mathematical objects created by a mathematician take precedence over the rules of logic.

This is why Brouwer rejected classical logic -- not because of any finitistic reason, but because (for example) classical logic permits disassembling the continuum into its set of points. Since (for Brouwer) the point of a continuum is that it is continuous, it followed that any logical principles (such as classical logic plus set theory) that permitted you to break up the continuum were fallacious. This is why he spent a lot of time on his so called "strong counterexamples", such as his proof that intuitionistically all total functions on the reals are continuous.

Notice that the direction of reasoning here is exactly the opposite of what a finitist would accept: Brouwer used the properties of the continuum to justify various finitary logical rules, rather than the other way around. The continuum was real, and logic just a façon-de-parler.

I find this kind of thing really interesting because it illustrates that the pretheoretical idea of truth can be formalized in many different ways, and that the various formalizations are not all compatible with each other. We are used to informal ideas like space having many different mathematical realizations -- metric spaces, topological spaces, vector spaces, etc -- but it is a little disconcerting (and a lot fascinating) to realize that logic and truth exhibit the same plural nature.

Hey Neel! Brouwer was a finitist in the sense that he did not accept infinitist axioms. His epistemology indeed was one of "mathematicians become able to assert mathematical truths as they engage in the process of constructing mathematical objects," but the justification was empiricism. I.e., his concept of establishing truth was by empirical, and therefore finitist. Here he is in "On the significance of the excluded middle in mathematics", 1923 (in Heijenoort):

> Within a specific finite "main system" we can always test (that is, either prove or reduce to absurdity) properties of systems, that is, test whether systems can be mapped, with prescribed correspondences between elements, into other systems; for the mapping determined by the property in question can in any case be performed in only a finite number of ways, and each of these can be undertaken by itself and pursued either to its conclusion or to a point of inhibition [here is his mention of induction that I provide below].

> ... On the basis of the testability just mentioned, there hold, for properties conceived within a specific finite main system, the principle of excluded middle

> ... It is a natural phenomenon, now, that numerous objects and mechanisms of the world of perception, considered in relation to extended complexes of facts and events, can be mastered if we think of them as (possibly partly unknown) finite discrete systems that for specific known parts are bound by specific laws of temporal concatenation. Hence the laws of theoretical logic, including the principle of excluded middle, are applicable to these objects and mechanisms in relation to the respective complexes of facts and events, even though here a complete empirical corroboration of the inferences drawn is usually materially excluded a priori and there cannot be any question of even a partial corroboration in the case of (juridical and other) inferences about the past.

Note his use of "testability", "natural phenomenon" and "empirical corroboration." So the source of truth is nature by way of empiricism, and that demands finitism. Even his reasoning about the continuum was finitist: no determination on order/separation can be made after examining a finite prefix of the decimal expansion of a real number (see ibid §2). If he were alive today, I have little doubt he would have been an ultra-finitist -- not any constructivist! -- because, as it turns out, there is no empirical justification (even in principle) to accept inifinite induction. The very arguments he uses to reject LEM must also reject unbounded induction: it is not verified by nature.

(Here's what he says on induction:

> Here the principle of mathematical induction often furnishes the means of carrying out such tests without individual consideration of every element involved in the mapping or of every possible way in which the mapping can be performed; consequently the test even for systems with a very large number of elements can at times be performed relatively rapidly.

After the discovery of computational complexity he would have had no choice but to be an ultra-finitist.)

As to the notion of truth, I completely agree, but here Alan Turing came up with a completely different perspective. Whereas both Brouwer and Russel were looking for Truth in mathematics (and Hilbert, too, although he was content to Truth in the contentual "real propositions" and the finitist rules of inferene), Turing rejected that notion altogether. To him, mathematics was a means whose intrinsic truth is irrelevant. It is valuable inasmuch as it is useful, not because it is true (see https://mdetlefsen.nd.edu/assets/201037/jf.turing.pdf).

You are being a bit too quick to equate finitism and constructivism. Hilbert was a finitist, but not a constructivist, and Brouwer was a constructivist, but he was not a finitist.

Brouwer's analysis of the continuum depends heavily upon the notion of a "free choice sequence" (aka a lawless sequence). The idea is that a creating subject -- i.e., you or me -- is free to make an unbounded sequence of choices to produce a sequence. At any finite time, you can only have made a finite number of arbitrary choices, but if you wait long enough you can make any number of arbitrary choices. Because these choices are arbitrary, free choice sequences cannot be described as being generated by any finite rule.

This is a constructive process, if you imagine (for example) generating a lawless sequence by throwing dice or from the clicks of a Geiger counter. But it's not a finitist one, because there is no finite data from which a choice sequence can be computed. This let Brouwer retain the idea that a mathematician can only have considered a finite amount of information at any point, without having to make any identification of the real numbers with computable functions.

In terms of complexity, there's an interesting analogy between choice sequences and the question of whether randomization gives you extra power -- the Miller-Rabin primality test lends immense force to the intuition that RP is stronger than P, but we might be centuries from proving it.

Even if we set aside randomness, though, an ultra-finitist/complexity-aware-logic is something that basically every logician I've ever talked to has agreed should exist, except we basically don't know how to do it. It's something that pretty clearly demands more creative insight than technical grunt, and unfortunately imaginative leaps don't come on demand. :/

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