From 71a88c495d27f17584c36e98dbd7a66eebfa3469 Mon Sep 17 00:00:00 2001 From: hyperpolymath <6759885+hyperpolymath@users.noreply.github.com> Date: Wed, 20 May 2026 16:59:59 +0100 Subject: [PATCH] fix(coq/cno): drop cno_decidable axiom (Rice's theorem territory) Owner-ruled drop. Universal decidability of is_CNO over arbitrary programs asks for a constructive decision procedure over an unbounded state space (Memory, Registers, IOState all unbounded; is_CNO's universally-quantified clauses range over all states). This is essentially the Rice's theorem situation: deciding a non-trivial semantic property of an arbitrary program is undecidable. Net axiom count in proofs/coq/common/CNO.v: 3 -> 2 with this commit. Refs hyperpolymath/standards#124, scoping doc standards#157 (Stage 3). Co-Authored-By: Claude Opus 4.7 (1M context) --- proofs/coq/common/CNO.v | 16 ++++++++++++++-- 1 file changed, 14 insertions(+), 2 deletions(-) diff --git a/proofs/coq/common/CNO.v b/proofs/coq/common/CNO.v index 193835c..3cd0893 100644 --- a/proofs/coq/common/CNO.v +++ b/proofs/coq/common/CNO.v @@ -572,9 +572,21 @@ Qed. (** ** Decidability *) (** Question: Is CNO verification decidable? *) -(** This is a major research question *) -Axiom cno_decidable : forall p, {is_CNO p} + {~ is_CNO p}. +(** Universal decidability of [is_CNO] over arbitrary programs was + previously asserted as an [Axiom] [cno_decidable]. That axiom has + been dropped (owner ruling, Stage 3 of standards#157): the + universal form asks for a constructive decision procedure over an + unbounded state space ([Memory : nat -> nat], unbounded + registers, unbounded I/O traces), and [is_CNO]'s + universally-quantified clauses range over all of them. This is + essentially the Rice's-theorem situation: deciding a non-trivial + semantic property of an arbitrary program is undecidable, so the + universal-decidability claim is not constructively achievable in + Coq and any client that wants decidability must work in a + restricted syntactic fragment of [Program] (which the current + development does not formalise). No theorem in this file depended + on it. *) (** ** Complexity *)