SyntacticRole
SyntacticRole enumerates the five syntactic roles subject, object, predicate, modifier, and complement. Linguists working in Recognition Science cite the enumeration when grounding universal grammar in the five-dimensional configuration space forced by configDim D = 5. The declaration is a direct inductive definition that automatically derives Fintype, DecidableEq, Repr, and BEq.
claimThe set of syntactic roles consists of the five elements subject, object, predicate, modifier, and complement.
background
In the module on syntax universals from configDim, syntactic categories are forced by the five-dimensional configuration space D = 5. This matches the five core phrase structure categories NP, VP, AP, PP, AdvP, which align with the 5-dimensional recognition taxonomy of the underlying D = 3 lattice. The module reinterprets Chomsky's universal grammar through Recognition Science, with zero sorry or axiom.
proof idea
The declaration is a direct inductive definition listing the five roles. Deriving clauses for DecidableEq, Repr, BEq, and Fintype are instantiated automatically by Lean without additional lemmas or tactics.
why it matters in Recognition Science
This supplies the role set used by syntacticRoleCount and SyntaxUniversalsCert to certify that the cardinality of syntactic roles equals five, matching the phrase categories. It fills the Tier C linguistics step by grounding universals in configDim = 5, which arises from the D = 3 spatial dimensions in the Recognition Science forcing chain. No open questions are addressed.
scope and limits
- Does not derive any syntactic rules or transformations between roles.
- Does not link roles to particular natural languages or empirical data.
- Does not prove the five-dimensional correspondence beyond cardinality.
- Does not address semantic or pragmatic interpretations of the roles.
formal statement (Lean)
25inductive SyntacticRole where
26 | subject | object | predicate | modifier | complement
27 deriving DecidableEq, Repr, BEq, Fintype
28