A ℙ≠ℕℙ proof for review (v1.0)

[wij]

Using C-like notation:

ℙ::= Set of decision problem which can be computed by TM in P-time.

ℕℙ::= Set of decision problem q of which the positive answer can be verified by
a certificate c. I.e. a decision function v(q,c) yields true in P-time.

Spec: Function "bool S(Prog,UInt)" decides whether or not the argument Prog
program (equal-powerful as TM) is satisfiable in the range specified by UInt,
and the algorithmic steps is bounded by a given polynomial formula P. IOW:
S(f,n)==true iff ∃v,x, x<=n, v(f,x) proves f(x)==true (e.g. v simulates f(x))
and Time(v(f,x))<=P(|f|+|x|) proves a P-time certificate.

From the specification, Problem(S)∈ℕℙ (precisely, ℕℙℂ).
S can be implemented by a DTM. And, a Prog u of which the function is defined as
follow will also exist (The implement of u is very different. The implement of S
and u as existence proof are omitted, because they are supposedly understood
immediately):

bool u(UInt x) {
return !S(u,x);
}

From Liar's paradox and the HP proof, u is a never-terminating (undecidable)
instance. If S(u,n) computes in greater than P time, the answer S(u,n)==false is
fine. But, if S is in P time, u(x) can be in P time, then, the only condition
for S to return false in this case is u(x)==false which will not happen.
P-time S is unimplementable. Therefore, Problem(S)∉ℙ, ℙ≠ℕℙ.
QED.