logicSystem_count
plain-language theorem explainer
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.
Claim. The 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
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.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.