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
