@cite{wood-2015} — Icelandic Morphosyntax and Argument Structure

@cite{wood-2015} @cite{kratzer-1996} @cite{pylkkanen-2008} @cite{schaefer-2008} @cite{cuervo-2003} @cite{alexiadou-schaefer-2015} @cite{wood-marantz-2017}

@cite{wood-2015} establishes that Icelandic -st (from historical reflexive sik) is the morphological reflex of non-agentive Voice across multiple syntactic configurations, not a single "reflexive" or "anticausative" morpheme.

Layer position

This file is the canonical Wood-2015 study site. The Icelandic Fragment (Fragments.Icelandic.Predicates) carries only consensus lexical data — verb forms, glosses, presence/absence of an active variant. Wood's analytical apparatus lives here:

• the six-way -st classification (StType),
• the anticausative-marking enum -st / -na / -ka / unmarked (AnticausativeMarking),
• the mapping from -st types to Voice flavors,
• per-verb projection bundles (StVerbInfo) carrying stType, marking, and root structure for each verb.

The ±D notation is sourced from @cite{alexiadou-schaefer-2015} (External Arguments in Transitivity Alternations, OUP) and refined in @cite{wood-marantz-2017}. Earlier versions of this fragment attributed ±θ/±D to @cite{schaefer-2008} alone, which was imprecise.

Key Claims Formalized

1. Voice–CAUSE independence (Ch. 3): The causal relation is shared across causative and anticausative alternants; Voice contributes only whether an external argument is introduced. Modeled here using @cite{cuervo-2003}'s VerbHead decomposition (@cite{wood-2015} himself uses a single v head; the multi-head decomposition is a linglib modeling convenience that captures the same independence structurally — see Theories/Syntax/Minimalist/Voice.lean §5).

2. -st as elsewhere exponent of Voice (Ch. 3, §3.3–3.5): -st spells out non-agentive Voice across anticausative, middle, reflexive, experiencer, inherent, and reciprocal configurations. The morphological uniformity masks syntactic diversity.

3. Voice projection locus (Ch. 3): @cite{wood-2015}'s Voice_{D}/Voice_{∅} distinction is captured structurally by VoiceProjectionLocus (in Voice.lean), with AnticausativeMarking.voiceLocus projecting from each morphological exponent (-st, -na, -ka) to its locus.

4. -st and -na complementarity (Ch. 3, §3.3): -st and -na spell out different Voice projections (Voice_{D} vs Voice_{∅}) and never co-occur. -ka is an exponent of v, not Voice.

5. Applicative interaction (Ch. 5): @cite{wood-2015} shows -st cannot merge in SpecApplP because Appl assigns dative case and -st lacks case features. The high/low Appl interaction theorems below follow @cite{pylkkanen-2008} and @cite{schaefer-2008}, not @cite{wood-2015}'s Icelandic-specific analysis (which argues Icelandic lacks true high applicatives).

inductive Wood2015.StType : Type

Classification of Icelandic -st constructions (@cite{wood-2015}). Each type maps to a distinct Voice configuration.

• anticausative : StType
• middle : StType
• reflexive : StType
• inherent : StType
• subjectExp : StType
• reciprocal : StType

@[implicit_reducible]

instance Wood2015.instDecidableEqStType : DecidableEq StType

Equations

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

@[implicit_reducible]

instance Wood2015.instReprStType : Repr StType

Equations

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

def Wood2015.instReprStType.repr : StType → ℕ → Std.Format

Equations

• One or more equations did not get rendered due to their size.
• Wood2015.instReprStType.repr Wood2015.StType.middle prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Wood2015.StType.middle")).group prec✝
• Wood2015.instReprStType.repr Wood2015.StType.reflexive prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Wood2015.StType.reflexive")).group prec✝
• Wood2015.instReprStType.repr Wood2015.StType.inherent prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Wood2015.StType.inherent")).group prec✝
• Wood2015.instReprStType.repr Wood2015.StType.subjectExp prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Wood2015.StType.subjectExp")).group prec✝
• Wood2015.instReprStType.repr Wood2015.StType.reciprocal prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Wood2015.StType.reciprocal")).group prec✝

def Wood2015.StType.voiceFlavor : StType → Minimalist.VoiceFlavor

Map each -st type to its Voice flavor.

Equations

• Wood2015.StType.anticausative.voiceFlavor = Minimalist.VoiceFlavor.nonThematic
• Wood2015.StType.middle.voiceFlavor = Minimalist.VoiceFlavor.expletive
• Wood2015.StType.reflexive.voiceFlavor = Minimalist.VoiceFlavor.reflexive
• Wood2015.StType.inherent.voiceFlavor = Minimalist.VoiceFlavor.nonThematic
• Wood2015.StType.subjectExp.voiceFlavor = Minimalist.VoiceFlavor.experiencer
• Wood2015.StType.reciprocal.voiceFlavor = Minimalist.VoiceFlavor.reflexive

inductive Wood2015.AnticausativeMarking : Type

How an anticausative is morphologically marked (@cite{wood-2015} Ch. 3, §3.3).

• -st spells out Voice_{D};
• -na spells out specifierless Voice_{∅};
• -ka spells out v (not Voice);
• unmarked: zero alternation, compatible with either Voice_{D} or Voice_{∅}, distinguished by independent diagnostics.

Per @cite{wood-2015} Ch. 3, §3.3, -st and -na never co-occur because they spell out different Voice types; -na and -ka never co-occur because -na requires v to be null/pruned.

• st : AnticausativeMarking
• na : AnticausativeMarking
• unmarked : AnticausativeMarking
• ka : AnticausativeMarking

@[implicit_reducible]

instance Wood2015.instDecidableEqAnticausativeMarking : DecidableEq AnticausativeMarking

Equations

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

@[implicit_reducible]

instance Wood2015.instReprAnticausativeMarking : Repr AnticausativeMarking

Equations

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

def Wood2015.instReprAnticausativeMarking.repr : AnticausativeMarking → ℕ → Std.Format

Equations

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

def Wood2015.AnticausativeMarking.voiceLocus : AnticausativeMarking → Minimalist.VoiceProjectionLocus

Each anticausative-marking morpheme picks out a position in Voice/v space (@cite{wood-2015} Ch. 3, §3.3). The structural distinction is visible to pattern matching, not hidden behind string equality on labels like "Voice_{D}".

Equations

• Wood2015.AnticausativeMarking.st.voiceLocus = Minimalist.VoiceProjectionLocus.voiceD
• Wood2015.AnticausativeMarking.na.voiceLocus = Minimalist.VoiceProjectionLocus.voiceBare
• Wood2015.AnticausativeMarking.unmarked.voiceLocus = Minimalist.VoiceProjectionLocus.voiceDOrBare
• Wood2015.AnticausativeMarking.ka.voiceLocus = Minimalist.VoiceProjectionLocus.vHead

def Wood2015.voiceToSuffix : Minimalist.VoiceFlavor → Option String

PF realization of Voice in Icelandic.

-st is the elsewhere exponent for Voice — it appears whenever Voice is non-agentive (modulo antipassive, which is unproductive in Icelandic).

Equations

• Wood2015.voiceToSuffix Minimalist.VoiceFlavor.agentive = none
• Wood2015.voiceToSuffix Minimalist.VoiceFlavor.causer = none
• Wood2015.voiceToSuffix Minimalist.VoiceFlavor.antipassive = none
• Wood2015.voiceToSuffix x✝ = some "-st"

structure Wood2015.StVerbInfo : Type

Wood-2015 analytical projection of a single Icelandic -st verb. Bundles the apparatus the slim Fragment doesn't carry: -st classification, anticausative marking, root-structure decomposition (@cite{cuervo-2003}-style notation per Voice.lean §5–§6), and the possessive-dative diagnostic.

• verb : Fragments.Icelandic.Predicates.IcelandicStVerb

  The lexical fragment entry.

• stType : StType

  Wood's -st classification.

• marking : AnticausativeMarking

  Anticausative-marking morpheme. Default -st.

• rootStructure : List Minimalist.VerbHead

  @cite{cuervo-2003}-style event decomposition.

• licensesPossessiveDative : Bool

  Does this verb license possessive datives (Wood Ch. 5 diagnostic)?

def Wood2015.instReprStVerbInfo.repr : StVerbInfo → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance Wood2015.instReprStVerbInfo : Repr StVerbInfo

Equations

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

def Wood2015.instBEqStVerbInfo.beq : StVerbInfo → StVerbInfo → Bool

Equations

• One or more equations did not get rendered due to their size.
• Wood2015.instBEqStVerbInfo.beq x✝¹ x✝ = false

@[implicit_reducible]

instance Wood2015.instBEqStVerbInfo : BEq StVerbInfo

Equations

• Wood2015.instBEqStVerbInfo = { beq := Wood2015.instBEqStVerbInfo.beq }

@[implicit_reducible]

instance Wood2015.instDecidableEqStVerbInfo : DecidableEq StVerbInfo

Equations

• Wood2015.instDecidableEqStVerbInfo = Wood2015.instDecidableEqStVerbInfo.decEq

def Wood2015.instDecidableEqStVerbInfo.decEq (x✝ x✝¹ : StVerbInfo) : Decidable (x✝ = x✝¹)

Equations

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

def Wood2015.opnast_info : StVerbInfo

opna / opnast 'open' — anticausative -st (@cite{wood-2015} Ch. 3). Active: Jón opnaði dyrnar 'John opened the door'; -st: Dyrnar opnuðust 'The door opened'.

Equations

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

def Wood2015.splundrast_info : StVerbInfo

splundra / splundrast 'shatter' — anticausative -st (@cite{wood-2015} Ch. 3, §3.5). Central example for the Voice–CAUSE independence argument.

Equations

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

def Wood2015.brotna_info : StVerbInfo

brjóta / brotna 'break' — anticausative with -na, NOT -st (@cite{wood-2015} Ch. 3, §3.3.2). Comparison case: -na spells out specifierless Voice_{∅} whereas -st picks Voice_{D}.

Equations

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

def Wood2015.seljast_info : StVerbInfo

selja / seljast 'sell' — middle -st (@cite{wood-2015}).

Equations

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

def Wood2015.lesast_info : StVerbInfo

lesa / lesast 'read' — middle -st (@cite{wood-2015}).

Equations

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

def Wood2015.badast_info : StVerbInfo

baða / baðast 'bathe' — reflexive -st (@cite{wood-2015}).

Equations

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

def Wood2015.klaedast_info : StVerbInfo

klæða / klæðast 'dress' — reflexive -st (@cite{wood-2015}).

Equations

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

def Wood2015.nalgast_info : StVerbInfo

nálgast 'approach' — inherent -st (@cite{wood-2015}). No active variant; -st is lexicalized.

Equations

• Wood2015.nalgast_info = { verb := Fragments.Icelandic.Predicates.nalgast, stType := Wood2015.StType.inherent, rootStructure := [Minimalist.VerbHead.vGO] }

def Wood2015.minnast_info : StVerbInfo

minnast 'remember' — inherent -st (@cite{wood-2015}). No active variant.

Equations

• Wood2015.minnast_info = { verb := Fragments.Icelandic.Predicates.minnast, stType := Wood2015.StType.inherent, rootStructure := [Minimalist.VerbHead.vBE] }

def Wood2015.leidast_info : StVerbInfo

leiðast 'be bored' — subject-experiencer -st (@cite{wood-2015}). Mér leiðist í skólanum 'I am bored in school'.

Equations

• Wood2015.leidast_info = { verb := Fragments.Icelandic.Predicates.leidast, stType := Wood2015.StType.subjectExp, rootStructure := [Minimalist.VerbHead.vBE] }

def Wood2015.kyssast_info : StVerbInfo

kyssa / kyssast 'kiss' — reciprocal -st (@cite{wood-2015}). Þau kyssast 'They kissed (each other)'.

Equations

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

def Wood2015.allStInfo : List StVerbInfo

All -st verb projections (excludes brotna which is -na-marked).

Equations

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

theorem Wood2015.cause_shared_across_alternation : have causativeDecomp := Minimalist.buildDecomposition Minimalist.voiceAgent opnast_info.rootStructure; have anticausativeDecomp := Minimalist.buildDecomposition Minimalist.voiceAnticausative opnast_info.rootStructure; Minimalist.hasCause causativeDecomp = true ∧ Minimalist.hasCause anticausativeDecomp = true

The causal relation is shared across causative and anticausative alternants (@cite{wood-2015} Ch. 3). Modeled using @cite{cuervo-2003}'s VerbHead decomposition: causative [vDO, vCAUSE, vGO, vBE]; anticausative [vCAUSE, vGO, vBE].

theorem Wood2015.opna_alternation : Minimalist.isCausative (Minimalist.buildDecomposition Minimalist.voiceAgent opnast_info.rootStructure) = true ∧ Minimalist.isInchoative (Minimalist.buildDecomposition Minimalist.voiceAnticausative opnast_info.rootStructure) = true

The causative alternation for opna / opnast: same root, different Voice.

theorem Wood2015.voice_alone_determines_causativity : Minimalist.buildDecomposition Minimalist.voiceAgent [Minimalist.VerbHead.vCAUSE, Minimalist.VerbHead.vGO, Minimalist.VerbHead.vBE] = [Minimalist.VerbHead.vDO, Minimalist.VerbHead.vCAUSE, Minimalist.VerbHead.vGO, Minimalist.VerbHead.vBE] ∧ Minimalist.buildDecomposition Minimalist.voiceAnticausative [Minimalist.VerbHead.vCAUSE, Minimalist.VerbHead.vGO, Minimalist.VerbHead.vBE] = [Minimalist.VerbHead.vCAUSE, Minimalist.VerbHead.vGO, Minimalist.VerbHead.vBE]

Voice alone determines causativity for change-of-state roots.

theorem Wood2015.st_covers_all_types : voiceToSuffix StType.anticausative.voiceFlavor = some "-st" ∧ voiceToSuffix StType.middle.voiceFlavor = some "-st" ∧ voiceToSuffix StType.reflexive.voiceFlavor = some "-st" ∧ voiceToSuffix StType.subjectExp.voiceFlavor = some "-st" ∧ voiceToSuffix StType.inherent.voiceFlavor = some "-st" ∧ voiceToSuffix StType.reciprocal.voiceFlavor = some "-st"

-st spells out Voice across all six construction types. Despite morphological uniformity, the underlying Voice configurations differ in ±θ/±D parameters.

theorem Wood2015.st_hides_theta_diversity : ¬Minimalist.voiceAnticausative.AssignsTheta ∧ ¬Minimalist.voiceMiddle.AssignsTheta ∧ Minimalist.voiceReflexive.AssignsTheta

Despite shared morphology, the Voice configurations differ. Anticausative and middle Voice do NOT assign θ; reflexive does. Stated using the canonical Voice constants from Voice.lean.

theorem Wood2015.stType_voiceFlavor_table : StType.anticausative.voiceFlavor = Minimalist.VoiceFlavor.nonThematic ∧ StType.middle.voiceFlavor = Minimalist.VoiceFlavor.expletive ∧ StType.reflexive.voiceFlavor = Minimalist.VoiceFlavor.reflexive ∧ StType.subjectExp.voiceFlavor = Minimalist.VoiceFlavor.experiencer

Lookup table for StType.voiceFlavor on the four typologically-distinct cells. Bundled into a single theorem so the table appears as one proof obligation.

theorem Wood2015.st_spells_out_nonagentive : voiceToSuffix Minimalist.VoiceFlavor.nonThematic = some "-st" ∧ voiceToSuffix Minimalist.VoiceFlavor.expletive = some "-st" ∧ voiceToSuffix Minimalist.VoiceFlavor.reflexive = some "-st" ∧ voiceToSuffix Minimalist.VoiceFlavor.experiencer = some "-st"

-st spells out all non-agentive Voice flavors.

theorem Wood2015.active_no_suffix : voiceToSuffix Minimalist.VoiceFlavor.agentive = none

Active Voice gets no suffix.

theorem Wood2015.parametric_diversity : StType.anticausative.voiceFlavor.toParams.selectsSpecifier = some true ∧ StType.anticausative.voiceFlavor.toParams.extArgSemantics = some Minimalist.ExternalArgSemantics.expletive ∧ StType.middle.voiceFlavor.toParams.selectsSpecifier = some false ∧ StType.middle.voiceFlavor.toParams.extArgSemantics = some Minimalist.ExternalArgSemantics.expletive ∧ StType.reflexive.voiceFlavor.toParams.selectsSpecifier = some true ∧ StType.reflexive.voiceFlavor.toParams.extArgSemantics = some Minimalist.ExternalArgSemantics.thematicArgument ∧ StType.subjectExp.voiceFlavor.toParams.selectsSpecifier = some true ∧ StType.subjectExp.voiceFlavor.toParams.extArgSemantics = some Minimalist.ExternalArgSemantics.thematicArgument

The six -st types occupy distinct cells in the ±θ/±D space. @cite{wood-2015}'s Voice_{D}/Voice_{∅} distinction maps to the ±D axis (selectsSpecifier); Voice semantics (Ø vs AGENT) maps to the ±λx axis.

theorem Wood2015.ethical_blocked_in_middle : Minimalist.applHigh.licensedWith Minimalist.voiceMiddle = false

High applicatives are blocked when Voice has no event semantics (@cite{pylkkanen-2008}, @cite{schaefer-2008}). Note: @cite{wood-2015} Ch. 5 argues Icelandic lacks true high applicatives; the asymmetry formalized here follows the cross-linguistic typology.

theorem Wood2015.possessive_survives_middle : Minimalist.applLowRecipient.licensedWith Minimalist.voiceMiddle = true

Low applicatives survive when Voice has no event semantics because they relate to the theme, not the event (@cite{pylkkanen-2008}).

theorem Wood2015.possessive_survives_anticausative : Minimalist.applLowRecipient.licensedWith Minimalist.voiceAnticausative = true

In anticausatives, possessive datives also survive.

theorem Wood2015.ethical_ok_in_active : Minimalist.applHigh.licensedWith Minimalist.voiceAgent = true

High applicatives ARE licensed with agentive Voice.

theorem Wood2015.dative_voice_asymmetry : Minimalist.applHigh.licensedWith Minimalist.voiceMiddle = false ∧ Minimalist.applHigh.licensedWith Minimalist.voiceAgent = true ∧ Minimalist.applLowRecipient.licensedWith Minimalist.voiceMiddle = true ∧ Minimalist.applLowRecipient.licensedWith Minimalist.voiceAgent = true

The full asymmetry: high applicatives require Voice with event semantics; low applicatives are independent of Voice (@cite{pylkkanen-2008}, @cite{schaefer-2008}).

theorem Wood2015.reflexive_predicts_agent : Minimalist.VoiceFlavor.reflexive.thetaRole = some ThetaRole.agent

Reflexive Voice predicts agent θ-role (agent acts on self).

theorem Wood2015.experiencer_predicts_experiencer : Minimalist.VoiceFlavor.experiencer.thetaRole = some ThetaRole.experiencer

Experiencer Voice predicts experiencer θ-role.

theorem Wood2015.anticausative_predicts_none : Minimalist.VoiceFlavor.nonThematic.thetaRole = none

Anticausative Voice predicts no external θ-role.

theorem Wood2015.middle_predicts_none : Minimalist.VoiceFlavor.expletive.thetaRole = none

Middle Voice predicts no external θ-role.

theorem Wood2015.st_blocked_from_specApplP : Minimalist.applLowRecipient.specCanBearCase false = false ∧ Minimalist.applLowRecipient.specCanBearCase true = true

@cite{wood-2015}'s key applicative claim: -st cannot merge in SpecApplP because Appl assigns dative case and -st lacks case features.

theorem Wood2015.appl_dative_retained_with_st : Minimalist.applLowRecipient.licensedWith Minimalist.voiceAnticausative = true

In ditransitive -st alternations, Appl datives are retained because Appl assigns case independently of Voice (@cite{wood-2015} Ch. 5, §5.3.1).

theorem Wood2015.st_na_different_voice_loci : AnticausativeMarking.st.voiceLocus ≠ AnticausativeMarking.na.voiceLocus

-st and -na spell out different Voice projection loci (@cite{wood-2015} Ch. 3). -st picks out Voice_{D}; -na picks out Voice_{∅}. They never co-occur. Stated structurally over VoiceProjectionLocus, so the inequality is genuine pattern distinction (not a string-equality coincidence on labels).

theorem Wood2015.ka_distinct_from_voice_exponents : AnticausativeMarking.ka.voiceLocus ≠ AnticausativeMarking.st.voiceLocus ∧ AnticausativeMarking.ka.voiceLocus ≠ AnticausativeMarking.na.voiceLocus

-ka spells out v, distinct from both Voice exponents.

theorem Wood2015.brotna_is_na : brotna_info.marking = AnticausativeMarking.na

brotna is -na marked, not -st marked.

theorem Wood2015.all_st_info_are_st_marked : (allStInfo.all fun (i : StVerbInfo) => i.marking == AnticausativeMarking.st) = true

All -st verbs in allStInfo carry the .st marking.

theorem Wood2015.anticausative_marking_varies : opnast_info.marking = AnticausativeMarking.st ∧ brotna_info.marking = AnticausativeMarking.na

Different anticausative roots select different Voice types: opnast takes -st (Voice_{D}), brotna takes -na (Voice_{∅}). The marking choice is lexically determined per root.

theorem Wood2015.anticausative_is_inchoative : ((List.filter (fun (i : StVerbInfo) => i.stType == StType.anticausative) allStInfo).all fun (i : StVerbInfo) => Minimalist.isInchoative i.rootStructure) = true

All anticausative -st verbs have inchoative root structure (no vDO, with vGO + vBE per @cite{cuervo-2003}).

theorem Wood2015.anticausative_verbs_are_cos : ((List.filter (fun (i : StVerbInfo) => i.stType == StType.anticausative) allStInfo).all fun (i : StVerbInfo) => i.rootStructure.contains Minimalist.VerbHead.vGO) = true

All anticausative -st verbs have change-of-state root structure (contains vGO; finer projection than isInchoative).

theorem Wood2015.inherent_no_active : ((List.filter (fun (i : StVerbInfo) => i.stType == StType.inherent) allStInfo).all fun (i : StVerbInfo) => !i.verb.hasActiveVariant) = true

Inherent -st verbs lack active variants.

theorem Wood2015.subjectexp_no_active : ((List.filter (fun (i : StVerbInfo) => i.stType == StType.subjectExp) allStInfo).all fun (i : StVerbInfo) => !i.verb.hasActiveVariant) = true

Subject-experiencer -st verbs lack active variants.

theorem Wood2015.info_count : allStInfo.length = 10

Ten -st verb info entries (excludes brotna, which is -na-marked).