Foundation Primitive Recognition Calculus Formal System Prcformal System Embeddi

The embedding theorem

A formal system is a precise language: a set of tokens, a set of expressions built from them, a way to distinguish two tokens, and a way to say one expression extends another. Standard examples include first-order logic, type theory, or a programming language's syntax. The Recognition Science framework defines such a system abstractly, then asks whether its own primitive recognition calculus, the discrete record of events it builds on, can be embedded into it.

The declaration PRCFormalSystem_embedding is a theorem in the machine-checked library of formal theorems. It states that the primitive recognition calculus, taken itself as a formal system, admits an embedding into any formal system that satisfies a single condition: it can distinguish the two endpoints of the primitive distinction. The proof is short and constructive: given such a system, map each endpoint to its corresponding token, map each finite trace to its corresponding expression, and the required preservation properties follow directly from the system's own definitions.

What this establishes is a closure property. The primitive recognition calculus is not an isolated construction; it can be represented inside any formal system expressive enough to tell its two basic tokens apart. The theorem is proved for the calculus itself as the minimal formal system, and the general embedding target, that every expressive formal system admits such an embedding, is also proved. This is a step in a larger build order, a certificate that the formal-system surface is closed.

The theorem does not claim that every external foundation, such as set theory or a specific proof assistant, satisfies this interface. That broader claim is explicitly left as the next layer of inevitability, not hidden in this result. The theorem also does not claim that the primitive recognition calculus is the only formal system, nor that it can express everything. It only establishes that the calculus can be faithfully translated into any system that meets the expressiveness condition.

theorem PRCFormalSystem_embedding :
    Nonempty (PRCEmbeddingInto PRCFormalSystem) :=
  FormalSystemEmbeddingTarget_proved PRCFormalSystem PRCFormalSystem_expressive

theorem FormalSystemEmbeddingTarget_proved :
    FormalSystemEmbeddingTarget := by
  intro F hF
  exact ⟨PRCEmbeddingInto.ofExpressive F hF⟩

theorem FormalSystemEmbeddingTarget_proved :
    FormalSystemEmbeddingTarget := by
  intro F hF
  exact ⟨PRCEmbeddingInto.ofExpressive F hF⟩

What this page does not claim

The theorem does not claim that every external foundation satisfies the formal-system interface. The theorem does not claim the primitive recognition calculus can express every statement in every formal system. The theorem does not claim the primitive recognition calculus is the only formal system.

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/FormalSystem.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: