TLDR; We hint at the possibility that there are problems that are neither solvable, nor the opposite, more precisely:

When a problem ranges over all problems it can represent, diagonalization forces a self-referential instance whose status cannot be uniformly settled: itself. Such a problem is not solvable, not unsolvable, but structurally impredicative^[1] within an intuitionistic setting.

What we present is neither an answer, nor a dissolution, but a fixed point theorem of problem adequacy in the sense of Poincaré^[2] and others. Our first argument demonstrates plausibility by reformulating a theory of provability semantics to one of problem solvability. A stronger formal argument through Gödel Numbering over problem solvability can be attained at: https://arxiv.org/abs/2511.14665.

We push Brouwer-Heyting-Kolmogorov (BHK) semantics^[3],

$\begin{array}{cc}\text{conj}& A\wedge B:a\in A,b\in B\\ \text{disj}& A\vee B:0+a\in A\text{or}1+b\in B\\ \text{impl}& A\to B:(A\to B)\text{map}\\ \text{absurdity}& \neg A:A\to \perp \\ \text{exist}& \exists xA\left(x\right):(x,a)\\ \text{forall}& \forall xA\left(x\right):x\mapsto a\end{array}$ 

into a domain where it is seldom invoked, and then notice that the failure of admissibility of some class separation in Heyting Arithmetic corresponds exactly to the same reflective trap^[4] identified by Russel, Gödel, and others. 

Consider how in complexity theory, uniform assertions like

$\begin{array}{c}\forall L\subseteq {\Sigma }^{\ast },[L\in NP⟹L\in P].\end{array}$

are treated as ordinary set-theoretic statements. The fact that such assertions hide a universal quantification over all NP-verifiers is almost never foregrounded, and the consequences of that hidden semantic quantifier, as a problem about problems would admit impredicativity, are not part of the discipline’s conceptual vocabulary. We thus formulate an isomorphism first: realizability of sentences as adequacy of problems, so that the question how solvability and provability relate in constructive logic, emulates the provability of solvability within class separation.

Realizer Logic

The realizability relation $⊩$ is defined relative to Heyting Arithmetic (HA) as the background formal theory, that is quite modest (see above). Formulas of HA receive BHK-style proof-objects, and the realizability clauses interpret HA’s connectives by assigning constructive operations in the usual proof-semantic sense. Atomic predicates describing polynomial-time and nondeterministic polynomial-time behavior are represented in HA by formulas $NPTime\left(e\right)$ and $PTime\left(e\right)$

Their realizers are positive computational witnesses:

$s⊩NPTime\left(e\right)⟺s=(k_s,f_s),t⊩PTime\left(e\right)⟺t=(k_t,g_t),$ 

where each tuple is an HA-definable finite object encoding a bounded trace or verifier. Since HA contains no primitive refutational form for these predicates, no atomic clause yields contradictory information. The BHK clauses for implication, negation, and universal quantification are imported as the intended semantics for the corresponding HA connectives:

Thus every connective of HA is interpreted by its BHK counterpart, and the shape of a realizer is dictated by the HA-formula in which it appears.

Admissibility and HA-Sentences

Each HA-sentence (A) is assigned a constructive problem-value:

$\left[\right[A\left]\right]:Sent\left(HA\right)\to Prob.$

A sentence is admissible when HA’s BHK semantics validate it:

$Adeq\left(A\right)⟺\exists r,(r⊩A).$

Under this perspective, HA’s formulas are meaningful only when the associated BHK interpretation supplies a realizer. HA serves as the syntactic carrier, and realizability supplies the semantic content: To realize the HA-sentence

$\phi \equiv \forall e\left(NPTime\right(e)\to \neg PTime(e\left)\right),$

a $\lambda$-term (r) must satisfy in the BHK interpretation:

$r⊩\forall e\left(NPTime\right(e)\to \neg PTime(e\left)\right).$

Unfolding the HA connectives via BHK semantics yields:
$\forall e,,\forall s,,\forall t,(s⊩NPTime\left(e\right)\wedge t⊩PTime\left(e\right)\Rightarrow r\left(e\right)\left(s\right)\left(t\right)⊩\perp ).$

Thus, within HA’s interpretation, each (r(e)) must be a higher-type functional:

$r\left(e\right):Real\left(NPTime\right(e\left)\right)\to (Real\left(PTime\right(e\left)\right)\to \perp ),$

computing, from any pair (s,t) of atomic HA-realizers, a contradiction.

Structural Constraint on Atomic HA-Realizers

The HA-definable realizers for $NPTime\left(e\right)\wedge PTime\left(e\right)$:

Encodes only positive computational behavior, are uniformly finite HA-objects, contain no negative information expressible in HA, and do not carry any negative content.

Hence the HA-definable product

$Real\left(NPTime\right(e\left)\right)\times Real\left(PTime\right(e\left)\right)$

consists solely of extensional, affirming witnesses. No HA-definable $\lambda$-term can extract a contradiction from such data, since HA provides no elimination rule for these atomic predicates that could yield absurdum.

Consequence for HA

Under BHK semantics inside HA:

(i) Totality requirement (HA-functional):
{r(e)(s)(t)} must be HA-defined for all atomic realizers.

(ii) Refutational requirement (BHK → HA):
 The HA-object {r(e)(s)(t)} must realize ($\perp$) in HA.

Because HA assigns no negative elimination principles to $NPTime$ or $PTime$, no HA-definable λ-term satisfies both constraints.

The failure occurs at the interface: HA’s syntax for implication and negation is clear, but their BHK semantics require computational acts that HA’s atomic predicates do not support. The consequence: Inadmissibility of a problem $\phi$ in HA

For every λ-term (r) definable in HA:

$\exists s,t,(s⊩NPTime\left(e\right)\wedge t⊩PTime\left(e\right)\wedge r\left(e\right)\left(s\right)\left(t\right)⊮\perp ).$

Therefore:

$\forall r\in \Lambda r⊮\phi .$

By the HA-admissibility criterion:
$\neg Adeq\left(\phi \right).$

Thus HA’s syntax can state $\phi$, but the HA–BHK semantics cannot assign it a constructive problem-value.

Conclusion: HA provides the formal language; realizability supplies the modest BHK semantics. The sentence,

$\forall e\left(NPTime\right(e)\to \neg PTime(e\left)\right),$

fails not because HA forbids it, nor because it expresses a false computational claim, but because HA’s atomic predicates, interpreted constructively, lack the negative structure required to support BHK-negation uniformly. The sentence cannot be supplied with an HA-realizer, and thus it fails the semantic admissibility test.

The conclusion is therefore:
(i) Syntactically, HA can parse the sentence.
(ii) Semantically, under BHK realizability, it denotes no constructive problem.
(iii) Hence its inadequacy is structural and traceable precisely to the HA–BHK interface.

Explanation: In intuitionistic logic the canonic instance of class separation is not rejected as false; rather, it is rejected as lacking constructive content. It does not describe any problem in the BHK sense for HA. A problem can't be assumed to be realizable a priori, it may, however, fail to be adequate in a formal sense, in which case it is only parsable syntactically without supporting realizers. The notion of a problem is fundamentally semantic, while the absence of a syntactic representation therefore does not, by itself, demonstrate non-existence.

Within the BHK framework, the situation is more stringent. The central intention of strict admissibility is precisely to identify meaning with the existence of realizers. Under this view, a formulation must come with a syntactically well-defined problem whose realizability witnesses its meaningfulness. Before one can even ask for a solution, a precise syntactic formulation is therefore required.

The point can be made without metaphor:

If one accept BHK as minimal semantic framework, the adequate sentence of P vs NP does not merely encode a computational separation; it attempts to internalize a problem whose subject matter is the entire problem–solution relation itself.

The only way to know whether an internal realizer for the HA-sentence $\phi$ 
exists is to solve the very external problem that $\phi$ was intended to encode. The trap is not conceptual or semantical; it is a fixed point produced by the interaction of HA, BHK semantics, and our atomic P/NP clauses.

The formal part follows a syntactic construction forming a Gödel Sentence as a Gödel Problem that is a member of the Problem Space. Informally:

Let P be the problem:
“Is the classification output for ⌜P⌝ correct?”
Let Q be the problem:
“Is the classification correct in virtue of its own diagonal
form?”
Let C be the problem:
“Must any total classifier deciding between {P, Q} on the
coded problem space misclassify at least one of them?”

To make an analogy,

 $T⊢\left(Prob\right[\forall e,\left(NPTime\right(e)\to \neg PTime(e\left)\right)\left]\right)$ 

could constitute the most intricate Rosser Sentence^[5] available, just as the most self-similar real^[6] is the hardest to approximate.

1. ^{^}

   see: Solomon Feferman, 2005, "Predicativity" in The Oxford Handbook of Philosophy of Mathematics and Logic. Oxford University Press: 590–624. 

2. ^{^}

   consult on Predicativism: N. Weaver. What Is Predicativism? available at: https://api.semanticscholar.org/CorpusID:40352024. cf: S. Feferman, Systems of predicative analysis, J. Symbolic Logic 29 (1964), 1-30. 

3. ^{^}

   cf: A. S. Troelstra and D. van Dalen. Constructivism in Mathematics, Vol. 1. North-Holland,

4. ^{^}

   cf: G. Boolos, J. P. Burgess, and R. C. Jeffrey. Computability and Logic. Cambridge University Press, 5th edition, 2007. ISBN 9780521877520.

5. ^{^}

   cf: Barkley Rosser (September 1936). "Extensions of some theorems of Gödel and Church". Journal of Symbolic Logic. 1 (3): 87–91. doi:10.2307/2269028

6. ^{^}

   cf: A. Hurwitz, “Über die angenäherte Darstellung der Irrationalzahlen durch rationale Zahlen,” Mathematische Annalen 39 (1891), 279–284.