LogicSystem
A minimal logic system consists of a type of propositions equipped with a binary provability relation. Researchers formalizing embeddings of logic into the universal structure of the Reality Recognition Framework cite this definition when constructing the completeness property. The declaration proceeds by direct structure introduction of the two fields with no proof obligations or lemmas applied.
claimA logic system consists of a type $Prop'$ of propositions together with a binary relation $proves : Prop' → Prop' → Prop$ of provability.
background
The module establishes the ultimate isomorphism asserting that physics, logic, and qualia embed into one universal structure R under phi-based scaling and ledger closure. The logic system structure supplies the simplified interface for the logic component of this claim. Upstream results include the actualization operator A that maps a configuration to the J-cost minimizer among its possibilities, the active-edge count A per fundamental tick at D=3, and the inductive enumeration of five logic variants (propositional through intuitionistic) from configuration dimension.
proof idea
The declaration is a structure definition that directly introduces the proposition type and the proves relation without invoking any lemmas or tactics.
why it matters in Recognition Science
This definition supplies the logic interface required by the FrameworkComplete property and the logic_embeds theorem, which together establish that every logic system embeds into the universal structure. It contributes to the parent result reality_recognition_framework_complete that packages the three embeddings to conclude the framework identity. The construction aligns with the module claim that reality is recognition rather than merely described by it.
scope and limits
- Does not encode inference rules or axioms for any concrete logic.
- Does not supply semantics or model theory for the propositions.
- Does not address consistency, completeness, or decidability.
- Does not connect to the phi-ladder, mass formulas, or J-cost functional.
formal statement (Lean)
60structure LogicSystem where
61 /-- Propositions. -/
62 Prop' : Type
63 /-- Provability. -/
64 proves : Prop' → Prop' → Prop
65
66/-- A qualia space (simplified). -/