This paper synthesizes a series of formal proofs to construct a unified theory on the logical limits of the Symbol Grounding Problem. We distinguish between internal meaning (sense), which formal systems can possess via axioms, and external grounding (reference), which is a necessary condition for connecting symbols to the world. We demonstrate through a four-stage argument that meaningful grounding within a formal system must arise from a process that is external, dynamic, and non-fixed algorithmic. First, we show that for a purely symbolic system, the impossibility of grounding is a direct consequence of its definition. Second, we extend this limitation to systems with any finite, static set of pre-established meanings (Semantic Axioms). By formally modeling the computationalist hypothesis-which equates grounding with internal derivation-we prove via Gödelian arguments that such systems cannot consistently and completely define a "groundability predicate" for all truths. Third, we demonstrate that the "grounding act" for emergent meanings cannot be inferred from internal rules but requires an axiomatic, meta-level update. Drawing on Turing's concept of Oracle Machines and Piccinini's analysis of the mathematical objection, we identify this update as physical transduction. Finally, we prove that this process cannot be simulated by a fixed judgment algorithm, validating the logical necessity of embodied interaction.

翻译：本文综合一系列形式化证明，构建了一个关于符号接地问题逻辑界限的统一理论。我们区分了形式系统可通过公理具备的内部意义（涵义），以及将符号与世界连接所必需的外部接地（指称）。通过一个四阶段论证，我们证明形式系统内有意义的接地必须源自一个外部、动态且非固定算法的过程。首先，我们表明对于纯符号系统，接地的不可行性是其定义的直接结果。其次，我们将这一限制扩展到任何具有有限、静态预设意义集合（语义公理）的系统。通过形式化建模计算主义假说——该假说将接地等同于内部推导——我们借助哥德尔式论证证明，此类系统无法一致且完备地为所有真命题定义“可接地性谓词”。第三，我们证明新兴意义的“接地行为”无法从内部规则推断，而需要公理化、元层级的更新。借鉴图灵的预言机概念及皮奇尼尼对数学质疑的分析，我们将此更新识别为物理转导。最后，我们证明该过程无法由固定判定算法模拟，从而验证了具身交互的逻辑必然性。