The Coq mailing list

[Laurent Théry <Laurent.Thery AT inria.fr>]

On 02/04/2015 03:30 PM, michel levy wrote:

I have read (not in details ) the proof in Coq (in the Coq'users contributions) of the Goedel second incompleteness theorem written by Russell O'connor.
This proof uses two unproven hypothesis known as the second and third Hilbert-Bernays-Löb derivations conditions :   
    Hypothesis HBL2 : forall f, SysPrf T (impH (box f) (box (box f))).
    Hypothesis HBL3 : forall f g, SysPrf T (impH (box (impH f g)) (impH (box f) (box g))).
Usually the second hypothesis is written
    2. T ⊢ Prov T ( φ ) ⇒ Prov T ( Prov T ( φ ) )
Did you know any proof (in Coq or in an assistant proof) of this second hypothesis ?
Even in the serious logic'books, this proof is omitted, as too long, too tedious.
   

-- 
email : michel.levy AT imag.fr
http://membres-liglab.imag.fr/michel.levy 

Maybe you should look at what Larry Paulson did recently on this tpoic with the isabelle theorem prover