LogicSystem
plain-language theorem explainer
The inductive definition enumerates five canonical logic systems that arise for configuration dimension five in Recognition Science. Researchers verifying completeness of the reality recognition framework cite this enumeration when quantifying the logic systems required to embed into the universal structure. The definition proceeds by listing five constructors and deriving decidable equality, representation, and finiteness automatically.
Claim. Let $L$ be the set whose elements are propositional logic, first-order logic, second-order logic, modal logic, and intuitionistic logic.
background
The module Mathematics.LogicSystemsFromConfigDim states that five canonical logic systems correspond to configDim D = 5. The local setting records zero sorry statements and zero axioms. This inductive type is distinct from the structure LogicSystem appearing in UltimateIsomorphism, which is defined by a proposition type Prop' together with a provability relation proves : Prop' → Prop' → Prop.
proof idea
The declaration is an inductive definition introducing five constructors. Deriving clauses automatically supply DecidableEq, Repr, BEq, and Fintype instances.
why it matters
The definition supplies the finite collection of logic systems required by FrameworkComplete in UltimateIsomorphism and by the theorem reality_recognition_framework_complete. It is referenced by logicSystem_count, which proves the cardinality equals five, and by logic_embeds, which constructs an embedding for each element. The enumeration matches the five-dimensional configuration space stated in the module documentation.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.