We identify operational inexpressibility, a structural property of term-rewriting proof systems: for a fixed input and dimension, every derivation ignores the dimension or leaves the target question unconstrained. The canonical instance is direct aggregation on the primitive recursion duplicator $F(x,y,Z)\to x$, $F(x,y,S(n))\to G(y,F(x,y,n))$, whose step argument $y$ is duplicated. A companion paper maps the non-representability frontier; we prove it is operational inexpressibility at the step-argument dimension. Sound responses split into construction methods extending the proof language and confession methods (dependency pairs, counter-projection, size-change termination, argument filtering) projecting away the unincorporable dimension under an external soundness license. Under any direct whole-term measure the recursor's mass profile coincides with that of a true circular reference: only the confession family's licensed projection separates them; non-derivability, TRS isomorphism and information equivalence are proved in Lean. Arts-Giesl soundness is a $Π^0_2$ principle; its subterm-criterion route is a size-change instance formalizable in $\mathrm{RCA}_0$ with an order-$ω$ termination measure. Within the analyzed family the duplicator is the unique structurally complete member requiring confession. The confessed burden grows quadratically against linear residual proof work; a Shannon-style validator recasts the obstruction as a divergent inefficiency coefficient. An architectural necessity theorem makes the duplicator the minimal faithful record-emitter. A layer-crossing schema places the dependency-pair confession in the Feferman-Beklemishev reflection family rather than the Lawvere-Yanofsky diagonal family, matching the six-step shape of Gödel's 1931 move. A witness-language hierarchy with minimal witness order $κ^*$ puts the orientation boundary at $κ^*(x)>0$.


翻译:暂无翻译

0
下载
关闭预览

相关内容

ACL 2025 | 大模型结构化知识提示的泛化能力研究
专知会员服务
29+阅读 · 2025年8月10日
Stabilizing Transformers for Reinforcement Learning
专知会员服务
61+阅读 · 2019年10月17日
Hierarchically Structured Meta-learning
CreateAMind
27+阅读 · 2019年5月22日
深度学习中Attention Mechanism详细介绍:原理、分类及应用
深度学习与NLP
10+阅读 · 2019年2月18日
A Technical Overview of AI & ML in 2018 & Trends for 2019
待字闺中
18+阅读 · 2018年12月24日
disentangled-representation-papers
CreateAMind
26+阅读 · 2018年9月12日
《pyramid Attention Network for Semantic Segmentation》
统计学习与视觉计算组
44+阅读 · 2018年8月30日
论文浅尝 | Improved Neural Relation Detection for KBQA
开放知识图谱
13+阅读 · 2018年1月21日
IJCAI | Cascade Dynamics Modeling with Attention-based RNN
KingsGarden
13+阅读 · 2017年7月16日
国家自然科学基金
0+阅读 · 2015年12月31日
国家自然科学基金
0+阅读 · 2015年12月31日
国家自然科学基金
0+阅读 · 2015年12月31日
国家自然科学基金
1+阅读 · 2015年12月31日
国家自然科学基金
0+阅读 · 2014年12月31日
国家自然科学基金
0+阅读 · 2014年12月31日
国家自然科学基金
0+阅读 · 2014年12月31日
国家自然科学基金
0+阅读 · 2014年12月31日
VIP会员
相关主题
最新内容
受限仓库多智能体取送中的动态安全等待点选择
《国防技术管理》印度智库报告最新45页
专知会员服务
3+阅读 · 8月28日
《美陆军最新条令:保障行动》
专知会员服务
4+阅读 · 8月28日
算法战场:人工智能如何重新定义军事力量
专知会员服务
6+阅读 · 8月28日
《北约联邦式电子战云架构》
专知会员服务
6+阅读 · 8月27日
《美陆军野战手册:空域管理战术》
专知会员服务
10+阅读 · 8月27日
相关VIP内容
ACL 2025 | 大模型结构化知识提示的泛化能力研究
专知会员服务
29+阅读 · 2025年8月10日
Stabilizing Transformers for Reinforcement Learning
专知会员服务
61+阅读 · 2019年10月17日
相关资讯
Hierarchically Structured Meta-learning
CreateAMind
27+阅读 · 2019年5月22日
深度学习中Attention Mechanism详细介绍:原理、分类及应用
深度学习与NLP
10+阅读 · 2019年2月18日
A Technical Overview of AI & ML in 2018 & Trends for 2019
待字闺中
18+阅读 · 2018年12月24日
disentangled-representation-papers
CreateAMind
26+阅读 · 2018年9月12日
《pyramid Attention Network for Semantic Segmentation》
统计学习与视觉计算组
44+阅读 · 2018年8月30日
论文浅尝 | Improved Neural Relation Detection for KBQA
开放知识图谱
13+阅读 · 2018年1月21日
IJCAI | Cascade Dynamics Modeling with Attention-based RNN
KingsGarden
13+阅读 · 2017年7月16日
相关基金
国家自然科学基金
0+阅读 · 2015年12月31日
国家自然科学基金
0+阅读 · 2015年12月31日
国家自然科学基金
0+阅读 · 2015年12月31日
国家自然科学基金
1+阅读 · 2015年12月31日
国家自然科学基金
0+阅读 · 2014年12月31日
国家自然科学基金
0+阅读 · 2014年12月31日
国家自然科学基金
0+阅读 · 2014年12月31日
国家自然科学基金
0+阅读 · 2014年12月31日
Top
微信扫码咨询专知VIP会员