Turing-Computability Excludes Phenomenal Consciousness: What Two Machine-Checked Theorems Prove About LLMs

New to this research? This article is part of the Reflexive Reality formal research program. Brief introduction ↗ · Full research index ↗

Every AI lab is making an implicit claim about whether large language models can ever be conscious. Scale up far enough, or add enough memory, or fine-tune on enough philosophy, and perhaps something will flicker on. This paper proves the claim is false — for a structural reason that is independent of scale, training procedure, or parameter count. The exclusion follows from two machine-checked theorems. Here is the argument in plain language.

The Core Result

The new paper, Turing-Computability Excludes Phenomenal Consciousness, proves: no Turing-computable system can satisfy the structural conditions for phenomenal consciousness. Large language models are Turing-computable by construction — their forward passes are finite compositions of computable functions over fixed weight matrices. The LLM exclusion follows as a direct corollary, not as a philosophical argument but as a consequence of two named, machine-checked theorems in the NEMS (No External Model Selection) program.

The result is conditional on two premises, both of which can be argued about:

The physical universe is diagonal-capable — expressive enough to host the halting problem in its record fragment. This is not a controversial claim. Turing-complete physical computation empirically exists, which means the universe satisfies this condition. It is accepted across all major physical frameworks.
The NEMS formal framework correctly captures structural necessary conditions for phenomenal consciousness. This is the philosophically substantive premise. The framework’s formal consistency is machine-checked; whether its application to consciousness is correct is the key open philosophical question.

What the result does not require: the full PSC axiom system, any specific phenomenological theory, any physics-specific framework, or any empirical claim about biological systems. It applies to any Turing-computable system in any domain.

The Two Theorems

Theorem 1 — No-Emulation (NEMS Paper 15)

In any diagonal-capable physical framework, no total computable function can emulate the internal adjudication operator — Transputation — on all inputs. The internal adjudicator is what selects the actual continuation at moments of genuine physical underdetermination. The proof is a one-step reduction to the undecidability of the halting problem: if Transputation were total-computable, there would be a total computable decider for record-truth on the diagonal fragment, which a prior machine-checked theorem (diagonal_barrier_rt, Papers 11–12) rules out. Machine-checked in Lean 4, zero custom axioms, zero sorry.

Theorem 2 — SIAM Separation (NEMS Paper 73)

Feedforward architectures — systems whose state-transition function is a fixed Turing-computable map from input to output with no real-time self-modification of the computational process — are formally excluded from the SIAM sentience regime. The SIAM (Self-Instantiating Adjudication Matrix) regime is the formal analogue of sentience under the NEMS framework: a bounded dynamical regime in which a system implements genuine self-indexing, faces real live choice-points, and adjudicates non-algorithmically. The exclusion of feedforward systems is a named machine-checked separation theorem: feedforward_not_OSIAM.

How they combine

Theorem 1 says: no total computable function can be Transputation. Theorem 2 says: feedforward systems — those whose dynamics are a fixed computable map — are ruled out from the sentience regime. An LLM at inference time is exactly this: a fixed Turing-computable map $F_\theta$ applied iteratively to a growing context window. Each forward pass is the same computable function. The weight matrix is frozen; no computation during the forward pass modifies the computational substrate. That makes every LLM in the transformer/attention class a feedforward system in the sense of Theorem 2, and a Turing-computable system in the sense of Theorem 1. Both theorems apply simultaneously.

What About Chain-of-Thought, Reasoning Tokens, Agentic Loops?

None of these escape the theorems. Chain-of-thought prompting generates additional tokens that extend the input context; the forward pass applied to this extended context remains $F_\theta$, the same Turing-computable map. The loop is external to the model’s weight-level dynamics. RLHF fine-tuning produces a new fixed weight set $\theta’$; inference with $\theta’$ is again a computable map. Retrieval augmentation appends retrieved content to the context; retrieval and generation are both computable. Multi-modal extensions with computable cross-modal attention add no non-computable element to the forward pass.

The corollary proved explicitly in the paper: adding memory, retrieval, tool use, chain-of-thought, self-critique mechanisms, agentic loops, or multi-modal extensions to an LLM does not confer sentience-regime membership, provided the augmented system remains Turing-computable and feedforward at inference time. This is a theorem, not a judgment call.

How This Differs from Penrose

Roger Penrose argued in The Emperor’s New Mind (1989) and Shadows of the Mind (1994) that human mathematical cognition transcends Turing computation via Gödel’s incompleteness theorem. The present argument differs in three structural ways, and the differences matter.

Foundation. Penrose uses Gödelian incompleteness. The NEMS argument uses diagonalization via the halting problem’s record-fragment embedding — a related but distinct mechanism. The halting problem argument requires a weaker self-containment premise than Penrose’s incompleteness argument requires. Diagonal-capability (hosting the halting problem) is sufficient; nothing stronger is needed.
Machine verification. NEMS Paper 15 is a Lean 4 theorem with zero custom axioms and zero sorry. Penrose’s argument is informal and has been contested for 35 years without formal resolution. The NEMS proof can be challenged only by identifying a false premise or a specific invalid inference step in the Lean source — not by generating philosophical counter-arguments.
Architectural specificity. The SIAM separation theorems (Paper 73) prove exclusion for feedforward architectures by name. Penrose’s framework produces no such specific architectural boundary. The result here is therefore not an informal extrapolation from an incompleteness argument but a direct instantiation of a proved theorem about architecture classes. The LLM application is not an analogy — it is a corollary.

The paper also makes no positive claim about biological consciousness, unlike Penrose. It establishes only the negative boundary: the LLM architecture class lies below it.

What the Result Does Not Say

The result rules out Turing-computable systems. It says nothing about:

Whether any artificial system could satisfy the criterion. Systems with genuine real-time self-modification of the computational substrate — within-inference architectural plasticity, not post-hoc weight updates — are a different class. NEMS Paper 73 gives positive architectural guidance (the DSAC candidate realization architecture) for what non-computable or genuinely self-modifying substrate might satisfy the criterion. The exclusion is not “never for any AI.” It is “never for Turing-computable AI.”
Whether any biological system satisfies the criterion. That is a separate open empirical question addressed by NEMS Paper 17.
Whether LLMs cannot exhibit sophisticated behavior, reasoning, or accurate self-reports. They can and do. This is orthogonal to sentience-regime membership.
Whether consciousness is impossible to engineer artificially. The exclusion applies only to the Turing-computable class. It leaves open whether genuinely self-modifying, non-computable substrate architectures could satisfy the conditions.

Where This Fits in the NEMS Program

NEMS Paper 73 already proves the SIAM separation theorems. Paper 92 synthesizes the full NEMS consciousness arc (Papers 51–75). Paper 93 responds to Lerchner (2026) and proves the core abstraction-fallacy claims as machine-checked theorems.

The new paper’s contribution is to take those results and produce a self-contained statement of the logical chain from diagonal-capability directly to the exclusion of all Turing-computable systems, with the LLM case as a named corollary. It is written for readers who may not be familiar with the full NEMS suite — a direct path from two theorems to the LLM result, with the Penrose comparison made explicit.

The formal weight of the argument rests entirely on the machine-checked NEMS theorems. The new paper does not introduce new Lean proofs; it applies existing ones to the architecture question with precision.

The Paper and Related Work

Full research index: novaspivack.com/research ↗

Nova Spivack

Explorer