A Calculus of Execution for Binary Relations: Admissibility Without Choice

Le résumé fourni par la source

Abstract Execution of discrete systems inherited its vocabulary from set theory, and with it an abstraction: a set element carries no origin, a relation no history. For mathematics this is a virtue; for execution it is a loss: a binary relation by itself records which pairs belong to it, but in the general non-functional case does not determine which among several available successors is admitted, under what criterion, or against which accumulated history. The consequence is direct: the same value admitted under different conditions is a different event. This paper proposes a specific way past that limitation. This paper develops a calculus in which admission is constitutive. An event enters the record only as a pair of a composite key — the ontology under which it was possible, the criterion under which it was admitted, and its position in the record — and a payload. The record is append-only, and the criterion is evaluated over it before every admission: Execute(Aτ, Cⁿ) = eₙ₊₁ iff τ(Cⁿ, ωτ), with C⁰ = ∅. The three objects this rests on — the record C, the ontology ωτ, and the criterion τ — occupy strictly increasing ranks and are mutually non-derivable, a fact that follows from rank separation together with independent specification. Three results follow under the explicit structural and effectiveness assumptions stated below, none requiring the Axiom of Choice. The sequential dependency of Execute is structurally analogous to dependent choice in that each admission is conditioned on the context produced by prior admissions, but no instance of the Axiom of Dependent Choice is invoked: where continuation is defined, the next admission is determined, for the fixed invocation, by the recorded context and the specified ontology and criterion. Admission requires no choice selector: each ωτ is single-valued where defined and τ is Boolean. Pre-admission addresses additionally provide a definable ordering wherever identification or serialization among independently determined abstractions is required — the instance coordinate is assigned only after admission. Since admission is decided from a finite prefix and, at each finite step, only finitely many active invocation instances contribute candidates, each contributing at most one realization, the admissible executions form a finitely branching tree whose body is closed, compact and Borel — the execution space is measurable, a fact that follows from finite branching, prefix-local admission, and the carrier's explicit encoding (§8), with determinism supplying the definable well-ordering that keeps the argument choice-free rather than supplying measurability on its own. And since convergence requires well-foundedness rather than monotonicity, criteria that consume a bounded resource — budgets, quotas, deadlines — fall inside the theory rather than outside it. The cardinality of that space separates two regimes by branching: countable where T contains no nonempty perfect pruned subtree, and continuum where it does. The countable case splits further by termination: T may be well-founded and terminate, or it may contain one or more infinite branches despite having no perfect subtree. Evolutive change is one possible source of persistent splitting, not a condition equivalent to continuum cardinality. Nondeterminism is therefore not removed but structured — it is the generative capacity of the specification, resolved before commitment and recorded with the coordinates under which it was resolved. Two consequences are of direct engineering interest, established in §7: Corollary 6 establishes that verification replay is deterministic from the recorded execution: the preceding prefix fixes the admission context and the ontology and criterion specifications in force, while the recorded event preserves the realization whose admission is being verified, and Corollary 5 formally identifies the control predicate with the admission predicate within the calculus, so that control and execution collapse into one act rather than two layers, structurally aligned with the Good Regulator principle — which permits evolutive change when a governing abstraction is itself admitted into the record it governs. Five minimal realization conditions are given, substrate-agnostic across architectural families; one independently published implementation is shown to instantiate them, and a further application, from the same research program, illustrates a concrete incompleteness result for external AI safety guardrails in a field currently searching for new formal concepts, following from the same decomposition. The scope is execution of discrete systems: no claim is made about decidability. Keywords: binary relation; execution calculus; admissibility; append-only context; definable selection; dependent choice; eschatological induction; Borel measurability; well-founded convergence; evolutive systems; nondeterminism; rank separation.

Ce résumé expose les affirmations des auteurs. BNTIC ne l’interprète pas comme une validation indépendante des résultats.