Clause constructions

[haspelmath-2025-nonverbal]

Clause.Construction: what kind of predication a clause instantiates — headed by a typical verb, or one of [haspelmath-2025-nonverbal]'s eight nonverbal clause constructions (his Table 1). The nonverbal region is structured by coordinates the paper itself exhibits: the four locopossessional types are the product of domain × pivot definiteness (his (22)), and the duonominal pair splits on the referentiality of the second nominal (§2); [aikhenvald-2015-art] §11.1.3's have vs belong definiteness contrast motivates the pivot coordinate independently. Classifications are equations on the coordinate projections, so the super-types of his Table 2, the predicational bifurcation of §6, and the copula's domain restriction (§7) are proved fibers rather than lists. Transitivity of verbal clauses is the orthogonal valency dimension.

Main definitions

• Clause.Construction — the construction space, with the named nonverbal cells (classificational, equational, predlocative, existential, appertentive, predpossessive) as coordinates
• secondDefinite?, domain?, pivotDefinite? — the coordinate projections
• Nonverbal, Duonominal, Ascriptive, Locational, Possessional, Locopossessional — super-types as fibers, with characterization lemmas
• Predicational — the §6 bifurcation
• Copular — the §7 copula domain

inductive Clause.LocPossDomain : Type

The two locopossessional domains ([haspelmath-2025-nonverbal] (22)): clauses about location vs about possession.

• locational : LocPossDomain
• possessional : LocPossDomain

@[instance_reducible]

instance Clause.instDecidableEqLocPossDomain : DecidableEq LocPossDomain

Equations

• Clause.instDecidableEqLocPossDomain x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[instance_reducible]

instance Clause.instReprLocPossDomain : Repr LocPossDomain

Equations

• Clause.instReprLocPossDomain = { reprPrec := Clause.instReprLocPossDomain.repr }

def Clause.instReprLocPossDomain.repr : LocPossDomain → ℕ → Std.Format

Equations

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

@[instance_reducible]

instance Clause.instFintypeLocPossDomain : Fintype LocPossDomain

Equations

• Clause.instFintypeLocPossDomain = { elems := { val := ↑Clause.LocPossDomain.enumList, nodup := Clause.LocPossDomain.enumList_nodup }, complete := Clause.instFintypeLocPossDomain._proof_1 }

inductive Clause.Construction : Type

The predication a clause instantiates: headed by a typical verb, or one of [haspelmath-2025-nonverbal]'s nonverbal construction blocks:

• duonominal: two nominal expressions (§2); the second nominal's definiteness splits classificational (indefinite, nonreferential classificatory nominal — Lee is a baker) from equational (both definite — Kim is my mother).
• attributional: property attribution (§3) — The bird is small.
• locopossessional: the (22) grid — domain × pivot (locatum or possessum) definiteness. The bird is on the roof / There is a bird on the roof / The boat belongs to me / I have a boat.
• hypartic: pure existence (§12) — God exists; not a special case of any other type.

• verbal : Construction
• duonominal (secondDefinite : Bool) : Construction
• attributional : Construction
• locopossessional (domain : LocPossDomain) (pivotDefinite : Bool) : Construction
• hypartic : Construction

def Clause.instDecidableEqConstruction.decEq (x✝ x✝¹ : Construction) : Decidable (x✝ = x✝¹)

Equations

• One or more equations did not get rendered due to their size.
• Clause.instDecidableEqConstruction.decEq Clause.Construction.verbal Clause.Construction.verbal = isTrue ⋯
• Clause.instDecidableEqConstruction.decEq Clause.Construction.verbal (Clause.Construction.duonominal secondDefinite) = isFalse ⋯
• Clause.instDecidableEqConstruction.decEq Clause.Construction.verbal Clause.Construction.attributional = isFalse Clause.instDecidableEqConstruction.decEq._proof_2
• Clause.instDecidableEqConstruction.decEq Clause.Construction.verbal (Clause.Construction.locopossessional domain pivotDefinite) = isFalse ⋯
• Clause.instDecidableEqConstruction.decEq Clause.Construction.verbal Clause.Construction.hypartic = isFalse Clause.instDecidableEqConstruction.decEq._proof_4
• Clause.instDecidableEqConstruction.decEq (Clause.Construction.duonominal secondDefinite) Clause.Construction.verbal = isFalse ⋯
• Clause.instDecidableEqConstruction.decEq (Clause.Construction.duonominal a) (Clause.Construction.duonominal b) = if h : a = b then h ▸ isTrue ⋯ else isFalse ⋯
• Clause.instDecidableEqConstruction.decEq (Clause.Construction.duonominal secondDefinite) Clause.Construction.attributional = isFalse ⋯
• Clause.instDecidableEqConstruction.decEq (Clause.Construction.duonominal secondDefinite) (Clause.Construction.locopossessional domain pivotDefinite) = isFalse ⋯
• Clause.instDecidableEqConstruction.decEq (Clause.Construction.duonominal secondDefinite) Clause.Construction.hypartic = isFalse ⋯
• Clause.instDecidableEqConstruction.decEq Clause.Construction.attributional Clause.Construction.verbal = isFalse Clause.instDecidableEqConstruction.decEq._proof_11
• Clause.instDecidableEqConstruction.decEq Clause.Construction.attributional (Clause.Construction.duonominal secondDefinite) = isFalse ⋯
• Clause.instDecidableEqConstruction.decEq Clause.Construction.attributional Clause.Construction.attributional = isTrue ⋯
• Clause.instDecidableEqConstruction.decEq Clause.Construction.attributional (Clause.Construction.locopossessional domain pivotDefinite) = isFalse ⋯
• Clause.instDecidableEqConstruction.decEq Clause.Construction.attributional Clause.Construction.hypartic = isFalse Clause.instDecidableEqConstruction.decEq._proof_14
• Clause.instDecidableEqConstruction.decEq (Clause.Construction.locopossessional domain pivotDefinite) Clause.Construction.verbal = isFalse ⋯
• Clause.instDecidableEqConstruction.decEq (Clause.Construction.locopossessional domain pivotDefinite) (Clause.Construction.duonominal secondDefinite) = isFalse ⋯
• Clause.instDecidableEqConstruction.decEq (Clause.Construction.locopossessional domain pivotDefinite) Clause.Construction.attributional = isFalse ⋯
• Clause.instDecidableEqConstruction.decEq (Clause.Construction.locopossessional domain pivotDefinite) Clause.Construction.hypartic = isFalse ⋯
• Clause.instDecidableEqConstruction.decEq Clause.Construction.hypartic Clause.Construction.verbal = isFalse Clause.instDecidableEqConstruction.decEq._proof_22
• Clause.instDecidableEqConstruction.decEq Clause.Construction.hypartic (Clause.Construction.duonominal secondDefinite) = isFalse ⋯
• Clause.instDecidableEqConstruction.decEq Clause.Construction.hypartic Clause.Construction.attributional = isFalse Clause.instDecidableEqConstruction.decEq._proof_24
• Clause.instDecidableEqConstruction.decEq Clause.Construction.hypartic (Clause.Construction.locopossessional domain pivotDefinite) = isFalse ⋯
• Clause.instDecidableEqConstruction.decEq Clause.Construction.hypartic Clause.Construction.hypartic = isTrue ⋯

@[instance_reducible]

instance Clause.instDecidableEqConstruction : DecidableEq Construction

Equations

• Clause.instDecidableEqConstruction = Clause.instDecidableEqConstruction.decEq

def Clause.instReprConstruction.repr : Construction → ℕ → Std.Format

Equations

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

@[instance_reducible]

instance Clause.instReprConstruction : Repr Construction

Equations

• Clause.instReprConstruction = { reprPrec := Clause.instReprConstruction.repr }

@[instance_reducible]

instance Clause.instFintypeConstruction : Fintype Construction

Equations

• Clause.instFintypeConstruction = Fintype.ofEquiv (Unit ⊕ Bool ⊕ Unit ⊕ (_ : Clause.LocPossDomain) × Bool ⊕ Unit) Clause.Construction.proxyTypeEquiv

The named nonverbal constructions (Table 1)

def Clause.Construction.classificational : Construction

Lee is a baker — definite subject, indefinite classificatory nominal (§2).

Equations

• Clause.Construction.classificational = Clause.Construction.duonominal false

def Clause.Construction.equational : Construction

Kim is my mother — two definite nominals (§2, §9).

Equations

• Clause.Construction.equational = Clause.Construction.duonominal true

def Clause.Construction.predlocative : Construction

The bird is on the roof — definite locatum (§4).

Equations

• Clause.Construction.predlocative = Clause.Construction.locopossessional Clause.LocPossDomain.locational true

def Clause.Construction.existential : Construction

There is a bird on the roof — indefinite existent (§4, §12).

Equations

• Clause.Construction.existential = Clause.Construction.locopossessional Clause.LocPossDomain.locational false

def Clause.Construction.appertentive : Construction

The boat belongs to me — definite possessum (§5).

Equations

• Clause.Construction.appertentive = Clause.Construction.locopossessional Clause.LocPossDomain.possessional true

def Clause.Construction.predpossessive : Construction

I have a boat — indefinite possessum (§5).

Equations

• Clause.Construction.predpossessive = Clause.Construction.locopossessional Clause.LocPossDomain.possessional false

Coordinate projections

def Clause.Construction.secondDefinite? : Construction → Option Bool

The second nominal's definiteness, for duonominal constructions.

Equations

• (Clause.Construction.duonominal b).secondDefinite? = some b
• x✝.secondDefinite? = none

def Clause.Construction.domain? : Construction → Option LocPossDomain

The (22) domain, for locopossessional constructions.

Equations

• (Clause.Construction.locopossessional d pivotDefinite).domain? = some d
• x✝.domain? = none

def Clause.Construction.pivotDefinite? : Construction → Option Bool

The pivot's (locatum's or possessum's) definiteness, for locopossessional constructions.

Equations

• (Clause.Construction.locopossessional d pivotDefinite).pivotDefinite? = some pivotDefinite
• x✝.pivotDefinite? = none

Super-types, as fibers

def Clause.Construction.Nonverbal (t : Construction) : Prop

Lacks a typical verb — [haspelmath-2025-nonverbal]'s cover concept.

Equations

• t.Nonverbal = (t ≠ Clause.Construction.verbal)

def Clause.Construction.Duonominal (t : Construction) : Prop

Two nominal expressions in correspondence (§2): the classificational + equational block.

Equations

• t.Duonominal = (t.secondDefinite? ≠ none)

def Clause.Construction.Ascriptive (t : Construction) : Prop

Ascribes a concept to the subject referent (§3): classificational + attributional.

Equations

• t.Ascriptive = (t.secondDefinite? = some false ∨ t = Clause.Construction.attributional)

def Clause.Construction.Locational (t : Construction) : Prop

The locational column of (22): predlocative + existential.

Equations

• t.Locational = (t.domain? = some Clause.LocPossDomain.locational)

def Clause.Construction.Possessional (t : Construction) : Prop

The possessional column of (22): predpossessive + appertentive.

Equations

• t.Possessional = (t.domain? = some Clause.LocPossDomain.possessional)

def Clause.Construction.Locopossessional (t : Construction) : Prop

The whole (22) grid: [clark-1978]'s "locationals".

Equations

• t.Locopossessional = (t.domain? ≠ none)

@[instance_reducible]

instance Clause.Construction.instDecidablePredNonverbal : DecidablePred Nonverbal

Equations

• x✝.instDecidablePredNonverbal = Clause.Construction.instDecidablePredNonverbal._aux_1 x✝

@[instance_reducible]

instance Clause.Construction.instDecidablePredDuonominal : DecidablePred Duonominal

Equations

• x✝.instDecidablePredDuonominal = Clause.Construction.instDecidablePredDuonominal._aux_1 x✝

@[instance_reducible]

instance Clause.Construction.instDecidablePredAscriptive : DecidablePred Ascriptive

Equations

• x✝.instDecidablePredAscriptive = Clause.Construction.instDecidablePredAscriptive._aux_1 x✝

@[instance_reducible]

instance Clause.Construction.instDecidablePredLocational : DecidablePred Locational

Equations

• x✝.instDecidablePredLocational = Clause.Construction.instDecidablePredLocational._aux_1 x✝

@[instance_reducible]

instance Clause.Construction.instDecidablePredPossessional : DecidablePred Possessional

Equations

• x✝.instDecidablePredPossessional = Clause.Construction.instDecidablePredPossessional._aux_1 x✝

@[instance_reducible]

instance Clause.Construction.instDecidablePredLocopossessional : DecidablePred Locopossessional

Equations

• x✝.instDecidablePredLocopossessional = Clause.Construction.instDecidablePredLocopossessional._aux_1 x✝

theorem Clause.Construction.locational_iff (t : Construction) : t.Locational ↔ t = predlocative ∨ t = existential

Table 2's locational super-type is exactly its two rows.

theorem Clause.Construction.possessional_iff (t : Construction) : t.Possessional ↔ t = appertentive ∨ t = predpossessive

Table 2's possessional super-type is exactly its two rows.

theorem Clause.Construction.ascriptive_iff (t : Construction) : t.Ascriptive ↔ t = classificational ∨ t = attributional

Table 2's ascriptive super-type is exactly its two rows.

theorem Clause.Construction.locopossessional_iff (t : Construction) : t.Locopossessional ↔ t.Locational ∨ t.Possessional

The (22) grid is the union of its two columns.

The predicational bifurcation (§6, Table 1)

def Clause.Construction.Predicational (t : Construction) : Prop

The clause has a topic-comment (subject-predicate) division: an element that is a predicate rather than a referring expression. Verbal clauses predicate; among the nonverbal types ([haspelmath-2025-nonverbal] §6), a duonominal predicates iff its second nominal is a nonreferential classificatory nominal, attributionals predicate, a locopossessional predicates iff its pivot is definite (the locative or appertentive phrase is then the predicate), and hypartics do not predicate.

Equations

• t.Predicational = (t = Clause.Construction.verbal ∨ t.secondDefinite? = some false ∨ t = Clause.Construction.attributional ∨ t.pivotDefinite? = some true)

@[instance_reducible]

instance Clause.Construction.instDecidablePredPredicational : DecidablePred Predicational

Equations

• x✝.instDecidablePredPredicational = Clause.Construction.instDecidablePredPredicational._aux_1 x✝

theorem Clause.Construction.predicational_iff (t : Construction) : t.Predicational ↔ t = verbal ∨ t = appertentive ∨ t = predlocative ∨ t = attributional ∨ t = classificational

Table 1's predicational rows, derived: verbal plus appertentive, predlocative, attributional, classificational.

theorem Clause.Construction.locopossessional_predicational_iff (d : LocPossDomain) (b : Bool) : (locopossessional d b).Predicational ↔ b = true

Inside the (22) grid, predicationality is pivot definiteness.

The copula's domain (§7)

A copula is a form marking a stative link between the two argument positions of an equational, ascriptive or locational clause; existives (Spanish hay) are copulas restricted to existential and predpossessive clauses (§7, §11). Form-based strategies (copula vs verbless clause, existives, transpossessives, …; [haspelmath-2025-nonverbal] §§5, 11; [aikhenvald-2015-art] §11.1.2) enter with the per-language fragments that instantiate them.

def Clause.Construction.Copular (t : Construction) : Prop

The construction admits a copula (§7): equational, ascriptive, or locational.

Equations

• t.Copular = (t.Duonominal ∨ t = Clause.Construction.attributional ∨ t.Locational)

@[instance_reducible]

instance Clause.Construction.instDecidablePredCopular : DecidablePred Copular

Equations

• x✝.instDecidablePredCopular = Clause.Construction.instDecidablePredCopular._aux_1 x✝

theorem Clause.Construction.copular_iff (t : Construction) : t.Copular ↔ t = equational ∨ t = classificational ∨ t = attributional ∨ t = predlocative ∨ t = existential

The copular constructions are exactly the five types §7 names — in particular, 'have' in a predpossessive and 'belong' in an appertentive are not copulas, and verbal clauses are outside the domain.