Icelandic Verb Fragment: -st Constructions

@cite{wood-2015} @cite{schaefer-2008}

Icelandic -st (historically sik → -sk → -st) is the morphological reflex of non-agentive Voice. @cite{wood-2015} shows that -st spells out Voice across at least six descriptive categories:

1. Anticausative -st: Voice_{D} + Ø semantics (e.g., opnast 'open')
2. Middle -st: Voice_{D} + Ø semantics (e.g., seljast 'sell')
3. Reflexive -st: Voice_{D} + AGENT semantics + binding (baðast 'bathe')
4. Inherent -st: lexicalized (nálgast 'approach')
5. Subject-experiencer -st: Voice_{D} + experiencer (leiðast 'be.bored')
6. Reciprocal -st: Voice_{D} + AGENT + reciprocal binding

The key argument: -st is NOT a single morpheme with a single meaning. It is a clitic that merges in the specifier of Voice_{D} (or SpecpP for figure reflexives) across multiple configurations. The shared PF realization obscures the underlying syntactic diversity.

Note: @cite{wood-2015}'s Voice parameterization uses Voice_{D} (has D-feature, projects specifier) vs Voice_{} (specifierless). The ±θ/±D labels used in the VoiceFlavor.toParams function follow @cite{schaefer-2008}'s notation.

Morphological Spell-Out

voiceToSuffix models the observation that all non-agentive Voice configurations spell out as -st in Icelandic. In @cite{wood-2015}'s analysis, -st is a clitic in SpecVoiceP, not a suffix on Voice itself; voiceToSuffix is a simplification for the fragment.

inductive Fragments.Icelandic.Predicates.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

instance Fragments.Icelandic.Predicates.instDecidableEqStType : DecidableEq StType

Equations

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

def Fragments.Icelandic.Predicates.instBEqStType.beq : StType → StType → Bool

Equations

• Fragments.Icelandic.Predicates.instBEqStType.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

instance Fragments.Icelandic.Predicates.instBEqStType : BEq StType

Equations

• Fragments.Icelandic.Predicates.instBEqStType = { beq := Fragments.Icelandic.Predicates.instBEqStType.beq }

def Fragments.Icelandic.Predicates.instReprStType.repr : StType → ℕ → Std.Format

Equations

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

instance Fragments.Icelandic.Predicates.instReprStType : Repr StType

Equations

• Fragments.Icelandic.Predicates.instReprStType = { reprPrec := Fragments.Icelandic.Predicates.instReprStType.repr }

def Fragments.Icelandic.Predicates.StType.voiceFlavor : StType → Minimalism.VoiceFlavor

Map each -st type to its Voice flavor.

Equations

• Fragments.Icelandic.Predicates.StType.anticausative.voiceFlavor = Minimalism.VoiceFlavor.nonThematic
• Fragments.Icelandic.Predicates.StType.middle.voiceFlavor = Minimalism.VoiceFlavor.expletive
• Fragments.Icelandic.Predicates.StType.reflexive.voiceFlavor = Minimalism.VoiceFlavor.reflexive
• Fragments.Icelandic.Predicates.StType.inherent.voiceFlavor = Minimalism.VoiceFlavor.nonThematic
• Fragments.Icelandic.Predicates.StType.subjectExp.voiceFlavor = Minimalism.VoiceFlavor.experiencer
• Fragments.Icelandic.Predicates.StType.reciprocal.voiceFlavor = Minimalism.VoiceFlavor.reflexive

inductive Fragments.Icelandic.Predicates.AnticausativeMarking : Type

How the anticausative is morphologically marked.

@cite{wood-2015} Ch. 3 derives three key generalizations:

• -st merges in SpecVoice_{D} (Voice with D-feature)
• -na spells out Voice_{} (specifierless Voice)
• -st and -na never co-occur (different Voice types)
• -ka is a spell-out of v (not Voice); -na and -ka never co-occur because -na requires v to be null/pruned

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

instance Fragments.Icelandic.Predicates.instDecidableEqAnticausativeMarking : DecidableEq AnticausativeMarking

Equations

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

instance Fragments.Icelandic.Predicates.instBEqAnticausativeMarking : BEq AnticausativeMarking

Equations

• Fragments.Icelandic.Predicates.instBEqAnticausativeMarking = { beq := Fragments.Icelandic.Predicates.instBEqAnticausativeMarking.beq }

def Fragments.Icelandic.Predicates.instBEqAnticausativeMarking.beq : AnticausativeMarking → AnticausativeMarking → Bool

Equations

• Fragments.Icelandic.Predicates.instBEqAnticausativeMarking.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

def Fragments.Icelandic.Predicates.instReprAnticausativeMarking.repr : AnticausativeMarking → ℕ → Std.Format

Equations

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

instance Fragments.Icelandic.Predicates.instReprAnticausativeMarking : Repr AnticausativeMarking

Equations

• Fragments.Icelandic.Predicates.instReprAnticausativeMarking = { reprPrec := Fragments.Icelandic.Predicates.instReprAnticausativeMarking.repr }

def Fragments.Icelandic.Predicates.AnticausativeMarking.voiceType : AnticausativeMarking → String

-st and -na are complementary: they spell out different Voice types.

Equations

• Fragments.Icelandic.Predicates.AnticausativeMarking.st.voiceType = "Voice_{D}"
• Fragments.Icelandic.Predicates.AnticausativeMarking.na.voiceType = "Voice_{}"
• Fragments.Icelandic.Predicates.AnticausativeMarking.unmarked.voiceType = "Voice_{D} or Voice_{}"
• Fragments.Icelandic.Predicates.AnticausativeMarking.ka.voiceType = "v (not Voice)"

def Fragments.Icelandic.Predicates.voiceToSuffix : Minimalism.VoiceFlavor → Option String

PF realization of Voice in Icelandic.

The key insight: -st does NOT correspond to a single Voice flavor. It is the elsewhere exponent for Voice — it appears whenever Voice is not agentive (active).

Equations

• Fragments.Icelandic.Predicates.voiceToSuffix Minimalism.VoiceFlavor.agentive = none
• Fragments.Icelandic.Predicates.voiceToSuffix Minimalism.VoiceFlavor.causer = none
• Fragments.Icelandic.Predicates.voiceToSuffix Minimalism.VoiceFlavor.antipassive = none
• Fragments.Icelandic.Predicates.voiceToSuffix x✝ = some "-st"

structure Fragments.Icelandic.Predicates.IcelandicStVerb : Type

An Icelandic verb entry in the -st / -na fragment.

• activeForm : Option String

  Active/bare form (if one exists)

• stForm : String

  The intransitive form (-st, -na, or same as active)

• gloss : String

  English gloss

• stType : StType

  Which -st construction type

• rootStructure : List Minimalism.VerbHead

  Root event structure (@cite{cuervo-2003} notation)

• hasActiveVariant : Bool

  Can this verb also appear without -st or -na?

• marking : AnticausativeMarking

  How the anticausative is morphologically marked

• licensesPossessiveDative : Bool

  Does this verb license possessive datives?

instance Fragments.Icelandic.Predicates.instReprIcelandicStVerb : Repr IcelandicStVerb

Equations

• Fragments.Icelandic.Predicates.instReprIcelandicStVerb = { reprPrec := Fragments.Icelandic.Predicates.instReprIcelandicStVerb.repr }

def Fragments.Icelandic.Predicates.instReprIcelandicStVerb.repr : IcelandicStVerb → ℕ → Std.Format

Equations

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

def Fragments.Icelandic.Predicates.instBEqIcelandicStVerb.beq : IcelandicStVerb → IcelandicStVerb → Bool

Equations

• One or more equations did not get rendered due to their size.
• Fragments.Icelandic.Predicates.instBEqIcelandicStVerb.beq x✝¹ x✝ = false

instance Fragments.Icelandic.Predicates.instBEqIcelandicStVerb : BEq IcelandicStVerb

Equations

• Fragments.Icelandic.Predicates.instBEqIcelandicStVerb = { beq := Fragments.Icelandic.Predicates.instBEqIcelandicStVerb.beq }

def Fragments.Icelandic.Predicates.opnast : IcelandicStVerb

opna/opnast 'open' — anticausative -st (@cite{wood-2015}). 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 Fragments.Icelandic.Predicates.splundrast : IcelandicStVerb

splundra/splundrast 'shatter' — anticausative -st (@cite{wood-2015}). Active: Ásta splundraði rúðunni 'Ásta shattered the window' -st: Rúðan splundraðist 'The window shattered' Central example in @cite{wood-2015} Ch. 3, §3.5.

Equations

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

def Fragments.Icelandic.Predicates.brotna : IcelandicStVerb

brjóta/brotna 'break' — anticausative with -na (NOT -st). Included as comparison: -na marks specifierless Voice_{} whereas -st merges in SpecVoice_{D} (@cite{wood-2015} Ch. 3, §3.3.2).

Equations

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

def Fragments.Icelandic.Predicates.seljast : IcelandicStVerb

selja/seljast 'sell' — middle -st (@cite{wood-2015}). Þessi bók seldist vel 'This book sold well'

Equations

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

def Fragments.Icelandic.Predicates.lesast : IcelandicStVerb

lesa/lesast 'read' — middle -st (@cite{wood-2015}). Þessi bók lesist vel 'This book reads well'

Equations

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

def Fragments.Icelandic.Predicates.badast : IcelandicStVerb

baða/baðast 'bathe' — reflexive -st (@cite{wood-2015}). Hún baðaðist 'She bathed (herself)'

Equations

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

def Fragments.Icelandic.Predicates.klaedast : IcelandicStVerb

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

Equations

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

def Fragments.Icelandic.Predicates.nalgast : IcelandicStVerb

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

Equations

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

def Fragments.Icelandic.Predicates.minnast : IcelandicStVerb

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

Equations

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

def Fragments.Icelandic.Predicates.leidast : IcelandicStVerb

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

Equations

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

def Fragments.Icelandic.Predicates.kyssast : IcelandicStVerb

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 Fragments.Icelandic.Predicates.allStVerbs : List IcelandicStVerb

All -st verb entries (excludes -na verbs like brotna).

Equations

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

theorem Fragments.Icelandic.Predicates.anticausative_st_is_nonthematic : StType.anticausative.voiceFlavor = Minimalism.VoiceFlavor.nonThematic

Anticausative -st maps to non-thematic Voice.

theorem Fragments.Icelandic.Predicates.middle_st_is_expletive : StType.middle.voiceFlavor = Minimalism.VoiceFlavor.expletive

Middle -st maps to expletive Voice.

theorem Fragments.Icelandic.Predicates.reflexive_st_is_reflexive : StType.reflexive.voiceFlavor = Minimalism.VoiceFlavor.reflexive

Reflexive -st maps to reflexive Voice.

theorem Fragments.Icelandic.Predicates.subjectexp_st_is_experiencer : StType.subjectExp.voiceFlavor = Minimalism.VoiceFlavor.experiencer

Subject-experiencer -st maps to experiencer Voice.

theorem Fragments.Icelandic.Predicates.alternating_have_active : ((List.filter (fun (x : IcelandicStVerb) => x.hasActiveVariant) allStVerbs).all fun (v : IcelandicStVerb) => v.activeForm.isSome) = true

All alternating verbs have active variants.

theorem Fragments.Icelandic.Predicates.inherent_no_active : ((List.filter (fun (v : IcelandicStVerb) => v.stType == StType.inherent) allStVerbs).all fun (v : IcelandicStVerb) => !v.hasActiveVariant) = true

Inherent -st verbs lack active variants.

theorem Fragments.Icelandic.Predicates.subjectexp_no_active : ((List.filter (fun (v : IcelandicStVerb) => v.stType == StType.subjectExp) allStVerbs).all fun (v : IcelandicStVerb) => !v.hasActiveVariant) = true

Subject-experiencer -st verbs lack active variants.

theorem Fragments.Icelandic.Predicates.anticausative_is_inchoative : ((List.filter (fun (v : IcelandicStVerb) => v.stType == StType.anticausative) allStVerbs).all fun (v : IcelandicStVerb) => Minimalism.isInchoative v.rootStructure) = true

All anticausative -st verbs have inchoative root structure.

theorem Fragments.Icelandic.Predicates.st_spells_out_nonagentive : voiceToSuffix Minimalism.VoiceFlavor.nonThematic = some "-st" ∧ voiceToSuffix Minimalism.VoiceFlavor.expletive = some "-st" ∧ voiceToSuffix Minimalism.VoiceFlavor.reflexive = some "-st" ∧ voiceToSuffix Minimalism.VoiceFlavor.experiencer = some "-st"

-st spells out all non-agentive Voice flavors.

theorem Fragments.Icelandic.Predicates.active_no_suffix : voiceToSuffix Minimalism.VoiceFlavor.agentive = none

Active Voice gets no suffix.

theorem Fragments.Icelandic.Predicates.st_na_different_voice_types : AnticausativeMarking.st.voiceType ≠ AnticausativeMarking.na.voiceType

-st and -na spell out different Voice types (@cite{wood-2015} Ch. 3). -st merges in SpecVoice_{D}; -na spells out Voice_{}. They can never co-occur on the same verb form.

theorem Fragments.Icelandic.Predicates.brotna_is_na : brotna.marking = AnticausativeMarking.na

brotna is -na marked, not -st marked.

theorem Fragments.Icelandic.Predicates.all_st_verbs_are_st_marked : (allStVerbs.all fun (v : IcelandicStVerb) => v.marking == AnticausativeMarking.st) = true

All verbs in allStVerbs are -st marked (default).

theorem Fragments.Icelandic.Predicates.anticausative_marking_varies : opnast.marking = AnticausativeMarking.st ∧ brotna.marking = AnticausativeMarking.na

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