4 ms·

What must be trusted in Coq in the kernel, which contains 30,000 lines of code for the latest development version. It cannot be completely verified by Coq itse

• yodsanklai 12y ago
  > It cannot be completely verified by Coq itself due to the Gödel theorem What can't be proved in Coq is that the proof system is consistent. However, we can in theory verify that the implementation of the proof system satisfies its specification (edit: maybe that's what you were saying!).
  • amelius 12y ago
    Doesn't the Gödel theorem say that such proof cannot be found for all conceivable systems; but that for any particular system, a proof could in principle be found?
    • ineol1 12y ago
      It's for _any_ such system. Edit : it says that if there is such a proof, then the system in inconsistant.
      • dkubb 12y ago
        Is it possible to prove most of the system so that the remaining unprovable parts are minimized?
        • TheLoneWolfling 12y ago
          Yep. And there are proof systems that use this approach (i.e. build a series of provers that each prove the next (more complex) one).
        • jbapple 12y ago
          Unfortunately, it is sometimes the case that the remaining unprovable part is the most epistemologically dubious part. See, for instance, "Coq in Coq", by Bruno Barras and Benjamin Werner, http://www.lix.polytechnique.fr/~barras/publi/coqincoq.pdf http://www.lix.polytechnique.fr/~barras/publi/coqincoq.pdf , in which the Calculus of Inductive Constructions is used to prove the consistency of the Calculus of Constructions. See also John Harrison's "Towards self-verification of HOL Light", http://www.cl.cam.ac.uk/~jrh13/papers/holhol.pdf http://www.cl.cam.ac.uk/~jrh13/papers/holhol.pdf , and Gentzen's consistency proof, https://en.wikipedia.org/wiki/Gentzen%27s_consistency_proof https://en.wikipedia.org/wiki/Gentzen%27s_consistency_proof , which use similar strategies (by assuming the existence of an inaccessible and assuming recursion up to epsilon_0). Sometimes one can get relative consistency results. For instance, I believe it is provable in ZF that if ZF is consistent, so if ZF+AC+(V=L)+GCH.
    • ttctciyf 12y ago
      I think it's something like this: you can't prove the consistency of a formal system using that same formal system, unless it is in fact inconsistent, but you can model a formal system from inside a larger formal system and then prove things like consistency about the smaller system from inside the larger one. But then the consistency of the larger system is unproven and you're stuck with an endless regress into ever larger FS's as you pursue the chimera.
      • ObviousScience 12y ago
        Only for sufficiently powerful systems, I believe. Things like first order logic are too simple to introduce the kinds of statements Godel used to prove the incompleteness theorem about arithmetic.
      • eli_gottlieb 12y ago
        Weirdly enough, as Gentzen showed, you can use a theory that is "sideways" to first-order logic, neither strictly more powerful nor weaker nor equivalent in power, to demonstrate the consistency of first-order logic. Strong normalization theorems are used for typed lambda calculi like the Calculus of Inductive Constructions to show consistency, as well.