We propose a programmatic study of a recurring pattern in logic-adjacent fields: the movement by which thought passes from local operation to projected totality. In some of such cases, a locally witnessed procedure is quietly reified into a claim about a completed domain or a self-standing object.
Reflexica asks whether, in any given case, a local witness has been illicitly converted into closure, or whether the formulation of some problem entails the consistency of such a procedure.
Preliminary state. Revised June 2026. Licensed under CC-BY.
We begin from an intuitionistic standpoint [Brouwer, 1913] and observe that Book IX, Proposition 20 of Euclid’s Elements [Euclid, 1956] does not begin from a completed set of primes.
It supplies an extension rule:
From any assigned finite multitude of primes, one constructs a number coprime to every member of that multitude. The proposition is an iterable and open-ended procedure before the contemporary presentation converts it into a claim about a completed domain. The difference concerns metamathematical commitment rather than attitude.
We recall the Tristram Shandy paradox [Russell, 1903]. The procedural, indeed constructive reading commits only to what that construction reaches, and no further. The existential reading permits the result to be expressed over a completed domain, the primes as a total collection, rather than as an indefinitely iterable extension operation. One reading foregrounds the construction by which a further prime divisor is obtained; the other licenses quantification over the resulting domain. Both readings are valid, though they carry different proof-theoretic and semantic commitments.
Classically, this is cost-free: the existential formulation preserves the theorem while suppressing the difference between a proposition proved in a completed domain and a witness extracted from a construction. The contrast is between a classically accepted existential $\exists x:A\,P(x)$ and its constructive interpretation as data: an object $a:A$ together with evidence for $P(a)$. Under propositions-as-types, this is represented by an inhabitant of $\Sigma{x:A}P(x)$ [Howard, 1980]. The relevant distinction here is between proof-theoretic signatures [Gentzen, 1935].
To establish that a number is composite, one produces a factor greater than one: a finite, extractable, checkable object. The witness supplies the computational content of the proof; in the case of compositeness, a factor pair $(a,b)$ is the finite object whose verification establishes the claim [Kleene, 1945]. Numbers alone, in a constructive sense, do not carry such a witness; it must be decided for them. Consequently:
Consider the asymmetry in the simple case below:
We write schematically. Compositeness has the form
so a proof may present a finite factor witness $(a,b)$. Primality is naturally expressed by bounded exclusion:
The left arrangement witnesses factorization directly as the factor is read off the shape, while the right is not known to admit a (geometric) primitive. No configuration of seven units exposes a nontrivial divisor, because there is none to exhibit. Primality must be established by exhaustive elimination, carried as a conclusion rather than read off as a positive configuration. The absence marks a lack of factor structure, independent of any gap in knowledge.
The lack of nontrivial factors is carried through coprimality, as a number differing by one from a common multiple of the assigned primes. Any assigned prime that measured both numbers would also measure their unit difference; none can therefore measure the constructed number. Whether that number is prime or is measured by another prime, the assigned multitude is refuted as exhaustive. The result is a reusable refutation schema, not an existential claim over a completed domain.
The contemporary restatement promotes this into a positive claim over the domain of primes. This introduces no immediate contradiction, but “conservative” has a meaning distinct from a proved conservative-extension theorem: the promotion preserves local practice while altering the semantic status of the object introduced. Its apparent harmlessness makes the transition easy to absorb.
By the early 20th century, tensions of this kind could no longer be dismissed as quirks [Gödel, 1931] [Heyting, 1931]. A theory may be locally impeccable and still carry a commitment in the way its existential conclusions are understood: a commitment that exceeds what the underlying procedure licenses. The difficulty is that the classical statement is also an epistemic posture, as a benign promissory reification.
This pattern, that recurs wherever local witness is taken to license global closure, does not impair mathematics or the sciences as they are ordinarily practiced; but it can become consequential at the periphery, where reflexivity, hard problems, foundational questions, and metamathematical phenomena converge, so that the unexamined passage from local witness to global closure begins to carry relevant structural weight.
Reflexica does not demand any replacement of existing foundations or calculi, including Type Theory [Martin-Löf, 1984], Constructive Mathematics [Beeson, 1985], or Homotopy Type Theory [Univalent Foundations Program, 2013]. It begins from the rigor these traditions already impose on constructive methods.
Importantly, within the Brouwer-Heyting-Kolmogorov interpretation, it is already touched implicitly: absurdity is not a hidden object disclosed by a theory, but the proposition for which no construction is given, while negation is a procedure that carries an assumed proof into that absence by contradiction [Troelstra and van Dalen, 1988]. The question proper to Reflexica begins later: What happens if an absence, once stabilized as obstruction, becomes available for promotion into a semantic primitive?
The term “Reflexica” is a rivaling antiphrasis borrowing from Impagliazzo’s Five Worlds taxonomy for average-case complexity [Impagliazzo, 1995], projecting a missing “uninhabited world.”
We use this image to ask why a lack of method, denoted as problems, is converted into semantic architecture at all. Complexity theory enters here as both object and symptom: a field whose dominant formulations may stall when coupled to a contradiction-free classical totality, and thence, no corrective can follow because the promotion remains also conservative: an existential claim that could be read back into some vague procedural idea.
The obstruction concerns a structural absence beyond the technical limitations of particular formalisms or their theoreticians: a gap that certain classical principles reify locally, converting it into a reflection principle against which the system recurses on itself, rather than making contact with an independent domain that could supply closure.
At a specific threshold, a theory might produce what functions as an essence claim after its intended closure has already been reached, or to seek a proposition that restores a transitivity the system has quietly lost. Neither operation announces itself as a departure, reading as ordinary mathematical practice. It is this readability that allows the passage to go unmarked. We can invent words for something we did not yet find, but if it is not to be found, we are reflecting. This reflection will be indistinguishable from genuine search. The closer we move to the void, the harder it becomes to distinguish genuine search from reflection.
We propose some core methodological principles:
From the above we extend to the following characteristic preliminary instruments:
The incomming cases proceed from a sensitizing pattern through structured and formal cases, then widen into schematic extensions: local practice encounters an absence, obstruction; that local condition is stabilized or reified; and a demand for semantic closure is then placed upon it.
Mackie’s Error Theory [Mackie, 1977] serves here as an introductory idea, rather than a formal case. The progression it illustrates is this: philosophical practice encounters an absence, stabilizes that absence through its own internal demands, and at some threshold there is a longing for a semantic object. The Mackie’s Argument from Queerness, which we interpret as a form of logical induction, names the strangeness of the moral properties that realist discourse appears to require, properties that are neither straightforwardly natural nor straightforwardly constructed.
We consider this to be the Reflexica moment: If Mackie’s diagnosis is correct, it cannot be confirmed by producing the objective moral property whose existence it denies; its correctness therefore cannot take the form of a positive witness for the very object whose absence it asserts. What the argument marks is a shadow in the strict BHK [Troelstra and van Dalen, 1988] sense: the relevant error is an absurdity, and absurdity admits no realization. What may be constructed is a refutation—a procedure that takes any purported witness of the objective moral property to contradiction—not a positive witness of the error itself. The absence is not merely a gap in the inventory but becomes theoretically active inside the practice it diagnoses.
We immediately see this pattern in how the halting predicate behaves [Turing, 1937]. Once a computation halts, its completed run supplies a finite, positive witness of that fact. If it does not halt, however, no finite stage certifies that it never will: at every unfinished stage, the computation may yet halt. Non-halting is therefore not established by the local procedure in the way halting is; it remains an open-ended claim whose closure requires more than the run itself supplies.
Whether the same passage recurs under more exact conditions is what the following sections investigate. That it appears in other phenomenological discussions suggests the pattern is not local to metaethics, though the complete image is what remains programmatic here.
We turn to something more structured: Newcomb’s Problem [Nozick, 1969].
Here the issue is predictive scope. The familiar story grants the predictor knowledge of the deliberation from which the choice emerges: whatever the agent thinks, the predictor has already classified the outcome of that thought and filled the opaque box accordingly. For a fixed agent in a fixed experiment, this is a coherent stipulation. The reflexive pressure appears when this casewise reliability is extended to every admissible decision procedure, including procedures in which the predictor’s own verdict enters the deliberation.
Newcomb’s Problem. Let there be two boxes. The transparent box contains $A=1000\,\mathrm{USD}$; the opaque box contains either $B=10^6\,\mathrm{USD}$ or $B=0$. Before the agent chooses, a predictor $P$ predicts whether the agent will take only the opaque box, $C_1$, or both boxes, $C_2$.
It places $10^6\,\mathrm{USD}$ in the opaque box after predicting $C_1$, and nothing in it after predicting $C_2$. The agent then chooses without observing $B$:
$$ \begin{array}{c|cc} & B=10^6 & B=0 \\ \hline C_1 & 10^6 & 0 \\ C_2 & 10^6+1000 & 1000 \end{array} $$For either fixed value of $B$, $C_2$ pays exactly $1000\,\mathrm{USD}$ more than $C_1$. Let $p=\Pr(B=10^6\,\mathrm{USD}\mid C_1)$ and $q=\Pr(B=10^6\,\mathrm{USD}\mid C_2)$. Conditioning instead on the act gives $\operatorname{EU}(C_1)=10^6p$ and $\operatorname{EU}(C_2)=1000+10^6q$.
Causal Decision Theory (CDT) [Lewis, 1981] holds $B$ fixed under intervention and recommends $C_2$. Evidential Decision Theory (EDT) [Jeffrey, 1965] conditions on the act and recommends $C_1$ whenever $p-q>10^{-3}$. Both calculations take the joint relation among the prediction, the box content, and the act as given. Problem Critique asks what range of decision procedures that relation can coherently cover.
The crucial quantifier is whatever the agent thinks. If the prediction claim ranges over an open-ended class of decision procedures, that class can contain procedures whose output depends on a representation of the prediction itself. Let $P(\ulcorner D\urcorner)\in\{C_1,C_2\}$ be the verdict that $P$ assigns to the procedure $D$. Once the class is closed under predictor-sensitive procedures, it contains the diagonal procedure
If $P$ predicts $C_1$, this procedure chooses $C_2$; if $P$ predicts $C_2$, it chooses $C_1$. The predictor therefore fails on $D_P^{\perp}$ whichever verdict it returns. The obstruction belongs to the universal scope of the prediction claim: a predictor can be stipulated for a restricted class that prevents its verdict from entering the procedures it evaluates, but it cannot remain correct over an open-ended class closed under this predictor-relative construction.
Newcomb’s Problem is thus a local model of the wider promotion tracked by Reflexica. The ordinary experiment stipulates success for one agent under one information structure. Oraclehood appears when that local success is read as the ability to know the outcome of any deliberation, including deliberation about the predictor. At that point the prediction is part of the process it predicts, and the evaluator is being asked to close its domain under its own evaluation.
A stochastic predictor avoids contradiction by relinquishing total correctness. Its reliability and the resulting payoffs remain well-defined inside a fixed model, while the diagonal case marks the boundary beyond which local predictive success cannot be promoted into a total evaluator for predictor-sensitive agents.
The preceding case has the same abstract shape that diagonalization makes exact: an evaluator is applied to a description whose behavior depends on that evaluation. The canonical formal case is, of course, Incompleteness [Gödel, 1931].
This topic is central to Reflexica because it binds a formal self-referential construction to the semantic question of what its sentence is entitled to mean. Only after this pause do the two readings become visible:
On an antirealist or broadly constructive picture, arithmetic truth does not outrun construction, or some admissible form of realization [Heyting, 1931] [Kleene, 1945] [Dummett, 1975]. In a way, Incompleteness is already internalized: A mathematical proposition is not treated as determinately true independently of the means by which it can be established.
On a realist (classical) picture, arithmetic truth has an essence independent of proof or warrant [Dummett, 2001] [Frege, 1918]. $\mathbb{N}$ forms a determinate domain, and arithmetic sentences have determinate truth-values whether or not a given proof system can establish them.
Notice how we do not get to stand outside both pictures and inspect, from a neutral position, which one is true. Any argument for one picture over the other must itself proceed by some method. Let that method be denoted by $M$. $M$ must be a proof-method, or at least a warrant-conferring method. It must tell us whether arithmetic is to be understood realistically or antirealistically. To “decide” between realism and antirealism, we would need a proof-method whose authority is not already being interpreted realistically or antirealistically. But no such neutral $M$ is available. If $M$ is understood antirealistically, it cannot establish semantic excess over proof, since such excess is precisely what the antirealist refuses. If $M$ is understood realistically, then it already assumes the semantic authority it was supposed to justify.
By the Diagonal Lemma [Boolos et al., 2007], one can construct a sentence $\mathsf{G}_{\mathrm{T}}$ such that
$\mathsf{G}_{\mathrm{T}}$ is stable across the dispute. Both can recognize the formal construction, and both can accept that, under the relevant consistency assumptions, $\mathrm{T}$ cannot prove $\mathsf{G}_{\mathrm{T}}$. The disagreement concerns what follows from this.
In the antirealist picture, Gödel’s Incompleteness Theorems remain a genuine formal result. They show that a sufficiently strong effective proof system cannot, on pain of inconsistency, prove its Gödel Sentence, but the antirealist does not thereby have to accept the further claim
That claim requires a notion of arithmetic truth that outruns proof or warrant. Yet such a notion is precisely what the antirealist rejects or refuses to treat as primitive. For the antirealist, then, Incompleteness is deflated. It becomes a theorem about the already (intuitionistically) internalized limits of a given formal system, not a revelation of an independently obtaining arithmetical fact. In this sense $\mathsf{G}_{\mathrm{T}}$ is or could be vacuous with respect to realism, because the semantic surplus needed for the realist conclusion has already been disallowed. The theorem still marks a boundary, it does not by itself license a stronger metaphysics of arithmetic truth.
In the realist picture, the same construction has greater force. If there is a determinate standard model of arithmetic, and if $\mathrm{T}$ is sound with respect to that model, then $\mathsf{G}_{\mathrm{T}}$ is true because what it says is the case. It says that it is not $\mathrm{T}$-provable, and, under the relevant assumptions, it is not $\mathrm{T}$-provable.
So the same formal construction now yields the proper separation
Here $\mathsf{G}_{\mathrm{T}}$ is not merely a boundary theorem about $\mathrm{T}$. It becomes a method for showing that arithmetic truth exceeds any given sufficiently strong effective formal system. $\mathsf{G}_{\mathrm{T}}$ is then read as an arithmetical truth not captured by the proof system whose provability predicate it mentions.
Thus $\mathsf{G}_{\mathrm{T}}$ is invariant across the dispute, but its semantics are not. The invariant construction is
The Second Incompleteness Theorem is central here: the formal diagonal does not decide between these readings, since it can be accepted in both regimes. What changes is the semantic promissory authority granted to the sentence after the formal result has been obtained.
If $M$ is treated antirealistically, then it cannot prove the existence of arithmetic truth beyond proof, since such truth is not admitted as an independent target. If $M$ is treated realistically, then it already presupposes the semantic excess it was meant to establish. $M$ is then exactly what cannot be neutrally supplied, and $\mathsf{G}_{\mathrm{T}}$ bleeds into our meta theory:
If $\mathrm{T}$ is read modestly, as a formal calculus, $\mathsf{G}_{\mathrm{T}}$ merely says: this sentence is not derivable in $\mathrm{T}$. Under the usual consistency assumptions, that is a true boundary statement about $\mathrm{T}$. If $\mathrm{T}$ is read ambitiously, as capturing proofhood, the same sentence becomes decisive. It is now a truth whose non-derivability separates proof from $\mathrm{T}$-derivation. Thus the diagonal is stronger than an objection to $\mathrm{T}$: it works whether $\mathrm{T}$ is treated as empty syntax or as ideal proof. In the first case it marks a limit; in the second it refutes the promotion.
This again seems to be a Reflection Principle [Feferman, 1962]: the demand for a proof of the correct theory of proof is itself caught in the dispute it seeks to resolve. Gödel’s Theorem is stable under both realism and antirealism, but it cannot neutrally choose between them, because the choice requires the very semantic authority under dispute.
We have to diagnose a limit, not only of $\mathrm{T}$, but of the attempt to adjudicate the status of proof from a position outside proof. Once a method is asked to certify the correct interpretation of method itself, it is no longer neutral.
Bekić’s Lemma [Bekić, 1984] gives the positive counterpart to diagonal obstruction. It says, in effect, that a simultaneous fixed point can sometimes be replaced by an ordered sequence of one-variable fixed points. For a mutually recursive system
the pair need not be treated as one opaque semantic whole. Under the relevant fixed-point conditions, one solves one equation parametrically and then solves the induced remaining equation. The dependence is not removed; it is given an order.
This supplies the useful criterion. A reflexive configuration often appears as semantic instability: the system refers to itself, depends on itself, or produces an invariant from which its generating distinctions cannot be recovered. Bisection asks whether that dependency can be made sequential:
When it succeeds, no completed external semantics is needed in advance. The system acquires a syntax that records how the fixed point is produced. The circularity remains, but it is no longer opaque. Church’s $\lambda$-calculus makes the boundary vivid: it does not first resolve the reflexivity of self-application in a completed semantics; it operationalizes it. What appears as a reflexive black box becomes traversable through reduction, and this finite syntactic discipline is sufficient for computational universality [Church, 1936].
The same distinction may transfer to machine-learning interpretability. An embedding vector has no meaning in isolation; its role is fixed by relations and distributions. A global map from internal states to human concepts may fail to exist as a single semantic object. Interventions are therefore proposed decompositions of a mutually dependent semantic field, not disclosures of a pre-existing atlas.
The methodological directive is consequently:
Bekić’s Lemma is central to Reflexica because it makes the alternative precise: can an apparently reflexive whole be decomposed into ordered syntactic dependencies, or does the demand for closure remain? We may isolate particular neural functions, circuits, and mechanisms without thereby obtaining a complete picture of the brain. Reflexica asks whether that missing whole is merely an unfinished achievement of inquiry, or whether there is no complete semantic picture to be recovered from the local accounts—a closure presumed by the question but not witnessed by its procedures.
The transfer from strict diagonalization to less formal settings is part of the program. A resonance across computation, linguistic competence, proof theory, and self-modeling is not yet evidence that these domains instantiate one phenomenon. The question is narrower: when does self-description become a demand that a local procedure close over the totality to which it belongs?
Consider a Turing Machine
with language
In a Tarskian register, the distinction is between the machine’s formal specification and a semantic extension assigned at the metalevel [Gruber, 2016]. A particular computation may witness that a string belongs to $L(\mathcal{M})$; the language itself is not another term available to the computation. It is the extension obtained when the machine’s activity is taken as a whole.
The same form appears in weaker empirical cases. Once Bob asks "How many words do you know?" from Alice, she answers only by estimate, as the requested inventory would have to be produced by the very competence being inventoried. A language model asked the same question also returns a local response rather than a retrieved census. Of course, these cases do not establish an identity with Incompleteness. They mark the point at which self-description begins to resemble a demand for closure, but what is more interesting is that any identification of the schema is itself obstructed.
Consider the refutation of the Lucas-Penrose Argument against mechanism: Let $\mathrm{T}$ be a formal system proposed as a model of mathematical reasoning. By Incompleteness, there is a sentence $\mathsf{G}_{\mathrm{T}}$. The next step, echoed by many popular depictions, is that the human mathematician can nevertheless see that $\mathsf{G}_{\mathrm{T}}$ is true. If $\mathrm{T}$ captured the mathematician’s reasoning, then the mathematician would have access to a truth unavailable to the system alleged to model her. Hence, mind exceeds mechanism.
Putnam’s counterargument is that the seeing is not free: to assert that $\mathsf{G}_{\mathrm{T}}$ is true, one must already be entitled to a semantic claim about $\mathrm{T}$: roughly, that $\mathrm{T}$ is sound for the relevant arithmetical domain [Putnam, 1995]. That entitlement is not supplied by $\mathrm{T}$ itself, it is semantic, exactly what Alice and Bob cannot see objectively. The argument therefore assumes, at the moment of insight, what it later presents as disclosed.
This addresses the validity of the argument, but the phenomenological force only partially. The subject does not ordinarily experience herself as assuming soundness and then deriving the truth of $\mathsf{G}_{\mathrm{T}}$. She experiences herself as seeing that $\mathsf{G}_{\mathrm{T}}$ is true. The missing premise has been identified, but the felt immediacy remains.
The historical criticism that $\mathsf{G}_{\mathrm{T}}$ is a trivial or degenerate case can be read, in this register, as precisely the Reflection Principle under examination: the alleged triviality marks the point at which the standpoint required to certify the sentence has already been imported.
The empirical analogue is a first-person halting problem. A system may produce a verdict about a procedure that is presented as its own, just as a subject may report that she sees the truth of $\mathsf{G}_{\mathrm{T}}$ for a system $\mathrm{T}$ said to capture her reasoning. The report is an empirical event: it can be observed, and perhaps mechanized. What it does not by itself supply is a witness that the reporting standpoint is identical with the procedure whose total correctness is being certified.
In the formal case, diagonalization blocks a total decider from remaining closed under its own counterexample. In the empirical case, the same structure reappears as a problem of evidence: Is a system’s first-person verdict genuine self-substituted closure rather than a verdict in which the target procedure has already been externalized?
A Large Language Model supplies the trivial argument. Realized by a Turing Machine, it can nevertheless form, state, and defend a judgment about whether a mechanistic system recognizes its own limits [Brown et al., 2020], including a first-person judgment that it has done so. The occurrence of that judgment is therefore compatible with mechanism by construction. What remains unwitnessed is the identity between the procedure producing the verdict and the total procedure whose correctness the verdict purports to certify.
The Turing-Zombie construction makes this distinction explicit. It is a Turing Machine $\mathcal{Z}$ with the relevant formal competence, effectively a theorem prover of the kind used in Dependent Type Theory [Martin-Löf, 1984] or the Calculus of Inductive Constructions [Rocq Development Team, 2025]. It can construct and verify the usual diagonal proof that there is no total Turing Machine $\mathcal{H}$ which decides, for arbitrary machines $x$ and inputs $y$, whether $x$ halts on $y$. Given a candidate decider $\mathcal{H}$, $\mathcal{Z}$ can form the diagonal machine
Then $\mathcal{D}_{\mathcal{H}}(\mathcal{D}_{\mathcal{H}})$ contradicts $\mathcal{H}$ either way. If $\mathcal{H}(\mathcal{D}_{\mathcal{H}},\mathcal{D}_{\mathcal{H}})$ says that $\mathcal{D}_{\mathcal{H}}$ halts, then $\mathcal{D}_{\mathcal{H}}$ loops. If $\mathcal{H}(\mathcal{D}_{\mathcal{H}},\mathcal{D}_{\mathcal{H}})$ says that $\mathcal{D}_{\mathcal{H}}$ does not halt, then $\mathcal{D}_{\mathcal{H}}$ halts. Therefore no such total decider $\mathcal{H}$ exists.
The Turing-Zombie understands this theorem in the only sense required here: it can construct the proof, verify its steps, and apply it to any externally presented candidate decider. Its blindness appears only when it is asked to occupy the impossible position itself, namely to be the total decider whose domain remains closed under the diagonal counterexample generated from that very decider. At that point there is no further stable output to produce, not because $\mathcal{Z}$ lacks the relevant formal faculty, but because the faculty itself generates the obstruction.
Many particular self-facts are decidable: $\mathcal{Z}$ may recognize features of its own code, simulate bounded fragments of its own behavior, and verify local claims about itself when the relevant object has been finitely presented. The obstruction concerns total closure. The Turing Machine $\mathcal{Z}$ can never see itself for how it is seen from a higher level: as an element of a total domain whose behavior is being evaluated from outside the very procedure that produces that behavior.
We see that Reflexica weakens the intended Lucas-Penrose Disanalogy substantially, which becomes a mere survivorship bias. A system may reason correctly about an externally presented formal object from a stronger background standpoint, just as the Turing-Zombie reasons about an externally presented candidate decider. That does not show that the system has closed the diagonal loop on itself. If $\mathrm{T}$ is the very system whose reasoning is being enacted, then the soundness needed to pass from non-provability to truth is precisely what cannot be generated from inside $\mathrm{T}$ without strengthening the standpoint.
This is also where ordinal and modal proof theory become relevant. The obstruction is not merely a negative limit; it generates controlled reflection progressions. Provability logic $\mathrm{GL}$ captures principles governing a single provability predicate, while polymodal provability logics such as $\mathrm{GLP}$ stratify provability across indexed modalities. In Beklemishev’s analysis, such systems organize iterated reflection principles and proof-theoretic ordinal progressions [Beklemishev, 2004]. Turing’s ordinal logics provide an earlier form of the same strategy: when a formal system reaches a consistency or completeness obstruction, one passes to a transfinite sequence of strengthened systems rather than closing the original system over its own correctness [Turing, 1939]. In Reflexica’s terms, the loop is not closed internally; it is replaced by a tower of explicitly marked standpoints.
Penrose reads a local, witnessed act, a subject producing a confident verdict about a system $\mathrm{T}$ said to model that subject’s reasoning, as licensing a global claim that minds can close the relevant diagonal loop while machines cannot. The Turing-Zombie blocks that promotion. The local episode witnesses only that a system can produce the verdict when operating from a standpoint not identical with the object under evaluation.
This is the passage from local self-report to global self-closure. The local phenomenon may be fully real: the subject sees, the machine classifies, the model reports, the system stabilizes a verdict. The question is whether that event licenses the stronger claim that the system has closed the total domain to which the event itself belongs.
The self-application would be another totalizing inference to conclude that no confident report of Gödelian self-insight is ever genuine self-application. What survives is narrower: given a system that reports Gödelian self-insight with stable confidence, has any witnessed procedure been exhibited that distinguishes genuine self-substituted closure from the external-object procedure available to a Turing-Zombie? At present, no such procedure has been exhibited. Such would be the queer object.
The pattern traced so far recurs inside the apparatus that seems best placed to escape it. Yedidia and Aaronson gave a 4,888-state construction of this kind [Yedidia and Aaronson, 2016]; subsequent reductions produced a 27-state version, later reduced to a 25-state machine and formally checked in Lean4 [Leng, 2025].
The conjecture's two truth values are not symmetric. If Goldbach is false, the machine halts at some finite step: a single counterexample, locally witnessable in Euclid's sense. This is a $\Sigma_1$ condition. If Goldbach is true, the machine never halts. But non-halting is not itself witnessed by any finite computation. It is a $\Pi_1$ condition: a totality claim, closed only by completing an uncompletable search.
Here $H(n)$ says that the Goldbach-search machine has halted by stage $n$. The asymmetry is the point: a counterexample is a local witness; the absence of all counterexamples is not.
It is tempting to think Busy Beaver supplies the missing ground. If $S(25)$ were known, one could run the 25-state Goldbach machine for $S(25)$ steps. If it had not halted by then, it never would, and Goldbach would be settled. On this reading, the totalization is not fictitious, only large. Busy Beaver appears to hand us a completed bound.
But this only moves the totalization upward. The function $S(n)$ is not computable. It is defined by surveying all halting $n$-state machines and taking the greatest halting time among them [Radó, 1962]. Thus $S(n)$ is itself a closure over halting behavior. To know $S(25)$ is already to have completed the relevant halting analysis for every 25-state machine.
So the apparent escape repeats the structure it was meant to overcome. The truth of Goldbach requires a non-halting fact about a particular search machine; the Busy Beaver bound requires halting and non-halting facts about the entire finite space of machines of the same size. The finite description of the space does not make its semantic classification recursively available.
In classical semantics, $S(25)$ denotes a definite integer. But that ontological determinacy does not supply epistemic access to it. The gap between a completed object and a procedure for reaching it is precisely what Reflexica has been naming throughout.
We see again: any proposed escape from a reflexive totalization, a function, an oracle, a growth rate, or a bound placed beyond ordinary search, faces the same dilemma. If it is computable, it cannot decide the totality it was introduced to close. If it is uncomputable, it has not grounded the closure; it has reproduced the closure one level up. There is no totalization-free floor inside recursive computation. Section 6 reaches the same conclusion for AI oraclehood, but here the obstruction has already appeared inside arithmetic.
Classical totalities and completed domains are undeniably productive; Reflexica asks what is added when local procedures are mistakenly read as completed, and what forms of obstruction have to appear.
For this reason, Reflexica is not an ultrafinitist program. It does not reject the use of idealized transfinite domains, its question concerns the point at which such objects are treated as licensed by a local procedure that does not itself witness the relevant closure.
The program therefore extends the diagnostic beyond formal mathematics without treating the extension as automatic. Its central task is to ask whether empirical cases exhibit disciplined analogues of classical undecidability, witness failure, and closure obstruction. A proper question is consequently:
To assert their identity in advance would transform a series of bounded observations into an unwitnessed totality claim, which is the very passage Reflexica seeks to mark. We identify a frontier at which formal logic, metamathematics, and self-modeling systems converge on a question that none of them, separately, has the resources to settle.
Hence, the final question becomes:
We ask whether a structural configuration consisting of self-relation or self-survey, a demand for closure, and an ensuing unwitnessed reification or obstruction is preserved across a change of substrate.
If it is, then Reflexica may name a limitative structure. If it is not, then the failure is itself diagnostic: the apparent recurrence belongs to our description of the cases rather than to a structure preserved across them.
All of the above can be seen as an update to constructive logic's complaint. It is the case that classical realism, an attitude carried on top of classic logic rather than entailed by it, has no internal notion of an inquiry that has stalled rather than concluded.
or more explicitly:
We consider to give a single name to a pattern that currently has none: a locally witnessed procedure quietly promoted into a claim about a completed domain, and the obstruction that surfaces long after that promotion is made. Self-modeling systems encounter versions of this behavior: a proof system’s reflection on its own consistency, a moral theory’s diagnosis of an error it cannot itself instantiate, a predictor’s totalization over agents whose choices are conditioned by the prediction.
Without shared vocabulary, they read as unrelated local difficulties rather than instances of one structure. Reflexica supplies that vocabulary and, with it, a discipline: a claim of completed closure is admissible only where the procedure producing it actually witnesses that closure, not merely where the domain is convenient to treat as settled.
This is why the excluded target is realism rather than any particular calculus. Realism, as Dummett isolates it, treats an unresolved case as a temporary gap over a fact that already obtains [Dummett, 2001] [Dummett, 1975]. That attitude is what licenses the promotion Reflexica tracks: it lets local absence of a witness be read as global presence of a fact, in logic as much as in ethics or in claims about a machine's self-understanding. Reflexica does not ask anyone to abandon classical logic or excluded middle to resist this; it asks that the promotion be made visible.
Note. Mathematics regularly permits this, except where the exceptions matter.
We recall Heidegger’s point that the sciences cannot take the Nichts as their object names the boundary. Here, logic fights back, such that Reflexica appears [Heidegger, 1929], not as an object within a domain, but as the reflection a system encounters when its demand for closure outruns every witness it can produce. The unity of the cases therefore cannot lie in a shared substrate, as no system can internalize its own substrate.
The only common denominator is human intuition and construction. This is where Reflexica touches intuitionism most directly: descriptions do not escape the finitude of the thought that forms them. Reflexica names this recurrence without pretending to have stepped outside it; or, if it does, it tries to make the mistake only once.
In this weak diagonal sense, it is trivial to state the theorem:
If a recursively realized AI system could provide closure on reflexive semantic problems, then the constructivist or antirealist restriction would fail. There would exist a neutral procedure capable of deciding, from within computation, the very semantic totalities whose closure constructivism denies. But Reflexica assumes that the realism-antirealism dispute is not decidable without producing a Queer Object. Therefore, AI cannot provide closure on reflexive semantic problems.
The relevant formal analogue is Rice’s Theorem [Rice, 1953].
No nontrivial semantic property of a computable function is decidable uniformly from the program's description. This does not by itself prove the Reflexica prediction, since the demand on AI is not merely a question about the extension of a partial computable function. But it gives the correct shape of the obstruction. Once the demand shifts from syntactic manipulation to semantic adjudication, the hope for a general recursive decision procedure disappears.
Consider a user who asks an AI system to find the paper that matters for a project. At first this appears to be an ordinary search problem. The system can retrieve papers, rank citations, summarize arguments, identify terminological overlap, and propose connections. But the phrase "matters for my project" does not name a fixed object already available in the database. It depends on the project's evolving interpretation of itself: what counts as central rather than peripheral, which analogy is productive rather than accidental, which objection is decisive rather than merely relevant, and which future direction the inquiry ought to take.
The more capable the AI becomes, the more it can expand this field of possible relevance. It can discover neighboring literatures, reconstruct hidden assumptions, generate alternative framings, and expose tensions the user had not yet formulated. But this does not close the problem. It intensifies it. Each improvement generates a richer semantic field that again requires an act of interpretation: among these newly visible possibilities, which one is the answer? If the AI could finally settle that question as a matter of procedure, it would be deciding a nontrivial semantic property of a reflexive domain. In that role, it would not merely be supplying local witnesses; it would be functioning as an oracle over the total semantic field of the inquiry.
Recent AI successes in mathematics do not refute this prediction. A new Erdős-style proof [Tsoukalas et al., 2026], a new matrix multiplication algorithm [Fawzi et al., 2022] may be an important datapoint, but its significance depends on the curve to which it belongs. If the result extends the existing trajectory of local mathematical competence, then it does not yet threaten the thesis. It shows that the system has moved farther along the same axis, not that it has changed axes.
This matters because oraclehood would not appear as a larger value on an ordinary progress curve. It would require a change in the kind of capacity being measured. A system that produces a new construction inside a fixed mathematical problem has still operated under given standards of success. The construction may be surprising, and it may outperform human methods, but it remains locally checkable. It does not decide the semantic totality in which the problem, its relevance, and its closure conditions are themselves at stake.
The prediction is therefore exposed in the present, not postponed into a distant future. Reflexica anticipates diminishing returns at the point where recursive amplification is asked to become semantic closure. The graph may rise, and it may rise quickly, but the closer the system comes to problems whose criteria are themselves under interpretation, the more additional capability should produce expanding candidate fields rather than final authority. More search, more synthesis, and more proof production should continue to generate local witnesses; they should not converge into a procedure that decides which semantic totality has been closed.
That is precisely what the Reflexica constraint denies. An AI realized by a Turing Machine can operate recursively over articulated inputs, latent patterns, explicit criteria, and locally checkable mathematical targets, but it cannot possess both consistency and oraclehood over a reflexive semantic totality. Hence the predicted stall is not a halt in technical capability.
The coming years will not merely show whether AI becomes more capable, they will show whether increasing capability begins to flatten, proliferate alternatives, or displace the closure question rather than resolve it. If it does, then even extraordinary mathematical discoveries will not be counterexamples but will demonstrate that AI can extend inquiry with increasing force, while still failing to close the reflexive semantic totality.
Reflexica is falsified once a “logical” Queer Object is discovered or constructed.