all_elim
plain-language theorem explainer
Universal elimination for stable trace predicates: if a universally quantified family holds at a finite trace, every instance holds there. Anyone wiring the first-pass PRC logic connectives or the trace-logic certificate cites this. The proof is a one-line exact application of the hypothesis at the chosen index.
Claim. Let $P$ be an $\alpha$-indexed family of stable trace predicates and let $T$ be a finite trace. If $\forall a\in\alpha$, $P(a)$ holds at $T$, then for every $a\in\alpha$, $P(a)$ holds at $T$.
background
In the Primitive Recognition Calculus, a finite trace is either empty or built by successive distinction acts (K2.4). A stable trace predicate is a proposition on such traces that persists under extension: once it holds on $T$, it holds on every $U$ that extends $T$.
Universal quantification packages an $\alpha$-indexed family of those predicates into one predicate whose holding means every member holds. Stability of the package is proved componentwise from the members' stability; the index type is verifier bookkeeping, not a new infinitary commitment. This module is the first PRC logic pass over finite traces.
proof idea
One-line wrapper. By definition of the universal connective, holding at $T$ is exactly $\forall a,,P(a)$ holds at $T$. The proof applies that hypothesis at the supplied index $a$.
why it matters
Gives the elimination rule for universal quantification on the PRC trace-logic surface. Downstream it is listed among the pieces assembled into the trace-logic certificate, which packages the propositional surface (truth, conjunction intro, and related rules) as one certificate object. Without elim, the universal connective would be intro-only and unusable when reasoning about verifier-indexed families of stable predicates. This is connective bookkeeping for the first logic pass; it does not yet touch the forcing chain (T0–T8), J-uniqueness, or the phi ladder.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.