δ-可判定性——在误差容限内判定

父节点：relaxing-undecidability

包含 sin、exp、常微分方程（ODE）的实数精确理论是不可判定的（你可以在其中编码整数和停机问题）。但只要把相等关系放松为任意的 δ>0，它就变得可判定了。

δ-可判定性（Gao–Avigad–Clarke，2012）

对于实数域上带有可计算函数的有界一阶语句 φ，一个 δ-判定过程会返回以下两者之一：

• "φ 为假"，或
• "φ 的 δ-弱化式为真"——即把 φ 中每个原子公式都放松 δ 之后得到的语句。 这两种情形只在 δ 范围内重叠，所以你被误导的幅度永远不会超过 δ——而 δ 可以由你自己去缩小。

为什么行得通：不可判定性的根源在于连续统上的精确比较；一个 δ-邻域的宽裕消除了无穷精度的刀刃效应（参见 robustness）。这一思路在 dReal 中实现，用于非线性算术和 ODE 可达性判定。

控制理论中的用途。对一个混合/非线性系统问"轨迹是否到达目标 ε-邻域 / 是否避开不安全集？"——精确地讲是不可判定的，但在实践中是δ-可判定的。这正是处理近似收敛问题的直接工具。

联系：recursive-harness 中的 P×C-满足化（satisficing）正是一个容差 δ——我们不问"是否完美？"，而问"残差是否 ≤ δ？"，而后者是可判定的。