I was expecting the worst, but this was actually a really well-done video explaining the issues to do with completeness, consistency, and decidability in mathematics, and how it relates to computer science. Highly recommended!

Moreover, there is also a lack of knowledge about Karl Popper and the scientific method in scientific circles. For most it is counter intuitive to understand the rejection of the inductivist approach of the scientific method and the limits sets by the empirical falsification. Accepting that in empirical sciences, no theory can be proven is at the opposite how education and teaching scientific theory is done and how the transfer of knowledge occurs in academia (being lessons at university or peer-reviewed research). I wish we could accept and teach a more probabilist view of the truth without the need to set in stone everything. It goes further than just science but it is really present in the scientific discouse.

This reminds me of Gettier’s two-pager “Is Justified True Belief Knowledge?” His counter examples rely on conclusions from cogent inductive arguments being true for the wrong reasons.

While I am far from being an expert on this topic, I have always felt that the importance of incompleteness theorems in computer science and mathematics has been overstated. Part of the reason is terminology – while it’s true in mathematical terms that “you can’t prove everything that’s true”, the statement sounds a lot deeper than it really is because the mathematicians are using a very specific definition of “proof” and “true” and “everything” that doesn’t necessarily correspond to the definitions we are all familiar with.

I like to see incompleteness as a modeling problem. We normally choose a certain set of axioms to encode our assumptions about the world. Those axioms aren’t exhaustive, so it’s possible to imagine two systems which satisfy the axioms but differ in other important ways, leading to statements that are “true” in one system but “false” in the other. If you want to narrow the scope of your analysis, you need to introduce more axioms – so we have things like parallel postulate to separate Euclidean from non-Euclidean geometry. This is a reminder that all models are wrong, but some are useful. If we study the world through a lens of a particular set of axioms, we might be able to use the axioms to prove things about the world, but behavior we observe in the world may or may not be a consequence of those axioms.

Philosophers brought up exactly this objection to Gödel’s initial work: Sure, perhaps the Peano natural numbers are incomplete, but that doesn’t mean that reality itself is incomplete or inconsistent, just that Peano’s definitions are incomplete.

Tarski saw how to extend Gödel’s work to cover this loophole. Tarski’s Undefinability of Truth is, broadly, the claim that a sufficiently-complex formal system is always unable to talk about its own notion of truth. Here, “proof” means a sequence of logical syllogisms, “true” means proofs that start from axioms, and “everything” means any objects which are described inside the formal system. Tarski took Gödel’s statement about natural numbers, and extended it to any system which claims to talk of beauty, love, truth, etc., as long as that system also happens to know about natural numbers.

What Gödel showed isn’t that all models of the natural numbers are wrong, but that some models of the natural numbers are useful. Rather, what they showed is that all theories of the natural numbers are incomplete at best. No finite listing of first-order axioms can fully describe the natural numbers; given any such set of axioms, Gödel showed how to generate an infinite list of axioms G₀, G₁, etc. which each denote a true-but-unprovable fact about natural numbers.

In general, we need to understand that theories (axioms and rules) are not the same as models (objects described by the axioms and rules), or else Skolem’s Paradox will keep us up at night.

Finally, we now know from category theory that there is a beautiful generalization of Gödel and Turing, known as Lawvere’s fixed-point theorem. Lawvere showed that Cantor, Turing, Gödel, Tarski, and others were all talking about the same situation, where a categorical construction – a transformation which can decide any possibility – is handed its own negation. Lawvere explains that the paradox comes from our interpretation of these constructions as self-referential, tying an imaginary knot which isn’t in the formal theory.

Raymond Smullyan’s Godel’s Incompleteness Theorems is a good introduction. The slick proof of the second incompleteness theorem using Löb’s theorem can be found in Boolos’ Provability Logic but that text is heavier…

I recently read and enjoyed An Introduction to Gödel’s Theorems, which is comprehensive and gradual, slowly exploring everything I talked about except for Lawvere’s work. Their version of Tarski starts on p197.

It’s hard to believe that a person could really prove that something can “never” happen — imagine if someone told you that we could never travel farther than our solar system — you’d look at them with suspicion.

I’d need a whole lot more technical and scientific evidence before accepting humanity will travel significantly within the solar system, never mind out of it.

Yeah that’s a strange phrasing. There’s plenty of math theorems that prove something can never happen. Off the top of my head, the irrationality of sqrt(2) comes to mind.

Yeah, I know what you mean – it’s definitely a bit frustrating when folks in programming circles bring up the halting problem and undecidability whenever you try to talk about formal verification, for example.

I think this was kind of touched on towards the end of the video, where the presenter explains how the incompleteness theorems didn’t result in the collapse of mathematics, and we can still do a huge amount of work in spite of them. And that the result of grappling with self-reference and undecidability in mathematics was many advances that we take for granted today. So while we have learned to accept it now I think it’s still incredibly useful to teach people about.

I like this way of thinking about it, but still it strikes me as incredible, and not at all obvious, that this same “parallel postulate problem” will crop up in any (sufficiently powerful) axiomatic system, and that we can prove this meta fact formally. It’s a mind-blowing intellectual achievement.

You can’t prove everything from any single set of axioms. What most people hear is that there are theorems which are unprovable in any and all systems, which is a very different idea. For example here is a rather large number of theorems that can’t be proved in ZFC set theory, but can be proved with extensions to ZFC: https://en.wikipedia.org/wiki/List_of_statements_independent_of_ZFC

It would be a bigger surprise today if we can find a theorem that is unprovable in all maths systems we can devise than the original ideas of incompleteness were last century.

I was expecting the worst, but this was actually a really well-done video explaining the issues to do with completeness, consistency, and decidability in mathematics, and how it relates to computer science. Highly recommended!

Moreover, there is also a lack of knowledge about Karl Popper and the scientific method in scientific circles. For most it is counter intuitive to understand the rejection of the inductivist approach of the scientific method and the limits sets by the empirical falsification. Accepting that in empirical sciences, no theory can be proven is at the opposite how education and teaching scientific theory is done and how the transfer of knowledge occurs in academia (being lessons at university or peer-reviewed research). I wish we could accept and teach a more probabilist view of the truth without the need to set in stone everything. It goes further than just science but it is really present in the scientific discouse.

This reminds me of Gettier’s two-pager “Is Justified True Belief Knowledge?” His counter examples rely on conclusions from cogent inductive arguments being true for the wrong reasons.

The few minutes starting here are the best explanation I’ve seen of why the halting problem is undecidable.

While I am far from being an expert on this topic, I have always felt that the importance of incompleteness theorems in computer science and mathematics has been overstated. Part of the reason is terminology – while it’s true in mathematical terms that “you can’t prove everything that’s true”, the statement sounds a lot deeper than it really is because the mathematicians are using a very specific definition of “proof” and “true” and “everything” that doesn’t necessarily correspond to the definitions we are all familiar with.

I like to see incompleteness as a

modeling problem. We normally choose a certain set of axioms to encode our assumptions about the world. Those axioms aren’t exhaustive, so it’s possible to imagine two systems which satisfy the axioms but differ in other important ways, leading to statements that are “true” in one system but “false” in the other. If you want to narrow the scope of your analysis, you need to introduce more axioms – so we have things like parallel postulate to separate Euclidean from non-Euclidean geometry. This is a reminder thatall models are wrong, but some are useful. If we study the world through a lens of a particular set of axioms, we might be able to use the axioms to prove things about the world, but behavior we observe in the world may or may not be a consequence of those axioms.Philosophers brought up exactly this objection to Gödel’s initial work: Sure, perhaps the Peano natural numbers are incomplete, but that doesn’t mean that reality itself is incomplete or inconsistent, just that Peano’s definitions are incomplete.

Tarski saw how to extend Gödel’s work to cover this loophole. Tarski’s Undefinability of Truth is, broadly, the claim that a sufficiently-complex formal system is always unable to talk about its own notion of truth. Here, “proof” means a sequence of logical syllogisms, “true” means proofs that start from axioms, and “everything” means

anyobjects which are described inside the formal system. Tarski took Gödel’s statement about natural numbers, and extended it to any system which claims to talk of beauty, love, truth, etc., as long as that system also happens to know about natural numbers.What Gödel showed isn’t that all models of the natural numbers are wrong, but that some models of the natural numbers are useful. Rather, what they showed is that all theories of the natural numbers are incomplete at best. No finite listing of first-order axioms can fully describe the natural numbers; given any such set of axioms, Gödel showed how to generate an infinite list of axioms G₀, G₁, etc. which each denote a true-but-unprovable fact about natural numbers.

In general, we need to understand that theories (axioms and rules) are not the same as models (objects described by the axioms and rules), or else Skolem’s Paradox will keep us up at night.

Finally, we now know from category theory that there is a beautiful generalization of Gödel and Turing, known as Lawvere’s fixed-point theorem. Lawvere showed that Cantor, Turing, Gödel, Tarski, and others were all talking about the same situation, where a categorical construction – a transformation which can decide any possibility – is handed its own negation. Lawvere explains that the paradox comes from our interpretation of these constructions as self-referential, tying an imaginary knot which isn’t in the formal theory.

Can you recommend any good accessible books (or other material) on formal model theory?

The kind of thing that would teach precisely what is meant by a sentence (from the Tarksi Wikipedia article) such as:

Raymond Smullyan’s

Godel’s Incompleteness Theoremsis a good introduction. The slick proof of the second incompleteness theorem using Löb’s theorem can be found in Boolos’Provability Logicbut that text is heavier…I recently read and enjoyed An Introduction to Gödel’s Theorems, which is comprehensive and gradual, slowly exploring everything I talked about except for Lawvere’s work. Their version of Tarski starts on p197.

I recently encountered https://stopa.io/post/269, which is quick but useful.

I’d need a whole lot more technical and scientific evidence before accepting humanity will travel significantly

withinthe solar system, never mind out of it.Yeah that’s a strange phrasing. There’s plenty of math theorems that prove something can never happen. Off the top of my head, the irrationality of sqrt(2) comes to mind.

https://en.wikipedia.org/wiki/Proof_by_contradiction#Irrationality_of_the_square_root_of_2

Interesting. This looks a bit like a formalization of the Münchausen trilemma.

Yeah, I know what you mean – it’s definitely a bit frustrating when folks in programming circles bring up the halting problem and undecidability whenever you try to talk about formal verification, for example.

I think this was kind of touched on towards the end of the video, where the presenter explains how the incompleteness theorems didn’t result in the collapse of mathematics, and we can still do a huge amount of work in spite of them. And that the result of grappling with self-reference and undecidability in mathematics was many advances that we take for granted today. So while we have learned to accept it now I think it’s still incredibly useful to teach people about.

I like this way of thinking about it, but still it strikes me as incredible, and not at all obvious, that this same “parallel postulate problem” will crop up in

any(sufficiently powerful) axiomatic system, and that we can prove this meta fact formally. It’s a mind-blowing intellectual achievement.You can’t prove everything from any single set of axioms. What most people hear is that there are theorems which are unprovable in any and all systems, which is a very different idea. For example here is a rather large number of theorems that can’t be proved in ZFC set theory, but can be proved with extensions to ZFC: https://en.wikipedia.org/wiki/List_of_statements_independent_of_ZFC

A project to formalize those ideas: https://en.wikipedia.org/wiki/Reverse_mathematics

It would be a bigger surprise today if we can find a theorem that is unprovable in all maths systems we can devise than the original ideas of incompleteness were last century.