11
$\begingroup$

Coq has been used to provide formal proofs to the Four Colour theorem, the Feit–Thompson theorem, and I'm sure many more. I was wondering - is there anything that can't be proved in theorem provers such as Coq?

A little extra question is if everything can be proved, will the future of mathematics consistent of a massive database of these proofs that everyone else will build on top of? To my naive mind, this feels like a much more rigorous way to express mathematics.

  • 5
    It shouldn't be possible due to Goedel's Incompleteness Theorem.2012-12-28
  • 1
    Define "everything" and "possible" :) It's not clear from what I've read that Coq "proved" Feit Thompson, only that it verified a proof. In theory, you can write a "dumb" proof generator that checks all possible proofs for correctness, and thus yields all provable results. Coq might be more efficient, but it cannot be more complete than that.2012-12-28
  • 0
    Putting it briskly, Gödel's First Incompleteness Theorem uses rather elementary reasoning (and it was very important to Gödel that this was the case). Which is why the Theorem is formalizable in arithmetic, the point we rely on to prove the Second Theorem!2012-12-28
  • 1
    Sure, but there is an "internal" meaning to incompleteness, and an "external" meaning to incompleteness. Basically, it is just saying that sufficiently complicated axioms cannot yield complete systems. That some axiom systems are incomplete is obvious (take the axiom for a ring and try to resolve the question "Is 1+1=0?") The shock of incompleteness is that we want our axioms to represent something, the natural numbers, we feel is "concrete." Essentially, complicated systems of axioms will have to be like the axiom for a ring.2012-12-28
  • 2
    The set of theorems of a computably-axiomatised first-order theory is computably enumerable – this is indisputable. So perhaps the question should be, can all of mathematics be captured in a sufficiently powerful first-order system?2012-12-28

4 Answers 4