Statement that inequality of P and NP obstructs finding a proof of their separation In this set of video lectures, Prof. Mulmuley emphasizes several times that P vs. NP is a very deep philosophical question at the core of Mathematics and that the fact that the two classes are not equal stands as an obstruction to proving that they are not equal (I paraphrase here, according to my limited understanding).

Now, I have two difficulties with this idea. Firstly, it was presented as though it were common mainstream belief (akin to the belief that P != NP). I did not come across this idea before, being expressed explicitly in this manner (maybe this is lack of exposure from my side).

The second difficulty is a bit more technical. P != NP tells something about hardness of finding proofs for provable statements, it does not saying anything about existence vs. non-existence of such proofs. Said naively, if P != NP, then this fact should not obstruct the existence of an easy, verifiable proof of this fact (other facts may provide such an obstruction though).

Am I misunderstanding something?

Note: I was not really sure if this question belongs to tcs.SE but I couldn't find a more suitable choice.
I also think that what was meant might have been obstructions akin to the natural proofs barrier of Razborov and Rudich. The barrier on a high level shows that current methods of proving circuit lower bounds are "self-defeating" when applied to the P vs NP problem. Suppose you want to prove that SAT is hard by showing that it satisfies some predicate which is not satisfied by problems in P. Suppose the predicate is satisfied by most boolean functions (the largeness property) and can be computed in time $2^{O(n)}$ on functions that take $n$ inputs, when given the $2^n$-size truth table of the function (the constructivity property). Razborov and Rudich show that if such a predicate exists, then there are no strong pseudorandom number generators. So the existence of the object we're trying to use to separate P from NP would itself imply a statement in the spirit of P=NP.

There are arguments why you expect that hardness predicates would satisfy the largeness property. Certain "formal complexity measures" have the property that if they lower bound the complexity of any one function, then they lower bound the complexity of most functions. Also, by the classical counting argument, most functions are hard, so if you expect that the predicate captures hardness, then it should be satisfied by most functions. The constructivity property gets to your question. It is true that there could in principle exist a hardness predicate that cannot be evaluated in time polynomial in the truth table of the function. But most combinatorial proofs of existence can be made constructive. Even proofs that on first inspection seem to use inherently non-constructive arguments were often later made constructive. Two recent examples are the algorithmic Lovasz Local Lemma of Moser and Tardos and Nikhil Bansal's constructive version of Spencer's discrepancy upper bound for general set systems. So it looks like we might not have proof methods that take us outside the realm of polynomial time constructions. 

Check the details in the natural proofs chapter of Arora-Barak: http://www.cs.princeton.edu/theory/complexity/naturalchap.pdf