not
plain-language theorem explainer
Negation of a stable trace predicate is implication into falsehood. Anyone building or citing the first Primitive Recognition Calculus logic layer uses this connective. The body is a one-line abbreviation: apply implication with the constantly-false predicate as consequent.
Claim. For a stable trace predicate $P$, define $\neg P$ by $\neg P := (P \to \bot)$, where $\bot$ is the stable predicate that holds at no finite trace, and implication means: at every future extension of the current trace, if $P$ holds then $\bot$ holds.
background
In the first PRC logic pass, a proposition is a TracePredicate: a predicate on finite traces that is stable under extension (if it holds at $T$ and $U$ extends $T$, it holds at $U$). Truth is the predicate true at every trace; falsehood is the predicate true at none.
Implication is not material implication at a single world. It is persistence along every future extension: $P \to Q$ holds at $T$ when every extension $U$ of $T$ with $P$ at $U$ also has $Q$ at $U$. That construction is itself stable under further extension.
This module packages the usual connectives (conjunction, disjunction, implication, negation, quantifiers) so that every connective returns a stable trace predicate. Negation is the classical reduction of $\neg P$ to $P \to \bot$.
proof idea
One-line definitional wrapper. Negation is literally implication of $P$ into the bottom predicate: imp P bottom. No separate stability proof is needed; stability is inherited from the implication constructor, whose proof already closes under transitive extension.
why it matters
Fills the negation slot in the TraceLogic connective suite alongside top, bottom, and, or, imp, and the quantifiers. Downstream intro/elim lemmas for the other connectives (e.g. and_intro, and_left) sit in the same namespace; negation is the dual building block for classical-style reasoning inside a stability-preserving logic on finite traces.
In the Recognition foundation stack this is scaffolding for a logic of recognition events rather than a physics identity (not a T0–T8 forcing step, RCL identity, or mass-ladder claim). It keeps every derived formula automatically extension-stable, which is the design invariant of the first PRC logic pass. No used-by edges are recorded yet; the declaration is infrastructure for later trace-logic theorems.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.