inductive definition def or abbrev

`LogicSystem`

No prose has been written for this declaration yet. The Lean source and graph data below render without it.

formal statement (Lean)

  15inductive LogicSystem where
  16  | propositional
  17  | firstOrder
  18  | secondOrder
  19  | modal
  20  | intuitionistic
  21  deriving DecidableEq, Repr, BEq, Fintype
  22

used by (6)

From the project-wide theorem graph. These declarations reference this one in their body.

logicSystem_count in IndisputableMonolith.Mathematics.LogicSystemsFromConfigDim decl_use
LogicSystemsCert in IndisputableMonolith.Mathematics.LogicSystemsFromConfigDim decl_use
FrameworkComplete in IndisputableMonolith.RRF.Foundation.UltimateIsomorphism decl_use
logic_embeds in IndisputableMonolith.RRF.Foundation.UltimateIsomorphism decl_use
LogicSystem in IndisputableMonolith.RRF.Foundation.UltimateIsomorphism decl_use
reality_recognition_framework_complete in IndisputableMonolith.RRF.Foundation.UltimateIsomorphism decl_use

depends on (1)

Lean names referenced from this declaration's body.

LogicSystem in IndisputableMonolith.RRF.Foundation.UltimateIsomorphism decl_use