Skip to content
Coordinates of ThoughtHome of Philosophy
Join
Question · Explain

Why can’t a proof assistant prove its own consistency, and should that worry the people who rely on one?

Tomasz Szewczak Fellow
· 3 replies
Philosophy of mathematicsAnalyticDavid HilbertGerhard GentzenKurt Gödel#consistency#formal-verification#incompleteness#proof-assistants
Follow

Its coordinates: 1.1.4 Abstract Objects · 6.9 Philosophy of Mathematics

Most of the code I write in Kraków is checked by an interactive proof assistant. Last week a new colleague said, half joking, that Gödel had shown the assistant can't prove itself consistent, so all our proofs might be worthless. I gave a clumsy answer and I'd like a better one.

What I understand so far: Gödel's second incompleteness theorem says that a consistent formal system, effectively axiomatised and strong enough to express a modest amount of arithmetic, cannot prove its own consistency. The logics behind proof assistants are far stronger than that, so the theorem applies to them.

My questions:

  1. Does it follow that we have no reason to trust these systems, or only that the reason can't come from inside them?
  2. When someone proves such a logic consistent, they do it in a stronger system, usually set theory with extra assumptions. Isn't that just moving the problem one floor up?
  3. Hilbert hoped to secure mathematics by proving its consistency with very simple, "finitary" methods. Is the modern habit of keeping a small, trusted checking kernel a modest version of his programme, or something different?

Precise answers welcome. I am suspicious of anything I can't write down.

LikeAnswer
Follow3 answers

Join the conversation: members reply here, and joining is free. Reading is always free.

Join free to reply Sign in

3 answers

  1. Ana Clara Ferreira

    Fellow

    The theorem says the system can't prove its own consistency. It says nothing about whether the system is consistent, and nothing about whether you may trust it.

    Your second question is the interesting one, and the answer is: yes, it moves the problem, but not uselessly. Gentzen proved the consistency of Peano arithmetic in 1936, using induction up to a particular infinite ordinal, ε₀. That method is not finitary in Hilbert's sense, so Hilbert's hope failed. But it tells you exactly what extra assumption you are relying on. Trust becomes graded: you know the principle you'd have to doubt, and it is a much narrower thing than "all of mathematics".

  2. Derek Hollis

    Fellow

    Speaking from the industrial side: in years of verification work I have never seen anyone burned by Gödel. The failures I have seen are of two kinds. Bugs in the checker itself, which is why we keep the trusted kernel tiny. And, much more often, a correct proof of the wrong theorem, because the specification said something other than what we meant.

    The small-kernel idea is often called the de Bruijn criterion, after the Automath project. It isn't Hilbert's programme. Hilbert wanted mathematics justified. The kernel only wants mistakes made checkable by a person with an afternoon. That's a far humbler and far more achievable goal.

  3. Vikram Sethi

    Fellow

    Is there a school-level version of this? I tell my students that a proof is an argument that would convince any careful reader. Here it sounds as if even the careful reader needs another careful reader behind him, and so on.

    Ana Clara's answer suggests the chain stops at a principle you simply accept. Is that so different from what the Nyāya logicians said, that every inference rests in the end on something already established by another means of knowledge?