15 ms·

Formalising Gödel's incompleteness theorems, I

83 points by furcyd 4y ago

tombert 4y ago
I started my PhD recently, and in the process I've had to learn Isabelle/HOL, and I gotta say that using it sort of feels like you're unlocking the keys to understanding the universe. Like, I understand that it's fundamentally still code, and so there are potential bugs in the kernel, but shear versatility and level of automation you get within Isabelle/HOL makes the development and understanding of proof feel like outright magic sometimes. Proof is really hard, and having a powerful tool to mechanically check it has nearly limitless potential.
- auggierose 4y ago
  Amen!
- thomasdziedzic 4y ago
  > using it sort of feels like you're unlocking the keys to understanding the universe. Completely agree! > having a powerful tool to mechanically check it has nearly limitless potential As someone working in the industry and playing with theorem provers in my spare time, I've never been able to bridge the gap between industry and theory enough to be able to use these formal methods on projects that I'm on.
  - tombert 4y ago
    Sadly I too have not found an employer that is willing to let me use any kind of theorem-proving software in production. Back when I was at Jet doing F#, I almost got permission to use F-Star [1], but that project never got to that point. My PhD is in regards to proving properties about robotics, so maybe in 5-6 years I'll have fully bridged industry and theory, but I wouldn't hold my breath :) [1] https://www.fstar-lang.org/ https://www.fstar-lang.org/
    - DennisP 4y ago
      Theorem-proving gets some use in the Ethereum community. Smart contracts are an ideal application for it: the code is short and bugs can be disastrous.
    - JadeNB 4y ago
      > Sadly I too have not found an employer that is willing to let me use any kind of theorem-proving software in production. Back when I was at Jet doing F#, I almost got permission to use F-Star [1], but that project never got to that point. As someone who doesn't code for a living, I am certain that this is a naïve question, but, if you want to use theorem-proving software for verification of existing code, does that require employer permission? Is the issue something like, e.g., you need the theorem-proving software and the code to be verified on the same machine, and you're not allowed to install the theorem-proving software on a work machine or to move the code to a non-work machine?
      - tombert 4y ago
        I meant that I couldn't get budget to do it. Obviously I could do a code verification in my free time, but my goal was to start the project with everything that could be written in FStar being written in FStar, with my coworkers onboard. I had root access to my laptop so I could install anything I wanted, but it's hard to do anything if you don't have budget allocated to do so. EDIT: I also should point out that I wanted to export the code from FStar to F# and use the exported and verified code.
      - bluGill 4y ago
        I work on a project that is 20 million lines of code - while large someone reading this is working on a project much larger. There is no way any human working alone can prove the whole thing. I have no idea how to even get started. Even if I did, until I can prove theorem proving is useful in the real world I'm stuck doing it as a side project: my boss will encourage it, but if I spend no more than a couple hours a week one it Now in my company we are worried about bugs and reliability. If I can show via example that theorem proving catches bugs they will train all developers on it and demand all code be proved. However proving quality needs to be something that is worth the effort, if it slightly increases quality but at the expense of making projects take 10 times as long it is probably not worth it except for specific areas of concern.
- joshmarlow 4y ago
  Off topic, but I'm an engineer whose math extends (shakily) into basic proofs (though I'm rusty). I tinkered quite a bit with Lean a couple of years ago and felt comfortable with it as a language, but I don't actually grok how to use it effectively for proving theorems (I'd love to get into formal verification). Do you have any recommendations for getting started? Something like a "Proofs for Hackers"?
  - opnitro 4y ago
    Software Foundations is always a great place to start! (https://softwarefoundations.cis.upenn.edu/ https://softwarefoundations.cis.upenn.edu/) It uses Coq not Isabelle, but it's a great starting point and contains a ton of useful information. The book is one large literate program, so it's easy to follow along and do the exercises.
  - tombert 4y ago
    Software Foundations (mentioned in a sister comment) is great, and highly recommended. If you want something more Isabelle-focused, the Concrete Semantics book is pretty good [1]. Not exactly the same, but if you want something a bit more approachable than Isabelle or Coq or Agda, it might be worth looking into TLA+. That can introduce you to predicate logic and state machines and set theory if you're not already familiar with them, and TLA+ is a lot more programmer-centric and less pure-mathey than Isabelle. TLA+ offers model checking for "brute force" verification, and also offers a formal proof system called TLAPS. Lamport's talks on TLA+ are quite good [2], and I found that learning Isabelle was a lot easier once I had a lot of practice with TLA+. [1] http://concrete-semantics.org/ http://concrete-semantics.org/ [2] https://lamport.azurewebsites.net/video/videos.html https://lamport.azurewebsites.net/video/videos.html
jameshart 4y ago
Someone needs to tell the mathematicians they are allowed to use variable names longer than a single character now.
- SemanticStrengh 4y ago
  that elitism has to stop, people should design hyeroglyphs-free programming languages optimized for mathematical expressions and proofs should be written in it. The lack of IDE support in regular mathML or PDF math is astonishing.
- paskozdilar 4y ago
  They fscked up when they decided to omit the dot when multiplying. So now it's impossible to differentiate between "varname" and "var*name".
  - JadeNB 4y ago
    > They fscked up when they decided to omit the dot when multiplying. So now it's impossible to differentiate between "varname" and "var*name". Well, since we don't use multi-letter variable names, no such distinction is necessary! But if, for some reason, we did do so, then these two cases would be typeset in LaTeX as \(varname\) and \(var\,name\) (or, rather, \(\mathit{var}\) and \(\mathit{var}\,\mathit{name}\), since TeX correctly interprets \(var\) as semantically `var` anyway).
    - paskozdilar 4y ago
      > Well, since we don't use multi-letter variable names, no such distinction is necessary! You remember the story about the Fox and the Grapes, right?
- SilasX 4y ago
  Go programmers, too. https://github.com/golang/go/wiki/CodeReviewComments#variable-names https://github.com/golang/go/wiki/CodeReviewComments#variabl...
- 4y ago
alok-g 4y ago
>> Formalisation of the internal calculus, HF HF seems 'hereditarily finite'. I wish someone presents the proof that's 'inlines' the explanation of the terminology used and defines them before using. For something as fundamental as Godel's theorems, this should be worth doing.
SemanticStrengh 4y ago
I feel like godel incompleteness is a cheap trick that mislead to think there are statements in ZFC that can't be proven except that those proven statement are contrived useless meta-statements.
- deltasepsilon 4y ago
  I'm going to assume you mean that the true unprovable sentences that Gödel constructed are contrived. I don't think I can convince you otherwise, except to say that others thought like you and eventually Paris and Harrington came up with [1]. You can make even more "concrete" statements, see the work of Chaitin, but all this stems from Hilbert's very concrete 10th problem [2]. I must say, be careful with "reasoning". For example, once a philosophy PhD minimized mathematics eloquently by saying all mathematical results are "tautological", hence uninteresting. Hence, why bother studying it, and in your case, why bother thinking Gödel did anything special. Why bother about anything at all... there's the rub. [1] https://en.wikipedia.org/wiki/Paris–Harrington_theorem https://en.wikipedia.org/wiki/Paris–Harrington_theorem [2] https://en.wikipedia.org/wiki/Hilbert's_tenth_problem https://en.wikipedia.org/wiki/Hilbert's_tenth_problem
  - SemanticStrengh 4y ago
    > Since Peano arithmetic cannot prove its own consistency by Gödel's second incompleteness theorem, this shows that Peano arithmetic cannot prove the strengthened finite Ramsey theorem. This seems quite circular, where the (claims mine) contrived statements enabling godel 2 incompletude theorem, make it unable to prove a non-contrived statement? Thanks for the reference though, I'll admit that is a topic I'm not familiar enough with to fully challenge it. > I must say, be careful with "reasoning". For example, once a philosophy PhD minimized mathematics eloquently by saying all mathematical results are "tautological", hence uninteresting. Hence, why bother studying it, and in your case, why bother thinking Gödel did anything special. Yeah that's a classic, it's a good thought experiment but that only prove that one must not be careful with the pruning that can enable high level reasoning but more with being careful of fallacious or misleading reasonings. Yes in theory, mathematical chain proofs are only tautologies derived from ZFC/higher order logic, so yes mathematics doesn't say anything new. However in practice, the task of unfolding reasoning chains and being able to refer to past lemnas as abtractions/objects, enable the reader to optimize for cognition, and hence the more proofs advances, the more we can discover, retain, understand and refer, useful tautological yet transitive knowledge.
deltaonefour 4y ago
If Godel's theorem applies to all formal systems. Then in formalizing Godel's theorem, doesn't that make the theorem apply to itself? So the calculus that formalises the theorem is either inconsistent or there are other true statements about it that can't be proven? Which is it? Can someone with a bigger brain elaborate on how the theorem applies to itself in a language for tiny brained people? No big words please.
- jameshart 4y ago
  I think the short version is: just because any formal system is guaranteed to be incomplete doesn't mean it can't prove useful things. And even an incomplete formal system can prove Gödel's Incompleteness Theorem.
- birriel 4y ago
  I asked a similar question a while back: https://news.ycombinator.com/item?id=27915824 https://news.ycombinator.com/item?id=27915824
- irq-1 4y ago
  > true statements about it that can't be proven? Its missing the qualifier: can't be proven in that system. They can be examined from outside the system, or say, with a different system.
  - qiskit 4y ago
    The problem still continues. Even if you add the unprovable formula ( lets say formula1) in System1 as an axiom to System2 ( System1 + formula1 ), System2 will have its own unprovable formulas even though formula1 would be superficially provable in System2. You could add the unprovable formulas in System2 as axioms to System3 but System3 will have its own unprovable formulas . Godel showed that it's simply the nature of any formal system with complexity greater than or equal to arithmetic.
- bumbledraven 4y ago
  Godel’s incompleteness theorems are about formal systems. A formal system can be thought of as an algorithm that takes a purported formal proof of some arithmetical statement (e.g. there is no largest twin prime) and returns true/false depending on whether the proof is correct. Call the algorithm a “proof checker” and say it “accepts” a statement if it returns true for some purported proof of the statement. Godel’s first incompleteness theorem says that at least one of the following is true: (1) There is some statement such that the checker accepts both the statement and the statement’s negation (e.g. the checker accepts both “2 + 2 = 4” and “2 + 2 ≠ 4”). This is called inconsistency. (2) There is some true statement which the checker will not accept. This is called incompleteness. Since Godel’s first incompleteness theorem is not a formal system, it does not apply to itself.
timcavel 4y ago
deleted 4y ago
[deleted]
deleted 4y ago
[deleted]

83 points by furcyd 4y ago

I started my PhD recently, and in the process I've had to learn Isabelle/HOL, and I gotta say that using it sort of feels like you're unlocking the keys to understanding the universe. Like, I understand that it's fundamentally still code, and so there are potential bugs in the kernel, but shear versatility and level of automation you get within Isabelle/HOL makes the development and understanding of proof feel like outright magic sometimes. Proof is really hard, and having a powerful tool to mechanically check it has nearly limitless potential.

auggierose 4y ago
Amen!
thomasdziedzic 4y ago
> using it sort of feels like you're unlocking the keys to understanding the universe. Completely agree! > having a powerful tool to mechanically check it has nearly limitless potential As someone working in the industry and playing with theorem provers in my spare time, I've never been able to bridge the gap between industry and theory enough to be able to use these formal methods on projects that I'm on.
- tombert 4y ago
  Sadly I too have not found an employer that is willing to let me use any kind of theorem-proving software in production. Back when I was at Jet doing F#, I almost got permission to use F-Star [1], but that project never got to that point. My PhD is in regards to proving properties about robotics, so maybe in 5-6 years I'll have fully bridged industry and theory, but I wouldn't hold my breath :) [1] https://www.fstar-lang.org/ https://www.fstar-lang.org/
  - DennisP 4y ago
    Theorem-proving gets some use in the Ethereum community. Smart contracts are an ideal application for it: the code is short and bugs can be disastrous.
  - JadeNB 4y ago
    > Sadly I too have not found an employer that is willing to let me use any kind of theorem-proving software in production. Back when I was at Jet doing F#, I almost got permission to use F-Star [1], but that project never got to that point. As someone who doesn't code for a living, I am certain that this is a naïve question, but, if you want to use theorem-proving software for verification of existing code, does that require employer permission? Is the issue something like, e.g., you need the theorem-proving software and the code to be verified on the same machine, and you're not allowed to install the theorem-proving software on a work machine or to move the code to a non-work machine?
    - tombert 4y ago
      I meant that I couldn't get budget to do it. Obviously I could do a code verification in my free time, but my goal was to start the project with everything that could be written in FStar being written in FStar, with my coworkers onboard. I had root access to my laptop so I could install anything I wanted, but it's hard to do anything if you don't have budget allocated to do so. EDIT: I also should point out that I wanted to export the code from FStar to F# and use the exported and verified code.
    - bluGill 4y ago
      I work on a project that is 20 million lines of code - while large someone reading this is working on a project much larger. There is no way any human working alone can prove the whole thing. I have no idea how to even get started. Even if I did, until I can prove theorem proving is useful in the real world I'm stuck doing it as a side project: my boss will encourage it, but if I spend no more than a couple hours a week one it Now in my company we are worried about bugs and reliability. If I can show via example that theorem proving catches bugs they will train all developers on it and demand all code be proved. However proving quality needs to be something that is worth the effort, if it slightly increases quality but at the expense of making projects take 10 times as long it is probably not worth it except for specific areas of concern.
joshmarlow 4y ago
Off topic, but I'm an engineer whose math extends (shakily) into basic proofs (though I'm rusty). I tinkered quite a bit with Lean a couple of years ago and felt comfortable with it as a language, but I don't actually grok how to use it effectively for proving theorems (I'd love to get into formal verification). Do you have any recommendations for getting started? Something like a "Proofs for Hackers"?
- opnitro 4y ago
  Software Foundations is always a great place to start! (https://softwarefoundations.cis.upenn.edu/ https://softwarefoundations.cis.upenn.edu/) It uses Coq not Isabelle, but it's a great starting point and contains a ton of useful information. The book is one large literate program, so it's easy to follow along and do the exercises.
- tombert 4y ago
  Software Foundations (mentioned in a sister comment) is great, and highly recommended. If you want something more Isabelle-focused, the Concrete Semantics book is pretty good [1]. Not exactly the same, but if you want something a bit more approachable than Isabelle or Coq or Agda, it might be worth looking into TLA+. That can introduce you to predicate logic and state machines and set theory if you're not already familiar with them, and TLA+ is a lot more programmer-centric and less pure-mathey than Isabelle. TLA+ offers model checking for "brute force" verification, and also offers a formal proof system called TLAPS. Lamport's talks on TLA+ are quite good [2], and I found that learning Isabelle was a lot easier once I had a lot of practice with TLA+. [1] http://concrete-semantics.org/ http://concrete-semantics.org/ [2] https://lamport.azurewebsites.net/video/videos.html https://lamport.azurewebsites.net/video/videos.html

jameshart 4y ago

Someone needs to tell the mathematicians they are allowed to use variable names longer than a single character now.

SemanticStrengh 4y ago
that elitism has to stop, people should design hyeroglyphs-free programming languages optimized for mathematical expressions and proofs should be written in it. The lack of IDE support in regular mathML or PDF math is astonishing.
paskozdilar 4y ago
They fscked up when they decided to omit the dot when multiplying. So now it's impossible to differentiate between "varname" and "var*name".
- JadeNB 4y ago
  > They fscked up when they decided to omit the dot when multiplying. So now it's impossible to differentiate between "varname" and "var*name". Well, since we don't use multi-letter variable names, no such distinction is necessary! But if, for some reason, we did do so, then these two cases would be typeset in LaTeX as \(varname\) and \(var\,name\) (or, rather, \(\mathit{var}\) and \(\mathit{var}\,\mathit{name}\), since TeX correctly interprets \(var\) as semantically `var` anyway).
  - paskozdilar 4y ago
    > Well, since we don't use multi-letter variable names, no such distinction is necessary! You remember the story about the Fox and the Grapes, right?
SilasX 4y ago
Go programmers, too. https://github.com/golang/go/wiki/CodeReviewComments#variable-names https://github.com/golang/go/wiki/CodeReviewComments#variabl...
4y ago

alok-g 4y ago

>> Formalisation of the internal calculus, HF HF seems 'hereditarily finite'. I wish someone presents the proof that's 'inlines' the explanation of the terminology used and defines them before using. For something as fundamental as Godel's theorems, this should be worth doing.

SemanticStrengh 4y ago

I feel like godel incompleteness is a cheap trick that mislead to think there are statements in ZFC that can't be proven except that those proven statement are contrived useless meta-statements.

deltasepsilon 4y ago
I'm going to assume you mean that the true unprovable sentences that Gödel constructed are contrived. I don't think I can convince you otherwise, except to say that others thought like you and eventually Paris and Harrington came up with [1]. You can make even more "concrete" statements, see the work of Chaitin, but all this stems from Hilbert's very concrete 10th problem [2]. I must say, be careful with "reasoning". For example, once a philosophy PhD minimized mathematics eloquently by saying all mathematical results are "tautological", hence uninteresting. Hence, why bother studying it, and in your case, why bother thinking Gödel did anything special. Why bother about anything at all... there's the rub. [1] https://en.wikipedia.org/wiki/Paris–Harrington_theorem https://en.wikipedia.org/wiki/Paris–Harrington_theorem [2] https://en.wikipedia.org/wiki/Hilbert's_tenth_problem https://en.wikipedia.org/wiki/Hilbert's_tenth_problem
- SemanticStrengh 4y ago
  > Since Peano arithmetic cannot prove its own consistency by Gödel's second incompleteness theorem, this shows that Peano arithmetic cannot prove the strengthened finite Ramsey theorem. This seems quite circular, where the (claims mine) contrived statements enabling godel 2 incompletude theorem, make it unable to prove a non-contrived statement? Thanks for the reference though, I'll admit that is a topic I'm not familiar enough with to fully challenge it. > I must say, be careful with "reasoning". For example, once a philosophy PhD minimized mathematics eloquently by saying all mathematical results are "tautological", hence uninteresting. Hence, why bother studying it, and in your case, why bother thinking Gödel did anything special. Yeah that's a classic, it's a good thought experiment but that only prove that one must not be careful with the pruning that can enable high level reasoning but more with being careful of fallacious or misleading reasonings. Yes in theory, mathematical chain proofs are only tautologies derived from ZFC/higher order logic, so yes mathematics doesn't say anything new. However in practice, the task of unfolding reasoning chains and being able to refer to past lemnas as abtractions/objects, enable the reader to optimize for cognition, and hence the more proofs advances, the more we can discover, retain, understand and refer, useful tautological yet transitive knowledge.

deltaonefour 4y ago

If Godel's theorem applies to all formal systems. Then in formalizing Godel's theorem, doesn't that make the theorem apply to itself? So the calculus that formalises the theorem is either inconsistent or there are other true statements about it that can't be proven? Which is it? Can someone with a bigger brain elaborate on how the theorem applies to itself in a language for tiny brained people? No big words please.

jameshart 4y ago
I think the short version is: just because any formal system is guaranteed to be incomplete doesn't mean it can't prove useful things. And even an incomplete formal system can prove Gödel's Incompleteness Theorem.
birriel 4y ago
I asked a similar question a while back: https://news.ycombinator.com/item?id=27915824 https://news.ycombinator.com/item?id=27915824
irq-1 4y ago
> true statements about it that can't be proven? Its missing the qualifier: can't be proven in that system. They can be examined from outside the system, or say, with a different system.
- qiskit 4y ago
  The problem still continues. Even if you add the unprovable formula ( lets say formula1) in System1 as an axiom to System2 ( System1 + formula1 ), System2 will have its own unprovable formulas even though formula1 would be superficially provable in System2. You could add the unprovable formulas in System2 as axioms to System3 but System3 will have its own unprovable formulas . Godel showed that it's simply the nature of any formal system with complexity greater than or equal to arithmetic.
bumbledraven 4y ago
Godel’s incompleteness theorems are about formal systems. A formal system can be thought of as an algorithm that takes a purported formal proof of some arithmetical statement (e.g. there is no largest twin prime) and returns true/false depending on whether the proof is correct. Call the algorithm a “proof checker” and say it “accepts” a statement if it returns true for some purported proof of the statement. Godel’s first incompleteness theorem says that at least one of the following is true: (1) There is some statement such that the checker accepts both the statement and the statement’s negation (e.g. the checker accepts both “2 + 2 = 4” and “2 + 2 ≠ 4”). This is called inconsistency. (2) There is some true statement which the checker will not accept. This is called incompleteness. Since Godel’s first incompleteness theorem is not a formal system, it does not apply to itself.

timcavel 4y ago

deleted 4y ago

[deleted]

deleted 4y ago

[deleted]