It's for _any_ such system. Edit : it says that if there is such a proof, then t...

dkubb · on March 25, 2015

Is it possible to prove most of the system so that the remaining unprovable parts are minimized?

jbapple · on March 25, 2015

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 , 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 , and Gentzen's 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.

TheLoneWolfling · on March 25, 2015

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).