Pith. sign in
module module moderate

IndisputableMonolith.Foundation.PrimitiveRecognitionCalculus.TraceLogic

show as:
view Lean formalization →

Defines the first-pass logic of Primitive Recognition Calculus: a proposition is a predicate on finite traces that remains true under any extension of the trace. Supplies the connectives (top, bottom, and, or, implication, negation) and quantifiers, plus basic introduction lemmas. Downstream FormalSystem and Kernel import this vocabulary. Structure is definitional scaffolding with short intro rules, not a deep derivation.

claimA PRC proposition is a predicate $P$ on finite traces such that whenever $P(\tau)$ holds and $\tau'$ extends $\tau$, one has $P(\tau')$. The module equips this class with $\top$, $\bot$, $\land$, $\lor$, $\to$, $\neg$, $\forall$, and $\exists$, together with the corresponding introduction rules.

background

Primitive Recognition Calculus (PRC) treats recognition events as finite traces. The upstream SameDiff module supplies the same/different comparison primitives on those traces. In this setting a logical claim cannot be a bare Boolean; it must survive further observation, i.e. remain true when the trace is extended.

The module therefore takes as its central object an extension-persistent predicate on finite traces (the doc-comment: "a proposition in the first PRC logic pass is a predicate on finite traces that persists under trace extension"). On that class it defines the standard propositional connectives and the two quantifiers, so later layers can write formulas without re-encoding persistence each time.

Notation follows ordinary logic: top and bottom are the constantly-true and constantly-false persistent predicates; and, or, imp, not are the pointwise connectives closed under persistence; all and exists_ quantify over the ambient domain while preserving the extension property.

proof idea

This is a definition module. TracePredicate packages the persistence side-condition; the connectives and quantifiers are defined so that persistence is inherited from the operands. The short lemmas (top_intro, and_intro, and_left, and siblings) are one-line introduction or projection rules that unfold those definitions. No substantial derivation or forcing argument lives here.

why it matters in Recognition Science

TraceLogic is the logical substrate for the PRC foundation layer. FormalSystem and Kernel both import it, so every later judgment, inference rule, or kernel soundness statement is written in this persistent-trace vocabulary rather than in raw Prop. In the broader Recognition Science stack this sits under Foundation: it does not yet force J-cost, phi, or the eight-tick octave (T5–T7), but it fixes what a "proposition about recognition" means before those quantitative layers attach. Without extension-persistence, formulas could flip under longer observation and the later forcing chain would not have a stable assertion language.

scope and limits

used by (2)

From the project-wide theorem graph. These declarations reference this one in their body.

depends on (1)

Lean names referenced from this declaration's body.

declarations in this module (23)