metaethicalPosition_count
plain-language theorem explainer
The theorem establishes that the finite type of metaethical positions contains exactly five elements, matching the configuration dimension of five. Metaethicists working from the Recognition Science derivation of positions from configDim would cite this to anchor their enumerations. The proof is a one-line wrapper that applies the decide tactic to the Fintype instance of the inductive type.
Claim. The set consisting of moral realism, constructivism, non-cognitivism, error theory, and moral relativism has cardinality $5$.
background
The module introduces five canonical metaethical positions tied to configuration dimension D equals 5. These comprise moral realism in its cognitivist form, constructivism, non-cognitivism also termed expressivism, error theory, and moral relativism. The inductive definition supplies the five constructors and derives the required DecidableEq, Repr, BEq, and Fintype instances for direct cardinality statements.
proof idea
The proof is a one-line wrapper that invokes the decide tactic. This tactic resolves the equality by exhaustive enumeration over the finite inductive type with its five constructors.
why it matters
The cardinality result is referenced directly in the definition of the metaethical positions certificate. It supplies the enumeration required for the philosophy depth section of the module. The statement aligns with the framework assignment of five positions to the configuration dimension.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.