LogicSystemsCert
plain-language theorem explainer
LogicSystemsCert records that the enumerated logic systems total exactly five under the configDim correspondence. Researchers mapping logic systems to configuration dimension five would cite this structure when building the canonical list. The definition is a direct record type whose single field asserts the Fintype cardinality of the five-constructor inductive type.
Claim. Let $L$ be the set whose elements are propositional logic, first-order logic, second-order logic, modal logic, and intuitionistic logic. LogicSystemsCert is the structure asserting that the cardinality of $L$ equals 5.
background
The module treats five canonical logic systems as corresponding to configDim equal to five. LogicSystem is the inductive type whose constructors are exactly those five systems and which derives a Fintype instance. An upstream structure in UltimateIsomorphism supplies a more general definition of a logic system consisting of a proposition type together with a provability relation between propositions.
proof idea
The structure is introduced directly by a single field that requires the Fintype cardinality of the inductive type to equal five. No lemmas or tactics are invoked; the definition rests on the derived Fintype instance for the five-constructor inductive type.
why it matters
The definition supplies the cardinality fact consumed by the downstream logicSystemsCert instance. It certifies the five systems as the content of configDim equal to five inside the Mathematics.LogicSystemsFromConfigDim module. The construction sits inside the Recognition Science program that enumerates logic systems available once the configuration dimension is fixed at five.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.