Witnessability of Undecidable Problems
summary
Claim: for a wide class of undecidable problems there is a computable transformation that, given the code of any decidable approximation, outputs a concrete input on which that approximation errs. The paper constructs a computable witness function f_P, proves K (diagonal halting problem) is witnessable, and shows closure under complements and many-one reductions, so Rice-style semantic properties are covered. Requires an admissible programming language; also constructs a non‑witnessable undecidable problem and shows both classes have cardinality 2^{aleph_0}.
AI-written summary · about
chapters (7)
- 0:00Introduction
- 0:48Background Motivation
- 4:25Main Result
- 14:17Implications
- 16:22Results
- 17:47Reflection
- 19:57Questions
related talks
15mClosing Remarks
14mAdequacy for Algebraic Effects Revisited
25mCubical Synthetic Homotopy Theory
15mProducts of Recursive Programs for Hypersafety Verification
21mUndecidability of Higher-Order Unification Formalised in Coq
31mAn Isabelle Formalization of Co-rewrite Pairs for Non-reachability in Term Rewriting
01h 02mThe Truth of a Procedure
21mBlack-box Constructive Proofs are Unavoidable