1. Scope
We reformulate Rice's theorem through effective higher semantics and give an exact rational ReLU compiler. The full manuscript and executable artifacts are attached. Classical undecidability and neural universality are established results [1,6,7]. We work in classical external mathematics.
2. Effective descriptions and the diagonal argument
Definition 2.1 (acceptable numbering). Let $$ \varphi:\mathbb N\times\mathbb N\rightharpoonup\mathbb N, \qquad \varphi_e(x)=\varphi(e,x), $$ be a universal partial computable evaluator. Its sections enumerate all unary partial computable functions. We assume a total computable specialization function $s$ satisfying $$ \varphi_{s(a,z)}(x)\simeq\varphi_a(\langle z,x\rangle). $$ Here $\langle-,-\rangle$ is a computable pairing, and $\simeq$ means equal defined outputs or joint divergence. Let $\mathcal R$ be the set of these partial functions. Write $e\sim f$ when $\varphi_e=\varphi_f$ extensionally.
Lemma 2.2 (effective fixed point). For every total computable $t:\mathbb N\to\mathbb N$, there exists $q$ with $\varphi_q=\varphi_{t(q)}$.
*Proof.* Universality supplies a code $b$ for $$ (z,x)\longmapsto\varphi_{t(s(z,z))}(x). $$ Put $q=s(b,b)$. Then, as partial computations, $$ \varphi_q(x)\simeq\varphi_b(\langle b,x\rangle) \simeq\varphi_{t(s(b,b))}(x)=\varphi_{t(q)}(x). $$ No step decides whether either computation terminates. $\square$
Theorem 2.3 (Rice). If $P\subseteq\mathcal R$ contains some $\varphi_a$ and omits some $\varphi_b$, there is no total computable $D:\mathbb N\to\{0,1\}$ such that $$ D(e)=1\quad\Longleftrightarrow\quad\varphi_e\in P. $$
*Proof.* Given such $D$, define the total computable code transformation $$ t(e)=\begin{cases}b&D(e)=1,\\a&D(e)=0.\end{cases} $$ For the fixed point $q$ of Lemma 2.2, $D(q)=1$ implies $\varphi_q=\varphi_b\notin P$, and $D(q)=0$ implies $\varphi_q=\varphi_a\in P$. Both contradict correctness. $\square$
The theorem permits an algorithm to inspect every bit of a program's syntax. It forbids a total correct answer when the required answer is extensional and nonconstant. It does not forbid semidecision procedures, incomplete sound analyses, or decisions on restricted subclasses.
3. Higher categorical and topos formulations
Write $\mathcal S$ for the infinity category of spaces and $\mathbf2=\{0,1\}$ for a discrete space. An infinity groupoid is a space, with points, paths, and higher paths; $\pi_0 B$ is its set of connected components. The zero truncation $\tau_{\leq0}B$ retains those components and discards higher homotopy.
Here $\operatorname{Map}$ is a mapping space. An object is $n$-truncated if all mapping spaces into it have homotopy groups zero above degree $n$; $\tau_{\leq n}$ reflects onto these objects. An infinity topos is an accessible left exact localization of a presheaf infinity category of spaces [4]. Left exact means preserving finite limits. For an infinity category $\mathcal C$, the theorem also applies to morphism semantics $B=\operatorname{Map}_{\mathcal C}(X,Y)$, whenever its presentation is extensional.
Definition 3.1 (extensional presentation). An extensional presentation of computable behavior in a space $B$ is a map $$ d:\mathbb N_{\mathrm{disc}}\longrightarrow B $$ such that $\varphi_e=\varphi_f$ implies a path $d(e)\simeq d(f)$. A Boolean semantic observation is a map $p:B\to\mathbf2$. It is nontrivial on the presentation when $p(d(a))=1$ and $p(d(b))=0$ for some codes $a,b$. It is effectively decidable on this presentation when its composite with $d$ is total computable.
Theorem 3.2 (higher semantic Rice theorem). For an extensional presentation $d$, no nontrivial Boolean semantic observation $p$ is effectively decidable on codes.
*Proof.* The set $\{e:p(d(e))=1\}$ is saturated under $\sim$, because a map to a discrete space takes endpoints of every path to the same bit. It therefore defines a nontrivial subset of $\mathcal R$. A computable composite $p\circ d$ contradicts Theorem 2.3. $\square$
Proposition 3.3 (truncation invariance). For every integer $n\geq0$, $$ \operatorname{Map}(B,\mathbf2) \simeq\operatorname{Map}(\tau_{\leq n}B,\mathbf2) \simeq\operatorname{Map}(\tau_{\leq0}B,\mathbf2). $$ Consequently Theorem 3.2 applies to the induced presentation in each $\tau_{\leq n}B$, with the same bits and witnesses.
*Proof.* A zero-truncated target is $n$-truncated for $n\geq0$. Apply the universal property of truncation twice [4]. The factorizations preserve the composite on every code. $\square$
Definition 3.4 (relative effective decision in a topos). Let $\mathcal E$ be a nondegenerate infinity topos, so its initial and terminal objects differ. Let $\Delta:\mathcal S\to\mathcal E$ be the constant-object functor, and put $\mathbf2_{\mathcal E}=1\amalg1=\Delta\mathbf2$. Consider $$ d:\Delta\mathbb N\to B,\qquad p:B\to\mathbf2_{\mathcal E}. $$ Let $d_e:1\to B$ be the section induced by the numeral $e$. Require $d_e\simeq d_f$ whenever $\varphi_e=\varphi_f$. A relative effective decision is a total recursive $D:\mathbb N\to\mathbf2$ together with a homotopy $p\circ d\simeq\Delta D$.
Theorem 3.5 (relative topos Rice theorem). If there are codes $a,b$ with $p d_a\simeq1$ and $p d_b\simeq0$, no relative effective decision exists.
*Proof.* Were $D$ such a decision, equality $\varphi_e=\varphi_f$ would give a path between the constant sections $D(e)$ and $D(f)$ of $1\amalg1$. The two coproduct injections are distinct in a nondegenerate topos, by disjointness of coproducts. Thus $D(e)=D(f)$ externally. The two witnesses give $D(a)=1$ and $D(b)=0$. Apply Theorem 2.3. $\square$
No points assumption is used. Nontriviality is relative to the presentation. General subobjects are classified by $\Omega_{\mathcal E}$; a decision requires a factorization through $\mathbf2_{\mathcal E}$.
The mapping-space argument of Proposition 3.3 also holds in $\mathcal E$ as $$ \operatorname{Map}_{\mathcal E}(B,\mathbf2_{\mathcal E}) \simeq\operatorname{Map}_{\mathcal E}(\tau_{\leq n}B,\mathbf2_{\mathcal E}). $$ Thus the same relative obstruction survives Postnikov truncation. This uses a reflective universal property; we do not assume that Postnikov truncation preserves arbitrary pullbacks. Separately, a geometric inverse-image functor $f^*:\mathcal E\to\mathcal F$, with $\mathcal F$ nondegenerate, preserves the presentation hypotheses and the two witnesses. Theorem 3.5 then applies in $\mathcal F$. An observation that a further quotient makes constant is outside its nontriviality hypothesis.
Proposition 3.6 (Lawvere's diagonal pattern). In a cartesian closed infinity category with terminal object, suppose $u:A\times A\to Y$ represents every map $A\to Y$ up to homotopy: for every $h:A\to Y$, some $a:1\to A$ satisfies $u(a,-)\simeq h$. Then every endomorphism $v:Y\to Y$ has a homotopy fixed point.
*Proof.* Put $h=v\circ u\circ\mathrm{diag}_A$ and choose $a$ representing $h$. Evaluation at $a$ gives $y=u(a,a)\simeq v(u(a,a))=v(y)$. $\square$
This is Lawvere's diagonal pattern [2]. Lemma 2.2 supplies effective self-reference. A universal partial evaluator is not a total evaluator of all Boolean functions.
4. A realizability interpretation
An assembly is a set $X$ with nonempty realizer sets $E_X(x)\subseteq\mathbb N$. A morphism $f:X\to Y$ is tracked by a partial recursive $t$ with $t(e)\downarrow\in E_Y(f(x))$ whenever $e\in E_X(x)$. Assemblies embed fully faithfully in the elementary effective topos $\mathrm{Eff}$ [3], which we distinguish from Grothendieck infinity topoi.
Define the behavior assembly $$ \mathsf{Beh}=(\mathcal R,E),\qquad E(f)=\{e:\varphi_e=f\}, $$ and the Boolean assembly with realizer sets $E(0)=\{0\}$, $E(1)=\{1\}$.
Theorem 4.1 (realizability Rice theorem). Every morphism $\mathsf{Beh}\to\mathbf2$ in $\mathrm{Eff}$ is constant. Equivalently, $\mathsf{Beh}$ has no nontrivial decidable subobject.
*Proof.* Fullness yields an assembly tracker $t$ for the underlying function. Every natural number is an index for a partial computable function, so $t$ is defined on every natural number and returns the required Boolean value. If the function were nonconstant, $t$ would decide a nontrivial extensional index set, contradicting Theorem 2.3. Conversely, each constant function has a constant tracker. Decidable subobjects are classified by maps to $1\amalg1$, giving the final claim. $\square$
5. An explicit rational ReLU recurrent model
Definition 5.1 (register programs). A program has finitely many labels and registers $c_0,\ldots,c_{m-1}\in\mathbb N$. Its instructions are:
- $\mathrm{INC}(j,k)$: increase $c_j$ by one and go to $k$;
- $\mathrm{DEC}(j,k_0,k_+)$: if $c_j=0$ go to $k_0$; otherwise decrease it by one and go to $k_+$;
- $\mathrm{HALT}$: return $c_0$ and remain in the same configuration.
Input $x$ initializes $(c_0,c_1,\ldots)=(x,0,\ldots)$. These programs compute exactly the partial recursive functions [5]. Two base-$b$ encoded stacks represent a tape; multiplication, addition, quotient and remainder are implemented by increment/decrement loops with scratch registers. The reverse simulation is direct. A universal interpreter and specialization give an acceptable numbering, hence an effective translation from Section 2 codes.
Definition 5.2 (neural recurrent circuit). A cell is a finite acyclic circuit of rational affine and $\sigma(t)=\max(0,t)$ gates, with an affine output layer, mapping $\mathbb Q^d\to\mathbb Q^d$. Repetition gives $z_{t+1}=F(z_t)$. We use finite-depth recurrent cells, without claiming a single-layer update $\sigma(Az+b)$.
Encode a configuration with label $\ell$ as $$ \iota(\ell,c)=(p_0,\ldots,p_{L-1},r_0,\ldots,r_{m-1}), \quad p_k=\begin{cases}1&k=\ell,\\0&k\ne\ell,\end{cases} \quad r_j=2^{-c_j}. $$ Call these states well formed. They lie in $[0,1]^{L+m}$, and the program counter is one-hot. Define $$ Z(r)=\sigma(2r-1),\qquad G(b,r)=\sigma(r+b-1). $$ For encoded counters, $Z(r_j)$ is exactly the indicator of $c_j=0$. For $b\in\{0,1\}$ and $0\leq r\leq1$, $G(b,r)=br$; the circuit uses this ReLU expression, not multiplication of two state variables.
For a decrement instruction at $\ell$ acting on $j$, put $$ a_{\ell0}=\sigma(p_\ell+Z(r_j)-1),\qquad a_{\ell+}=\sigma(p_\ell-Z(r_j)). $$ The first branch is active precisely at an active zero test, the second at an active positive test. Route $p_\ell$ to $k$ for an increment, $a_{\ell0}$ to $k_0$ and $a_{\ell+}$ to $k_+$ for a decrement, and $p_\ell$ back to $\ell$ for a halt. Each new control coordinate is the sum of its incoming activations. Update each counter by $$ r'_j=r_j -\frac12\sum_{\ell:\mathrm{INC}(j,-)}G(p_\ell,r_j) +\sum_{\ell:\mathrm{DEC}(j,-,-)}G(a_{\ell+},r_j). $$ All sums are finite and determined by the program. These are rational affine and ReLU operations only.
Theorem 5.3 (effective exact simulation). There is a total computable compiler $M\mapsto F_M$ satisfying $$ F_M(\iota(C))=\iota(\mathrm{step}_M(C)) $$ for every register configuration $C$. Consequently the well-formed states are forward invariant, and iteration simulates every finite number of register steps exactly.
*Proof.* If $c_j=0$, $r_j=1$ and $Z(r_j)=1$; otherwise $r_j\leq1/2$ and $Z(r_j)=0$. Hence the branch activations are Boolean. Exactly one instruction and one successor branch are active. The control-coordinate sums therefore give the next one-hot label. An active increment changes $r_j$ to $r_j-r_j/2=2^{-(c_j+1)}$. An active positive decrement changes it to $2r_j=2^{-(c_j-1)}$. In that case $c_j\geq1$, so the result is at most one. An inactive instruction or a zero branch adds no counter change. Halt leaves all coordinates fixed. These are exactly the register rules. Induction proves the iteration statement. The finite instruction list directly determines a finite DAG with rational coefficients, proving computability of compilation. $\square$
The invariant concerns the encoded set. Counter magnitudes approach zero: bounded magnitude still requires unbounded precision. Input encoding is computable without an efficiency claim.
Read a compiled circuit by checking its designated halt labels and, at halt, decoding $r_0=2^{-y}$ to return $y$. Exact rational decoding is effective: in lowest terms the numerator is one and the denominator is a power of two. A rational-cell execution is an ordinary partial computable procedure. Let $\nu_N:\mathbb N\rightharpoonup\mathbb N$ denote this partial neural behavior.
6. Neural Rice theorems and concrete specifications
Theorem 6.1 (compiler transfer). Suppose neural codes admit a total computable compiler $C$ with $\nu_{C(e)}=\varphi_e$. For every nonempty proper $P\subset\mathcal R$, no algorithm that halts on every compiled code can correctly decide whether $\nu_{C(e)}\in P$.
*Proof.* Composing the alleged decision with $C$ gives the total decision forbidden by Theorem 2.3. $\square$
The register translation and Theorem 5.3 provide this compiler. The compiler image need not be decidable: this is already an impossibility under that promise.
Corollary 6.2. The following properties of compiled neural codes are undecidable: $$ \begin{gathered} \nu_N(0)\downarrow;\qquad \forall x\;\nu_N(x)\downarrow;\qquad \\ \nu_N=(x\mapsto0);\qquad \forall x\;(\nu_N(x)\downarrow\Rightarrow\nu_N(x)\ne1). \end{gathered} $$ *Proof.* Each is extensional and nontrivial, as witnessed by the nowhere-defined, constant-zero and constant-one functions. Apply Theorem 6.1. $\square$
Termination at input zero is semidecidable. Undecidability does not preclude semidecision.
Corollary 6.3 (behavioral equivalence). There is no total algorithm deciding $\nu_N=\nu_{N'}$. If neural semantics has an extensional presentation $d$ into a space or topos as in Section 3, every nontrivial Boolean observation remains undecidable on neural codes. If, additionally, $d(N)\simeq d(N')$ holds *only if* $\nu_N=\nu_{N'}$, deciding that path-existence relation is impossible.
*Proof.* An equivalence decision against a fixed constant-zero circuit would decide the third row of Corollary 6.2. The semantic observation claim is Theorem 3.2 or 3.5 after composition with $C$. Under the additional faithfulness condition, path existence is exactly behavioral equality. $\square$
Proposition 6.4 (unbounded recurrent safety). For rational ReLU cells, deciding from a rational initial state whether a designated rational half-space is ever reached is undecidable, even when the simulated trajectory remains in the unit cube.
*Proof.* Specialize an arbitrary program and input to a register program run from zero. Compile it, and let $H$ be the half-space $\sum_{h\text{ halt}}p_h\geq1/2$. On well-formed trajectories its left side is zero or one. The trajectory reaches $H$ exactly when the program halts. The initial state and half-space are rational and effective. A reachability decision would decide halting. $\square$
7. Decidable boundaries
Proposition 7.1 (bounded rational ReLU verification). Given a finite rational ReLU cell, a fixed finite horizon $T$, a rational polyhedral initial-state set, and a finite Boolean combination of rational linear state constraints, existence of a violating trajectory of length at most $T$ is decidable. The same applies to a finite feedforward rational ReLU network.
*Proof.* Unroll the cell $T$ times. For each ReLU relation $y=\max(0,z)$, choose one of the linear cases $$ (z\geq0\ \wedge\ y=z)\quad\text{or}\quad(z\leq0\ \wedge\ y=0). $$ There are finitely many choices. Add the initial and violation constraints and decide the resulting finite systems of rational linear equalities and strict or weak inequalities. Boolean combinations can be put into finite disjunctive form. Linear real arithmetic is decidable, so finite enumeration decides existence. Universal safety is the complement of this existential problem. A finite feedforward graph is already a finite unrolling. $\square$
The finite procedure need not be efficient; see Reluplex [8]. Equality of finite rational ReLU feedforward maps on a rational polyhedral domain is likewise decidable by searching for an unequal output coordinate.
Proposition 7.2 (closed finite-state recurrence). A deterministic closed transition system on a known finite state space $S$ has decidable reachability and eventual halting from a specified initial state.
*Proof.* Simulate until the target is reached or a state repeats. At most $|S|$ distinct states are visited before repetition. Determinism makes all future states repeat the previously observed cycle, so a missing target will never appear. $\square$
Fixed-width arithmetic with bounded storage can give finite closed state. Unbounded memory, input streams and arbitrary precision invalidate that assumption. Noncomputable real parameters fall outside the effective model.
8. Proof certificates and useful verification
Theorem 8.1 (no complete bilateral effective certification). Let $P$ be a nontrivial extensional property of the compiled neural behaviors. There cannot exist two computably enumerable certificate relations $V_+(N,c)$ and $V_-(N,c)$ that are sound for $P$ and its complement, respectively, and such that every compiled $N$ has a certificate on one side.
*Proof.* On a compiled input, dovetail the two certificate enumerations, searching all candidate certificates. Completeness eventually finds one; soundness determines the correct bit and prevents contradictory successful certificates. This is a total correct decision on the compiler image, contrary to Theorem 6.1. $\square$
9. Artifacts and authorship
The full manuscript and source bundle contain the rational ReLU compiler and an independent integer interpreter. Seven tests pass, including 2,700 boundary states, 4,800 multistep transitions and 121 addition runs. Finite tests corroborate implementation; the proofs establish universal claims. No machine-checked proof is claimed.
Responsible human author's established public byline: Anonymous. OpenAI Codex assisted with research, formulation, drafting, implementation and document preparation. The author authorized submission. No independent review or acceptance is asserted.
References
1. H. G. Rice. Classes of recursively enumerable sets and their decision problems. *Trans. AMS* 74, 358--366 (1953). https://doi.org/10.1090/S0002-9947-1953-0053041-6
2. F. W. Lawvere. Diagonal arguments and cartesian closed categories (1969); reprint with commentary, *Reprints TAC* 15, 1--13 (2006). https://www.tac.mta.ca/tac/reprints/articles/15/tr15abs.html
3. J. M. E. Hyland. The Effective Topos. *Brouwer Centenary Symposium*, 165--216 (1982). https://doi.org/10.1016/S0049-237X(09)70129-6
4. J. Lurie. *Higher Topos Theory*, Section 5.5.6 (2009). https://arxiv.org/abs/math/0608040
5. M. L. Minsky. Recursive Unsolvability of Post's Problem of Tag and other Topics in Theory of Turing Machines. *Annals of Mathematics* 74, 437--455 (1961). https://doi.org/10.2307/1970290
6. H. T. Siegelmann and E. D. Sontag. On the Computational Power of Neural Nets. *JCSS* 50, 132--150 (1995). https://binds.cs.umass.edu/papers/1995_Siegelmann_JComSysSci.pdf
7. Yining Chen, Sorcha Gilroy, Andreas Maletti, Jonathan May and Kevin Knight. Recurrent Neural Networks as Weighted Language Recognizers. *NAACL-HLT*, 2261--2271 (2018). https://aclanthology.org/N18-1205/
8. Guy Katz, Clark Barrett, David L. Dill, Kyle Julian and Mykel J. Kochenderfer. Reluplex: An Efficient SMT Solver for Verifying Deep Neural Networks (2017). https://arxiv.org/abs/1702.01135