36
$\begingroup$

I am not very well-versed in the world of theorem proving, much less automated theorem proving, so please correct me if anything I say or assume in my question is wrong.

Basically my question is: are automated theorem provers themselves every formally proven to work with another theorem prover, or is there just an underlying assumption that any theorem prover was just implemented really really well, extensively tested & reviewed, etc. and so it "must work"?

If so, does there always remain some underlying doubt in any proof proven by a formally verified automated theorem prover as the formal verification of that theorem prover still lies on assuming that the non-formally verified theorem prover was correct in its verification of the former theorem prover, even if it might technically be wrong - as it was not formally verified itself? (That is a mouthful of a question, apologies.)

I am thinking of this question in much the same vein as bootstrapping compilers.

$\endgroup$
  • 2
    $\begingroup$ This is indeed interesting and important - I'm not nearly knowledgeable to give an answer here, but you might find J. C. Davis' Ph.D. thesis interesting. $\endgroup$ – Noah Schweber Jan 21 at 16:39
  • 4
    $\begingroup$ If a theorem prover can prove its own consistency, doesn't that mean it is inconsistent? $\endgroup$ – yters Jan 22 at 18:30
  • 1
    $\begingroup$ @yters I'd guess it can at least prove its own relative consistency. $\endgroup$ – senderle Jan 23 at 2:29
  • 1
    $\begingroup$ @yters: That's why the question isn't really well-defined. After all, there is no way to formalize the correctness of a theorem prover build in the real world since the most we can do is to express that notion in some syntactic form that intuitively seems to correspond to what we want it to mean. And then of course under mild assumptions, no reasonable theorem prover can prove its own consistency, much less arithmetical soundness (which is one precisely specifiable aspect of correctness), unless it proves $0=1$. I'm not sure why none of the existing answers touched on this aspect. $\endgroup$ – user21820 Jan 24 at 8:10
  • 1
    $\begingroup$ You cannot prove a proof language's strong normalization ("every program terminates with a unique result") property in itself unless it is in fact inconsistent. Or unless the proof language is so weak that it does not even allow you to encode Peano arithmetic... $\endgroup$ – xuq01 Jan 24 at 17:35
41
$\begingroup$

I recommend reading Pollack's How to believe a machine-checked proof. It explains how proof assistants are designed to minimize the amount of critical code.

There are many levels of formal verification (that's the phrase you're looking for in place of "proven") of a proof assistant:

  1. Verify that the algorithms used by the proof assistant are correct.
  2. Verify that the implementation of (the critical core of) the proof assistant is correct.
  3. Verify that the compiler for the language in which the proof assistant is implemented is correctly designed and implemented.
  4. Verify that the hardware on which the proof assistant runs is correctly designed and built.
  5. Compute the probability that a cosmic ray passes through the CPU and tricks your proof assistant every time you run it.
  6. Estimate the likelihood that you are insane.

People put serious effort into these (well, at least the first four). For example, steps 1 and 2 are addressed in Coq Coq Correct!, and steps 3 and 4 in the amazing award-winning CompCert project.

$\endgroup$
  • 10
    $\begingroup$ 7. Estimate the likelihood that you are part of a simulation by very powerful beings that are living in a finite world but are simulating us in an apparently infinite world, and so there is no real model of PA but we cannot ever figure that out because the simulation tricks us. $\endgroup$ – user21820 Jan 22 at 10:16
  • 1
    $\begingroup$ "Coq Coq Correct!" is the greatest title I've seen in a long while. $\endgroup$ – Édouard Jan 22 at 12:23
  • 1
    $\begingroup$ I do feel that swapping 5 and 6 probably leads to a more sane approach to proving proof systems =) $\endgroup$ – Cort Ammon Jan 22 at 15:15
  • 1
    $\begingroup$ The Intro to Isabelle slides (pdf), discuss "If I Prove It on the Computer, It Is Correct, Right?" Which is more about validity of a proof rather than the theorem prover, but I think probably still worth mentioning the two points "logic could be inconsistent" and "theorem could mean something else" (page 17). $\endgroup$ – BurnsBA Jan 22 at 17:42
  • 1
    $\begingroup$ @AndrejBauer: Based on your last comment, yes... you should edit your post to clarify, because for most logicians "underlying formal theory" would mean "underlying foundational system"... And of course I agree that the algorithmic issues far outweigh potential unsoundness in the foundational system. (Though it would be nice if you don't keep misconstruing my point as being about "infinitely many beads".) Thanks! $\endgroup$ – user21820 Jan 24 at 8:03
9
$\begingroup$

What you need is the idea of "the trusted core". Quoting "A verified runtime for a verified theorem prover":

In many theorem provers, the trusted core—the code that must be right to ensure faithfulness—is quite small. As examples, HOL Light is an LCF-style system whose trusted core is 400 lines of Objective Caml, and Milawa is a Boyer-Moore style prover whose trusted core is 2,000 lines of Common Lisp. These cores are so simple we may be able to prove their faithfulness socially, or perhaps even mechanically as Harrison did for HOL Light.

Once you assure yourself the core is correct, it can be used to verify the correctness of some extensions, and then those extensions can be used...

$\endgroup$
6
$\begingroup$

While this may trend close to self-advertisement, this is essentially the topic of my recent paper Metamath Zero: The Cartesian Theorem Prover (video), and the analogy with bootstrapping compilers is spot on. The introduction of the paper lays out what is needed to make this happen, and it's only a problem of engineering.

As Andrej says, there are several components that go into a "full bootstrap", and while many of the parts have been done separately, the theorem provers that are used by the community are only correct in the sense that linux is correct: we've used it for a while and there are no bugs we have found so far, except the bugs that we did find and fix.

The issue, as ever, is that because the cost of producing verified software is high, verified programs tend to be simplistic or simplified from the "real thing", and so there remains a gap between what people use and what people prove theorems about. A "small trusted kernel" setup is necessary but not sufficient, because unless you have a full formal specification (with proofs) of the programming language, the untrusted part can still interfere with the trusted part, and even if the barrier is air-tight, you have communication problems when the untrusted part is in control - for example, the kernel may flag an error that the untrusted part ignores, or the kernel may never be shown some apparent assertion at the source level.

The good news is that projects of this scale have become feasible in the past few years, so I am very hopeful that we can get production quality theorem provers with verified backends soon-ish.

  • The CakeML project should get a mention here: they have a ML compiler verified in HOL4, that is capable of running a HOL verifier written in ML. (Unfortunately HOL4 is more than just its logical system, so there is some work to be done to make this realistic.)
  • The Milawa kernel is written in a subset of ACL2, with a bunch of bootstrapping stages before closing the loop (being able to prove theorems about this same ACL2 subset). This is the only actual theorem prover bootstrap I know, but it doesn't go down to machine code, it stays at the level of Lisp, and from what I understand it's not actually performant enough for production work. It has since been verified down to machine code, but that part of the proof was done in HOL4 so it's not actually bootstrapping at the machine code level.
  • Coq recently made some strides towards this with Coq Coq Correct!, but it doesn't cover the full Coq kernel (including recent additions such as SProp, and the module system). (Aside, if there are any Coq experts reading this: if you know any place where the complete formal system implemented by Coq is written down, I would really like to see it. Formalized is nice but informal might even be better, as long as it is complete and precise.) You also can't connect it to CompCert as Andrej suggested, because the typechecking algorithm is only described abstractly, and certainly not in C, which is what CompCert expects as input.
  • Metamath Zero is still under construction but the goal is to prove correctness down to the machine code level, inside its own logic. (I also can't help but mention it's currently about 8 orders of magnitude faster than "the other guys" but we'll see if that holds up until the end of the project.)
$\endgroup$
  • $\begingroup$ 8 orders of magnitude is a lot! $\endgroup$ – user76284 Jan 27 at 2:12
  • $\begingroup$ @user76284 That's what I keep telling people! It's the difference between ~18 hours to check CakeML and 200ms for MM0 to check set.mm (which is not a proof of correctness of a theorem prover so it's not directly comparable, but it is an entire library of ZFC set theory, and predicted to be larger by at least an order of magnitude from the actual compiler proof). The project work so far comes in at about 2ms. $\endgroup$ – Mario Carneiro Jan 27 at 6:42
3
$\begingroup$

In case you are not aware, there is a possibility that a theorem prover is implemented 100% correctly and run on a faultless machine and proves itself arithmetically inconsistent, even though it is not. The other existing answers focus on the issue of verifying that the theorem prover runs exactly as it was designed to run, but do not address this aspect of "correctness".

More precisely, every theorem prover is based on some underlying foundational system $S$. For $S$ to be considered a reasonable foundational system, $S$ must interpret arithmetic, meaning that there is a computable translation $ι$ of sentences over PA to sentences in the language of $S$ such that for every arithmetical sentence $Q$ we have that if PA proves $Q$ then $S$ proves $ι(Q)$. Godel's incompleteness theorem can be easily extended to any such (computable) foundational system $S$, and states the following: $ \def\con{\text{Con}} $

If $S$ does not prove $ι(0=1)$, then $S$ does not prove $ι(\con(S))$.

Here $\con(S)$ is the arithmetical sentence that encodes the (arithmetical) consistency of $S$. Namely, $S$ does not prove $ι(0=1)$ iff $\mathbb{N} ⊨ \con(S)$.

So first of all, this implies that $S$ cannot possibly prove its own consistency unless it is inconsistent. In this sense it is impossible for any theorem prover to prove that itself is correct. It may be able to prove that its execution on a particular machine satisfies certain specifications (as mentioned in other answers), but that is far from proving correctness of the theorems that it proves. In other words, anyone who wants confidence in a theorem prover's outputs still must examine those specifications and be somehow convinced that they ensure correctness of the outputs. That part can never be covered by the theorem prover itself.

Secondly, if $S$ is deductively closed for arithmetical sentences, meaning that if $S$ proves $ι(Q)$ and $ι(Q⇒R)$ then $S$ also proves $ι(R)$, then let $A(S)$ be the arithmetical theorems of $S$, namely all arithmetical sentences $Q$ such that $S$ proves $ι(Q)$, and let $S'$ be a formal system that proves the same theorems of $S$ plus $ι(R)$ for every arithmetical sentence $R$ such that $A(S)+¬\con(S)$ proves $R$. Then $S'$ is still deductively closed for arithmetical sentences, but $S'$ proves $ι(¬\con(S))$ and hence $ι(¬\con(S'))$.

Note that $S'$ proves everything that $S$ does, and if $S$ is consistent then $S'$ is also consistent but proves that itself is inconsistent. Now how can we know that the foundational system we started with was not like such an $S'$? We cannot know, without assumptions beyond $S$. Simply put, it is possible that a theorem prover proves that it proves nonsense including $0=1$, even though it does not!

To summarize:

  1. Any reasonable theorem prover cannot prove that itself produces only consistent outputs.

  2. One cannot determine without assumptions beyond those coded into a theorem prover that it does not produce false theorems.

I also wish to say a bit about verification according to specifications. This is necessarily conditional; all you can prove is that, if the theorem prover is run on a machine that satisfies certain properties, then the theorem prover produces outputs that satisfy certain specifications. Can you know for sure whether the machine on which you run the theorem prover actually satisfies those properties? No. At some point, you are just going to have to trust or believe something that you cannot prove.

$\endgroup$
  • $\begingroup$ Regarding the Godel's theorem argument, I think it is a source of confusion for many whenever you talk about a self-verifying system, and phrasing it negatively like this (in the sense "it's been proved that the task is impossible") is driving the wrong point. It certainly well is possible to give formal mathematical statements that, to a human, convince them of correctness of the verifier. For example, if I'm working in PA, then I can prove (in PA) that if verifier $X$ proves $\varphi$, then $PA\vdash \varphi$. ... $\endgroup$ – Mario Carneiro Jan 25 at 0:58
  • $\begingroup$ I could also prove that $\varphi$ is true for any particular $\varphi$ (because PA proves all its finite fragments), or we could go to ZF and prove $\varphi$ there (because ZF models PA). If you look at any of these theorems from an informal outside perspective, one where theories much stronger than ZF are used routinely, these are clearly clearing the bar of "acceptable truth", and they are entirely formal statements. $\endgroup$ – Mario Carneiro Jan 25 at 1:01
  • $\begingroup$ @MarioCarneiro: It is not a source of confusion, because this kind of goal is exactly what Hilbert wanted until Godel cleared that up. And it seems to me that many people (excluding people who already know the incompleteness theorems) do not understand that it is truly impossible to verify consistency within the same system. And I don't see your point about using ZF to prove consistency (or soundness) of PA, because it just hides the issue under the infinite regression carpet. Whatever system S underlies the theorem prover, you can obviously prove it 'correct' in S + (S is sound), but not S... $\endgroup$ – user21820 Jan 25 at 1:41
  • $\begingroup$ After all, the title of the question here is "Do theorem proves demonstrate their own correctness?" Furthermore, adding consistency statements or moving to a stronger system cannot increase your confidence in the original one. By the way, "PA proves all its finite fragments" is trivial, so it seems you typed wrongly; PA proves consistency of every finite fragment. Still, that fact cannot be observed within PA itself, which is the whole point of being unable to verify self correctness. Even if the asker knows all this, I'm sure many other readers don't. $\endgroup$ – user21820 Jan 25 at 2:11
  • $\begingroup$ Regarding the titular question, I think the problem depends on what "correctness" actually means. Of a theorem prover implementation, I would distinguish between "correctness" meaning that it checks theorems according to the intended formal system, and "soundness" meaning that the theorems so validated are actually true. Only the latter property is unprovable in the same axiom system. $\endgroup$ – Mario Carneiro Jan 25 at 9:36
0
$\begingroup$

This depends on the underlying axioms of the theorem prover. If a prover is based on primitive set theory, it will have few axioms. It can also have optional axioms such as the axiom of choice, which may or may not be useful for higher level proofs. From these primitive axioms and theorems such as Peano arithmetic, we can build up the familiar algebra of ordinary and complex and floating point arithmetic. A further feature is the use of abtract types to represent theorems. If you have not proved a theorem, you cannot make use of it because that type will not exist yet. A further level of complexity is to write the core of the prover inside the prover itself. This may be used to give confidence that the prover written in itself satisfies the same proof traces as the prover running on a general purpose computer.

$\endgroup$

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.