MetaethicalPosition
plain-language theorem explainer
MetaethicalPosition enumerates the five canonical metaethical stances that Recognition Science associates with configDim equal to five. Metaethicists or framework auditors cite the enumeration when verifying that the philosophy layer contains exactly these positions with no omissions. The declaration is a direct inductive definition that lists the five cases and derives decidable equality plus finite type structure via the deriving clause.
Claim. The inductive type of metaethical positions consists of the five constructors moral realism, constructivism, non-cognitivism, error theory, and moral relativism.
background
Recognition Science sets the configuration dimension to five to match the number of metaethical positions. The module lists them explicitly as moral realism (cognitivist), constructivism, non-cognitivism (expressivism), error theory, and moral relativism. This supplies the philosophical depth component of the framework with no dependence on the forcing chain, J-cost, or phi-ladder.
proof idea
The declaration is an inductive definition that introduces the five positions as constructors and attaches the deriving clause to obtain DecidableEq, Repr, BEq, and Fintype instances automatically.
why it matters
This definition supplies the enumeration required by the downstream cardinality theorem that proves Fintype.card equals five and by the certification structure MetaethicalPositionsCert. It realizes the module claim that configDim equals five in the metaethical domain and closes the philosophy file with zero sorries or axioms.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.