Stassen (1985): Comparison and Universal Grammar

This file formalizes Stassen's typology of comparative constructions and his explanation of it by temporal chaining. A comparative assigns its standard noun phrase derived case, the case of the comparee, or a fixed case, and a fixed-case standard is the direct object of a verb of exceeding or an adverbial in a separative, allative or locative case, which gives six types. A temporal chain is consecutive or simultaneous and is balanced, both predicates keeping their rank, or deranked, one predicate reduced, either only under identity of subjects or absolutely, and an absolutely deranked consecutive chain reduces its anterior or its posterior predicate, which gives the seven syntactic types of chaining. The book's thesis is that a language models its comparative on one of its chains, and its chaining-based universals follow from the modelling. Over the fragments, Japanese, Korean, Turkish and Hindi-Urdu have the separative comparative the book lists them under, Mandarin and Swahili the exceed one, Swahili also a secondary conjoined one and English the particle one, and the converbs of Korean and Turkish derank their chains as a separative comparative requires.

Main definitions

• Stassen1985.Type1985, Stassen1985.type1985: the six comparative types and the type of a construction, read off its anatomy
• Stassen1985.ChainType: the seven syntactic types of temporal chaining, with their temporality, strategy, conditionality and direction
• Stassen1985.Models: the chains a comparative type is modelled on
• Stassen1985.strategy: the strategy a medial verb form shows

Main results

• Stassen1985.toWALS_type1985, caseAssignment_type1985, spatialCase_type1985: the type agrees with the construction's anatomy and collapses to the type of the atlas
• Stassen1985.universal1A to Stassen1985.universal4: the chaining-based universals
• Stassen1985.separative_fragments, mandarin_exceed, english_particle, swahili_double_option: the fragments' constructions under the typology
• Stassen1985.korean_consistent, Stassen1985.turkish_consistent: the chains a separative comparative is modelled on have the strategy the converbs show

Implementation notes

• The universals are stated over the modelling relation, as the book states them of a language that has a comparative of the type, so each says that a chain the type is modelled on has the property. The chaining data of the sample that Part Two of the book tests the universals against are not transcribed, and the language types of §4.7 under the Principle of Parallel Chaining and the procedure-based universals of chapter 15 are not formalized.
• A clause-chaining fragment records the form of a medial verb but neither the conditionality of its deranking nor the direction of the reduced predicate, so it yields a strategy and not a chain type.
• The mixed comparatives of §2.5, the conjoined exceed comparatives of Fulani, Acholi, Motu, Tamazight and Temne, have no type here, and neither has an adverbial standard in no spatial case, such as the Finnish partitive or the Swahili kuliko the book calls indeterminate.

References

• L. Stassen, Comparison and Universal Grammar (1985)
• L. Stassen, Comparative Constructions (2013)

The six comparative types

inductive Stassen1985.Type1985 : Type

The comparative types are the three adverbial types, by the spatial case of the standard, the exceed type, and the two derived-case types.

• separative : Type1985
• allative : Type1985
• locative : Type1985
• exceed : Type1985
• conjoined : Type1985
• particle : Type1985

@[instance_reducible]

instance Stassen1985.instDecidableEqType1985 : DecidableEq Type1985

Equations

• Stassen1985.instDecidableEqType1985 x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Stassen1985.instReprType1985.repr : Type1985 → ℕ → Std.Format

Equations

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

@[instance_reducible]

instance Stassen1985.instReprType1985 : Repr Type1985

Equations

• Stassen1985.instReprType1985 = { reprPrec := Stassen1985.instReprType1985.repr }

@[instance_reducible]

instance Stassen1985.instFintypeType1985 : Fintype Type1985

Equations

• Stassen1985.instFintypeType1985 = { elems := { val := ↑Stassen1985.Type1985.enumList, nodup := Stassen1985.Type1985.enumList_nodup }, complete := Stassen1985.instFintypeType1985._proof_1 }

def Stassen1985.Type1985.toWALS : Type1985 → Comparative.ComparativeType

The type of the atlas, which collapses the adverbial types into one.

Equations

• Stassen1985.Type1985.separative.toWALS = Comparative.ComparativeType.locational
• Stassen1985.Type1985.allative.toWALS = Comparative.ComparativeType.locational
• Stassen1985.Type1985.locative.toWALS = Comparative.ComparativeType.locational
• Stassen1985.Type1985.exceed.toWALS = Comparative.ComparativeType.exceed
• Stassen1985.Type1985.conjoined.toWALS = Comparative.ComparativeType.conjoined
• Stassen1985.Type1985.particle.toWALS = Comparative.ComparativeType.particle

def Stassen1985.Type1985.caseAssignment : Type1985 → Comparative.CaseAssignment

The case assignment of a type is derived for the conjoined and particle types and fixed otherwise.

Equations

• Stassen1985.Type1985.conjoined.caseAssignment = Comparative.CaseAssignment.derived
• Stassen1985.Type1985.particle.caseAssignment = Comparative.CaseAssignment.derived
• x✝.caseAssignment = Comparative.CaseAssignment.fixed

def Stassen1985.Type1985.fixedEncoding : Type1985 → Option Comparative.FixedCaseEncoding

The encoding of a fixed-case standard.

Equations

• Stassen1985.Type1985.exceed.fixedEncoding = some Comparative.FixedCaseEncoding.directObject
• Stassen1985.Type1985.separative.fixedEncoding = some Comparative.FixedCaseEncoding.adverbial
• Stassen1985.Type1985.allative.fixedEncoding = some Comparative.FixedCaseEncoding.adverbial
• Stassen1985.Type1985.locative.fixedEncoding = some Comparative.FixedCaseEncoding.adverbial
• Stassen1985.Type1985.conjoined.fixedEncoding = none
• Stassen1985.Type1985.particle.fixedEncoding = none

def Stassen1985.Type1985.spatialCase : Type1985 → Option Case

The spatial case of an adverbial standard.

Equations

• Stassen1985.Type1985.separative.spatialCase = some Case.abl
• Stassen1985.Type1985.allative.spatialCase = some Case.all
• Stassen1985.Type1985.locative.spatialCase = some Case.loc
• x✝.spatialCase = none

theorem Stassen1985.Type1985.caseAssignment_eq_derived_iff (t : Type1985) : t.caseAssignment = Comparative.CaseAssignment.derived ↔ t = particle ∨ t = conjoined

Derived case is exactly the conjoined and particle types.

theorem Stassen1985.Type1985.fixedEncoding_eq_adverbial_iff (t : Type1985) : t.fixedEncoding = some Comparative.FixedCaseEncoding.adverbial ↔ t.spatialCase.isSome = true

Adverbial encoding is exactly the spatial triad.

def Stassen1985.type1985 (c : Comparative) : Option Type1985

The type of a construction, read off its anatomy; none for an adverbial standard in no spatial case.

Equations

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

theorem Stassen1985.toWALS_type1985 {c : Comparative} {t : Type1985} (h : type1985 c = some t) : t.toWALS = c.type

The type of a construction collapses to the type its anatomy derives in the typology of the atlas.

theorem Stassen1985.caseAssignment_type1985 {c : Comparative} {t : Type1985} (h : type1985 c = some t) : t.caseAssignment = c.caseAssignment

The case assignment of a construction's type is the construction's.

theorem Stassen1985.spatialCase_type1985 {c : Comparative} {t : Type1985} (h : type1985 c = some t) (hs : t.spatialCase.isSome = true) : t.spatialCase = c.standardCase

The spatial case of an adverbial type is the case of the construction's standard.

Temporal chaining

inductive Stassen1985.Temporality : Type

A chain is consecutive, one event after the other, or simultaneous.

• consecutive : Temporality
• simultaneous : Temporality

@[instance_reducible]

instance Stassen1985.instDecidableEqTemporality : DecidableEq Temporality

Equations

• Stassen1985.instDecidableEqTemporality x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[instance_reducible]

instance Stassen1985.instReprTemporality : Repr Temporality

Equations

• Stassen1985.instReprTemporality = { reprPrec := Stassen1985.instReprTemporality.repr }

def Stassen1985.instReprTemporality.repr : Temporality → ℕ → Std.Format

Equations

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

@[instance_reducible]

instance Stassen1985.instFintypeTemporality : Fintype Temporality

Equations

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

inductive Stassen1985.Strategy : Type

A chain is balanced, both predicates keeping their structural rank, or deranked, one predicate reduced.

• balancing : Strategy
• deranking : Strategy

@[instance_reducible]

instance Stassen1985.instDecidableEqStrategy : DecidableEq Strategy

Equations

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

def Stassen1985.instReprStrategy.repr : Strategy → ℕ → Std.Format

Equations

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

@[instance_reducible]

instance Stassen1985.instReprStrategy : Repr Strategy

Equations

• Stassen1985.instReprStrategy = { reprPrec := Stassen1985.instReprStrategy.repr }

@[instance_reducible]

instance Stassen1985.instFintypeStrategy : Fintype Strategy

Equations

• Stassen1985.instFintypeStrategy = { elems := { val := ↑Stassen1985.Strategy.enumList, nodup := Stassen1985.Strategy.enumList_nodup }, complete := Stassen1985.instFintypeStrategy._proof_1 }

inductive Stassen1985.Conditionality : Type

A deranked chain reduces a predicate only under identity of the subjects, or absolutely.

• conditional : Conditionality
• absolute : Conditionality

@[instance_reducible]

instance Stassen1985.instDecidableEqConditionality : DecidableEq Conditionality

Equations

• Stassen1985.instDecidableEqConditionality x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Stassen1985.instReprConditionality.repr : Conditionality → ℕ → Std.Format

Equations

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

@[instance_reducible]

instance Stassen1985.instReprConditionality : Repr Conditionality

Equations

• Stassen1985.instReprConditionality = { reprPrec := Stassen1985.instReprConditionality.repr }

@[instance_reducible]

instance Stassen1985.instFintypeConditionality : Fintype Conditionality

Equations

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

inductive Stassen1985.Direction : Type

A deranked consecutive chain reduces its anterior or its posterior predicate.

• anterior : Direction
• posterior : Direction

@[instance_reducible]

instance Stassen1985.instDecidableEqDirection : DecidableEq Direction

Equations

• Stassen1985.instDecidableEqDirection x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Stassen1985.instReprDirection.repr : Direction → ℕ → Std.Format

Equations

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

@[instance_reducible]

instance Stassen1985.instReprDirection : Repr Direction

Equations

• Stassen1985.instReprDirection = { reprPrec := Stassen1985.instReprDirection.repr }

@[instance_reducible]

instance Stassen1985.instFintypeDirection : Fintype Direction

Equations

• Stassen1985.instFintypeDirection = { elems := { val := ↑Stassen1985.Direction.enumList, nodup := Stassen1985.Direction.enumList_nodup }, complete := Stassen1985.instFintypeDirection._proof_1 }

inductive Stassen1985.ChainType : Type

The seven syntactic types of temporal chaining (§4.6). A consecutive chain is balanced, conditionally deranked with its posterior predicate reduced, or absolutely deranked with its anterior or its posterior predicate reduced, and a simultaneous chain is balanced, conditionally deranked or absolutely deranked.

• consecutiveBalanced : ChainType
• consecutiveConditional : ChainType
• consecutiveAnterior : ChainType
• consecutivePosterior : ChainType
• simultaneousBalanced : ChainType
• simultaneousConditional : ChainType
• simultaneousAbsolute : ChainType

@[instance_reducible]

instance Stassen1985.instDecidableEqChainType : DecidableEq ChainType

Equations

• Stassen1985.instDecidableEqChainType x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Stassen1985.instReprChainType.repr : ChainType → ℕ → Std.Format

Equations

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

@[instance_reducible]

instance Stassen1985.instReprChainType : Repr ChainType

Equations

• Stassen1985.instReprChainType = { reprPrec := Stassen1985.instReprChainType.repr }

@[instance_reducible]

instance Stassen1985.instFintypeChainType : Fintype ChainType

Equations

• Stassen1985.instFintypeChainType = { elems := { val := ↑Stassen1985.ChainType.enumList, nodup := Stassen1985.ChainType.enumList_nodup }, complete := Stassen1985.instFintypeChainType._proof_1 }

def Stassen1985.ChainType.temporality : ChainType → Temporality

The temporality of a chain type.

Equations

• Stassen1985.ChainType.consecutiveBalanced.temporality = Stassen1985.Temporality.consecutive
• Stassen1985.ChainType.consecutiveConditional.temporality = Stassen1985.Temporality.consecutive
• Stassen1985.ChainType.consecutiveAnterior.temporality = Stassen1985.Temporality.consecutive
• Stassen1985.ChainType.consecutivePosterior.temporality = Stassen1985.Temporality.consecutive
• Stassen1985.ChainType.simultaneousBalanced.temporality = Stassen1985.Temporality.simultaneous
• Stassen1985.ChainType.simultaneousConditional.temporality = Stassen1985.Temporality.simultaneous
• Stassen1985.ChainType.simultaneousAbsolute.temporality = Stassen1985.Temporality.simultaneous

def Stassen1985.ChainType.strategy : ChainType → Strategy

The strategy of a chain type.

Equations

• Stassen1985.ChainType.consecutiveBalanced.strategy = Stassen1985.Strategy.balancing
• Stassen1985.ChainType.simultaneousBalanced.strategy = Stassen1985.Strategy.balancing
• x✝.strategy = Stassen1985.Strategy.deranking

def Stassen1985.ChainType.conditionality : ChainType → Option Conditionality

The conditionality of a deranked chain type.

Equations

• Stassen1985.ChainType.consecutiveConditional.conditionality = some Stassen1985.Conditionality.conditional
• Stassen1985.ChainType.simultaneousConditional.conditionality = some Stassen1985.Conditionality.conditional
• Stassen1985.ChainType.consecutiveAnterior.conditionality = some Stassen1985.Conditionality.absolute
• Stassen1985.ChainType.consecutivePosterior.conditionality = some Stassen1985.Conditionality.absolute
• Stassen1985.ChainType.simultaneousAbsolute.conditionality = some Stassen1985.Conditionality.absolute
• Stassen1985.ChainType.consecutiveBalanced.conditionality = none
• Stassen1985.ChainType.simultaneousBalanced.conditionality = none

def Stassen1985.ChainType.direction : ChainType → Option Direction

The direction of a deranked consecutive chain type, posterior for the conditionally deranked one.

Equations

• Stassen1985.ChainType.consecutiveConditional.direction = some Stassen1985.Direction.posterior
• Stassen1985.ChainType.consecutivePosterior.direction = some Stassen1985.Direction.posterior
• Stassen1985.ChainType.consecutiveAnterior.direction = some Stassen1985.Direction.anterior
• x✝.direction = none

theorem Stassen1985.ChainType.conditionality_isSome_iff (ct : ChainType) : ct.conditionality.isSome = true ↔ ct.strategy = Strategy.deranking

A chain type has a conditionality exactly when it deranks.

theorem Stassen1985.ChainType.direction_isSome_iff (ct : ChainType) : ct.direction.isSome = true ↔ ct.temporality = Temporality.consecutive ∧ ct.strategy = Strategy.deranking

A chain type has a direction exactly when it is a deranked consecutive chain, since a simultaneous chain has no anterior or posterior predicate.

inductive Stassen1985.Models : ChainType → Type1985 → Prop

The book's thesis is that a comparative is modelled on a temporal chain. A particle comparative is modelled on a balanced chain of either temporality, a conjoined comparative on the balanced simultaneous chain, an exceed comparative on a conditionally deranked chain, usually the simultaneous one, and the three adverbial comparatives on the absolutely deranked chains, the separative on the anterior consecutive, the allative on the posterior consecutive and the locative on the simultaneous one.

• particleConsecutive : Models ChainType.consecutiveBalanced Type1985.particle
• particleSimultaneous : Models ChainType.simultaneousBalanced Type1985.particle
• conjoined : Models ChainType.simultaneousBalanced Type1985.conjoined
• exceedConsecutive : Models ChainType.consecutiveConditional Type1985.exceed
• exceedSimultaneous : Models ChainType.simultaneousConditional Type1985.exceed
• separative : Models ChainType.consecutiveAnterior Type1985.separative
• allative : Models ChainType.consecutivePosterior Type1985.allative
• locative : Models ChainType.simultaneousAbsolute Type1985.locative

@[instance_reducible]

instance Stassen1985.instDecidableModels (ct : ChainType) (t : Type1985) : Decidable (Models ct t)

Equations

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

theorem Stassen1985.exists_models (t : Type1985) : ∃ (ct : ChainType), Models ct t

Every comparative type is modelled on some chain type.

The chaining-based universals (§5.2)

theorem Stassen1985.universal1A {ct : ChainType} {t : Type1985} (h : Models ct t) (hd : t.caseAssignment = Comparative.CaseAssignment.derived) : ct.strategy = Strategy.balancing

Universal 1A says that a derived-case comparative is modelled on a balanced chain.

theorem Stassen1985.universal1B {ct : ChainType} {t : Type1985} (h : Models ct t) (hf : t.caseAssignment = Comparative.CaseAssignment.fixed) : ct.strategy = Strategy.deranking

Universal 1B says that a fixed-case comparative is modelled on a deranked chain.

theorem Stassen1985.universal2A {ct : ChainType} (h : Models ct Type1985.exceed) : ct.conditionality = some Conditionality.conditional

Universal 2A says that an exceed comparative is modelled on a conditionally deranked chain.

theorem Stassen1985.universal2B {ct : ChainType} {t : Type1985} (h : Models ct t) (ha : t.fixedEncoding = some Comparative.FixedCaseEncoding.adverbial) : ct.conditionality = some Conditionality.absolute

Universal 2B says that an adverbial comparative is modelled on an absolutely deranked chain.

theorem Stassen1985.universal3A {ct : ChainType} (h : Models ct Type1985.separative) : ct = ChainType.consecutiveAnterior

Universal 3A says that a separative comparative is modelled on the absolutely deranked anterior consecutive chain.

theorem Stassen1985.universal3B {ct : ChainType} (h : Models ct Type1985.allative) : ct = ChainType.consecutivePosterior

Universal 3B says that an allative comparative is modelled on the absolutely deranked posterior consecutive chain.

theorem Stassen1985.universal3C {ct : ChainType} (h : Models ct Type1985.locative) : ct = ChainType.simultaneousAbsolute

Universal 3C says that a locative comparative is modelled on the absolutely deranked simultaneous chain.

theorem Stassen1985.universal4 {ct : ChainType} (h : Models ct Type1985.conjoined) : ct = ChainType.simultaneousBalanced

Universal 4 says that a conjoined comparative is modelled on the balanced simultaneous chain.

The fragments

def Stassen1985.strategy : UD.VerbForm → Strategy

The strategy a medial verb form shows is balancing when the form is finite and deranking otherwise.

Equations

• Stassen1985.strategy UD.VerbForm.Fin = Stassen1985.Strategy.balancing
• Stassen1985.strategy x✝ = Stassen1985.Strategy.deranking

theorem Stassen1985.separative_fragments (c : Comparative) : c ∈ [Japanese.Comparison.yori, Korean.Comparison.boda, Turkish.Comparison.dan, HindiUrdu.Comparison.se] → type1985 c = some Type1985.separative

The ablative standards of Japanese, Korean, Turkish and Hindi-Urdu are separative comparatives, the type the book lists the four languages under.

theorem Stassen1985.mandarin_exceed : type1985 Mandarin.Comparison.bi = some Type1985.exceed

Mandarin has an exceed comparative, the type the book lists it under.

theorem Stassen1985.english_particle : type1985 English.Comparison.than = some Type1985.particle

English has a particle comparative, the construction of §9.4.

theorem Stassen1985.swahili_double_option : type1985 Swahili.Comparison.kushinda = some Type1985.exceed ∧ type1985 Swahili.Comparison.conjoined = some Type1985.conjoined ∧ type1985 Swahili.Comparison.kuliko = none

Swahili has a primary exceed comparative and a secondary conjoined one, the double option of the book's chapter 10, and its kuliko construction, an adverbial standard in no spatial case, is the indeterminate case the book calls it.

theorem Stassen1985.korean_consistent (ct : ChainType) : Models ct Type1985.separative → ∀ (c : Korean.Converb), ct.strategy = strategy c.verbForm

Korean has a separative comparative and deranked chains, so the chain its comparative is modelled on has the strategy its converbs show.

theorem Stassen1985.turkish_consistent (ct : ChainType) : Models ct Type1985.separative → ∀ (c : Turkish.Converb), ct.strategy = strategy c.verbForm

Turkish likewise has a separative comparative and deranked chains.