4 ms·
Is it possible to prove most of the system so that the remaining unprovable parts are minimized?
by dkubb 12y ago
Is it possible to prove most of the system so that the remaining unprovable parts are minimized?
- TheLoneWolfling 12y agoYep. 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 agoUnfortunately, 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.