The Coq mailing list

[michel levy <michel.levy1948 AT gmail.com>]

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