Gender — dimensions of interpretation

[SS20] [Ham19] [Mer14a] [Sau03]

Which dimension of meaning a gender inference lives in, classified per lexical item — not per language or per category ([SS20]). Their Greek noun classes, diagnosed by focus constructions (more stable than [Mer14a]'s ellipsis judgments, which they could not replicate):

• Class I (adherfos/adherfi 'brother/sister'): the gender inference is in both the asserted and presupposed dimensions — focus alternatives carry it (GenderInferences.dual).
• Class III marked members (dhaskala 'teacher.F'): presupposed only — the feminine restricts focus comparison, the masculine is neutral (GenderInferences.presupposedOnly).
• Class II epicenes (jatros 'doctor'): no semantic gender inference; inferences arise pragmatically via competition with the opposite GENDER (GenderInferences.bare; the Maximize-Presupposition-style derivation is study content, cf. [Sau03]).

The fourth cell — asserted but not presupposed — is unattested in their Greek classes (InferenceLocus.greek_asserted_imp_presupposed) but is not excluded by the type: it is precisely [Ham19]'s analysis of French lexical gender (feminine asserts λ x, x is female; masculine contributes nothing), argued against presuppositional accounts on the epicene test (#la singe for a known-female monkey). The presuppositional tradition ([Sau03]) remains correct for pronominal gender — pronominal and lexical gender are partially distinct facets ([Ham19]; also [Kra15] on pronominal-gender-only languages).

Implementation notes

• GenderInferences carries Option-al restrictors per dimension: absence of an inference is distinct from a trivial one — that distinction is [SS20]'s typology. InferenceLocus is its Boolean shadow, derived by GenderInferences.locus, never stipulated separately.
• GenderInfo is the discourse-knowledge layer (what participants know about a referent's gender), distinct from both dimensions of lexical content; its eventual re-grounding target is this typology.

Inference loci

structure Gender.InferenceLocus : Type

Which dimensions of meaning carry a gender inference for a given lexical item ([SS20]).

• asserted : Bool

  The inference is part of asserted content.

• presupposed : Bool

  The inference is part of presupposed content.

def Gender.instDecidableEqInferenceLocus.decEq (x✝ x✝¹ : InferenceLocus) : Decidable (x✝ = x✝¹)

Equations

• One or more equations did not get rendered due to their size.

@[implicit_reducible]

instance Gender.instDecidableEqInferenceLocus : DecidableEq InferenceLocus

Equations

• Gender.instDecidableEqInferenceLocus = Gender.instDecidableEqInferenceLocus.decEq

def Gender.instReprInferenceLocus.repr : InferenceLocus → ℕ → Std.Format

Equations

• One or more equations did not get rendered due to their size.

@[implicit_reducible]

instance Gender.instReprInferenceLocus : Repr InferenceLocus

Equations

• Gender.instReprInferenceLocus = { reprPrec := Gender.instReprInferenceLocus.repr }

@[implicit_reducible]

instance Gender.instFintypeInferenceLocus : Fintype InferenceLocus

Equations

• Gender.instFintypeInferenceLocus = Fintype.ofEquiv ((_ : Bool) × Bool) Gender.InferenceLocus.proxyTypeEquiv

def Gender.InferenceLocus.dual : InferenceLocus

Class I: inference in both dimensions (Greek adherfos).

Equations

• Gender.InferenceLocus.dual = { asserted := true, presupposed := true }

def Gender.InferenceLocus.presupposedOnly : InferenceLocus

Class III marked members: presupposed only (Greek dhaskala).

Equations

• Gender.InferenceLocus.presupposedOnly = { asserted := false, presupposed := true }

def Gender.InferenceLocus.competition : InferenceLocus

Class II epicenes: no semantic inference; gender competition does the pragmatic work (Greek jatros).

Equations

• Gender.InferenceLocus.competition = { asserted := false, presupposed := false }

def Gender.InferenceLocus.assertedOnly : InferenceLocus

[Ham19]'s French lexical gender: asserted, not presupposed — the cell unattested in [SS20]'s Greek classes.

Equations

• Gender.InferenceLocus.assertedOnly = { asserted := true, presupposed := false }

theorem Gender.InferenceLocus.greek_asserted_imp_presupposed (l : InferenceLocus) : l ∈ [dual, presupposedOnly, competition] → l.asserted = true → l.presupposed = true

[SS20]'s Greek classes satisfy a containment: asserted gender is also presupposed. An observation about their inventory, not a well-formedness filter — [Ham19]'s assertedOnly violates it by design.

Gender inferences

structure Gender.GenderInferences (E : Type u_2) : Type u_2

The gender inferences a gendered noun form carries over a domain E of referents: an optional restrictor per dimension of meaning ([SS20]). none = no inference in that dimension.

• asserted : Option (E → Prop)

  Restrictor contributed to asserted content, if any.

• presupposed : Option (E → Prop)

  Restrictor contributed to presupposed content, if any.

def Gender.GenderInferences.locus {E : Type u_1} (g : GenderInferences E) : InferenceLocus

The Boolean shadow: which dimensions carry an inference.

Equations

• g.locus = { asserted := g.asserted.isSome, presupposed := g.presupposed.isSome }

def Gender.GenderInferences.dual {E : Type u_1} (P : E → Prop) : GenderInferences E

Class I construction: one restrictor in both dimensions (adherfos = male sibling, asserted and presupposed).

Equations

• Gender.GenderInferences.dual P = { asserted := some P, presupposed := some P }

def Gender.GenderInferences.presupposedOnly {E : Type u_1} (P : E → Prop) : GenderInferences E

Class III construction: restrictor presupposed only (dhaskala).

Equations

• Gender.GenderInferences.presupposedOnly P = { asserted := none, presupposed := some P }

def Gender.GenderInferences.assertedOnly {E : Type u_1} (P : E → Prop) : GenderInferences E

[Ham19] construction: restrictor asserted only (French lionne = female ∧ lion by Predicate Modification).

Equations

• Gender.GenderInferences.assertedOnly P = { asserted := some P, presupposed := none }

def Gender.GenderInferences.bare {E : Type u_1} : GenderInferences E

Class II construction: no semantic gender inference (jatros).

Equations

• Gender.GenderInferences.bare = { asserted := none, presupposed := none }

@[simp]

theorem Gender.GenderInferences.locus_dual {E : Type u_1} (P : E → Prop) : (dual P).locus = InferenceLocus.dual

@[simp]

theorem Gender.GenderInferences.locus_presupposedOnly {E : Type u_1} (P : E → Prop) : (presupposedOnly P).locus = InferenceLocus.presupposedOnly

@[simp]

theorem Gender.GenderInferences.locus_assertedOnly {E : Type u_1} (P : E → Prop) : (assertedOnly P).locus = InferenceLocus.assertedOnly

@[simp]

theorem Gender.GenderInferences.locus_bare {E : Type u_1} : bare.locus = InferenceLocus.competition

Discourse-level gender knowledge

inductive GenderInfo : Type

Gender knowledge state for a discourse referent.

Distinct from the comparative Gender label a noun's agreement class carries: GenderInfo describes what the discourse participants know or assume about a referent's gender. Motivated by [Arn26]'s observation that singular they is licensed by two inversely correlated pragmatic conditions: one requiring an underspecified discourse representation, the other requiring knowledge that the referent's pronouns are they/them. See also [New92], [New98], and [CILG21].

• known : Gender → GenderInfo

  Gender is known to discourse participants and matches a morphosyntactic agreement class. Example: "my sister" → .known .feminine

• unspecified : GenderInfo

  Gender is unknown, irrelevant, or not elaborated in the discourse. Example: "every student", "someone", "the clerk" (in passing).

@[implicit_reducible]

instance instDecidableEqGenderInfo : DecidableEq GenderInfo

Equations

• instDecidableEqGenderInfo = instDecidableEqGenderInfo.decEq

def instDecidableEqGenderInfo.decEq (x✝ x✝¹ : GenderInfo) : Decidable (x✝ = x✝¹)

Equations

• instDecidableEqGenderInfo.decEq (GenderInfo.known a) (GenderInfo.known b) = if h : a = b then h ▸ isTrue ⋯ else isFalse ⋯
• instDecidableEqGenderInfo.decEq (GenderInfo.known a) GenderInfo.unspecified = isFalse ⋯
• instDecidableEqGenderInfo.decEq GenderInfo.unspecified (GenderInfo.known a) = isFalse ⋯
• instDecidableEqGenderInfo.decEq GenderInfo.unspecified GenderInfo.unspecified = isTrue ⋯

def instReprGenderInfo.repr : GenderInfo → ℕ → Std.Format

Equations

• One or more equations did not get rendered due to their size.
• instReprGenderInfo.repr GenderInfo.unspecified prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "GenderInfo.unspecified")).group prec✝

@[implicit_reducible]

instance instReprGenderInfo : Repr GenderInfo

Equations

• instReprGenderInfo = { reprPrec := instReprGenderInfo.repr }

def instBEqGenderInfo.beq : GenderInfo → GenderInfo → Bool

Equations

• instBEqGenderInfo.beq (GenderInfo.known a) (GenderInfo.known b) = (a == b)
• instBEqGenderInfo.beq GenderInfo.unspecified GenderInfo.unspecified = true
• instBEqGenderInfo.beq x✝¹ x✝ = false

@[implicit_reducible]

instance instBEqGenderInfo : BEq GenderInfo

Equations

• instBEqGenderInfo = { beq := instBEqGenderInfo.beq }

def Gender.toGenderInfo (g : Gender) : GenderInfo

Lift a comparative gender label to discourse-level knowledge.

Equations

• g.toGenderInfo = GenderInfo.known g

def GenderInfo.toGender : GenderInfo → Option Gender

Extract the gender label, if known.

Equations

• (GenderInfo.known a).toGender = some a
• GenderInfo.unspecified.toGender = none

theorem GenderInfo.roundtrip_known (g : Gender) : g.toGenderInfo.toGender = some g

Round-trip: known gender survives the coarsening.