Yes, it still relies on the interpretation.

]]>But you’re still invoking some “intended model”, so as before “soundness” is not a property of the system but of some particular semantics for it.

]]>how is that informal notion of “trust”/“soundness” different from consistency?

In principle, it has nothing to do with consistency; although in practice, if one wants to do only consistent mathematics, then soundness requires consistency. But it's easy to be consistent and unsound!

Here is a system of axioms for arithmetic (in classical untyped first-order logic with equality, a nullary operator $0$ for zero, a unary operator $S$ for the successor, and binary operators $+$ for addition and $\cdot$ for multiplication):

- $\forall\, x,\; S x \ne 0$,
- $\forall\, x,\; \forall\, y,\; S x = S y \;\Rightarrow x = y$,
- $\forall\, x,\; x + 0 = x$,
- $\forall\, x,\; \forall\, y,\; x + S y = S (x + y)$,
- $\forall\, x,\; x \cdot 0 = x$,
- $\forall\, x,\; \forall\, y,\; x \cdot S y = (x \cdot y) + x$.

This system is consistent, but it is *not* (under the specified interpretation) sound.

Formally, one could give an interpretation of this system in (say) Peano Arithmetic and prove that the interpretation is unsound; informally, I indicated in parentheses when I introduced the language what the interpretation (in ‘reality’) was supposed to be, and this interpretation is unsound.

(If anybody cannot spot the error, it's in the next axiom to last.)

]]>Ta! Using my phone and didn’t check the URL worked.

]]>Try that again: Some relevant discussion. (You have to make sure the http is in there!)

]]>Some relevant discussion on an old MO question of mine.

]]>But how is that informal notion of “trust”/”soundness” different from consistency?

]]>In an absolute sense, soundness means that every theorem is true. Of course, this relies on an interpretation (to assign meaning to the sentences in the formal system), and (as you and I know even though some people prefer to pretend otherwise) there is no absolute notion of mathematical truth for the interpretation to take values in either. So really, soundness is (as you say) simply a relationship between a syntax and a model.

But in this case, we want an informal notion of soundness anyway. The point is, if we’re using Coq to verify a proof a theorem that we want to sure is (in some informal sense) actually true, then we want to be sure that Coq verifies only proofs of true statements. Since Coq is complicated, this is hard, but if we can bootstrap this by proving, in a stripped-down simplified version, that Coq is conservative over this stripped-down version (which I’m not sure is what really has been done), then we only have to look at the simple version. Then it’s an informal question: do you trust this simple version, which you can fully comprehend? If so, we’re good!

]]>@Toby, what does it mean to say that a formal system is “sound”? I’m used to thinking of soundness as a property of semantics, i.e. of the relationship between a formal system (syntax) and some model of it.

]]>Three years ago I mentioned Sasha Borovik’s prediction that in twenty years Inna Capdeboscq will be the last non-retired mathematician in the world able to repair the proof. Of course, along with a verified proof, it would be wonderful if people could develop the field so as to make the proof simpler, i.e., the Darwin mentioned in the quote here might come along.

]]>What is especially exciting to me is the prospect of going on and verifying the classification of finite simple groups. The experts who contributed to this monumental effort are aging or passing on, and there is a danger that there aren’t enough younger people with the requisite training (in what is an extremely specialized field) to critically survey the proof. Meanwhile others use the classification theorem in their research.

I hope I live to see such a computerized verification.

]]>Yes, for essentially the same reason that mathematics did not collapse when Russell found his paradox.

Although it is really soundness that we want, not just consistency. Being inconsistent is only the most extreme way to be unsound.

]]>Although, it seems very unlikely to me that Coq would ever accidentally be inconsistent in just such a way that someone trying to formalize a real mathematical proof would *accidentally* take advantage of to get around a flaw in the proof.

I believe that Coq has been proved correct using a bare-bones stripped-down version of Coq, which in turn is quite small and amenable to verification by a human (unlike the proof of Feit and Thompson). But I don't know the details; probably the Types Forum knows this better. And I do know that Coq was inconsistent once, briefly, by mistake; so Jean is right to want to check!

]]>I heard about this from the type theorists here at Princeton. An awesome achievement!!

]]>Subject: [Math-visitors] remarkable achievement in proof verification

Date: Wed, 17 Oct 2012 13:22:57 -0400

From: Jean Gallier <jean@cis.upenn.edu>

To: faculty@math.upenn.edu, grad@math.upenn.edu, visitors@math.upenn.edu

Dear all,

I learned from the "Types Forum" that a group of researchers at MSR/INRIA

led by Georges Gonthier completed a formal verification (in Coq) of the

"Odd order theorem," due to Feit and Thompson

(every finite group of odd order is solvable).

The task of proof verification in Coq took 6 years. The Coq development contains

~ 170 000 lines of code

~ 4200 definitions

~ 15 000 theorems.

They did find small gaps, but all could be patched.

For more details, see

http://www.msr-inria.inria.fr/Projects/math-components/feit-thompson

In particular, at the end of the page, look at the "final theory graph."

The question remains: how do we know (and prove) that Coq is correct?

We have to verify the verifier!

Best,

-- Jean ]]>