Pith. sign in
module module moderate

IndisputableMonolith.Foundation.PrimitiveRecognitionCalculus.TraceLogic

show as:
view Lean formalization →

Defines the first-pass logic of Primitive Recognition Calculus: propositions are predicates on finite traces that remain true under extension. Connectives (top, bottom, and, or, implication, negation) and quantifiers are built as operations on those predicates, with introduction rules for the stable fragment. Downstream FormalSystem and Kernel import this layer as the logical substrate for PRC.

claimA PRC proposition is a predicate $P$ on finite traces such that if $P(\tau)$ holds and $\tau'$ extends $\tau$, then $P(\tau')$ holds. The module equips this class with $\top$, $\bot$, $\land$, $\lor$, $\to$, $\neg$, $\forall$, and $\exists$, plus introduction lemmas for the persistent fragment.

background

Primitive Recognition Calculus treats recognition events as finite traces. The SameDiff layer (imported here) supplies the underlying sameness and difference structure on those traces. A proposition in the first logic pass is not an arbitrary formula: it is a predicate on traces that is stable under extension, so once a claim holds of a prefix it continues to hold as the trace grows.

That persistence condition is the defining filter. Logical connectives are realized as operations that preserve the class: conjunction and disjunction act pointwise on traces; implication and negation are defined so the result remains extension-stable; universal and existential quantification range over the appropriate parameters while keeping the persistence property.

The module sits in the Foundation domain of the Recognition Science stack, below the formal system and kernel that will treat these predicates as the atomic logical layer of PRC.

proof idea

This is primarily a definition module. TracePredicate packages the extension-persistence condition. The connectives top, bottom, and, or, imp, not, all, and exists_ are defined as operations on such predicates. Short introduction lemmas (top_intro, and_intro, and_left, and siblings) discharge the obvious closure and elimination facts for the stable fragment; there is no deep forcing or uniqueness argument at this layer.

why it matters in Recognition Science

FormalSystem and Kernel both import this module, so every later PRC judgment is built on extension-stable trace predicates rather than on raw classical Prop. That choice keeps the logic aligned with recognition as an accumulating process: claims are about what has already been distinguished along a finite history and cannot be revoked by further extension. In the broader Recognition framework this is scaffolding for the foundation stack that eventually feeds the forcing chain, not a T5–T8 step itself. It closes the gap between SameDiff’s raw sameness structure and a usable internal logic for PRC.

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)