IndisputableMonolith.Philosophy.MetaethicalPositionsFromConfigDim

   1import Mathlib
   2import IndisputableMonolith.Constants
   3
   4/-!
   5# Metaethical Positions from configDim — Philosophy Depth
   6
   7Five canonical metaethical positions (= configDim D = 5):
   8  moral realism (cognitivist), constructivism, non-cognitivism
   9  (expressivism), error theory, moral relativism.
  10
  11Lean status: 0 sorry, 0 axiom.
  12-/
  13
  14namespace IndisputableMonolith.Philosophy.MetaethicalPositionsFromConfigDim
  15
  16inductive MetaethicalPosition where
  17  | moralRealism
  18  | constructivism
  19  | nonCognitivism
  20  | errorTheory
  21  | moralRelativism
  22  deriving DecidableEq, Repr, BEq, Fintype
  23
  24theorem metaethicalPosition_count :
  25    Fintype.card MetaethicalPosition = 5 := by decide
  26
  27structure MetaethicalPositionsCert where
  28  five_positions : Fintype.card MetaethicalPosition = 5
  29
  30def metaethicalPositionsCert : MetaethicalPositionsCert where
  31  five_positions := metaethicalPosition_count
  32
  33end IndisputableMonolith.Philosophy.MetaethicalPositionsFromConfigDim
  34