Foundation Primitive Recognition Calculus Formal System Prcformal System Express

The expressive formal system

A formal system, in the general sense, is a set of symbols and rules for combining them. The declaration PRCFormalSystem_expressive concerns a particular, very small formal system built inside the Recognition Science framework. The framework's ledger, a discrete record of events, starts from a primitive distinction between two endpoints, left and right. The declaration proves that the framework's own formal system can distinguish these two endpoints. That is the whole content of the word "expressive" here: the system has enough structure to tell its two starting tokens apart.

Before the framework's turn, the classical idea deserves its due. A formal system, such as Peano arithmetic or the lambda calculus, is expressive when it can represent the distinctions its user needs. The framework's system is deliberately minimal: its tokens are the two endpoints, its expressions are finite traces of events, and one expression extends another exactly when the corresponding trace does. The proof that the system is expressive reduces to the fact that the left endpoint is not the right endpoint, a distinction that holds by definition of the endpoint type.

In Recognition Science, this declaration is a step in a larger argument. The framework aims to derive physical structure from the forced cost of recognition. The declaration establishes that the primitive distinction, the first split in the ledger, is visible inside the framework's own formal system. It also proves that any formal system with the same minimal interface, one that can distinguish the two endpoints and preserve finite trace extension, embeds the primitive recognition calculus. The framework's library, a machine-checked collection of formal theorems, records this as a certificate: the formal-system surface is closed, and the embedding theorem holds.

The declaration does not claim more than it proves. It does not show that every external formal system, such as Peano arithmetic or Zermelo-Fraenkel set theory, satisfies this interface. That broader claim is the next layer of the framework's argument, not a consequence of this declaration. It also does not derive any physical constant or law. The declaration is a structural result about the framework's own formal system, not an empirical claim about the world.

theorem PRCFormalSystem_expressive :
    PRCFormalSystem.Expressive := by
  exact Endpoint.left_ne_right

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

What this page does not claim

The declaration does not show that every external formal system, such as Peano arithmetic, satisfies the interface. The declaration does not derive any physical constant or law. The declaration does not establish that the primitive recognition calculus is the only formal system with this property.

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: