Gödel's Proof as a proof strategy for P = NP or P != NP I have had this thought for quite a while. Gödel proved the incompleteness of arithmetic by creating a one-to-one correspondence with a number and certain numerical relationships to create a statement that says, in effect, "I cannot be proven." 
My question is: has there been any attempt to go the other direction? That is, has anyone succeeded in showing that an arbitrary statement -- such as P=NP -- Is a statement that says of itself that it has no proof? In order for this to happen, a one-to-one relationship needs to be shown between what that means in the mathematics of it and its "meta meaning". In short, Gödel went from meta-meaning ("this statement cannot be proven") and constructed a number that, in effect, stated this meta-meaning. Has there been attempts to show that statements already in existence have a meta meaning stating that they cannot be proven? if so, has anybody used this strategy to prove or disprove P=NP's provability? It may be a simple question, but it has been bothering me for a while. Thanks for reading :)
 A: My thoughts on the subject, which must be taken with a grain of salt as I'm far from being an expert on this subject (or any subject, to that matter):
This idea was mentioned in Douglas Hofstadter's "Godel, Escher, Bach", but I never saw it seriously discussed. As far as I know, no independence proof (e.g. the independence of the Continuum hypothesis) has ever used such a technique, and it's hard to see why P=NP will be different.
It is worth remembering that Godel's statement is difficult to build. In effect, you can think of it as a logical encoding of a small computer program which knows how to decode Godel's numbering and knows how to check proofs (in an effective system, i.e. one in which proof checking is computable), and to top it all, it also contains an encoding of itself using a smart diagonalization trick. This is not something you stumble upon; it is a very delicate construct. 
I see no reason to assume that a statement such as P=NP, which deals with a class of Turing machines, can be re-interpreted as discussing itself. If such a far-fetched interpretation can be made for P=NP, why can't it also be done for, say, IP=PSPACE (which is well known to be true)?
So although this idea is quite fascinating, I see no reason to believe it is true; however, it might be explored by taking some toy independent statements and trying to see if they can be re-interpreted in a way they talk about themselves (I think it will already prove immensely difficult because of the complexity of making a statement talk about itself). I would start there, not attack P=NP directly.
It is also worth mentioning that there is no apparent reason why P=NP is undecidable. There are many indications that it is undecidable using standard methods (e.g. diagonalization - see Baker-Gill-Solovay) but many other complexity-theory problems had a similar difficulties and were laid to rest using a clever new formulation or point of view (IP=PSPACE being a nice example).
A: In fact, a distant relative of the concept you suggest has been applied to a question of complexity; as Gadi alludes to briefly in a comment, while Peano Arithmetic (the theory of addition and multiplication over the natural numbers) is incomplete (this is the core of Godel's theorem), Presburger Arithmetic - the theory of only addition over the natural numbers - is decidable, but it's hard: it requires doubly-exponential time.  It turns out that this can be proved via a version of Godel's proof; the key is that multiplication can be 'approximated' in the theory of addition, up to a certain level:

For each natural number $k$ there is a formula $M_k(x,y,z)$ of length $O(k)$ in the language of addition such that $M_k$ is true if $x\times y = z$ and $\displaystyle{x\lt 2^{2^{2k}}}$.

This implies that if the theory of addition were decidable without using exponentially large numbers, then the theory of addition and multiplication (i.e., Peano Arithmetic) would also be decidable - essentially, the constructions of Godel's proof would go through using the additive approximation to multiplication to build a Godel sentence.  Since we know the conclusion is false, the hypothesis must also be, and the theory of addition is exponentially hard.  This is laid out in Paul Young's paper "Godel theorems, exponential difficulty and undecidability of arithmetic theories: an exposition" in the Recursion Theory collection; you can find most of the paper on Google Books.
A: This question is fundamentally misinterpreting Godel's theorem. As far as we know, there is not a single "unprovable theorem", all theorems should be provable if they are meaningful, and provable in a natural system of mathematics, extending arithmetic with appropriate higher infinity axioms.
The objects constructed by Godel's theorem are unprovable in a given axiomatic system only, their natural function is as new axioms, which strengthen the axiom system in ways that allow them to be proven. Within set theory, you use axioms of higher infinity (inaccessible cardinals of various types) to do this.
Godel's theorem explains why you need these stronger axioms, and why these axioms produce new true theorems about arithmetic (although such enormously infinite objects are not particularly absolute themselves). But it does not mean that there is any question whatsoever that is undecidable in the sense of this question. In particular, the idea that P!=NP could be "undecidable" is not reasonable.
But P!=NP is not a simple statement, it says that there does not exist a computer program such that for any instance of 3SAT, it halts, and the eventual output satisfies this instance three sat. The structure of this statement is (not)(exists)(forall)(exists), or (forall)(exists)(forall), and this is Pi-3 (meaning three alternating quantifiers, starting with forall), and any true Pi-3 statement is hard to prove.
[ EDIT: Kaveh points out below that the innermost quantification is fake--- you don't need to do a quantification to check when a program in P halts--- it is guaranteed to halt in polynomial time. So if you phrase it properly, including the order n of the polynomial running time in the outermost "there exists", the innermost quantification is bounded above, and so it doesn't count as a step up. The proper statement: For all programs R and integers n such that R(p) stops changing in time less than $p^n$, there exists an instance of SAT indexed by integer P, such that the output of R(P) after Pn steps is not a solution to P. The proper phrasing shows that this is a $\Pi_2$ statement, not $\Pi_3$. $\Pi_2$ statements are not as difficult.]
The statement that every theorem should be provable from an axiom of higher infinity is not a theorem--- it is difficult to even formulate the statement precisely, because it it refers to a process of higher-infinity which cannot be formalized completely within an axiom system. But this is an article of mathematical faith--- articulated by Cohen in "Set Theory and the Continuum Hyptothesis". You might want to restrict this article of faith to Pi-1 statements, to statment
For a better discussion, see this: https://mathoverflow.net/questions/72062/what-are-some-proofs-of-godels-theorem-which-are-essentially-different-from-th/72151#72151
A: It has been shown that P=NP( or P != NP) cannot be proved by diagonalization, using diagonalization. The proof of this relies on giving an oracle to a Turing Machine. See the references below:
http://courses.csail.mit.edu/6.841/spring09/scribe/lect02.pdf
http://www.chronon.org/articles/PvNP.html
A: There have been statements without the meta-meaning shown to be unprovable in PA.  Two are the Paris-Harrington theorem and Goodstein's theorem, but they do not seem to bear on P=NP.
A: I am far from an expert also, but every independent statement can be interpreted as saying 'I am not provable', thats what it means to be undecidable. And every theorem says 'I am provable'.
