Foundation Primitive Recognition Calculus Trace Logic All Intro

The universal quantifier

In ordinary logic, the universal quantifier "for all" is a simple device: it asserts that a statement holds for every member of a collection. In a logic built for recognition, the process of recording discrete events, the quantifier must answer an additional question. If a statement is true at one moment, does it remain true when the record grows longer? The framework's answer is that a universal statement "for every x, P(x)" is true at a given trace, a finite record of events, exactly when P(x) is true for every x at that same trace. The declaration all_intro states this rule: to prove the universal statement, it suffices to prove each instance at the current trace.

The deeper content lies in what happens as the trace extends. A predicate in this calculus is not merely a yes-or-no question; it is a stable one. The framework defines a predicate as stable when, if it holds on a trace, it also holds on every extension of that trace. This persistence is built into all_intro through the surrounding definitions. The universal quantifier inherits stability from its instances: if each P(a) is stable, then the combined statement "for all a, P(a)" is stable as well. The rule does not merely state a syntactic equivalence; it preserves the semantic guarantee that recognition never has to be undone.

The framework's machine-checked library of formal theorems records this result. The declaration all_intro is a theorem in that library, proved from the definitions of stability and the universal quantifier. It is one of several introduction and elimination rules, such as all_elim, exists_intro, and imp_elim, that together give the trace logic its constructive character. The library also contains a headline certificate, trace_logic_certificate, which packages the first pass of this trace logic as a single theorem.

What all_intro does not claim is just as important. It does not assert that the universal quantifier is complete, that every true statement is provable. It does not claim that the logic can decide every question, or that the trace logic is the only possible logic of recognition. The rule is a local one: it tells how to introduce a universal statement, not how to handle every logical situation. It is a foundation stone, not a finished building.

theorem all_intro {α : Type} {P : α → TracePredicate} {T : Trace}
    (h : ∀ a : α, (P a).holds T) :
    (all P).holds T := by
  exact h

/-- Universal quantification over a verifier-indexed family of stable trace
predicates. The family parameter is verifier bookkeeping; stability is still a
finite-trace theorem. -/
def all {α : Type} (P : α → TracePredicate) : TracePredicate where
  holds := fun T => ∀ a : α, (P a).holds T
  stable := by
    intro T U hTU h a
    exact (P a).stable hTU (h a)

What this page does not claim

The universal quantifier is complete, meaning every true statement is provable. The trace logic can decide every question or is the only possible logic of recognition. The all_intro rule alone establishes the framework's larger physical consequences.

Verify this page

Every tagged claim above names its theorem. To check one yourself rather than trust this page, elaborate the source module with Lean 4 and audit its axiom basis:

$ lake env lean IndisputableMonolith/Foundation/PrimitiveRecognitionCalculus/TraceLogic.lean
expected axiom basis: [propext, Classical.choice, Quot.sound] (the Lean kernel's standard three; no RS-specific axioms)

A page whose claims cannot be reproduced this way does not ship. In production, every anchor links to the exact declaration in the public source release, and this block carries the build receipt for the page itself.

Derived articles

This page is generated by a question-recursion engine: the questions its answers raise become the next pages. The current agenda, with open targets marked red: