Bochnak & Hanink (2021): Clausal embedding in Washo: complementation vs. modification

This file formalizes Bochnak and Hanink's two strategies of clausal embedding in Washo. A presuppositional predicate selects a nominalized clause as a DP complement. A non-presuppositional predicate is intransitive, and its dependent-mood clause is an adjoined modifier. We read selection off the Fragment's frames and derive Table 2 from it: a predicate selects iff it takes the nominalizer as clause-typer, and the selected clause is a CP under D while the modifier is a MoodP without C.

The nominalized complement is Hanink's familiar DP over the FPROP type-shift, so it denotes the individual whose content is the embedded proposition. It is defined when that individual is familiar, not when the proposition is true, which is the paper's case against a lexical factivity presupposition (not_factive). The dependent mood is generalized conjunction, so a modifier equates the content of the attitude event with its clause, and two modifiers on one event cannot carry different contents (stack_eq).

Implementation notes

• Cat has no mood head, so the MoodP of (47b) is the T-level spine; what matters is that it projects neither C nor D.
• The holder and theme arguments of the event semantics in (78) and (92) are not represented, the content function drops the paper's world index, and the independent mood -i, the identity (74), has no declaration.
• not_factive is a structural witness about the familiar DP, not a Washo datum.

TODO

• Conjunction over propositions (97) in concessive adjuncts, and the tenseless simultaneous adjuncts of (100)–(101) (§5.5).

References

• [BH21]
• [Han21]
• [Kas15]
• [Ell16]

Selection

def BochnakHanink2021.Selects (v : Washo.Verb) : Prop

A predicate selects if it has an internal-argument frame (§3.2.2).

Equations

• BochnakHanink2021.Selects v = ¬v.IsIntransitive

@[instance_reducible]

instance BochnakHanink2021.instDecidablePredVerbSelects : DecidablePred Selects

Equations

• BochnakHanink2021.instDecidablePredVerbSelects v = { decide := !decide v.IsIntransitive, reflects_decide := ⋯ }

theorem BochnakHanink2021.selects_iff_takes_ge (v : Washo.Verb) : v ∈ Washo.verbs → (Selects v ↔ v.Takes Washo.ge)

A predicate selects iff it takes the nominalizer as clause-typer.

def BochnakHanink2021.complementSpine : Minimalist.ClauseSpine

The spine of a nominalized complement, a CP under a silent D (3).

Equations

• BochnakHanink2021.complementSpine = Minimalist.ClauseSpine.cP.append [Minimalist.Cat.D]

def BochnakHanink2021.modifierSpine : Minimalist.ClauseSpine

The spine of a dependent-mood modifier, a MoodP without C ((4), (47b)).

Equations

• BochnakHanink2021.modifierSpine = Minimalist.ClauseSpine.tP

def BochnakHanink2021.spine (v : Washo.Verb) : Minimalist.ClauseSpine

The spine of the clause a predicate embeds.

Equations

• BochnakHanink2021.spine v = if BochnakHanink2021.Selects v then BochnakHanink2021.complementSpine else BochnakHanink2021.modifierSpine

theorem BochnakHanink2021.spine_projects_D_iff (v : Washo.Verb) : v ∈ Washo.verbs → (Minimalist.Cat.D ∈ spine v ↔ v.typer = Washo.ge) ∧ (Minimalist.Cat.C ∈ spine v ↔ v.typer = Washo.ge)

The embedded clause projects D, and then also C, iff it bears the nominalizer (Table 2).

theorem BochnakHanink2021.suus_selects_gumsuus_not : Selects Washo.suus ∧ ¬Selects Washo.gumsuus

'Dream' selects without the reflexive and not with it ((53)–(55)).

Denotations

def BochnakHanink2021.fprop {E W : Type} (cont : E → W → Prop) (p : W → Prop) : E → Prop

The FPROP type-shift, the property of the individuals whose content is p (76).

Equations

• BochnakHanink2021.fprop cont p x = (cont x = p)

def BochnakHanink2021.complement {E W : Type} (cont : E → W → Prop) (p : W → Prop) (d : ℕ) : Reference.Description E W

The nominalized complement with index d, the familiar DP over FPROP (77).

Equations

• BochnakHanink2021.complement cont p d = Reference.Description.anaphoric (fun (x : Assignment E) (x_1 : W) (x_2 : E) => BochnakHanink2021.fprop cont p x_2) d

theorem BochnakHanink2021.denote_complement {E W : Type} (cont : E → W → Prop) (p : W → Prop) (d : ℕ) (g : Assignment E) (s : W) : Semantics.Denotes.denote (complement cont p d) g s = Reference.iota fun (x : E) => cont x = p ∧ Hanink2021.idxVar d g x

The complement denotes the familiar individual whose content is the embedded proposition (78).

theorem BochnakHanink2021.denote_complement_isSome_iff {E W : Type} (cont : E → W → Prop) (p : W → Prop) (d : ℕ) (g : Assignment E) (s : W) : (Semantics.Denotes.denote (complement cont p d) g s).isSome = true ↔ cont (g d) = p

The complement is defined iff its antecedent has the embedded content (§5.3).

theorem BochnakHanink2021.not_factive : ∃ (cont : Unit → Bool → Prop) (p : Bool → Prop) (g : Assignment Unit) (s : Bool), (Semantics.Denotes.denote (complement cont p 0) g s).isSome = true ∧ ¬p s

The complement can be defined at a situation where its content is false: familiarity is not factivity (§5.3.1), the warrant for (86)–(87) in §5.3.2.

def BochnakHanink2021.dependentMood {α : Type u_1} (P Q : α → Prop) : α → Prop

The dependent mood is generalized conjunction (75).

Equations

• BochnakHanink2021.dependentMood P Q = P ⊓ Q

theorem BochnakHanink2021.dependentMood_fprop {E W : Type} (cont : E → W → Prop) (p : W → Prop) (V : E → Prop) (x : E) : dependentMood (fprop cont p) V x ↔ cont x = p ∧ V x

A dependent-mood clause equates the content of the event it modifies with its proposition (92).

theorem BochnakHanink2021.stack_eq {E W : Type} (cont : E → W → Prop) (p q : W → Prop) (V : E → Prop) {x : E} (h : dependentMood (fprop cont p) (dependentMood (fprop cont q) V) x) : p = q

Two dependent-mood clauses on one event have the same content (§5.4).