δ-decidability — decide up to a tolerance

Parent: relaxing-undecidability

The exact theory of the reals with sin, exp, ODEs is undecidable (you can encode integers and halting). But relax equality by an arbitrary δ>0 and it becomes decidable.

δ-decidability (Gao–Avigad–Clarke, 2012)

For a bounded first-order sentence φ over the reals with computable functions, a δ-decision procedure returns one of:

• "φ is false", or
• "the δ-weakening of φ is true" — i.e. φ with every atom relaxed by δ. These overlap only within δ, so you can never be misled by more than δ — and δ is yours to shrink.

Why it works: the source of undecidability is exact comparisons on a continuum; a δ-ball of slack removes the infinite-precision knife-edge (cf. robustness). Implemented in dReal for nonlinear arithmetic and ODE reachability.

Control use. "Does the trajectory reach the target ε-ball / avoid the unsafe set?" for a hybrid/nonlinear system — undecidable exactly, δ-decidable in practice. This is the direct tool for approximate convergence questions.

Tie: P×C-satisficing in the recursive-harness is exactly a tolerance δ — we don't ask "is it perfect?", we ask "is the residual ≤ δ?", which is checkable.