Is such a long answer suitable in OT? If not, where should I move it?
tl;dr Naive ultrafinitism is based on real observations, but its proposals are a bit absurd. Modern ultrafinitism has close ties with computation. Paradoxically, taking ultrafinitism seriously has led to non-trivial developments in classical (usual) mathematics. Finally: ultrafinitism would probably be able to interpret all of classical mathematics in some way, but the details would be rather messy.
1 Naive ultrafinitism
1.1. There are many different ways of representing (writing down) mathematical objects.
The naive ultrafinitist chooses a representation, calls it explicit, and says that a number is “truly” written down only when its explicit representation is known. The prototypical choice of explicit representation is the tallying system, where 6 is written as ||||||. This choice is not arbitrary either: the foundations of mathematics (e. g. Peano arithmetic) use these tally marks by necessity.
However, the integers are a special^1 case, and in the general case, the naive ultrafinitist insistance on fixing a representation starts looking a bit absurd. Take Linear Algebra: should you choose an explicit basis of R3 that you use indiscriminately for every problem; or should you use a basis (sometimes an arbitary one) that is most appropriate for the problem at hand?
1.2. Not all representations are equally good for all purposes.
For example, enumerating the prime factors of 2*3*5 is way easier than doing the same for ||||||||||||||||||||||||||||||, even though both represent the same number.
1.3. Converting between representations is difficult, and in some cases outright impossible.
Lenstra earned $14,527 by converting the number known as RSA-100 from “positional” to “list of prime factors” representation.
Converting 3\^\^\^3 from up-arrow representation to the binary positional representation is not possible for obvious reasons.
As usual, up-arrow notation is overkill. Just writing the decimal number 100000000000000000000000000000000000000000000000000000000000000000000000000000000 would take more tally-marks than the number of atoms in the observable universe. Nonetheless, we can deduce a lot of things about this number: it is an even number, and its larger than RSA-100. Nonetheless, I can manually convert it to “list of prime factors” representation: 2\^80 * 5\^80.
2 Constructivism
The constructivists were the first to insist that algorithmic matters be taken seriously. Constructivism separates concepts that are not computably equivalent. Proofs with algorithmic content are distinguished from proofs without such content, and algorithmically inequivalent objects are separated.
For example, there is no algorithm for converting Dedekind cuts to equivalence classes of rational Cauchy sequences. Therefore, the concept of real number falls apart: constructively speaking, the set of Cauchy-real numbers is very different from the set of Dedekind-real numbers.
This is a tendency in non-classical mathematics: concepts that we think are the same (and are equivalent classically) fall apart into many subtly different concepts.
Constructivism separates concepts that are not computably equivalent. Computability is a qualitative notion, and even most constructivists stop here (or even backtrack, to regain some classicality, as in the foundational program known as Homotopy Type Theory).
3. Modern ultra/finitism
The same way constructivism distinguished qualitatively different but classically equivalent objects, one could starts distinguishing things that are constructively equivalent, but quantitatively different.
One path leads to the explicit approach to representation-awareness. For example, LNST^4 explicitly distinguishes between the set of binary natural numbers B and the set of tally natural numbers N. Since these sets have quantitatively different properties, it is not possible to define a bijection between B and N inside LNST.
Another path leads to ultrafinitism.
The most important thinker in modern ultra/finitism was probably Edward Nelson. He observed that the “set of effectively representable numbers” is not downward-closed: even though we have a very short notation for 3\^\^\^3, there are lots of numbers between 0 and 3^^^3 that have no such short representation. In fact, by elementary considerations, the overwhelming majority of them cannot ever have a short representation.
What’s more, if our system of notation allows for expressing big enough numbers, then the “set of effectively representable numbers” is not even inductive because of the Berry paradox. In a sense, the growth of ‘bad enough’ functions can only be expressed in terms of themselves. Nelson’s hope was to prove the inconsistency of arithmetic itself using a similar trick. His attempt was unsuccessful: Terry Tao pointed out why Nelson’s approach could not work.
This correspondence turned out to be very powerful, leading to many paradoxical developments: including finitistic^3 extension of Set Theory; a radically elementary treatment of Probability Theory and a new ways of formalising the Infinitesimal Calculus.
4. Answering your question
What kind of mathematics would we still be able do (cryptography, analysis, linear algebra …)?
All of it; modulo translating the classical results to the subtler, ultra/finitistic language. This holds even for the silliest versions of ultrafinitism. Imagine a naive ultrafinitist mathematician, who declares that the largest number is m. She can’t state the proposition R(n,2^(m)), but she can still state its translation R(log_2 n,m), which is just as good.
Translating is very difficult even for the qualitative case, as seen in this introductory video about constructive mathematics. Some theorems hold for Dedekind-reals, others for Cauchy-reals, et c. Similarly, in LNST, some theorems hold only for “binary naturals”, others only for “tally naturals”. It would be even harder for true ultrafinitism: the set of representable numbers is not downward-closed.
This was a very high-level overview. Feel free to ask for more details (or clarification).
^1 The integers are absolute. Unfortunately, it is not entirely clear what this means.
^2 coincidentally, the latter notion prompted my very first contribution to LW
^3 in this so-called Internal Set Theory, all the usual mathematical constructions are still possible, but every set of standard numbers is finite.
^4 Light Naive Set Theory. Based on Linear Logic. Consistent with unrestricted comprehension.
Is such a long answer suitable in OT? If not, where should I move it?
Anywhere is better than nowhere.
I think this is sufficiently good to go directly to Main article, but generally the safe option is to publish a Discussion article (which in case of success can be later moved to Main).
I would really like seeing more articles like this on LW—articles written by people who deeply understand what they write about. (Preferably with more examples, because this was difficult to follow without clicking the hyperlinks. But that may be just my personal preference.)
So, here are the options:
leave it here; (the easiest)
repost as an article; (still very easy)
rewrite as a more detailed article or series of articles (difficult)
Can’t the set of effectively representable numbers be inductive if we decide that “the smallest number not effectively representable” does not effectively represent a number?
“The smallest positive integer not definable in under twelve words” isn’t an effective representation of a number any more than “The number I’m thinking of” or “Potato potato potato potato potato” are.
Sure, that’s exactly what we have to do, on pain of inconsistency. We have to disallow representation schemas powerful enough to internalise the Berry paradox, so that “the smallest number not definable in less than 11 words” is not a valid representation. Cf. the various set theories, where we disallow comprehension schemas strong enough to internalise Russell’s paradox, so that “the set of all sets that don’t contain themselves” is not a valid comprehension.
Nelson thought that, similarly to how we reject “the smallest number not effectively representable” as an invalid representation, we should also reject e.g. “3^^^3″ as an invalid representation; not because of the Berry paradox, but because of a different one, one that he ultimately could not establish.
Nelson introduced a family of standardness predicates, each one relative to a hyper-operation notation (addition, multiplication, exponentiation, the ^^-up-arrow operation, the ^^^-up-arrow notation and so on). Since standardness is not a notion internal to arithmetic, induction is not allowed on these predicates (i. e. ‘0’ is standard, and if ‘x’ is standard then so is ‘x+1’, but you cannot use induction to conclude that therefore everything is standard).
He was able to prove that the standardness of n and m implies the standardness of n+m, and that of n×m. However, the corresponding result for exponentiation is provably false and the obstruction is non-associativity. What’s more, even if we can prove that 2^^d is standard, this does not mean that the same holds for 2^^(d+1).
At this point, Nelson attempted to prove that an explicit recursion of super-exponential length does not terminate, thereby establishing that arithmetic is inconsistent, and vindicating ultrafinitism as the only remaining option. His attempted proof was faulty, with no obvious fix. Nelson continued looking for a valid proof until his death last September.
One common method of resolving this is to cash out “representable” numbers in terms of outputs of halting turing machines, so that paradoxes of Berry’s sort require solving the halting problem and are therefore not themselves representations.
Some Turing machines have been proven to not halt; some have not. There must exist at least one Turing machine which no Turing machine can ever prove does not halt. (It is trivial to prove that a Turing machine halts if it does)
Since there are a countably infinite number of Turing machines, there must be at most a countably infinite number of characteristics such that only every non-halting Turing machine has one or more of those characteristics. If we suppose that each of these characteristics can be checked by a single Turing machine that halts when it proves that the target does not halt, then we have a contradiction (since we can build a Turing metamachine oracle that diagonalizes a countably infinite number of machines each testing one property).
Therefore there exists some characteristic of a Turing machine which is sufficient for that machine to be non-halting, such that it cannot be proven that said characteristic is sufficient.
I wonder what a program that doesn’t halt but cannot be proven not to halt looks like? What does the output look like after 2BB(n) steps? It must have a HALT function somewhere accessible, or else it would be trivial to prove that it never halted, but likewise said function must never happen, which means that the condition must never happen; but the condition must be accessible, or it would be trivial to prove that it never halted...
I think the typical example is if you do a search for a proof of inconsistency in Peano arithmetic. You don’t expect to find any inconsistencies, but you can’t prove that you won’t.
I believe that an ultrafinitist arithmetic would still be incomplete. By that I mean that classical mathematics could prove that a sufficiently powerful ultrafinitist arithmetic is necessarily incomplete. The exact definition of “sufficiently powerful”, and more importantly, the exact definition of “ultrafinitistic” would require attention. I’m not aware of any such result or on-going investigation.
The possibility of an ultrafinitist proof of Gödel’s theorem is a different question. For some definition of “ultrafinitistic”, even the well-known proofs of Gödel’s theorem qualify. Mayhap^1 someone will succed where Nelson failed, and prove that “powerful systems of arithmetic are inconsistent”. However, compared to that, Gödel’s 1st incompleteness theorem, which merely states that “powerful systems of arithmetic are either incomplete or inconsistent”, would seem rather… benign.
Is such a long answer suitable in OT? If not, where should I move it?
tl;dr Naive ultrafinitism is based on real observations, but its proposals are a bit absurd. Modern ultrafinitism has close ties with computation. Paradoxically, taking ultrafinitism seriously has led to non-trivial developments in classical (usual) mathematics. Finally: ultrafinitism would probably be able to interpret all of classical mathematics in some way, but the details would be rather messy.
1 Naive ultrafinitism
1.1. There are many different ways of representing (writing down) mathematical objects.
The naive ultrafinitist chooses a representation, calls it explicit, and says that a number is “truly” written down only when its explicit representation is known. The prototypical choice of explicit representation is the tallying system, where 6 is written as ||||||. This choice is not arbitrary either: the foundations of mathematics (e. g. Peano arithmetic) use these tally marks by necessity.
However, the integers are a special^1 case, and in the general case, the naive ultrafinitist insistance on fixing a representation starts looking a bit absurd. Take Linear Algebra: should you choose an explicit basis of R3 that you use indiscriminately for every problem; or should you use a basis (sometimes an arbitary one) that is most appropriate for the problem at hand?
1.2. Not all representations are equally good for all purposes.
For example, enumerating the prime factors of 2*3*5 is way easier than doing the same for ||||||||||||||||||||||||||||||, even though both represent the same number.
1.3. Converting between representations is difficult, and in some cases outright impossible.
Lenstra earned $14,527 by converting the number known as RSA-100 from “positional” to “list of prime factors” representation.
Converting 3\^\^\^3 from up-arrow representation to the binary positional representation is not possible for obvious reasons.
As usual, up-arrow notation is overkill. Just writing the decimal number 100000000000000000000000000000000000000000000000000000000000000000000000000000000 would take more tally-marks than the number of atoms in the observable universe. Nonetheless, we can deduce a lot of things about this number: it is an even number, and its larger than RSA-100. Nonetheless, I can manually convert it to “list of prime factors” representation: 2\^80 * 5\^80.
2 Constructivism
The constructivists were the first to insist that algorithmic matters be taken seriously. Constructivism separates concepts that are not computably equivalent. Proofs with algorithmic content are distinguished from proofs without such content, and algorithmically inequivalent objects are separated.
For example, there is no algorithm for converting Dedekind cuts to equivalence classes of rational Cauchy sequences. Therefore, the concept of real number falls apart: constructively speaking, the set of Cauchy-real numbers is very different from the set of Dedekind-real numbers.
This is a tendency in non-classical mathematics: concepts that we think are the same (and are equivalent classically) fall apart into many subtly different concepts.
Constructivism separates concepts that are not computably equivalent. Computability is a qualitative notion, and even most constructivists stop here (or even backtrack, to regain some classicality, as in the foundational program known as Homotopy Type Theory).
3. Modern ultra/finitism
The same way constructivism distinguished qualitatively different but classically equivalent objects, one could starts distinguishing things that are constructively equivalent, but quantitatively different.
One path leads to the explicit approach to representation-awareness. For example, LNST^4 explicitly distinguishes between the set of binary natural numbers B and the set of tally natural numbers N. Since these sets have quantitatively different properties, it is not possible to define a bijection between B and N inside LNST.
Another path leads to ultrafinitism.
The most important thinker in modern ultra/finitism was probably Edward Nelson. He observed that the “set of effectively representable numbers” is not downward-closed: even though we have a very short notation for 3\^\^\^3, there are lots of numbers between 0 and 3^^^3 that have no such short representation. In fact, by elementary considerations, the overwhelming majority of them cannot ever have a short representation.
What’s more, if our system of notation allows for expressing big enough numbers, then the “set of effectively representable numbers” is not even inductive because of the Berry paradox. In a sense, the growth of ‘bad enough’ functions can only be expressed in terms of themselves. Nelson’s hope was to prove the inconsistency of arithmetic itself using a similar trick. His attempt was unsuccessful: Terry Tao pointed out why Nelson’s approach could not work.
However, Nelson found a way to relate unexpressibly huge numbers to non-standard models of arithmetic^(2).
This correspondence turned out to be very powerful, leading to many paradoxical developments: including finitistic^3 extension of Set Theory; a radically elementary treatment of Probability Theory and a new ways of formalising the Infinitesimal Calculus.
4. Answering your question
All of it; modulo translating the classical results to the subtler, ultra/finitistic language. This holds even for the silliest versions of ultrafinitism. Imagine a naive ultrafinitist mathematician, who declares that the largest number is m. She can’t state the proposition R(n,2^(m)), but she can still state its translation R(log_2 n,m), which is just as good.
Translating is very difficult even for the qualitative case, as seen in this introductory video about constructive mathematics. Some theorems hold for Dedekind-reals, others for Cauchy-reals, et c. Similarly, in LNST, some theorems hold only for “binary naturals”, others only for “tally naturals”. It would be even harder for true ultrafinitism: the set of representable numbers is not downward-closed.
This was a very high-level overview. Feel free to ask for more details (or clarification).
^1 The integers are absolute. Unfortunately, it is not entirely clear what this means.
^2 coincidentally, the latter notion prompted my very first contribution to LW
^3 in this so-called Internal Set Theory, all the usual mathematical constructions are still possible, but every set of standard numbers is finite.
^4 Light Naive Set Theory. Based on Linear Logic. Consistent with unrestricted comprehension.
Anywhere is better than nowhere.
I think this is sufficiently good to go directly to Main article, but generally the safe option is to publish a Discussion article (which in case of success can be later moved to Main).
I would really like seeing more articles like this on LW—articles written by people who deeply understand what they write about. (Preferably with more examples, because this was difficult to follow without clicking the hyperlinks. But that may be just my personal preference.)
So, here are the options:
leave it here; (the easiest)
repost as an article; (still very easy)
rewrite as a more detailed article or series of articles (difficult)
Can’t the set of effectively representable numbers be inductive if we decide that “the smallest number not effectively representable” does not effectively represent a number?
“The smallest positive integer not definable in under twelve words” isn’t an effective representation of a number any more than “The number I’m thinking of” or “Potato potato potato potato potato” are.
Sure, that’s exactly what we have to do, on pain of inconsistency. We have to disallow representation schemas powerful enough to internalise the Berry paradox, so that “the smallest number not definable in less than 11 words” is not a valid representation. Cf. the various set theories, where we disallow comprehension schemas strong enough to internalise Russell’s paradox, so that “the set of all sets that don’t contain themselves” is not a valid comprehension.
Nelson thought that, similarly to how we reject “the smallest number not effectively representable” as an invalid representation, we should also reject e.g. “3^^^3″ as an invalid representation; not because of the Berry paradox, but because of a different one, one that he ultimately could not establish.
Nelson introduced a family of standardness predicates, each one relative to a hyper-operation notation (addition, multiplication, exponentiation, the ^^-up-arrow operation, the ^^^-up-arrow notation and so on). Since standardness is not a notion internal to arithmetic, induction is not allowed on these predicates (i. e. ‘0’ is standard, and if ‘x’ is standard then so is ‘x+1’, but you cannot use induction to conclude that therefore everything is standard).
He was able to prove that the standardness of n and m implies the standardness of n+m, and that of n×m. However, the corresponding result for exponentiation is provably false and the obstruction is non-associativity. What’s more, even if we can prove that 2^^d is standard, this does not mean that the same holds for 2^^(d+1).
At this point, Nelson attempted to prove that an explicit recursion of super-exponential length does not terminate, thereby establishing that arithmetic is inconsistent, and vindicating ultrafinitism as the only remaining option. His attempted proof was faulty, with no obvious fix. Nelson continued looking for a valid proof until his death last September.
One common method of resolving this is to cash out “representable” numbers in terms of outputs of halting turing machines, so that paradoxes of Berry’s sort require solving the halting problem and are therefore not themselves representations.
… Unless there exists something other than a Turing machine that can solve the halting problem.
Which of course leads us to things like “The set of Turing machines that do not halt and cannot be proven to not halt by any Turing machine”.
See the Church-Turing thesis for more on this topic.
I think I was on a slightly different topic:
Some Turing machines have been proven to not halt; some have not. There must exist at least one Turing machine which no Turing machine can ever prove does not halt. (It is trivial to prove that a Turing machine halts if it does)
Since there are a countably infinite number of Turing machines, there must be at most a countably infinite number of characteristics such that only every non-halting Turing machine has one or more of those characteristics. If we suppose that each of these characteristics can be checked by a single Turing machine that halts when it proves that the target does not halt, then we have a contradiction (since we can build a Turing metamachine oracle that diagonalizes a countably infinite number of machines each testing one property).
Therefore there exists some characteristic of a Turing machine which is sufficient for that machine to be non-halting, such that it cannot be proven that said characteristic is sufficient.
I wonder what a program that doesn’t halt but cannot be proven not to halt looks like? What does the output look like after 2BB(n) steps? It must have a HALT function somewhere accessible, or else it would be trivial to prove that it never halted, but likewise said function must never happen, which means that the condition must never happen; but the condition must be accessible, or it would be trivial to prove that it never halted...
I think the typical example is if you do a search for a proof of inconsistency in Peano arithmetic. You don’t expect to find any inconsistencies, but you can’t prove that you won’t.
More like trying to find the Godel statement of the universe; it provably exists, and provably cannot be positively identified.
Thank you for this insightful and comprehensive reply!
I have a follow-up question: Would ultrafinitist arithmetic still be incomplete due to Gödel’s incompleteness theorem?
I believe that an ultrafinitist arithmetic would still be incomplete. By that I mean that classical mathematics could prove that a sufficiently powerful ultrafinitist arithmetic is necessarily incomplete. The exact definition of “sufficiently powerful”, and more importantly, the exact definition of “ultrafinitistic” would require attention. I’m not aware of any such result or on-going investigation.
The possibility of an ultrafinitist proof of Gödel’s theorem is a different question. For some definition of “ultrafinitistic”, even the well-known proofs of Gödel’s theorem qualify. Mayhap^1 someone will succed where Nelson failed, and prove that “powerful systems of arithmetic are inconsistent”. However, compared to that, Gödel’s 1st incompleteness theorem, which merely states that “powerful systems of arithmetic are either incomplete or inconsistent”, would seem rather… benign.
^1 very unlikely, but not cosmically unlikely
What is LNST?
Edit: Nevermind, saw the footnote.