It is! It is surprisingly difficult to come up with a grammar and a proof that it cannot be recognized by a PEG. Part of the reason is probably that PEGs and CFGs are quite different: A CFG is a set of generative rules which specify a set of strings, whereas a PEG is actually more like a recursive program.
OK. I thought you meant that a non-constructive proof existed that there is such a CFG. That's how I interpreted "Finally, since PEG can be parsed in linear time, there must also be some CFG which cannot be recognized by any PEG". But I see that on cstheory you wrote instead (being more precise?) "most probably ... PEG does not contain CFG".
Ah, yes, that's because the non-linear complexity of binary matrix multiplication (which CFG parsing can be reduced to) is strongly suspected to be a lower bound, but I don't think that there is a formal proof of it (I am not an expert in complexity theory, so I am just basing this on what some authors seem to suggest). So, the non-constructive argument is a "proof" in the same sense that some results can be proved by first assuming that P /= NP.
There's an open question on Stack Exchange for anyone who feel like taking a stab at the problem: http://cstheory.stackexchange.com/questions/34792/does-peg-c...