3 ms·

Do we even know if it's possible to prove correctness of a theorem-prover, in a very general sense? At some point, that would imply that some theorem-prover wou

Do we even know if it's possible to prove correctness of a theorem-prover, in a very general sense? At some point, that would imply that some theorem-prover would have to prove its own correctness (either by proving itself directly or by proving itself through a loop of theorem-provers). This seems intuitively like it start to run up against Gödel-style incompleteness problems.

im3w1l 7y ago
Seems like the ideal would be a number of theorem provers each capable of verifying the next. And the first one simple enough to be verified with pen and paper
AgentOrange1234 7y ago
Provers in the LCF tradition have tiny cores that avoid having to trust lots of code. There are also reflective provers that can admit self-verified extensions. One project, called Milawa, had several layers of this.
digama0 7y ago
It does, but only if you state the theorem in a particular way. Let's say that you have a verifier A, that checks theorems in Peano Arithmetic (PA). Inside that logic, you can define what a computer is, how it executes, what PA is, what a verifier is, and what it means for a program to verify theorems of PA. Then you can have a sequence of bytes (verifier B), and prove that they represent a program that verifies theorems of PA. What have you proven? Well, verifier A (using PA) proves that "verifier B proves theorems of PA". That means that "if B says phi is true, PA |- phi". We would have a hard time actually running verifier B inside the logic of verifier A (that entails running all the steps of the computation B does as theorem applications inside verifier A), but even if we did, we would obtain a proof of "PA |- phi". If we assume A correctly implements PA, then that means PA |- "PA |- phi". In general, this is the best we can do. If we assume further that PA is a sound axiom system, i.e. when it proves facts about numbers then we won't find concrete counterexamples, then this strengthens to PA |- phi and then to phi itself, so we've learned that phi is true. The plan is to prove inside verifier A (that is, MM0) the statement "Here is a sequence of bytes. It is an executable that when executed has the property that if it succeeds on input "T |- phi", then T |- phi." The bootstrapping part is that the sequence of bytes in question is in fact the code of verifier A. In order to support statements of the form "here is a sequence of bytes", the verifier also has the ability to output bytes as part of its operation (it's not just a yes/no oracle), and assert facts about the encoding of those bytes in the logic.
dooglius 7y ago
You would just prove that it is equivalent to a simple specification of the axiomatic system.

im3w1l 7y ago

Seems like the ideal would be a number of theorem provers each capable of verifying the next. And the first one simple enough to be verified with pen and paper

AgentOrange1234 7y ago

Provers in the LCF tradition have tiny cores that avoid having to trust lots of code. There are also reflective provers that can admit self-verified extensions. One project, called Milawa, had several layers of this.

digama0 7y ago

It does, but only if you state the theorem in a particular way. Let's say that you have a verifier A, that checks theorems in Peano Arithmetic (PA). Inside that logic, you can define what a computer is, how it executes, what PA is, what a verifier is, and what it means for a program to verify theorems of PA. Then you can have a sequence of bytes (verifier B), and prove that they represent a program that verifies theorems of PA. What have you proven? Well, verifier A (using PA) proves that "verifier B proves theorems of PA". That means that "if B says phi is true, PA |- phi". We would have a hard time actually running verifier B inside the logic of verifier A (that entails running all the steps of the computation B does as theorem applications inside verifier A), but even if we did, we would obtain a proof of "PA |- phi". If we assume A correctly implements PA, then that means PA |- "PA |- phi". In general, this is the best we can do. If we assume further that PA is a sound axiom system, i.e. when it proves facts about numbers then we won't find concrete counterexamples, then this strengthens to PA |- phi and then to phi itself, so we've learned that phi is true. The plan is to prove inside verifier A (that is, MM0) the statement "Here is a sequence of bytes. It is an executable that when executed has the property that if it succeeds on input "T |- phi", then T |- phi." The bootstrapping part is that the sequence of bytes in question is in fact the code of verifier A. In order to support statements of the form "here is a sequence of bytes", the verifier also has the ability to output bytes as part of its operation (it's not just a yes/no oracle), and assert facts about the encoding of those bytes in the logic.

dooglius 7y ago

You would just prove that it is equivalent to a simple specification of the axiomatic system.