logicSystem_count
The inductive type LogicSystem enumerates five canonical logic systems, so its Fintype cardinality equals five. Researchers deriving the number of logic systems from configuration dimension in Recognition Science cite this count to fix configDim at five. The proof is a one-line decide tactic that exhausts the finite inductive constructors.
claimThe finite type of canonical logic systems has cardinality five, where the systems are propositional logic, first-order logic, second-order logic, modal logic, and intuitionistic logic.
background
LogicSystem is an inductive type whose five constructors are propositional, firstOrder, secondOrder, modal, and intuitionistic. The module sets these five systems equal to configDim D = 5 and reports zero sorries or axioms. This local enumeration builds on the simplified structure LogicSystem from UltimateIsomorphism, which supplies a Prop' type and a proves relation.
proof idea
The proof is a one-line wrapper that applies the decide tactic to compute Fintype.card directly from the DecidableEq and Fintype instances derived for the inductive type.
why it matters in Recognition Science
This theorem supplies the five_systems field inside the logicSystemsCert definition. It confirms the module claim that five logic systems arise at configDim D = 5, closing the enumeration step without sorries. The count aligns with the framework's use of finite discrete structures but does not invoke the forcing chain or RCL.
scope and limits
- Does not derive the five systems from the T0-T8 forcing chain.
- Does not prove that these systems are complete or unique outside the given enumeration.
- Does not connect the count to phi-ladder, mass formulas, or physical constants.
- Does not address logic systems beyond the five listed constructors.
formal statement (Lean)
23theorem logicSystem_count : Fintype.card LogicSystem = 5 := by decide
proof body
24