imp
plain-language theorem explainer
Implication of two stable finite-trace predicates holds at T when every future extension that satisfies the antecedent also satisfies the consequent. Stability of the compound predicate is free from transitivity of trace extension. Used to define negation, to eliminate implications, and as part of the first TraceLogic certificate surface.
Claim. Let $P$ and $Q$ be predicates on finite traces that persist under extension. Define $(P \Rightarrow Q)$ to hold at a trace $T$ precisely when, for every extension $U$ of $T$, if $P$ holds at $U$ then $Q$ holds at $U$. The resulting predicate is itself stable under further extension.
background
In the primitive recognition calculus, a finite trace is built by successive distinction acts (empty, or extend by one act). Extension means the later trace is the earlier one followed by some suffix; that relation is reflexive and transitive.
A TracePredicate is not an arbitrary Prop on traces: it must hold persistently along every extension (the stability field). The module builds a first-pass propositional surface on that class: top, bottom, conjunction, disjunction, and implication, all required to land back in TracePredicate.
Implication is the Kripke-style clause relative to the extension preorder: truth at the present world means the material implication holds at every accessible future world. Because accessibility is transitive, that clause is automatically stable, so implication is a well-typed connective on the stable fragment.
proof idea
The holds field is the universal quantification over extensions: for all $U$ extending $T$, $P(U)$ implies $Q(U)$.
Stability is a short tactic proof. Assume the implication holds at $T$, $U$ extends $T$, and we are given a further extension $V$ of $U$ with $P(V)$. Transitivity of extension (extends_trans) yields that $V$ extends $T$, so the hypothesis at $T$ applies directly and returns $Q(V)$. No separate induction on traces is needed.
why it matters
This is the implication connective of the first PRC logic pass. Downstream, negation is defined as implication into falsehood (not P := imp P bottom), and imp_elim is the corresponding modus-ponens-along-extensions rule.
It also appears among the connectives that the TraceLogicCertificate headline structure packages: a nonempty proposition surface with intro rules for truth and conjunction, of which implication is part of the ambient algebra.
In the broader Recognition stack this is foundation scaffolding, not a forcing-chain step (T5–T8) or a constants claim. It equips later holographic and record arguments with a stable, extension-persistent implication on finite recognition traces.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.