[FOM] Strict reverse mathematics of incompleteness.

[Daniel Mehkeri]

Are there any reverse mathematical results relevant to Gödel's 
incompleteness theorems? It has been mentioned that even Robinson's Q 
does not prove its own consistency. But I am also wondering about 
something orthogonal to that: not just what is required of a formal 
system for the incompleteness theorems to apply to it, but also what is 
required of a formal system to prove the incompleteness theorems.

This would be at the level of "strict" reverse mathematics as Friedman 
calls it. I am vaguely aware that encoding of syntax becomes an issue 
here, and so the question may not even be precise enough as stated. 
Unfortunately I don't know how to state it more precisely than that.

This is relevant to the Con(PA) discussion of course. Briefly, if the 
incompleteness theorems cause us to doubt Con(PA), then why not doubt 
Con(Q)? But if Con(Q) is in doubt, then why believe the incompleteness 
theorems? So it might be useful to have a better idea of what the 
incompleteness theorems require.

Daniel Mehkeri