Computability

Today is #PhilosophyFriday πŸ€”!

Today we'll be talking about the philosophical problem that kick-started all of Computer Science!

❓ Can we answer all mathematical questions? πŸ§΅πŸ‘‡


πŸ“† At the turn of the 20th century, the success of geometry, algebra, analysis and logic was hinting that it should be possible to unify all mathematics under a single theory.

Each of these fields had proven extremely useful, and there were seemingly not many problems left.


So they got together in 1900 to discuss the future of mathematics, and decide which were the most important problems left.

🎩 David Hilbert proposed 23 problems that he said should be solved by the end of the century. Today, all but 6 are either resolved or proven unsolvable.


But there is one that had far-reaching implications beyond mathematics. The question is this:

πŸ‘‰ Prove that the axioms of arithmetic are consistent.

Stated like this, it seems mostly harmless. But what does it mean?


Intuitively, an axiomatic system is consistent if there is no way you can prove a contradictory fact using logic.

This is super important, because if a theory allows internal contradictions to exist, then you could prove whatever crazy thing you want!

(πŸ€” Politics, anyone?)


Hilbert was convinced that, of course, arithmetic has to be consistent!

☝️ Otherwise, math itself, the purest intellectual invention of humanity, would be nothing different from the daily rambling of crazy people.

The answer, it turns, is absolutely mind-blowing.


In 1931, Kurt GΓΆdel proved something incredible:

🀯 In any sufficiently strong mathematical theory, there are always some true theorems that nevertheless cannot be proven within that theory.

Moreover, the question "is this theory consistent?" is one of them.


This was the first nail in the coffin of mathematical self-righteousness.

πŸ‘‰ If arithmetic, analysis, or algebra is consistent (which we hope they are), then that cannot be proven by mathematical means using arithmetic, analysis, or algebra.


The second nail came a couple of years later.

🀯 In 1933 Alfred Tarski proved that, in any sufficiently strong mathematical theory, the concept of "truth" cannot be formally defined inside that theory.


The final nail was put simultaneously by Alan Turing and Alonso Church in 1936.

🀯 They both showed, by different means, that it is impossible to write an algorithm to determine if any given theorem can be proved from a set of axioms.


These results collectively showed that there are very important questions in mathematics that we cannot answer within mathematics.

  • πŸ’‘ We cannot objectively define what truth is.
  • πŸ’‘ We cannot prove all truths.
  • πŸ’‘ We cannot be sure we don't have internal contradictions.

Up to 1930, most mathematics believed there was no such thing as an "unsolvable" problem. Now we know there are plenty. Many are esoteric problems, but some are very concrete. One of the most relevant ones is this:

πŸ‘‰ There is no way to be 100% sure a program is correct.


What does this mean, philosophically speaking?

⭐ It shows that there is an inherent gap between what is true, and what can be known. Mathematics, and by extension, Computer Science, cannot give us all the answers.

Is up to you to choose what this means for you.


As usual, if you like this topic, reply in this thread or @ me at any time. Feel free to ❀️ like and πŸ” retweet if you think someone else could benefit from knowing this stuff.

🧡 Read this thread online at https://apiad.net/tweetstorms/philosophyfriday-computability


Stay curious πŸ––:


πŸ—¨οΈ You can see this tweetstorm as originally posted in this Twitter thread.