Let LA denote polynomia time arithmetic, Con_LA the equation stating the consistency of LA, LAJ the system LA+Con_LA, and E2A double expnential 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

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

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