5 ms·

Gödel proved that we will never get such a prover: https://en.wikipedia.org/wiki/G%C3%B6del%27s_incompleteness_theorems https://en.wikipedia.org/wiki/G%C3%B6del

Gödel proved that we will never get such a prover: https://en.wikipedia.org/wiki/G%C3%B6del%27s_incompleteness_theorems https://en.wikipedia.org/wiki/G%C3%B6del%27s_incompleteness_... Particularly, he proved that it is impossible for a formal system to prove its own consistency.

informatimago 10y ago
However, prover[p-1] can prove prover[p], modulo the bugs prover[p-1]. Then prover[p-2] can prove prover[p-1], modulo the bugs in prover[p-2]. If you can have prover[i-1] is simplier than prover[i], and prover[0] is so simple that any 5-years old can prove it's correct, then you win.
- randallsquared 10y ago
  Something seems wrong about this. Could you not describe the combination of all provers as a formal system? Would this system then not run afoul of Goedel?
  - deleted 10y ago
    [deleted]
  - lmkg 10y ago
    This approach can only describe formal systems that are finite combinations of such provers.
  - crpatino 10y ago
    Theoretically, you are 100% correct. In practice, it is still worthwhile to have N redundant independently developed provers to prove each other, and to benchmark against each other. This will help uncover subtle bugs that result from ordinary programming mistakes. This will, however, not protect against deeper issues that are common to all N provers. e.g. Potential biases or mistaken assumptions in the formal verification comunity. At the end of the day, it is an engineering decision. How much of the available resources are you willing to through at the practical problem of making your implementation approach asymptotically to the theoretical limits. The fact that those limits is indeed a peg or two below perfection is an independent issue.
    - nickpsecurity 10y ago
      "In practice, it is still worthwhile to have N redundant independently developed provers to prove each other, and to benchmark against each other. This will help uncover subtle bugs that result from ordinary programming mistakes." I strongly advise that to deal with both mistakes and subversion. Mutually-suspicious parties in various countries using different logics, compilers, hardware, etc. with a common, executable spec that's basically state machines or functions. That way they get same output from same input. So, when I saw Milawa was verified first-order, I immediately looked for other verifications of first-order provers (found 1). Then the idea would be diverse implementations of executable parts of that stack with diverse reviews of logic combinations they did. Exhaustive testing done by each party. Even do implementations of key parts of TCB in other logics to check results. The prover with its code is trustworthy when everyone got the same results on same logics, code, shared tests, and individual tests. Plus have paper copies of the resulting text files with hashes stashed away somewhere in case a nation-state wants to throw money at countering diversity via hacking host systems. ;) Then we rinse and repeat for more complex provers. The fun never stops in this game.
  - vilhelm_s 10y ago
    The end result you get out is something like "if the prover n accepts the claim P, then prover 1 also accepts the claim P". In logical terms you can think of it as a relative consistency proof. In practice, even much simpler theorems would already raise our confidence a lot. E.g., the inference rules of Coq can be stated in a couple of pages of text, but the kernel checker that you need to trust is 14k lines of OCaml. A proof that the checker actually correctly implements the inference rules would already catch the majority of the bugs that happen in practice. Because of Gödel we then can't hope for a proof in Coq that there is no way to use those inference rules to derive False, but that's less of a concern.
- JadeNB 10y ago
  > prover[0] is so simple that any 5-years old can prove it's correct This seems like the perfect time to misquote Groucho Marx: "This is so simple a child of 5 could prove it. Somebody bring me a child of 5!"
- nickpsecurity 10y ago
  Good thinking. That's exactly how they did it: https://news.ycombinator.com/item?id=12762224 https://news.ycombinator.com/item?id=12762224
pfortuny 10y ago
Mmmhhhh.... Arithmetic in computers is bot infinite, so one might have a consistence theorem for "computers with arithmetic modulo 2^3000" for example.
- schoen 10y ago
  Your exponent is a bit too small, though; it should be 2^(number of bits of RAM), like 2^34359738368 for a computer with 4 GB RAM (plus a little bit for CPU registers). Assuming that the computer programs under study aren't allowed to interact with a disk, of course. :-)
  - aruggirello 10y ago
    Or with the Internet :-D
JadeNB 10y ago
> Gödel proved that we will never get such a prover Not one that can handle Peano arithmetic—but there are plenty of interesting systems sub-Peano arithmetic. Presburger arithmetic (https://en.wikipedia.org/wiki/Presburger_arithmetic https://en.wikipedia.org/wiki/Presburger_arithmetic) is the one that springs to mind; I doubt that it's directly useful as a theorem prover, but it does show that interesting mathematics can be done in complete theories.
- acchow 10y ago
  Right, but the system we're interested in is normal computers, which is more powerful than arithmetic.
  - JadeNB 10y ago
    > Right, but the system we're interested in is normal computers, which is more powerful than arithmetic. On the other hand, a theorem prover does not have to be able to prove everything about a system to be able to prove some useful things. One might also say "the system mathematicians are interested in is all of mathematics, which is more powerful than arithmetic", or, for that matter, "the system programmers are interested in is all of theoretical computation, which is (at least) Turing complete"—but sometimes it's useful intentionally to restrict our power. (I think of https://news.ycombinator.com/item?id=10567408 https://news.ycombinator.com/item?id=10567408 , for example.) (If we're being very picky, then, as pfortuny points out (https://news.ycombinator.com/item?id=12762192 https://news.ycombinator.com/item?id=12762192), a computer, having only a finite address space, isn't even as powerful as ordinary arithmetic; but it's fair to guess that this isn't a useful kind of pickiness.)
Senji 10y ago
In the general case, we could just ignore general recurrsion and circular definitions or self refferencing functions. Then we win.
- simondedalus 10y ago
  The problem is that Gödel builds self-reference. It's not like Peano arithmetic has recursion or self-reference operators. To put it another way, in order to disqualify self-reference, you would need to employ a higher order proof system--which gives the game away anyway.
ahelwer 10y ago
Honestly this objection always seemed very handwavey to me, especially given how much abuse the incompleteness theorems endure during extension beyond statements about the Natural numbers. Like, what exactly happens if you try to write a bootstrapped theorem prover? Does a deity descend from the heavens to unplug your keyboard? I'd be very interested in reading a paper or blog post documenting a practical attempt here.
- lmkg 10y ago
  The incompleteness theorem effectively states that some statements will require an infinite amount of time for this bootstrapping approach to work. The only deity involved is the finite-ness of the natural world.
- simondedalus 10y ago
  I don't mean to be rude, but this objection only seems handwave-y if you don't understand Gödel's proofs (common), or you have some refutation of them (obviously uncommon, but definitely interesting). This is a good not-too-technical but not-condescending explanation https://www.amazon.com/G%C3%B6dels-Proof-Ernest-Nagel/dp/0814758371 https://www.amazon.com/G%C3%B6dels-Proof-Ernest-Nagel/dp/081... (it does get into the technical details; it just doesn't go line by line as you would if you wanted to recreate the proofs). As long as you have the expressive power of Peano arithmetic (which all programming languages ought to, and definitely all proof systems ought to), you can find a Gödel sentence in the system and thus prove that it can't prove, of itself, "x is consistent". It's worth looking into, if only for the enjoyment.
  - hinkley 10y ago
    Have you ever written a compression algorithm? You do know that Shannon proved that general purpose compression is impossible, right? Why bother if that 75% compression ratio is provably impossible?
  - ahelwer 10y ago
    It isn't at all obvious that "a theorem prover proving itself correct" and "an axiomatic system proving its own consistency" are the same thing, beyond both being in the category of things which refer to themselves in the domain of mathematical proofs. Software correctness isn't the same as consistency. A program is correct if it refines its specification, and an axiomatic system is consistent if it does not lead to contradiction. Before doing a deep dive into Gödel we need to firmly establish we're actually looking at the right problem. Even if Gödel is shown to apply in the strict generalized theoretical sense, it might be irrelevant to practice. Theory and practice often differ enough for practice to be very useful; we easily prove halting for most programs we care about, compute solutions to average-case NP-Complete problems without a noticeable rise in CPU temp, and (as the other poster at this level said) write compression algorithms which work well on all relevant inputs. This is poor analogous reasoning, of course, but I include it because demonstration of universal practical pitfall would be very interesting in much the same way specific manifestations of availability loss in fault-tolerant consensus algorithms are interesting. Really though, I am tired of the above exact exchange playing out in every thread I've seen here on formal verification. Someone raises the obvious concern of bugs in the theorem prover. Someone else raises the bootstrapping solution, cribbed from compilers. Someone else raises the Gödel objection; and there the conversation dies. Dig deeper.
Houshalter 10y ago
You don't need to prove that Peano arithmetic is consistent! You just need to prove that the theorem prover doesn't contain any bugs, i.e. that it correctly implements peano arithmetic. That's a much lower bar, and theorem provers have verified themselves in the past.
ZephyrP 10y ago
This is actually a common misconception perpetuated by zealous Scientific American reporters (and cognitive scientists :) . Many complete, consistent self-justifying axiom systems exist today. Formal verification schemes employing metamathematical logic also exist and can be both complete and consistent. Even MORE systems have been created that can verify their own semantic tableux exclusively (and by extension are consistent & decidable). Even still there are systems like Presburger Arithmetic, which can by proven decidable (although they cannot prove themselves) On page 12 of the english translation (and possibly the original german), Godel addresses certain criteria for distinguishing a sufficiently powerful system (as well as recursively axiomitizable, etc). I have personally written such a software verification scheme, and even have an inferior interaction mode for SMT solvers that can help you verify such schemes (it's in my profile & github). There are also great books like the extremely cheesily-named graduate textbook: "Your Guide to Automated Reasoning", that examine this issue from every perspective imaginable.

informatimago 10y ago

However, prover[p-1] can prove prover[p], modulo the bugs prover[p-1]. Then prover[p-2] can prove prover[p-1], modulo the bugs in prover[p-2]. If you can have prover[i-1] is simplier than prover[i], and prover[0] is so simple that any 5-years old can prove it's correct, then you win.

randallsquared 10y ago
Something seems wrong about this. Could you not describe the combination of all provers as a formal system? Would this system then not run afoul of Goedel?
- deleted 10y ago
  [deleted]
- lmkg 10y ago
  This approach can only describe formal systems that are finite combinations of such provers.
- crpatino 10y ago
  Theoretically, you are 100% correct. In practice, it is still worthwhile to have N redundant independently developed provers to prove each other, and to benchmark against each other. This will help uncover subtle bugs that result from ordinary programming mistakes. This will, however, not protect against deeper issues that are common to all N provers. e.g. Potential biases or mistaken assumptions in the formal verification comunity. At the end of the day, it is an engineering decision. How much of the available resources are you willing to through at the practical problem of making your implementation approach asymptotically to the theoretical limits. The fact that those limits is indeed a peg or two below perfection is an independent issue.
  - nickpsecurity 10y ago
    "In practice, it is still worthwhile to have N redundant independently developed provers to prove each other, and to benchmark against each other. This will help uncover subtle bugs that result from ordinary programming mistakes." I strongly advise that to deal with both mistakes and subversion. Mutually-suspicious parties in various countries using different logics, compilers, hardware, etc. with a common, executable spec that's basically state machines or functions. That way they get same output from same input. So, when I saw Milawa was verified first-order, I immediately looked for other verifications of first-order provers (found 1). Then the idea would be diverse implementations of executable parts of that stack with diverse reviews of logic combinations they did. Exhaustive testing done by each party. Even do implementations of key parts of TCB in other logics to check results. The prover with its code is trustworthy when everyone got the same results on same logics, code, shared tests, and individual tests. Plus have paper copies of the resulting text files with hashes stashed away somewhere in case a nation-state wants to throw money at countering diversity via hacking host systems. ;) Then we rinse and repeat for more complex provers. The fun never stops in this game.
- vilhelm_s 10y ago
  The end result you get out is something like "if the prover n accepts the claim P, then prover 1 also accepts the claim P". In logical terms you can think of it as a relative consistency proof. In practice, even much simpler theorems would already raise our confidence a lot. E.g., the inference rules of Coq can be stated in a couple of pages of text, but the kernel checker that you need to trust is 14k lines of OCaml. A proof that the checker actually correctly implements the inference rules would already catch the majority of the bugs that happen in practice. Because of Gödel we then can't hope for a proof in Coq that there is no way to use those inference rules to derive False, but that's less of a concern.
JadeNB 10y ago
> prover[0] is so simple that any 5-years old can prove it's correct This seems like the perfect time to misquote Groucho Marx: "This is so simple a child of 5 could prove it. Somebody bring me a child of 5!"
nickpsecurity 10y ago
Good thinking. That's exactly how they did it: https://news.ycombinator.com/item?id=12762224 https://news.ycombinator.com/item?id=12762224

pfortuny 10y ago

Mmmhhhh.... Arithmetic in computers is bot infinite, so one might have a consistence theorem for "computers with arithmetic modulo 2^3000" for example.

schoen 10y ago
Your exponent is a bit too small, though; it should be 2^(number of bits of RAM), like 2^34359738368 for a computer with 4 GB RAM (plus a little bit for CPU registers). Assuming that the computer programs under study aren't allowed to interact with a disk, of course. :-)
- aruggirello 10y ago
  Or with the Internet :-D

JadeNB 10y ago

> Gödel proved that we will never get such a prover Not one that can handle Peano arithmetic—but there are plenty of interesting systems sub-Peano arithmetic. Presburger arithmetic (https://en.wikipedia.org/wiki/Presburger_arithmetic https://en.wikipedia.org/wiki/Presburger_arithmetic) is the one that springs to mind; I doubt that it's directly useful as a theorem prover, but it does show that interesting mathematics can be done in complete theories.

acchow 10y ago
Right, but the system we're interested in is normal computers, which is more powerful than arithmetic.
- JadeNB 10y ago
  > Right, but the system we're interested in is normal computers, which is more powerful than arithmetic. On the other hand, a theorem prover does not have to be able to prove everything about a system to be able to prove some useful things. One might also say "the system mathematicians are interested in is all of mathematics, which is more powerful than arithmetic", or, for that matter, "the system programmers are interested in is all of theoretical computation, which is (at least) Turing complete"—but sometimes it's useful intentionally to restrict our power. (I think of https://news.ycombinator.com/item?id=10567408 https://news.ycombinator.com/item?id=10567408 , for example.) (If we're being very picky, then, as pfortuny points out (https://news.ycombinator.com/item?id=12762192 https://news.ycombinator.com/item?id=12762192), a computer, having only a finite address space, isn't even as powerful as ordinary arithmetic; but it's fair to guess that this isn't a useful kind of pickiness.)

Senji 10y ago

In the general case, we could just ignore general recurrsion and circular definitions or self refferencing functions. Then we win.

simondedalus 10y ago
The problem is that Gödel builds self-reference. It's not like Peano arithmetic has recursion or self-reference operators. To put it another way, in order to disqualify self-reference, you would need to employ a higher order proof system--which gives the game away anyway.

ahelwer 10y ago

Honestly this objection always seemed very handwavey to me, especially given how much abuse the incompleteness theorems endure during extension beyond statements about the Natural numbers. Like, what exactly happens if you try to write a bootstrapped theorem prover? Does a deity descend from the heavens to unplug your keyboard? I'd be very interested in reading a paper or blog post documenting a practical attempt here.

lmkg 10y ago
The incompleteness theorem effectively states that some statements will require an infinite amount of time for this bootstrapping approach to work. The only deity involved is the finite-ness of the natural world.
simondedalus 10y ago
I don't mean to be rude, but this objection only seems handwave-y if you don't understand Gödel's proofs (common), or you have some refutation of them (obviously uncommon, but definitely interesting). This is a good not-too-technical but not-condescending explanation https://www.amazon.com/G%C3%B6dels-Proof-Ernest-Nagel/dp/0814758371 https://www.amazon.com/G%C3%B6dels-Proof-Ernest-Nagel/dp/081... (it does get into the technical details; it just doesn't go line by line as you would if you wanted to recreate the proofs). As long as you have the expressive power of Peano arithmetic (which all programming languages ought to, and definitely all proof systems ought to), you can find a Gödel sentence in the system and thus prove that it can't prove, of itself, "x is consistent". It's worth looking into, if only for the enjoyment.
- hinkley 10y ago
  Have you ever written a compression algorithm? You do know that Shannon proved that general purpose compression is impossible, right? Why bother if that 75% compression ratio is provably impossible?
- ahelwer 10y ago
  It isn't at all obvious that "a theorem prover proving itself correct" and "an axiomatic system proving its own consistency" are the same thing, beyond both being in the category of things which refer to themselves in the domain of mathematical proofs. Software correctness isn't the same as consistency. A program is correct if it refines its specification, and an axiomatic system is consistent if it does not lead to contradiction. Before doing a deep dive into Gödel we need to firmly establish we're actually looking at the right problem. Even if Gödel is shown to apply in the strict generalized theoretical sense, it might be irrelevant to practice. Theory and practice often differ enough for practice to be very useful; we easily prove halting for most programs we care about, compute solutions to average-case NP-Complete problems without a noticeable rise in CPU temp, and (as the other poster at this level said) write compression algorithms which work well on all relevant inputs. This is poor analogous reasoning, of course, but I include it because demonstration of universal practical pitfall would be very interesting in much the same way specific manifestations of availability loss in fault-tolerant consensus algorithms are interesting. Really though, I am tired of the above exact exchange playing out in every thread I've seen here on formal verification. Someone raises the obvious concern of bugs in the theorem prover. Someone else raises the bootstrapping solution, cribbed from compilers. Someone else raises the Gödel objection; and there the conversation dies. Dig deeper.

Houshalter 10y ago

You don't need to prove that Peano arithmetic is consistent! You just need to prove that the theorem prover doesn't contain any bugs, i.e. that it correctly implements peano arithmetic. That's a much lower bar, and theorem provers have verified themselves in the past.

ZephyrP 10y ago

This is actually a common misconception perpetuated by zealous Scientific American reporters (and cognitive scientists :) . Many complete, consistent self-justifying axiom systems exist today. Formal verification schemes employing metamathematical logic also exist and can be both complete and consistent. Even MORE systems have been created that can verify their own semantic tableux exclusively (and by extension are consistent & decidable). Even still there are systems like Presburger Arithmetic, which can by proven decidable (although they cannot prove themselves) On page 12 of the english translation (and possibly the original german), Godel addresses certain criteria for distinguishing a sufficiently powerful system (as well as recursively axiomitizable, etc). I have personally written such a software verification scheme, and even have an inferior interaction mode for SMT solvers that can help you verify such schemes (it's in my profile & github). There are also great books like the extremely cheesily-named graduate textbook: "Your Guide to Automated Reasoning", that examine this issue from every perspective imaginable.