Computability and logic · existing Mathlib declaration

Rice's Theorem

Suppose a semantic property of partial functions can be decided computably from program codes. If one partial-recursive function has that property, then every partial-recursive function has it.

program code
partial recursive function
semantic property
computable predicate
semantic undecidability

The theorem at a glance

Rice's theorem at a glance

A source-bound editorial overview of the exact Mathlib formulation. The image is explanatory; the statement map, formal type, and pinned source remain authoritative.

An ivory, forest-green, and gold Rice theorem poster sends program codes through evaluation, shows partial-recursive f inside a semantic property, and uses a self-reference loop to force arbitrary partial-recursive g into the same property. — Computable semantic membership and one admitted partial-recursive witness force every partial-recursive function into the property.

Formal orientation

Statement map

This deterministic map orients the reader from the mathematical summary to the pinned declaration and exact checked form. The HTML statement below is authoritative.

Inspected at the original 1536 × 1024 RGB pixels after a correction restored the required f ∈ C hypothesis. The diagram shows computable semantic membership, partial-recursive f with f ∈ C, arbitrary partial-recursive g, a self-referential code, the eval decision, and the one-way conclusion g ∈ C; no iff or empty/universal claim remains. — Once computable semantic membership admits one partial-recursive behavior, the fixed-point route forces every partial-recursive behavior into the same property.

Complementary intuition

A mathematical landmark

Rice's theorem draws a foundational boundary around algorithmic reasoning about programs: a computable decision procedure cannot separate partial-recursive functions by a nontrivial semantic property. Mathlib's selected endpoint proves this through a self-referential code in its partial-evaluation model.

The low-text schematic gives the theorem a visual identity; it does not replace the source-bound poster or exact statement.

Authoritative formal type

Exact Mathlib statement

theorem ComputablePred.rice (C : Set (ℕ →. ℕ)) (h : ComputablePred fun c => Nat.Partrec.Code.eval c ∈ C) {f g} (hf : Nat.Partrec f) (hg : Nat.Partrec g) (fC : f ∈ C) : g ∈ C

Selected evidence declaration text

theorem ComputablePred.rice (C : Set (ℕ →. ℕ)) (h : ComputablePred fun c => Nat.Partrec.Code.eval c ∈ C) {f g} (hf : Nat.Partrec f) (hg : Nat.Partrec g) (fC : f ∈ C) : g ∈ C

ProofAtlas record

What has been checked

Upstream indexedPinned source bytes verified locally

Locally reproducedExact upstream declaration replayed

Reviewed pageCurrent public presentation reviewed

Accepted Atlas resultNot recorded for the preferred artifact

These states distinguish upstream identity, local reproduction, review, and Atlas acceptance. This page is part of the public, read-only Mathlib landmark collection.

Claim boundary

No new theorem is claimed

This target indexes Mathlib's implication form of Rice's theorem. For a semantic property C of partial functions, assume program-code membership through eval is computable. If one partial-recursive f belongs to C, then every partial-recursive g belongs to C. It is specific to Mathlib's partial-function and program-code model and does not classify arbitrary syntactic code properties or all noncomputable semantic properties.

Proof Atlas did not originate Rice's theorem or Mathlib's declaration.
The formal statement is tied to Mathlib's `Nat.Partrec` and `Nat.Partrec.Code` representation, not every machine model simultaneously.
The hypothesis decides a property of evaluated partial functions from their program codes; the theorem does not classify arbitrary syntactic properties of codes.
The conclusion ranges over partial-recursive f and g, not all arbitrary partial functions.
This endpoint is a one-way implication, not the separate rice₂ empty-or-universal equivalence.
The generated explanation and visuals are not proof evidence.

Provenance

Origin and evidence stay separate

Existing declaration: ComputablePred.rice in mathlib
Relationship: The checked artifact is the upstream declaration itself
Preferred checked artifact: artifact.library.mathlib.rice-theorem.v001
Source handling: Verified upstream reference; no mirrored source package