The Impossibility of Internal Semantic Critique in Arithmetical Theories

It is a common philosophical intuition that any critical judgment about a text, when formulated within a logical system, inevitably refers not to the text itself but only to its formal image constructed inside that system. This note provides a precise metamathematical formulation of this idea and proves a rigorous limitation. Working in ZFC as a metatheory, we consider an arbitrary consistent, recursively axiomatizable first‑order theory T containing Robinson's arithmetic Q. A text is identified with a finite string over a fixed finite alphabet. Using a primitive recursive Gödel numbering we associate to each text X a natural number ⌜X⌝. The critic's judgment is represented by a proof in T of some formula Φ (⌜X⌝). Our main theorem shows that no formula of T can correctly reflect a genuinely semantical property of the text—such as being a true arithmetical sentence—when applied to its code. The proof is a direct application of Tarski's undefinability theorem together with basic recursion theory: the set of true arithmetical sentences is not recursively enumerable, whereas for any recursively axiomatizable theory T and any formula Θ (x), the set ψ: T ⊢ Θ (⌜ψ⌝) is always recursively enumerable. We generalize this result to any non‑recursively enumerable property and analyze the minimal arithmetical assumptions required, showing that the theorem holds for any theory interpreting IΔ₀+Ω₁. Connections with reflection principles and the Second Incompleteness Theorem are discussed. Consequently, any formal criticism operating within T can only speak about the code as an arithmetical object; the connection to the original text must be made on the metalevel, outside T. The paper includes a detailed discussion of the philosophical implications for automated text analysis, program verification, and the philosophy of mathematics, as well as open questions about the minimal arithmetic strength required for the theorem to hold.