Can we prove that to prove P != NP is NP-Complete.

P!=NP seems to be a very hard question. But I didn't know whether anyone has quantified its hardness. So I ask the following question. Given a suitable formal system F, is finding a proof with less than n symbols for P != NP an NP-complete problem? (Asymptotic time of finding proof with respect to the proof length.)

It's clearly in NP since given a proof of length n, we can use rules in formal system F to determine whether each line follows from the above. However, it's not clear o me whether it should be NP-Complete.

If this problem is NP-Complete, then to prove that P != NP is practically impossible. The implication is that we can settle P != NP only if P = NP.

No, it's certainly not $NP$-complete; it's in $P$.

Either there is a proof of $P \; != NP$ or there isn't (if in fact $P \; != NP$, there's no guarantee that there is a proof of that). If there is a proof, there is a proof of a certain length $N$. Then for any $n > N$, to exhibit a proof of length $< n$ takes constant time (namely, you just print out THAT proof). If there is no proof, then of course you can't exhibit such a proof, and the answer (again, in constant time) is just "No, it can't be done".