logicSystem_count
plain-language theorem explainer
The inductive type of logic systems has exactly five elements, enumerating propositional, first-order, second-order, modal, and intuitionistic logics. Researchers deriving logic systems from configuration dimension five in Recognition Science would cite this count. The proof is a one-line decide tactic on the derived Fintype instance.
Claim. Let $L$ be the type whose elements are the five canonical logic systems: propositional, first-order, second-order, modal, and intuitionistic. Then the cardinality of $L$ is 5.
background
The module Mathematics.LogicSystemsFromConfigDim defines five canonical logic systems tied to configuration dimension D = 5. The inductive type enumerates exactly these five cases and derives Fintype, DecidableEq, Repr, and BEq instances, enabling direct cardinality computation.
proof idea
The proof is a one-line wrapper that applies the decide tactic. The tactic succeeds because the inductive definition together with the derived Fintype instance makes the equality decidable.
why it matters
This theorem supplies the five_systems field inside the LogicSystemsCert definition. It fills the module-level claim that five logic systems match configDim = 5 and supports downstream certification steps in the Recognition framework.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.