Wood (2015): Icelandic Morphosyntax and Argument Structure

This file formalizes [Woo15]'s account of the Icelandic clitic -st. It is not an exponent of Voice: it originates in an argument position, a specifier that it fills while contributing nothing to the semantics, and cliticizes to the verb. It may merge in a specifier that imposes no case requirement, so in SpecVoiceP and SpecpP but not in SpecApplP, which demands dative, nor in a direct object position (Position.AdmitsSt). A θ-role introduced by a head is saturated by a DP in its specifier or passed up to the next argument-introducing head; with -st in its specifier a head passes its role up, and since Voice is the highest such head, a Voice with -st in its specifier must be expletive (VoiceP.expletive_of_st), and an agentive vP like murder has no -st anticausative (VoiceP.no_st_of_thematic). An anticausative arises in two ways, specifierless Voice or Voice with a D feature checked by -st (VoiceP.anticausative_iff), the expletive non-active and expletive active cells of the substrate's typology (VoiceP.cell_of_anticausative); with thematic Voice, -st can only sit lower, in SpecpP, where p's figure role passes up to the DP in SpecVoiceP, the figure reflexive (st_specP_of_thematic). The alternation therefore lives in Voice over a fixed verb, where [Cue03] puts it in v with no Voice in the inchoative (alternation_in_voice, alternation_in_v).

The morphology follows from locality: -ka spells out v in the context of listed roots and -na spells out specifierless Voice in the context of listed roots, which requires Voice to be adjacent to the root at spell-out, so v must be zero (na_only_if_v_zero). Hence -na and -ka never co-occur, -na never co-occurs with -st, whose Voice carries a D feature, and -ka is compatible with both (na_ka_exclusive, na_st_exclusive, voiceExponent_ka).

Implementation notes

The word is a ComplexHead over the heads v and Voice with v the only cyclic head, and the allomorphy domain is the substrate's SeesRoot, adjacency across phonologically null heads. The lists of roots for -ka and -na are parameters. Voice is a cell of Minimalist.Voice, thematic when the vP is agentive, and its D feature is read from the cell. The reciprocal, denominal, modal passive and láta constructions of the book's sixth chapter are recorded in the examples.

References

• [Woo15]
• [Cue03]
• [Emb10]
• [Sch08a]
• [WM17]

Where -st merges

inductive Wood2015.Position : Type

The argument positions of the verb phrase.

• specVoice : Position
• specP : Position
• specAppl : Position
• directObject : Position

@[instance_reducible]

instance Wood2015.instDecidableEqPosition : DecidableEq Position

Equations

• Wood2015.instDecidableEqPosition x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Wood2015.instReprPosition.repr : Position → ℕ → Std.Format

Equations

• One or more equations did not get rendered due to their size.
• Wood2015.instReprPosition.repr Wood2015.Position.specVoice prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Wood2015.Position.specVoice")).group prec✝
• Wood2015.instReprPosition.repr Wood2015.Position.specP prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Wood2015.Position.specP")).group prec✝
• Wood2015.instReprPosition.repr Wood2015.Position.specAppl prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Wood2015.Position.specAppl")).group prec✝

@[instance_reducible]

instance Wood2015.instReprPosition : Repr Position

Equations

• Wood2015.instReprPosition = { reprPrec := Wood2015.instReprPosition.repr }

def Wood2015.Position.IsSpecifier : Position → Prop

The specifier positions of the argument-introducing heads.

Equations

• Wood2015.Position.specVoice.IsSpecifier = True
• Wood2015.Position.specP.IsSpecifier = True
• Wood2015.Position.specAppl.IsSpecifier = True
• Wood2015.Position.directObject.IsSpecifier = False

def Wood2015.Position.AdmitsCaseless : Position → Prop

This decides whether a position lets a caseless element merge in it: Appl demands dative of its specifier, Voice and p demand nothing.

Equations

• Wood2015.Position.specAppl.AdmitsCaseless = Minimalist.applLowRecipient.SpecCanBearCase none
• x✝.AdmitsCaseless = True

def Wood2015.Position.AdmitsSt (p : Position) : Prop

-st merges in a specifier position with no case requirement.

Equations

• p.AdmitsSt = (p.IsSpecifier ∧ p.AdmitsCaseless)

@[instance_reducible]

instance Wood2015.instDecidablePredPositionIsSpecifier : DecidablePred Position.IsSpecifier

Equations

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

@[instance_reducible]

instance Wood2015.instDecidablePredPositionAdmitsCaseless : DecidablePred Position.AdmitsCaseless

Equations

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

@[instance_reducible]

instance Wood2015.instDecidablePredPositionAdmitsSt : DecidablePred Position.AdmitsSt

Equations

• Wood2015.instDecidablePredPositionAdmitsSt x✝ = { decide := decide x✝.IsSpecifier && decide x✝.AdmitsCaseless, reflects_decide := ⋯ }

theorem Wood2015.admitsSt_iff (p : Position) : p.AdmitsSt ↔ p = Position.specVoice ∨ p = Position.specP

-st merges in SpecVoiceP and SpecpP, not in SpecApplP nor as a direct object.

Voice and its specifier

inductive Wood2015.Occupant : Type

The specifier of Voice holds a DP, the clitic -st, or nothing, for the specifierless Voice.

• dp : Occupant
• st : Occupant
• none : Occupant

@[instance_reducible]

instance Wood2015.instDecidableEqOccupant : DecidableEq Occupant

Equations

• Wood2015.instDecidableEqOccupant x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[instance_reducible]

instance Wood2015.instReprOccupant : Repr Occupant

Equations

• Wood2015.instReprOccupant = { reprPrec := Wood2015.instReprOccupant.repr }

def Wood2015.instReprOccupant.repr : Occupant → ℕ → Std.Format

Equations

• Wood2015.instReprOccupant.repr Wood2015.Occupant.dp prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Wood2015.Occupant.dp")).group prec✝
• Wood2015.instReprOccupant.repr Wood2015.Occupant.st prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Wood2015.Occupant.st")).group prec✝
• Wood2015.instReprOccupant.repr Wood2015.Occupant.none prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Wood2015.Occupant.none")).group prec✝

structure Wood2015.VoiceP : Type

A VoiceP has its head, a cell of the substrate's typology, thematic when the vP is agentive and Voice introduces the agent role, and what occupies its specifier.

• head : Minimalist.Voice.Head
• spec : Occupant

@[instance_reducible]

instance Wood2015.instDecidableEqVoiceP : DecidableEq VoiceP

Equations

• Wood2015.instDecidableEqVoiceP = Wood2015.instDecidableEqVoiceP.decEq

def Wood2015.instDecidableEqVoiceP.decEq (x✝ x✝¹ : VoiceP) : Decidable (x✝ = x✝¹)

Equations

• Wood2015.instDecidableEqVoiceP.decEq { head := a, spec := a_1 } { head := b, spec := b_1 } = if h : a = b then h ▸ if h : a_1 = b_1 then h ▸ isTrue ⋯ else isFalse ⋯ else isFalse ⋯

def Wood2015.instReprVoiceP.repr : VoiceP → ℕ → Std.Format

Equations

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

@[instance_reducible]

instance Wood2015.instReprVoiceP : Repr VoiceP

Equations

• Wood2015.instReprVoiceP = { reprPrec := Wood2015.instReprVoiceP.repr }

def Wood2015.VoiceP.Coherent (V : VoiceP) : Prop

The specifier is empty exactly when the head has no D feature: Voice{D} against Voice{∅}.

Equations

• V.Coherent = (V.spec = Wood2015.Occupant.none ↔ ¬V.head.HasD)

def Wood2015.VoiceP.Interpretable (V : VoiceP) : Prop

A role introduced by the highest argument-introducing head must be saturated by a DP in its specifier: the agent role of a thematic Voice has nowhere to be passed up to.

Equations

• V.Interpretable = (V.head.IsThematic → V.spec = Wood2015.Occupant.dp)

def Wood2015.VoiceP.Expletive (V : VoiceP) : Prop

Voice is expletive when it introduces no role.

Equations

• V.Expletive = ¬V.head.IsThematic

def Wood2015.VoiceP.Anticausative (V : VoiceP) : Prop

An anticausative projects no DP external argument.

Equations

• V.Anticausative = (V.spec ≠ Wood2015.Occupant.dp)

@[instance_reducible]

instance Wood2015.VoiceP.instDecidableCoherent (V : VoiceP) : Decidable V.Coherent

Equations

• V.instDecidableCoherent = { decide := decide (V.spec = Wood2015.Occupant.none) == decide ¬V.head.HasD, reflects_decide := ⋯ }

@[instance_reducible]

instance Wood2015.VoiceP.instDecidableInterpretable (V : VoiceP) : Decidable V.Interpretable

Equations

• V.instDecidableInterpretable = { decide := if h : V.head.IsThematic then decide ((fun (a : V.head.IsThematic) => V.spec = Wood2015.Occupant.dp) h) else true, reflects_decide := ⋯ }

@[instance_reducible]

instance Wood2015.VoiceP.instDecidableExpletive (V : VoiceP) : Decidable V.Expletive

Equations

• V.instDecidableExpletive = { decide := !decide V.head.IsThematic, reflects_decide := ⋯ }

@[instance_reducible]

instance Wood2015.VoiceP.instDecidableAnticausative (V : VoiceP) : Decidable V.Anticausative

Equations

• V.instDecidableAnticausative = { decide := !decide (V.spec = Wood2015.Occupant.dp), reflects_decide := ⋯ }

theorem Wood2015.VoiceP.expletive_of_st {V : VoiceP} (h : V.Interpretable) (hs : V.spec = Occupant.st) : V.Expletive

With -st in its specifier, Voice must be expletive.

theorem Wood2015.VoiceP.expletive_of_none {V : VoiceP} (h : V.Interpretable) (hs : V.spec = Occupant.none) : V.Expletive

Specifierless Voice is expletive.

theorem Wood2015.VoiceP.no_st_of_thematic {V : VoiceP} (h : V.Interpretable) (ht : V.head.IsThematic) : V.spec ≠ Occupant.st

An agentive vP, like murder, has no -st anticausative.

theorem Wood2015.VoiceP.anticausative_iff {V : VoiceP} : V.Anticausative ↔ V.spec = Occupant.none ∨ V.spec = Occupant.st

An anticausative is formed with specifierless Voice, or with Voice whose D feature is checked by -st.

theorem Wood2015.VoiceP.expletive_of_anticausative {V : VoiceP} (h : V.Interpretable) (ha : V.Anticausative) : V.Expletive

Either way, Voice is expletive: the VoiceP denotes what the vP denotes.

theorem Wood2015.VoiceP.cell_of_anticausative {V : VoiceP} (h : V.Interpretable) (hc : V.Coherent) : (V.spec = Occupant.st → V.head.params = Minimalist.Voice.anticausative.params) ∧ (V.spec = Occupant.none → V.head.params = Minimalist.Voice.middle.params)

An -st anticausative is the substrate's expletive active cell, Voice.anticausative, and a specifierless one its expletive non-active cell, Voice.middle: Voice{D} and Voice{∅}.

structure Wood2015.StClause : Type

A clause where -st merges: its VoiceP and the position -st occupies.

• voice : VoiceP
• site : Position
• siteAdmits : self.site.AdmitsSt
• site_voice : self.site = Position.specVoice ↔ self.voice.spec = Occupant.st

  -st is in SpecVoiceP exactly when it is Voice's specifier.

theorem Wood2015.st_specP_of_thematic (C : StClause) (h : C.voice.Interpretable) (ht : C.voice.head.IsThematic) : C.site = Position.specP

Under thematic Voice, -st merges in SpecpP: the figure reflexive.

Where the alternation lives, against [Cue03]

For Wood the two alternants of opna share the verb, root and v, and differ in Voice alone, thematic against expletive; for [Cue03] they differ in v, vDO against vGO over the same state, and the inchoative has no Voice to vary. The two accounts are incompatible on the locus of the alternation, and the substrate lets each be stated.

theorem Wood2015.alternation_in_voice : Minimalist.Voice.agentive.IsThematic ∧ ¬Minimalist.Voice.anticausative.IsThematic ∧ Minimalist.Voice.agentive.HasD ∧ Minimalist.Voice.anticausative.HasD

For Wood, the active and the -st anticausative are one verb under two Voice heads, the thematic active cell and the expletive active cell.

theorem Wood2015.alternation_in_v : Minimalist.LittleV.Causative [Minimalist.LittleV.vDO, Minimalist.LittleV.vBE] ∧ Minimalist.LittleV.Inchoative [Minimalist.LittleV.vGO, Minimalist.LittleV.vBE] ∧ [Minimalist.LittleV.vDO, Minimalist.LittleV.vBE].tail = [Minimalist.LittleV.vGO, Minimalist.LittleV.vBE].tail ∧ Minimalist.LittleV.LicensesVoice [Minimalist.LittleV.vDO, Minimalist.LittleV.vBE] ∧ ¬Minimalist.LittleV.LicensesVoice [Minimalist.LittleV.vGO, Minimalist.LittleV.vBE]

For Cuervo, the causative and the inchoative differ in the head over the state, and the inchoative admits no Voice at all.

The exponents of v and Voice

inductive Wood2015.Head : Type

Above the root the verb has v, with or without the -ka exponent, and Voice, with or without a D feature.

• v (ka : Bool) : Head
• voice (hasD : Bool) : Head

@[instance_reducible]

instance Wood2015.instDecidableEqHead : DecidableEq Head

Equations

• Wood2015.instDecidableEqHead = Wood2015.instDecidableEqHead.decEq

def Wood2015.instDecidableEqHead.decEq (x✝ x✝¹ : Head) : Decidable (x✝ = x✝¹)

Equations

• Wood2015.instDecidableEqHead.decEq (Wood2015.Head.v a) (Wood2015.Head.v b) = if h : a = b then h ▸ isTrue ⋯ else isFalse ⋯
• Wood2015.instDecidableEqHead.decEq (Wood2015.Head.v ka) (Wood2015.Head.voice hasD) = isFalse ⋯
• Wood2015.instDecidableEqHead.decEq (Wood2015.Head.voice hasD) (Wood2015.Head.v ka) = isFalse ⋯
• Wood2015.instDecidableEqHead.decEq (Wood2015.Head.voice a) (Wood2015.Head.voice b) = if h : a = b then h ▸ isTrue ⋯ else isFalse ⋯

def Wood2015.instReprHead.repr : Head → ℕ → Std.Format

Equations

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

@[instance_reducible]

instance Wood2015.instReprHead : Repr Head

Equations

• Wood2015.instReprHead = { reprPrec := Wood2015.instReprHead.repr }

def Wood2015.Head.Cyclic : Head → Prop

v is the categorizer, hence cyclic; Voice is not.

Equations

• (Wood2015.Head.v ka).Cyclic = True
• (Wood2015.Head.voice hasD).Cyclic = False

def Wood2015.Head.Null : Head → Prop

A head is phonologically null when it has no overt exponent: v without -ka. Voice's own exponent is what is being determined, so it counts as overt.

Equations

• (Wood2015.Head.v ka).Null = (ka = false)
• (Wood2015.Head.voice hasD).Null = False

@[instance_reducible]

instance Wood2015.instDecidablePredHeadCyclic : DecidablePred Head.Cyclic

Equations

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

@[instance_reducible]

instance Wood2015.instDecidablePredHeadNull : DecidablePred Head.Null

Equations

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

def Wood2015.verb (r : DistributedMorphology.Root) (ka hasD : Bool) : DistributedMorphology.ComplexHead DistributedMorphology.Root Head

The verb consists of a root, v, and Voice.

Equations

• Wood2015.verb r ka hasD = { root := r, heads := [Wood2015.Head.v ka, Wood2015.Head.voice hasD] }

def Wood2015.voiceIdx (r : DistributedMorphology.Root) (ka hasD : Bool) : Fin (verb r ka hasD).heads.length

Voice's position in the verb.

Equations

• Wood2015.voiceIdx r ka hasD = ⟨1, ⋯⟩

theorem Wood2015.rootLocal_voice (r : DistributedMorphology.Root) (ka hasD : Bool) : (verb r ka hasD).RootLocal Head.Cyclic (voiceIdx r ka hasD)

Voice is in the root's cycle: v is the only cyclic head.

theorem Wood2015.seesRoot_voice_iff (r : DistributedMorphology.Root) (ka hasD : Bool) : (verb r ka hasD).SeesRoot Head.Cyclic Head.Null (voiceIdx r ka hasD) ↔ ka = false

Voice sees the root exactly when v is phonologically zero.

def Wood2015.Ka (kaRoots : Set DistributedMorphology.Root) (r : DistributedMorphology.Root) : Prop

v is spelled out -ka in the context of the listed roots.

Equations

• Wood2015.Ka kaRoots r = (r ∈ kaRoots)

def Wood2015.Na (naRoots : Set DistributedMorphology.Root) (r : DistributedMorphology.Root) (ka hasD : Bool) : Prop

Specifierless Voice is spelled out -na in the context of the listed roots, which it must see at spell-out; everywhere else Voice is the elsewhere zero.

Equations

• Wood2015.Na naRoots r ka hasD = (hasD = false ∧ r ∈ naRoots ∧ (Wood2015.verb r ka hasD).SeesRoot Wood2015.Head.Cyclic Wood2015.Head.Null (Wood2015.voiceIdx r ka hasD))

@[instance_reducible]

instance Wood2015.instDecidableNaOfDecidablePredRootMemSet (naRoots : Set DistributedMorphology.Root) [DecidablePred fun (x : DistributedMorphology.Root) => x ∈ naRoots] (r : DistributedMorphology.Root) (ka hasD : Bool) : Decidable (Na naRoots r ka hasD)

Equations

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

theorem Wood2015.na_only_if_v_zero {naRoots : Set DistributedMorphology.Root} {r : DistributedMorphology.Root} {ka hasD : Bool} (h : Na naRoots r ka hasD) : ka = false

-na requires v to be zero: an overt v breaks Voice's adjacency to the root.

theorem Wood2015.na_ka_exclusive {naRoots : Set DistributedMorphology.Root} {r : DistributedMorphology.Root} {hasD : Bool} : ¬Na naRoots r true hasD

-na and -ka never co-occur.

theorem Wood2015.na_st_exclusive {naRoots : Set DistributedMorphology.Root} {r : DistributedMorphology.Root} {ka : Bool} : ¬Na naRoots r ka true

-na never marks an -st verb: -st checks the D feature of Voice, and -na spells out Voice without one.

theorem Wood2015.na_of_listed {naRoots : Set DistributedMorphology.Root} {r : DistributedMorphology.Root} (h : r ∈ naRoots) : Na naRoots r false false

A listed root with zero v and specifierless Voice takes -na.

inductive Wood2015.VoiceExponent : Type

The exponent of Voice.

• na : VoiceExponent
• zero : VoiceExponent

@[instance_reducible]

instance Wood2015.instDecidableEqVoiceExponent : DecidableEq VoiceExponent

Equations

• Wood2015.instDecidableEqVoiceExponent x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[instance_reducible]

instance Wood2015.instReprVoiceExponent : Repr VoiceExponent

Equations

• Wood2015.instReprVoiceExponent = { reprPrec := Wood2015.instReprVoiceExponent.repr }

def Wood2015.instReprVoiceExponent.repr : VoiceExponent → ℕ → Std.Format

Equations

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

def Wood2015.voiceExponent (naRoots : Set DistributedMorphology.Root) [DecidablePred fun (x : DistributedMorphology.Root) => x ∈ naRoots] (r : DistributedMorphology.Root) (ka hasD : Bool) : VoiceExponent

Voice is spelled out -na where the rule applies and by the elsewhere zero otherwise.

Equations

• Wood2015.voiceExponent naRoots r ka hasD = if Wood2015.Na naRoots r ka hasD then Wood2015.VoiceExponent.na else Wood2015.VoiceExponent.zero

theorem Wood2015.voiceExponent_ka (naRoots : Set DistributedMorphology.Root) [DecidablePred fun (x : DistributedMorphology.Root) => x ∈ naRoots] (r : DistributedMorphology.Root) (hasD : Bool) : voiceExponent naRoots r true hasD = VoiceExponent.zero

A -ka verb has zero Voice whether or not Voice carries a D feature: -ka is compatible with specifierless Voice and with -st.

theorem Wood2015.voiceExponent_st (naRoots : Set DistributedMorphology.Root) [DecidablePred fun (x : DistributedMorphology.Root) => x ∈ naRoots] (r : DistributedMorphology.Root) (ka : Bool) : voiceExponent naRoots r ka true = VoiceExponent.zero

An -st verb has zero Voice whether or not v is -ka.