Rett (2020): Separate but equal: a typology of equative constructions

This file formalizes the chapter's semantic typology of equatives. Descriptively, languages mark an equative by a relativizer standard marker with or without a parameter marker, by a predicate meaning equal or an adverbial meaning equally, by conjoined clauses, by a case-marked standard, or by dedicated morphemes, Strategy. Three diagnostics sort these into the classes of Figure 3, Class: predicative equatives have no weak at least reading; implicit equatives, the standard-marker-only relatives and the conjoined ones, are evaluative; and explicit equatives, whose parameter is marked, split into the sufficientive ones, which factor modifiers like twice can modify, and the demonstrative ones, which they cannot. The class semantics of section 5 derive the first two diagnostics: the sufficientive equative relates degree sets by inclusion, sufficientive_iff, the demonstrative one predicates the standard's maximal degree of the target, demonstrative_iff, so both hold when the target exceeds the standard and neither mentions a standard of tallness, while the implicit equative equates two evaluative properties, implicit_evaluative, and the predicative one an equality, not_predicative_of_lt. Modifiability is the chapter's claim that only the sufficientive strategy involves degree quantification. The examples of sections 3 and 4 are checked against Figure 3, judgment_iff_expected, and the sufficientive is the equative μ b ≤ μ a read at extent sets, sufficientive_iff.

Implementation notes

The descriptive strategies split the parameter-marked relatives into sufficientive and demonstrative as section 4.3 does; case-marked and dedicated strategies have no class, as the chapter leaves them for future research. The Slovenian cells of Figure 2 that the chapter leaves uncertain have no rows.

References

• J. Rett, Separate but equal: a typology of equative constructions (2020)
• J. Rett, The semantics of evaluativity (2015)
• C. Kennedy, Modes of comparison (2007)

Strategies and classes

inductive Rett2020b.Strategy : Type

The descriptive strategies of section 3, the parameter-marked relatives split as in section 4.3.

• smOnly : Strategy

  The strategy with only a relativizer standard marker, English tall like Bill or Italian come.

• demonstrative : Strategy

  The strategy with a degree-demonstrative parameter marker and a relativizer standard marker, Italian tanto … quanto or Spanish tan … como.

• sufficientive : Strategy

  The strategy with a sufficientive parameter marker and a relativizer standard marker, English as … as or German so … wie.

• predicateMain : Strategy

  The strategy with a main predicate meaning equal, Swahili sawa.

• predicateAdverbial : Strategy

  The strategy with an adverbial meaning equally, Mandarin yíyàng or Swedish lika.

• conjoined : Strategy

  Conjoined parallel clauses, often with an additive particle.

• caseMarked : Strategy

  The strategy with a case marker or adposition as standard marker, as in Greenlandic and Quechua.

• dedicated : Strategy

  The strategy with construction-specific markers, Welsh cyn … â.

@[instance_reducible]

instance Rett2020b.instDecidableEqStrategy : DecidableEq Strategy

Equations

• Rett2020b.instDecidableEqStrategy x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

inductive Rett2020b.Class : Type

The theoretical classes of Figure 3.

• predicative : Class
• sufficientive : Class
• demonstrative : Class
• implicit : Class

@[instance_reducible]

instance Rett2020b.instDecidableEqClass : DecidableEq Class

Equations

• Rett2020b.instDecidableEqClass x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[instance_reducible]

instance Rett2020b.instFintypeClass : Fintype Class

Equations

• Rett2020b.instFintypeClass = { elems := { val := ↑Rett2020b.Class.enumList, nodup := Rett2020b.Class.enumList_nodup }, complete := Rett2020b.instFintypeClass._proof_1 }

def Rett2020b.Strategy.class? : Strategy → Option Class

Figure 3's classification; the predicate subtypes pattern together, the standard-marker-only relatives and the conjoined equatives are implicit, and the case-marked and dedicated strategies are left open.

Equations

• Rett2020b.Strategy.smOnly.class? = some Rett2020b.Class.implicit
• Rett2020b.Strategy.conjoined.class? = some Rett2020b.Class.implicit
• Rett2020b.Strategy.demonstrative.class? = some Rett2020b.Class.demonstrative
• Rett2020b.Strategy.sufficientive.class? = some Rett2020b.Class.sufficientive
• Rett2020b.Strategy.predicateMain.class? = some Rett2020b.Class.predicative
• Rett2020b.Strategy.predicateAdverbial.class? = some Rett2020b.Class.predicative
• Rett2020b.Strategy.caseMarked.class? = none
• Rett2020b.Strategy.dedicated.class? = none

inductive Rett2020b.Diagnostic : Type

The diagnostics of section 4.1 are the continuation in fact she's taller, the continuation but she's short, and a factor modifier.

• weak : Diagnostic
• evaluativity : Diagnostic
• factor : Diagnostic

@[instance_reducible]

instance Rett2020b.instDecidableEqDiagnostic : DecidableEq Diagnostic

Equations

• Rett2020b.instDecidableEqDiagnostic x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[instance_reducible]

instance Rett2020b.instFintypeDiagnostic : Fintype Diagnostic

Equations

• Rett2020b.instFintypeDiagnostic = { elems := { val := ↑Rett2020b.Diagnostic.enumList, nodup := Rett2020b.Diagnostic.enumList_nodup }, complete := Rett2020b.instFintypeDiagnostic._proof_1 }

def Rett2020b.Class.HasWeakReading : Class → Prop

Every class but the predicative one has a weak, at least reading.

Equations

• Rett2020b.Class.predicative.HasWeakReading = False
• x✝.HasWeakReading = True

def Rett2020b.Class.Evaluative : Class → Prop

The implicit class alone is evaluative.

Equations

• Rett2020b.Class.implicit.Evaluative = True
• x✝.Evaluative = False

def Rett2020b.Class.Modifiable : Class → Prop

The sufficientive class alone admits a factor modifier, being the only one whose parameter marker is a degree quantifier.

Equations

• Rett2020b.Class.sufficientive.Modifiable = True
• x✝.Modifiable = False

@[instance_reducible]

instance Rett2020b.instDecidablePredClassHasWeakReading : DecidablePred Class.HasWeakReading

Equations

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

@[instance_reducible]

instance Rett2020b.instDecidablePredClassEvaluative : DecidablePred Class.Evaluative

Equations

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

@[instance_reducible]

instance Rett2020b.instDecidablePredClassModifiable : DecidablePred Class.Modifiable

Equations

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

def Rett2020b.Class.Expects (c : Class) : Diagnostic → Prop

A diagnostic sentence is expected to be acceptable for a class with the weak continuation when the class has a weak reading, the short continuation when it is not evaluative, and the factor modifier when it is modifiable.

Equations

• c.Expects Rett2020b.Diagnostic.weak = c.HasWeakReading
• c.Expects Rett2020b.Diagnostic.evaluativity = ¬c.Evaluative
• c.Expects Rett2020b.Diagnostic.factor = c.Modifiable

@[instance_reducible]

instance Rett2020b.instDecidablePredDiagnosticExpects (c : Class) : DecidablePred c.Expects

Equations

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

The class semantics

def Rett2020b.predicative {E : Type u_1} {D : Type u_2} (μ : E → D) (a b : E) : Prop

A predicative equative holds when the target's degree equals the standard's.

Equations

• Rett2020b.predicative μ a b = (μ a = μ b)

def Rett2020b.sufficientive {E : Type u_1} {D : Type u_2} [LinearOrder D] (μ : E → D) (a b : E) : Prop

The sufficientive equative, the set-based as of (5-b), holds when the standard's degrees are among the target's.

Equations

• Rett2020b.sufficientive μ a b = (Set.Iic (μ b) ⊆ Set.Iic (μ a))

def Rett2020b.demonstrative {E : Type u_1} {D : Type u_2} [LinearOrder D] (μ : E → D) (a b : E) : Prop

The demonstrative equative (86) holds when the target has the maximal degree of the standard's degree relative.

Equations

• Rett2020b.demonstrative μ a b = ∃ (d : D), IsGreatest (Set.Iic (μ b)) d ∧ d ≤ μ a

def Rett2020b.implicit {E : Type u_1} {D : Type u_2} [LinearOrder D] (μ : E → D) (s : D) (a b : E) : Prop

The implicit equative (81) holds when the target and the standard share the evaluative property of exceeding the standard of comparison s.

Equations

• Rett2020b.implicit μ s a b = (s < μ a ∧ s < μ b)

def Rett2020b.sufficientiveFactor {E : Type u_1} {D : Type u_2} [LinearOrder D] (μ : E → D) (a b : E) (f : D → D) : Prop

A factor modifier scales the standard's degrees before the sufficientive relates them.

Equations

• Rett2020b.sufficientiveFactor μ a b f = (f '' Set.Iic (μ b) ⊆ Set.Iic (μ a))

theorem Rett2020b.sufficientive_iff {E : Type u_1} {D : Type u_2} [LinearOrder D] (μ : E → D) (a b : E) : sufficientive μ a b ↔ μ b ≤ μ a

theorem Rett2020b.demonstrative_iff {E : Type u_1} {D : Type u_2} [LinearOrder D] (μ : E → D) (a b : E) : demonstrative μ a b ↔ μ b ≤ μ a

theorem Rett2020b.sufficientiveFactor_iff {E : Type u_1} {D : Type u_2} [LinearOrder D] (μ : E → D) (a b : E) {f : D → D} (hf : Monotone f) : sufficientiveFactor μ a b f ↔ f (μ b) ≤ μ a

Under a monotone factor, the modified sufficientive relates the scaled standard to the target: twice as tall is having twice the standard's degree.

theorem Rett2020b.sufficientive_of_lt {E : Type u_1} {D : Type u_2} [LinearOrder D] (μ : E → D) (a b : E) (h : μ b < μ a) : sufficientive μ a b

A sufficientive equative has the weak reading: it holds when the target exceeds the standard.

theorem Rett2020b.demonstrative_of_lt {E : Type u_1} {D : Type u_2} [LinearOrder D] (μ : E → D) (a b : E) (h : μ b < μ a) : demonstrative μ a b

theorem Rett2020b.implicit_of_lt {E : Type u_1} {D : Type u_2} [LinearOrder D] (μ : E → D) (s : D) (a b : E) (hb : s < μ b) (h : μ b < μ a) : implicit μ s a b

theorem Rett2020b.not_predicative_of_lt {E : Type u_1} {D : Type u_2} [LinearOrder D] (μ : E → D) (a b : E) (h : μ b < μ a) : ¬predicative μ a b

A predicative equative has no weak reading: it fails when the target exceeds the standard.

theorem Rett2020b.implicit_evaluative {E : Type u_1} {D : Type u_2} [LinearOrder D] (μ : E → D) (s : D) (a b : E) (h : implicit μ s a b) : s < μ a

The implicit equative is evaluative: it entails that the target exceeds the standard of comparison.

theorem Rett2020b.nonevaluative {E : Type u_1} {D : Type u_2} [LinearOrder D] (μ : E → D) (s : D) (a b : E) (hab : μ a = μ b) (hs : μ a ≤ s) : predicative μ a b ∧ sufficientive μ a b ∧ demonstrative μ a b ∧ ¬implicit μ s a b

The other equatives are not evaluative: with the target and the standard alike and no taller than the standard of comparison, the predicative, sufficientive and demonstrative equatives hold while the implicit one fails.

The chapter's examples

def Rett2020b.Strategy.labels : List (String × Strategy)

The strategies by their paperFeatures labels.

Equations

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

def Rett2020b.Diagnostic.labels : List (String × Diagnostic)

The diagnostics by their paperFeatures labels.

Equations

• Rett2020b.Diagnostic.labels = [("weak", Rett2020b.Diagnostic.weak), ("evaluativity", Rett2020b.Diagnostic.evaluativity), ("factor", Rett2020b.Diagnostic.factor)]

structure Rett2020b.Row : Type

An example records its strategy, the diagnostic it applies if any, and the judgment.

• strategy : Strategy
• diagnostic : Option Diagnostic
• judgment : Judgment

def Rett2020b.Row.ofDatum (e : Datum) : Option Row

A datum read into its row.

Equations

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

theorem Rett2020b.isSome_ofDatum (e : Datum) : e ∈ Examples.all → (Row.ofDatum e).isSome = true

Every example is read.

def Rett2020b.data : List Row

The chapter's examples.

Equations

• Rett2020b.data = List.filterMap Rett2020b.Row.ofDatum Rett2020b.Examples.all

theorem Rett2020b.judgment_iff_expected (d : Row) : d ∈ data → ∀ (c : Class), d.strategy.class? = some c → ∀ (x : Diagnostic), d.diagnostic = some x → (d.judgment = Judgment.acceptable ↔ c.Expects x)

A diagnostic sentence is acceptable exactly when Figure 3 expects it of the strategy's class.

theorem Rett2020b.class_attested (c : Class) : ∃ d ∈ data, d.strategy.class? = some c

Every class of Figure 3 is attested among the examples.