The Executability Gate: Anchor-Failure Detection (V₂)

The Executability Gate: Anchor-Failure Detection (V₂)

Extending the Consistency Gate

The Consistency Gate (Passarelli 2026) specifies a validator V₁ that catches substrate-cancellation: premise sets containing {φ, ¬φ} are identified, returned as diagnostic objects, and removed before the inference engine fires. This covers one species of non-executable input.

The second species — anchor-failure — is not yet formally specified. Anchor-failure occurs when an expression provides no verdict-stabilizing target: the evaluation it requests depends recursively on the output of that same evaluation, with no independent ground. The liar paradox, Turing’s D(D), and Gödel’s G are instances.

This section specifies V₂: a validator that catches anchor-failure by checking whether the evaluative dependencies of an input are well-founded.

The Problem V₂ Solves

V₁ catches bad premises — content that is already in the premise set before the engine runs. The classical objection to extending the gate to Turing and Gödel is: “nothing non-executable was fed in as a premise; the metatheory constructed a perfectly lawful object using ordinary formal resources — coding, substitution, self-application, representability — and then proved something about it.”

This objection correctly identifies that the non-executable expression is not sitting in the premise set. It is generated during the derivation. The derivation uses legitimate operations (coding, substitution, diagonalization) to construct an object whose evaluative dependencies are circular. V₂ does not ban those operations. It checks the dependency structure of the object they produce before that object is submitted as input to further evaluation.

V₂ is not a content filter. It does not reject strings. It does not ban self-reference. It checks whether a specification, when submitted as input to the proof-theoretic engine for derivation of consequences, requests an evaluation that terminates.

Definitions

Evaluative request. A triple R = ⟨e, v, S⟩ where e is a well-formed expression, v is a verdict type (truth, provability, halting, oracle-verdict, membership), and S is the evaluative context (a formal system, a semantic regime, a computational framework — whatever provides the rules under which the verdict is sought).

Evaluative dependency. An evaluative request R₁ = ⟨e₁, v₁, S₁⟩ has an evaluative dependency on request R₂ = ⟨e₂, v₂, S₂⟩ if R₁ is constructed such that its verdict is defined as a function of R₂’s verdict. This is a structural claim about the construction of R₁: the definition of e₁ specifies that the v₁-verdict on e₁ in S₁ is a function of the v₂-verdict on e₂ in S₂. The dependency is in the specification, not in the process of checking it. Notation: R₁ → R₂.

The criterion is constructional, not operational. It does not depend on whether an evaluator happens to consult R₂ during its work on R₁. It depends on whether R₁’s definition routes through R₂’s verdict. This is inspectable from the construction of R₁ without running the engine.

Dependency formation rules. The dependency function D: R → P(R) is generated by the following rules. These are not exhaustive but cover the cases relevant to this paper:

Rule 1 (Negation). D(⟨¬φ, truth, S⟩) includes ⟨φ, truth, S⟩. The truth of a negation is defined as a function of the truth of the negated sentence.

Rule 2 (Provability predicate). D(⟨Prov(⌜φ⌝), truth, S⟩) includes ⟨φ, provability, S⟩. The truth of a provability claim about φ is defined as a function of the provability of φ. This is the cross-verdict-type rule: it generates an edge from a truth request to a provability request.

Rule 3 (Definitional expansion). If e is introduced by definition as φ — that is, e is constructed such that its content is stipulated to be φ — then D(⟨e, v, S⟩) includes ⟨φ, v/, S⟩, where v/ is the verdict type appropriate to the content of φ. When v = provability and φ is a sentence with propositional content, v* = truth: the provability of a defined sentence depends on the truth-evaluative structure of its defining content. This is because proving e in S requires determining whether the content of e — which is φ — holds, and “holds” is a truth-type verdict on φ.

This rule explicitly licenses verdict-type crossing. The provability of G depends on the truth of ¬Prov(⌜G⌝), not on the provability of ¬Prov(⌜G⌝). The rule generates the edge D(⟨G, provability, S⟩) includes ⟨¬Prov(⌜G⌝), truth, S⟩. From there, Rules 1 and 2 generate the remaining edges that close the cycle back to ⟨G, provability, S⟩.

Rule 4 (Oracle-behavior bridge). When a program P is constructed to define its behavior on input x as a function of an oracle H’s verdict on x:

1. D(⟨P(x), halting, F⟩) includes ⟨H(x), oracle-verdict, F⟩. The program’s halting behavior is defined through the oracle’s verdict on the input. “Oracle-verdict” is a distinct verdict type from “halting”: it is the verdict H produces, which P then acts on.

2. D(⟨H(x), oracle-verdict, F⟩) includes ⟨x, halting, F⟩. The oracle’s verdict on x is defined as a function of x’s halting behavior — that is what the oracle is supposed to determine.

3. When x = P, (b) becomes: D(⟨H(P), oracle-verdict, F⟩) includes ⟨P(P), halting, F⟩. The oracle’s verdict on P requires determining P’s halting behavior, which by (a) requires the oracle’s verdict on P. The cycle closes.

This formulation keeps the oracle’s verdict and the program’s behavior as distinct request types rather than compressing both into the halting triple. The cycle in D(D) is: ⟨D(D), halting, F⟩ → ⟨H(D), oracle-verdict, F⟩ → ⟨D(D), halting, F⟩. Two distinct requests, two edges, one cycle.

Rule 5 (Self-predication). D(⟨φ, v, S⟩) includes ⟨φ, v, S⟩ when φ is constructed such that its v-verdict in S is defined as a direct function of its own v-verdict in S. This rule catches the liar: L’s truth is defined as a function of L’s truth.

Rule 6 (Provability decomposition). D(⟨φ, provability, S⟩) includes ⟨φ, truth, S⟩ when φ is a sentence whose content does not reference the provability apparatus of S. That is: the provability of φ in S depends on whether φ’s content holds under S’s interpretation. This rule generates downward edges from provability requests to the truth-evaluative structure of the sentence, which in turn grounds out in the axioms and definitions of S via the other rules.

When φ’s content DOES reference S’s provability apparatus — as G does — Rule 3 (definitional expansion) generates the relevant edges instead, and those edges may cycle. Rule 6 applies to sentences whose content is arithmetically or structurally grounded. Rule 3 applies to sentences whose content is defined in terms of the provability predicate. The two rules are not in competition; they apply to different constructions.

Rule 7 (Grounding). D(⟨a, membership, S⟩) = ∅ when a is an axiom of S. Axiom membership is fixed by the definition of S and does not depend on any further verdict. Axioms are terminal nodes in the dependency graph.

Cycle-fatality principle. A reachable ungrounded cycle is fatal even if other grounded paths from the same request also exist. V₂ does not ask “is there some path that grounds out?” It asks “is there any path that cycles without ground?” If yes, the request fails. The existence of a grounded path does not rescue a request that also has a cyclic path. This matters because in principle every provability request in a sufficiently expressive system has edges into the system’s derivational structure (grounded paths). Gödel’s G has those paths too. What makes G fail is that it also has a cyclic path — generated by Rules 3, 1, and 2 — that no grounded path cancels. The criterion is: all paths must ground out, not merely some.

Dependency path. A sequence R₁ → R₂ → … → Rₙ where each request is constructed such that its verdict is defined as a function of the next request’s verdict.

Grounded target. A request g is grounded if D(g) = ∅ or if every path from g terminates in a request with D = ∅. Grounded requests have verdicts that are defined independently of any request in the path leading to them.

Dependency cycle. A dependency path R₁ → R₂ → … → Rₙ → R₁ where the construction returns to a request already in the path. No request in the cycle is grounded, because every request’s verdict is defined as a function of a request whose verdict is defined as a function of … itself.

Well-founded request. An evaluative request is well-founded if every dependency path from it reaches a grounded target in finitely many steps.

Anchor-failure. An evaluative request exhibits anchor-failure if it contains a dependency cycle: at least one dependency path returns to a request already in the path, and no exit from the cycle reaches a grounded target.

Formal Specification

V₂ does not range over bare expressions. An expression in isolation is content. It becomes an evaluative request when it is submitted to an engine for a specific verdict: truth, provability, halting, oracle-verdict, membership. The same expression can generate different dependency structures under different verdict types. V₂ ranges over evaluative requests as defined above.

Let R be the set of evaluative requests generable from the evaluative context’s resources. Let D: R → P(R) be the dependency function generated by the formation rules. D maps each evaluative request to the set of evaluative requests whose verdicts it is constructed to depend on.

V₂: R → {pass, fail(C)}

where C is a witness cycle: a sequence ⟨r₁, r₂, …, rₙ⟩ such that r₁ ∈ D(rₙ) and for each i, rᵢ₊₁ ∈ D(rᵢ).

V₂(R) = pass if every path through the dependency graph from R reaches a grounded target in finitely many steps.

V₂(R) = fail(C) if there exists a dependency cycle C reachable from R with no exit to a grounded target.

When V₂(R) = fail(C), the system returns a diagnostic object identifying the cycle C. The expression e is not destroyed. It remains as content in the system. What is blocked is the evaluative request R — the submission of e for verdict v in system S — because the evaluation R requests does not terminate.

The Full Gate

The executability gate is the conjunction of V₁ and V₂.

For premise sets: V₁ checks joint consistency. Contradictory pairs are caught, diagnosed, and removed.

For evaluative requests submitted to the engine: V₂ checks well-foundedness of evaluative dependencies. Dependency cycles are caught, diagnosed, and the request is held — the expression remains as content but the evaluative request is not processed.

The gate sits between syntactic evaluation (Layer 1) and proof-theoretic evaluation (Layer 2). Layer 1 checks that each expression is well-formed. The gate (Layer 1.5) checks that the well-formed expressions, individually (V₂: each evaluative request has well-founded dependencies) and jointly (V₁: no contradictory pairs), request evaluations that terminate. Layer 2 runs the full classical engine on everything that passes.

Application: The Liar

“This statement is false.”

Let L = “L is false.”

The evaluative request is R = ⟨L, truth, T⟩ where T is any semantic regime that admits an unrestricted truth predicate applicable to sentences of its own language.

L is constructed such that its truth value is defined as a function of its own truth value. By Rule 5 (self-predication): D(R) includes R. The path is a cycle of length 1. There is no exit to a grounded target. L’s truth verdict is defined in terms of L’s truth verdict. No external anchor stabilizes the evaluation.

V₂(R) = fail(⟨R⟩).

Diagnostic: dependency cycle of length 1, no grounded exit. Generated by Rule 5.

The string L remains as content. The evaluative request — determine L’s truth value in T — is not submitted to the engine.

Application: Turing’s D(D)

Turing’s proof constructs, within a computational framework F:

• H: a hypothetical total computable function within F that takes a program description and returns halt/non-halt.
• D: a program that, given input p, queries H(p) and does the opposite. If H(p) = halt, D loops. If H(p) = non-halt, D halts.
• The critical input: D(D). D applied to its own description.

The evaluative request is R = ⟨D(D), halting, F⟩.

Evaluative dependency analysis of R:

D is constructed such that its behavior on input p is defined as a function of H’s halting verdict on p. Specifically: D inverts H’s output. This is in D’s definition — not discovered during evaluation, but specified at construction.

When D is applied to itself, the dependency structure is generated by Rule 4 (oracle-behavior bridge): by Rule 4(a), D(⟨D(D), halting, F⟩) includes ⟨H(D), oracle-verdict, F⟩. By Rule 4(b), D(⟨H(D), oracle-verdict, F⟩) includes ⟨D(D), halting, F⟩. By Rule 4(c), since x = D = P, the cycle closes.

Let R = ⟨D(D), halting, F⟩ and R₁ = ⟨H(D), oracle-verdict, F⟩.

Dependency path generated by Rules 4(a) and 4(b): R → R₁ → R.

The path cycles: R → R₁ → R. Two distinct request types — halting and oracle-verdict — two edges, one cycle. D is defined to consult H. H’s oracle-verdict on D is defined by D’s halting behavior. D’s halting behavior is defined by H’s oracle-verdict. No request in the cycle is grounded. There is no independent target — no fact external to the cycle — that the verdict is defined in terms of.

V₂(R) = fail(⟨R, R₁⟩).

Diagnostic: dependency cycle of length 2 between the program’s halting request and the oracle’s verdict request, no grounded exit. Generated by Rules 4(a) and 4(b).

Note what V₂ does not do: it does not ban self-reference. It does not ban the construction of D. It does not ban self-application in general. The cycle arises specifically when D is applied to itself AND the resulting dependency structure is circular with no grounded exit. The critical factor is not self-application alone but the combination of self-application with a definition that routes through the very verdict being sought. An adversarial input x ≠ D could also fail V₂ if x is constructed such that H’s verdict on x depends on x’s behavior which depends on H’s verdict — the gate catches the dependency structure, not the identity of the input. What V₂ checks is the shape of the dependency graph, regardless of how it was generated.

Application: Gödel’s G

Gödel’s proof constructs, within a formal system S of sufficient expressive power:

• A coding scheme that assigns natural numbers to formulas and proofs.
• A predicate Prov(x) that holds when x is the code of a formula provable in S.
• The Gödel sentence G, which is equivalent to ¬Prov(⌜G⌝): “the formula with my code number is not provable in S.”

The evaluative request is R = ⟨G, provability, S⟩.

Evaluative dependency analysis of R:

G is constructed such that its content is ¬Prov(⌜G⌝). This is not discovered during proof search. It is specified at construction: G is defined as the sentence that asserts its own unprovability in S. The dependency is in the definition.

The provability of G in S depends on G’s content. By Rule 3 (definitional expansion): G is defined as ¬Prov(⌜G⌝), so D(⟨G, provability, S⟩) includes ⟨¬Prov(⌜G⌝), truth, S⟩. The verdict-type crossing from provability to truth is explicit in Rule 3: proving G in S requires determining whether the content of G — which is ¬Prov(⌜G⌝) — holds. By Rule 1 (negation): the truth of ¬Prov(⌜G⌝) is defined as a function of the truth of Prov(⌜G⌝). By Rule 2 (provability predicate): the truth of Prov(⌜G⌝) is defined as a function of the provability of G. The provability of G is R.

Let R₁ = ⟨¬Prov(⌜G⌝), truth, S⟩ and R₂ = ⟨Prov(⌜G⌝), truth, S⟩.

Dependency path generated by Rules 3, 1, and 2: R → R₁ → R₂ → R.

The cycle drops out mechanically from the formation rules. R depends on R₁ by Rule 3 (definitional expansion, with verdict-type crossing from provability to truth). R₁ depends on R₂ by Rule 1 (negation). R₂ depends on R by Rule 2 (provability predicate, crossing from truth back to provability). Every edge is rule-generated. Every verdict-type crossing is explicit. The cycle is constructional: G is built to reference its own provability status in S. There is no independent target — no fact external to the cycle — that G’s provability verdict is defined in terms of.

Note: G also has grounded paths. As a sentence of arithmetic, its provability request generates edges into S’s derivational structure via Rule 6, which terminate in axioms via Rule 7. But by the cycle-fatality principle, a reachable ungrounded cycle is fatal even when grounded paths also exist. All paths must ground out, not merely some.

A classical reader might object: “the system does not need a prior verdict on G to search for a proof of G; it just manipulates formulas mechanically.” But V₂ does not check what the engine does during proof search. It checks the dependency structure of the evaluative request as constructed. G’s definition routes its own provability verdict through itself via Rules 3, 1, and 2. That structure is inspectable before the engine runs. It is not a property of evaluation. It is a property of construction.

V₂(R) = fail(⟨R, R₁, R₂⟩).

Diagnostic: dependency cycle of length 3 between the sentence’s provability, the truth of its negated provability predicate, and the truth of its provability predicate, no grounded exit. Generated by Rules 3, 1, and 2.

Again: V₂ does not ban coding, does not ban the Prov predicate, does not ban self-reference in arithmetic. The representability of syntax within arithmetic is a legitimate formal resource. What V₂ catches is the specific evaluative request that results when these resources are combined to produce an expression whose provability verdict cycles without ground. G as a string in the language of arithmetic is content. R = ⟨G, provability, S⟩ — the request to derive whether this sentence, whose provability is defined as a function of its own provability, is provable — is a non-terminating evaluative request.

Application: Non-Self-Referential Arithmetic (the “passes” case)

“Is the Goldbach conjecture provable in Peano Arithmetic?”

The Goldbach conjecture states: every even integer greater than 2 is the sum of two primes. Call it GB.

The evaluative request is R = ⟨GB, provability, PA⟩.

Evaluative dependency analysis of R:

GB is constructed such that its content asserts a universal property of even integers. By Rule 6 (provability decomposition): the provability of GB in PA decomposes into the chain of derivational dependencies that would have to hold — routing through definitions of “even integer,” “prime,” and “sum,” through PA’s inference rules, and terminating in PA’s axioms. None of these intermediate dependencies reference GB’s own provability status. GB does not reference itself. It references arithmetic structure.

Dependency path generated by Rules 6 and 7: R → ⟨intermediate lemmas, provability, PA⟩ → … → ⟨PA’s axioms, membership, PA⟩ → grounded (Rule 7).

PA’s axioms are grounded targets by Rule 7: their membership in PA is fixed by the definition of PA, independently of any particular derivation attempt. No cycle. Every dependency path from R reaches ground.

V₂(R) = pass.

The engine runs. Whether GB is provable in PA is an open question, but it is a well-founded question. The dependency graph terminates in grounded targets. The engine may or may not resolve it — that is a question of the engine’s power, not the input’s structure. Groundedness is not decidability. V₂ does not promise the engine will produce an answer. It promises the input is the kind of thing an answer could in principle be produced for.

The contrast with G is now level-clean. Both R = ⟨G, provability, S⟩ and R = ⟨GB, provability, PA⟩ are provability requests in formal systems. G’s provability verdict cycles through itself. GB’s provability verdict terminates in PA’s axioms. Same verdict type, same kind of system, different dependency structures. That is what V₂ discriminates.

This is the diagnostic working as intended: V₂ does not dissolve open problems. It dissolves circular specifications. Hard questions with grounded targets pass the gate and enter the engine. The engine may or may not resolve them. That is the engine’s business. The gate’s business is ensuring the input is executable.

What V₂ Does Not Do

V₂ does not ban self-reference. Programs that examine their own source code, formal systems that represent their own syntax, recursive functions that call themselves — all of these can pass V₂ provided the dependency paths ground out. A recursive function with a base case is self-referential and well-founded. A quine (a program that outputs its own source code) is self-referential and well-founded — its output depends on its structure, not on an evaluative verdict about itself.

V₂ does not ban diagonalization as a technique. Cantor’s diagonal argument, for example, is well-founded: the constructed real number’s digits depend on the list entries, which are grounded targets. The dependency path does not cycle.

V₂ does not limit the expressive power of formal systems. Every well-formed expression remains expressible. Every coding scheme remains available. Every substitution and self-application operation remains legal. What V₂ constrains is not what can be expressed but what evaluative requests can be submitted to the engine. The constraint is: the evaluative dependencies of the request must bottom out.

V₂ does not resolve open problems. It has nothing to say about P vs. NP, the Riemann hypothesis, or the Goldbach conjecture. These are well-founded evaluative requests that pass the gate. Their difficulty is in the engine, not the request.

The Executability Criterion, Unified

The full executability gate enforces one condition with two manifestations:

V₁ (substrate-cancellation): Does the input jointly cancel a condition constitutive of discrimination’s applicability? Test: check premise sets for contradictory pairs {φ, ¬φ}. If found, the input requests an evaluation in which something both holds and doesn’t hold. The evaluation cannot produce a verdict because the substrate on which discrimination operates has been cancelled.

V₂ (anchor-failure): Does the input request an evaluation whose dependencies are circular? Test: check whether every dependency path from the input reaches a grounded target. If not — if the path cycles back to the input or to an expression in the path — the evaluation cannot produce a verdict because there is no independent target to stabilize it.

Both are instances of one principle: an evaluation that cannot terminate cannot be submitted as an executable request. The gate does not assess truth, provability, or meaning. It assesses whether the evaluative request has the structural property of being completable. Non-completable requests are held as content and returned as diagnostics. Completable requests enter the engine at full classical power.

Decidability of V₂

The same engineering caveat from the Consistency Gate paper applies. Detecting arbitrary dependency cycles in the general case is undecidable — it reduces to the problem of determining program behavior, which is the very issue under discussion.

V₂ is a normative admissibility condition first and an implementation problem second. The specification says: no input with circular evaluative dependencies reaches the engine. This is a constraint on what counts as executable input, the same way syntactic well-formedness is a constraint on what counts as parseable input. Whether the constraint can always be checked in finite time is an engineering question. Whether the constraint is correct is a logical question. These are separate.

The implementation is approximate. For the cases that matter — liar-style constructions, diagonal arguments, Gödel-style self-referential sentences — the dependency structure is syntactically transparent. The cycle in D(D) is visible by inspection: D is defined to query H about its own input and invert the result. The cycle in G is visible by construction: G is constructed to assert its own unprovability. These are not hidden cycles requiring deep analysis to detect. They are the explicit design of the constructions.

For novel or opaque cases, the same incremental, bounded, heuristic approach from V₁ applies. Check what you can check. Improve the checking. Never weaken the engine to compensate for what you can’t check. The gate is a precondition, not an algorithm. Its specification is the constraint. Its implementation is engineering. The computational difficulty of implementation does not collapse the architectural claim.

Compact Summary

V₂ checks whether the evaluative dependencies of a request are well-founded. An evaluative request is a triple ⟨e, v, S⟩: expression, verdict type, evaluative context. Dependency edges are generated by explicit formation rules (negation, provability predicate, definitional expansion, oracle-behavior bridge, self-predication, provability decomposition, grounding). A request is well-founded if every dependency path from it reaches a grounded target — a request whose verdict is defined independently of the evaluation in progress. A request exhibits anchor-failure if it contains a dependency cycle with no grounded exit. A reachable ungrounded cycle is fatal even when other grounded paths from the same request exist: all paths must ground out, not merely some.

The liar, D(D), and Gödel’s G all fail V₂. In each case the cycle drops out mechanically from the formation rules, not from narrative interpretation: Rule 5 generates the liar’s self-loop; Rules 4(a) and 4(b) generate D(D)’s oracle-behavior cycle; Rules 3, 1, and 2 generate G’s provability-truth-provability cycle.

Non-self-referential problems (Goldbach, Riemann, P vs. NP) pass V₂: Rules 6 and 7 decompose their provability requests into grounded derivational chains terminating in axioms. The contrast with Gödel is level-clean: both are provability requests in formal systems; one cycles, the other grounds out.

V₂ does not ban self-reference. It bans circular evaluative dependencies without ground. Self-referential constructions with base cases, grounded recursion, and independent targets pass the gate.

Together, V₁ and V₂ constitute the full executability gate. V₁ catches substrate-cancellation. V₂ catches anchor-failure. Both enforce the same underlying condition: the evaluation a request specifies must be structurally completable. The gate sits between syntactic validation and the inference engine. Everything that passes receives the full classical engine without modification. Everything that fails is held as content and returned as a diagnostic.

Author

Tom Passarelli

License

CC0. This work is in the public domain.