Let LA denote polynomial time arithmetic, Con_LA the equation stating the
consistency of LA, LAJ the system LA+Con_LA, and E2A double exponential time
arithmetic.

A manuscript of mine provides a proof that Con_LA is provable in E2A.
Further, a formula F of LA is provable in E2A iff if is provable in LAJ.
from Con_LA.  Since the second incompleteness theorem holds for LAJ,
Con_LAJ is not provable in E2A.

It is straightforward to show that an LAJ proof of 0=1 can be transformed,
verifiably in single exponential time arithmetic, to an LA proof of
a formula of the form "LA(H(x))=N" where H is a closed term of LA and N
is the dyadic numeral for the Godel number of 0=1.  

It then follows that "There is no LA proof of a formula of the form
'LA(H(x))=N'" is not provable in LE2A.

The proof of Con_LA in E2A makes use of the function Val(F,a), which has
value 1 if the formula F is true at the assignment a, else 0.  A lemma of
the above-mentioned manuscript states that it is provable in E2A that
if P_4(x)=F then Val(F,a)=1, where P_4 is a version of LA suitable for
proving the lemma.

The question is, why isn't it provable in E2A that Val("LA(H)=N",a)=0?

I have uploaded a more detailed version of the question at
 [https://www.researchgate.net/publication/371077325_A_Question_on_an_Unprovabili
ty_Proof][1]


  [1]: https://www.researchgate.net/publication/371077325_A_Question_on_an_Unprovabili%20ty_Proof