Want to take part in these discussions? Sign in if you have an account, or apply for one below
Vanilla 1.1.10 is a product of Lussumo. More Information: Documentation, Community Support.
I heard about this from the type theorists here at Princeton. An awesome achievement!!
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!
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.
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.
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.
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.
@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.
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!
But how is that informal notion of “trust”/”soundness” different from consistency?
Some relevant discussion on an old MO question of mine.
Try that again: Some relevant discussion. (You have to make sure the http is in there!)
Ta! Using my phone and didn’t check the URL worked.
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):
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.)
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.
Yes, it still relies on the interpretation.
1 to 16 of 16