inductive
definition
LogicSystem
show as:
view math explainer →
open explainer
Generate a durable explainer page for this declaration.
open lean source
IndisputableMonolith.Mathematics.LogicSystemsFromConfigDim on GitHub at line 15.
browse module
All declarations in this module, on Recognition.
explainer page
depends on
used by
formal source
12
13namespace IndisputableMonolith.Mathematics.LogicSystemsFromConfigDim
14
15inductive LogicSystem where
16 | propositional
17 | firstOrder
18 | secondOrder
19 | modal
20 | intuitionistic
21 deriving DecidableEq, Repr, BEq, Fintype
22
23theorem logicSystem_count : Fintype.card LogicSystem = 5 := by decide
24
25structure LogicSystemsCert where
26 five_systems : Fintype.card LogicSystem = 5
27
28def logicSystemsCert : LogicSystemsCert where
29 five_systems := logicSystem_count
30
31end IndisputableMonolith.Mathematics.LogicSystemsFromConfigDim