32
$\begingroup$

I am currently reading Theorem Proving in Lean, a document dealing with how to use Lean (an open source theorem prover and programming language). My question stems from chapter 11.

The particular section of the chapter that I'm interested in discusses the history and philosophical context of an initially "essentially computational" style of mathematics, until the 19th century, when a "more "conceptual"" understanding of mathematics was required.

The following quote is taken from the second paragraph of section 11.1 of the linked document.

The goal was to obtain a powerful “conceptual” understanding without getting bogged down in computational details, but this had the effect of admitting mathematical theorems that are simply false on a direct computational reading.

This is by no means essential to the understanding of the contents of the document itself, but I'm curious to ask what examples of theorems are false in a "direct computational reading".

In other words, are there any examples of theorems that are true conceptually, but false computationally?

$\endgroup$
  • 1
    $\begingroup$ Maybe related to Constructive Mathematics. $\endgroup$ – Mauro ALLEGRANZA Jul 4 '18 at 11:39
  • 1
    $\begingroup$ See also Five stages of accepting constructive mathematics and Constructive Mathematics. $\endgroup$ – Mauro ALLEGRANZA Jul 4 '18 at 11:47
  • 1
    $\begingroup$ IMO, the author is alluding to one of many examples of classical theorems of e.g. anlaysis proving by reductio the existence of a certain number/function without providing a way to "locate" such an object: see @Andrej Bauer 's discussion above (page 492) regarding classical vs constructive proof of the Intermediate value theorem. $\endgroup$ – Mauro ALLEGRANZA Jul 4 '18 at 12:03
  • $\begingroup$ Yes, I wish to know about examples in the differences between "conceptual" (maybe non-constructive? I'm not sure) and "computational" (constructive?) - in which case the intermediate value theorem as stated above seems to show that difference well. Thanks! $\endgroup$ – Elliott Macneil Jul 4 '18 at 12:07
49
$\begingroup$

Here is a longer quote from the article linked in the question:

For most of its history, mathematics was essentially computational: geometry dealt with constructions of geometric objects, algebra was concerned with algorithmic solutions to systems of equations, and analysis provided means to compute the future behavior of systems evolving over time. From the proof of a theorem to the effect that “for every x, there is a y such that …”, it was generally straightforward to extract an algorithm to compute such a y given x.

In the nineteenth century, however, increases in the complexity of mathematical arguments pushed mathematicians to develop new styles of reasoning that suppress algorithmic information and invoke descriptions of mathematical objects that abstract away the details of how those objects are represented. The goal was to obtain a powerful “conceptual” understanding without getting bogged down in computational details, but this had the effect of admitting mathematical theorems that are simply false on a direct computational reading.

With that, we see that the authors are talking about theorems of the form "for every $x$ there is a $y$ ...". There are many such theorems that are true classically, and where objects of the type of $x$ and $y$ could be represented by a computer, but where there is no program to produce $y$ from $x$. This area of study overlaps constructive mathematics and computability theory. In computability theory, rather than just proving that particular theorems are not computably true, we instead try to classify how uncomputable the theorems are. There is also a research field of proof mining which is able to extract algorithms from a number of classical proofs (of course, not all). This program has led to new concrete bounds for theorems in analysis, among other things.

The phenomenon of uncomputability in classical mathematical theorems is very widespread. I will give just a few examples, trying to include several areas of mathematics.

Hilbert's 10th Problem One example comes from Hilbert's 10th problem. Given a multivariable polynomial with integer coefficients, there is a natural number $n$ so that $n = 1$ if the polynomial has an integer root, and $n = 0$ otherwise. This is a trivial classical theorem, but the MDRP theorem shows exactly that there is no program that can produce $n$ from the polynomial in every case.

That is, given a multivariable polynomial with integer coefficients, where we can substitute integers for the variables, there is no effective way to decide whether $0$ is in the range. The proof uses classical computability theory, and shows that this decision problem is equivalent to the halting problem, a benchmark example of an uncomputable decision problem.

Jordan forms Anther example comes when we work with infinite precision real numbers, so that a real number is represented as a Cauchy sequence of rationals that converges at a fixed rate. These sequences can be manipulated by programs, and this is a standard part of computable analysis.

We know from linear algebra that every square matrix over the reals has a Jordan canonical form. However, there is no program that, given a square matrix of infinite precision reals, produces the Jordan canonical form matrix.

The underlying reason for this is continuity: fixing a dimension $N$, the map that takes an $N \times N$ matrix to its Jordan form is not continuous. However, if this function were computable then it would be continuous, giving a contradiction.

Countable graph theory It is easy to represent a countable graph for a computer: we let natural numbers represent the nodes and we provide a function that tells whether there is an edge between any two given nodes. It is a classical theorem that "for each countable graph there is a set of nodes so that the set has exactly one node from each connected component". This is false computationally: there are countable graphs for which the edge relation is computable, but there is no computable set that selects one node from each connected component.

König's Lemma Every infinite, finitely branching tree has an infinite path. However, even if the tree itself is computable, there does not need to be an infinite computable path.

Intermediate value theorem Returning to analysis, we can also represent continuous functions from the reals to the reals in a way that, given an infinite precision real number, a program can compute the value of the function at that number, producing another infinite precision real number. The representation is called a code of the function.

The intermediate value theorem is interesting because it is computably true in a weak sense but not in a stronger sense.

  • It is true that, for any computable continuous function $[0,1] \to \mathbb{R}$ with $f(0)\cdot f(1) < 0$, there is a computable real $\xi \in [0,1]$ with $f(\xi) = 0$. So, if we lived in a world where everything was computable, the intermediate value theorem would be true.

  • At the same time, there is not a computable functional $G$ that takes as input any code for a continuous function $f$ satisfying the hypotheses above, and produces a $\xi = G(f)$ with $f(\xi) = 0$. So, although the intermediate value theorem might be true, there is no way to effectively find or construct the root just given a code for the continuous function.

$\endgroup$
  • 1
    $\begingroup$ Thank you for the additional details! This gives a variety of examples, all of which show exactly what I was looking for :> $\endgroup$ – Elliott Macneil Jul 4 '18 at 13:34
  • $\begingroup$ Aren't there an uncountable number of countable graphs? $\endgroup$ – DanielV Jul 4 '18 at 13:51
  • 3
    $\begingroup$ @DanielV: yes. We can pass any countable graph to a Turing machine by passing the characteristic function of the edge relation, so even though there are uncountably many, it still makes sense to ask whether we can compute a set of component representatives from that relation. But there are even computable graphs with no computable set of component representatives. There are also uncountably many finitely branching infinite trees, of course, and uncountably many continuous functions $[0,1] \to \mathbb{R}$. $\endgroup$ – Carl Mummert Jul 4 '18 at 15:05
  • $\begingroup$ Why is it that if Jordan form was computable then it would be continuous? $\endgroup$ – Serge Seredenko Jul 5 '18 at 8:43
  • $\begingroup$ @Serge Seredenko: this has to do with the way that computation on infinite precision reals works; nothing to do with Jordan form particularly. When we compute a real number $y$ from a real $x$, the computation moves step by step, and each step only looks at a finite approximation to $x$. As these steps are carried out, a sequence of approximations converging to $y$ is produced. Since each of these approximations of $y$ only depends on a sufficient approximation of $x$ (i.e. the fact that $x$ is in some neighborhood), the resulting function ends up being continuous. $\endgroup$ – Carl Mummert Jul 5 '18 at 19:52
3
$\begingroup$

This paper by Potgieter has examples to show that, in a suitable computational sense, Brouwer's Fixed point theorem is false. Quoting from the abstract:

The main results, the counter-examples of Orevkov and Baigger, imply that there is no procedure for finding the fixed point in general by giving an example of a computable function which does not fix any computable point.

$\endgroup$

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.