Icelandic Verb Case Frames

[Thr07] [YMJ87] [ZMT85]

Case Frames ([Thr07] §4.1.2.2, ex. 4.48)

Of the 16 logically possible two-case combinations (4 × 4), only 5 are reasonably common for dyadic verbs ([YMJ87]): NA, ND, NG, DN, AA. Two more (AN, GN) are extremely rare or restricted to one construction each. Seven (DA, DD, DG, GA, GD, GG, and transitive NN) do not occur at all.

Quirky Subject Properties ([Thr07] §4.1.2.1)

Oblique subjects pass 9 of 10 subject diagnostics ([ZMT85], [Thr07] §4.1.1):

1. Precede verb in default word order (§4.1.1.1)
2. Invert with verb in yes/no questions (§4.1.1.1)
3. Block expletive það constructions (§4.1.1.3)
4. Bind clause-internal reflexives sig (§4.1.1.4)
5. Bind long-distance reflexives (§4.1.1.5)
6. License conjunction reduction / subject ellipsis (§4.1.1.6)
7. Embed under ECM verbs, preserving case (§4.1.1.7)
8. Control PRO in infinitival complements (§4.1.1.8, limited)
9. Extract from embedded clauses (§4.1.1.9)

The ONE diagnostic they fail: verb agreement. The finite verb agrees with the nominative argument (regardless of position), not the quirky subject. When no nominative argument is present, the verb shows default 3sg agreement ([Thr07] ex. 4.47).

Triadic (Ditransitive) Frames ([Thr07] §4.1.2.3, ex. 4.62)

Subject is always nominative in ditransitives. Six patterns are attested for the two objects: NDA (>220 verbs), NAD (~40), NDG (~30), NDD (~30), NAG (~20), NAA (~2).

Case Assignment ([ZMT85])

Quirky case is fixed (lexical): it is preserved under raising and is not affected by passivization. Structural case (NOM, ACC in standard frames) is derived: it changes under passivization (ACC object → NOM subject in passive). This distinction is encoded via CaseAssignment from Case.

structure Icelandic.Verbs.VerbCaseFrame : Type

A verb's case frame: the cases assigned to its arguments. Theory-neutral — records the morphological facts without committing to a particular analysis of WHY these cases appear.

The two post-verbal argument slots follow linear order: firstObject is the first NP after the verb (typically IO in NDA frames), secondObject is the second (typically DO in NDA frames). [Thr07] §4.1.2.3 discusses the difficulty of labeling these as "direct" vs "indirect" in Icelandic.

• form : String

  Icelandic citation form

• gloss : String

  English gloss

• subjectCase : Case

  Case of the subject (first argument)

• firstObject : Option Case

  Case of the first post-verbal argument, if any

• secondObject : Option Case

  Case of the second post-verbal argument, if any

• subjectCaseAssignment : Features.CaseAssignment

  How the subject's case is assigned: .derived (structural — changes under passivization/raising) or .fixed (lexical/quirky — preserved under raising). Default: NOM → derived, all others → fixed.

@[implicit_reducible]

instance Icelandic.Verbs.instReprVerbCaseFrame : Repr VerbCaseFrame

Equations

• Icelandic.Verbs.instReprVerbCaseFrame = { reprPrec := Icelandic.Verbs.instReprVerbCaseFrame.repr }

def Icelandic.Verbs.instReprVerbCaseFrame.repr : VerbCaseFrame → ℕ → Std.Format

Equations

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

def Icelandic.Verbs.instBEqVerbCaseFrame.beq : VerbCaseFrame → VerbCaseFrame → Bool

Equations

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

@[implicit_reducible]

instance Icelandic.Verbs.instBEqVerbCaseFrame : BEq VerbCaseFrame

Equations

• Icelandic.Verbs.instBEqVerbCaseFrame = { beq := Icelandic.Verbs.instBEqVerbCaseFrame.beq }

def Icelandic.Verbs.VerbCaseFrame.quirkySubject (v : VerbCaseFrame) : Bool

Is the subject non-nominative (quirky)? Derived from the case frame, not stored redundantly.

Equations

• v.quirkySubject = (v.subjectCase != Case.nom)

def Icelandic.Verbs.elska : VerbCaseFrame

elska 'love' — NA frame ([Thr07] ex. 4.56a). Hann elskar hana. 'He(N) loves her(A).'

Equations

• Icelandic.Verbs.elska = { form := "elska", gloss := "love", subjectCase := Case.nom, firstObject := some Case.acc }

def Icelandic.Verbs.lesa : VerbCaseFrame

lesa 'read' — NA frame ([Thr07] ex. 4.56b). Hún las bókina. 'She(N) read book-the(A).'

Equations

• Icelandic.Verbs.lesa = { form := "lesa", gloss := "read", subjectCase := Case.nom, firstObject := some Case.acc }

def Icelandic.Verbs.hjalpa : VerbCaseFrame

hjálpa 'help' — ND frame ([Thr07] ex. 4.57a). Hún hjálpaði honum. 'She(N) helped him(D).'

Equations

• Icelandic.Verbs.hjalpa = { form := "hjálpa", gloss := "help", subjectCase := Case.nom, firstObject := some Case.dat }

def Icelandic.Verbs.strauka : VerbCaseFrame

strauka 'pet' — ND frame ([Thr07] ex. 4.57b). Ég strauk kettinum. 'I(N) petted cat-the(D).'

Equations

• Icelandic.Verbs.strauka = { form := "strauka", gloss := "pet", subjectCase := Case.nom, firstObject := some Case.dat }

def Icelandic.Verbs.kasta : VerbCaseFrame

kasta 'throw' — ND frame ([Thr07] ex. 4.57c). Hann kastaði boltanum. 'He(N) threw ball-the(D).'

Equations

• Icelandic.Verbs.kasta = { form := "kasta", gloss := "throw", subjectCase := Case.nom, firstObject := some Case.dat }

def Icelandic.Verbs.sakna : VerbCaseFrame

sakna 'miss' — NG frame ([Thr07] ex. 4.58a). Hann saknar hennar. 'He(N) misses her(G).'

Equations

• Icelandic.Verbs.sakna = { form := "sakna", gloss := "miss", subjectCase := Case.nom, firstObject := some Case.gen }

def Icelandic.Verbs.krefja : VerbCaseFrame

krefja 'demand' — NG frame ([Thr07] ex. 4.58b). Ég krefst bóta. 'I(N) demand compensation(G).'

Equations

• Icelandic.Verbs.krefja = { form := "krefja", gloss := "demand", subjectCase := Case.nom, firstObject := some Case.gen }

def Icelandic.Verbs.lika : VerbCaseFrame

líka 'like' — DN frame ([Thr07] ex. 4.61b). Henni líkuðu hestarnir. 'Her(D) liked(pl.) horses-the(Npl.).' Verb agrees with NOM object hestarnir, not DAT subject henni.

Equations

• Icelandic.Verbs.lika = { form := "líka", gloss := "like", subjectCase := Case.dat, firstObject := some Case.nom }

def Icelandic.Verbs.batna : VerbCaseFrame

batna 'get better' — DN frame ([Thr07] ex. 4.61c). Barninu batnaði veikin. 'Child-the(D) got-better sickness(N).'

Equations

• Icelandic.Verbs.batna = { form := "batna", gloss := "get better/recover", subjectCase := Case.dat, firstObject := some Case.nom }

def Icelandic.Verbs.leidastCF : VerbCaseFrame

leiðast 'be bored' — DN frame ([Thr07] ex. 4.61d). Stráknum leiddust kennararnir. 'Boy-the(D) bored(pl.) teachers-the(Npl.).' Also an -st verb (see Predicates.lean).

Equations

• Icelandic.Verbs.leidastCF = { form := "leiðast", gloss := "be bored", subjectCase := Case.dat, firstObject := some Case.nom }

def Icelandic.Verbs.askotnast : VerbCaseFrame

áskotnast 'get by luck' — DN frame ([Thr07] ex. 4.61a). Mér áskotnuðust peningar. 'Me(D) lucked-onto(pl.) money(Npl.).'

Equations

• Icelandic.Verbs.askotnast = { form := "áskotnast", gloss := "get by luck", subjectCase := Case.dat, firstObject := some Case.nom }

def Icelandic.Verbs.vanta : VerbCaseFrame

vanta 'lack/need' — AA frame ([Thr07] ex. 4.60a). Hana vantar vinnu. 'Her(A) lacks work(A).'

Equations

• Icelandic.Verbs.vanta = { form := "vanta", gloss := "lack/need", subjectCase := Case.acc, firstObject := some Case.acc }

def Icelandic.Verbs.dreyma : VerbCaseFrame

dreyma 'dream' — AA frame ([Thr07] ex. 4.60b). Mig dreymdi draum. 'Me(A) dreamt dream(A).'

Equations

• Icelandic.Verbs.dreyma = { form := "dreyma", gloss := "dream", subjectCase := Case.acc, firstObject := some Case.acc }

def Icelandic.Verbs.bresta : VerbCaseFrame

bresta 'fail (of courage)' — AA frame ([Thr07] ex. 4.60c). Harald brast kjark. 'Harold(A) failed courage(A).'

Equations

• Icelandic.Verbs.bresta = { form := "bresta", gloss := "fail (of courage)", subjectCase := Case.acc, firstObject := some Case.acc }

def Icelandic.Verbs.syfja : VerbCaseFrame

ACC-NOM impersonal — extremely rare, possibly one construction ([Thr07] ex. 4.52a, parenthesized in ex. 4.48 grid). Hana hefur líklega sótt syfja. 'Her(A) has probably sought sleepiness(N).' The ACC experiencer occupies subject position; the NOM theme syfja 'sleepiness' is a nominative noun, not a verb. The verbal predicate in this construction is sækja (pp. sótt).

Equations

• Icelandic.Verbs.syfja = { form := "syfja", gloss := "sleepiness (ACC-NOM impersonal)", subjectCase := Case.acc, firstObject := some Case.nom }

def Icelandic.Verbs.vera_kostur : VerbCaseFrame

GEN-NOM — extremely restricted, all examples involve the copula vera and a fixed predicative noun ([Thr07] ex. 4.54-4.55). Þess var þá enginn kostur. 'Of-that(G) was then no(N) choice(N).' 'That was not possible then.'

Equations

• Icelandic.Verbs.vera_kostur = { form := "vera (kostur)", gloss := "be an option (copula + pred. noun)", subjectCase := Case.gen, firstObject := some Case.nom }

def Icelandic.Verbs.gefa : VerbCaseFrame

gefa 'give' — NDA frame ([Thr07] ex. 4.63a). María gaf Haraldi bókina. 'Mary(N) gave Harold(D) book-the(A).' Most common ditransitive pattern (>220 verbs).

Equations

• Icelandic.Verbs.gefa = { form := "gefa", gloss := "give", subjectCase := Case.nom, firstObject := some Case.dat, secondObject := some Case.acc }

def Icelandic.Verbs.segja : VerbCaseFrame

segja 'tell' — NDA frame ([Thr07] ex. 4.62).

Equations

• Icelandic.Verbs.segja = { form := "segja", gloss := "tell", subjectCase := Case.nom, firstObject := some Case.dat, secondObject := some Case.acc }

def Icelandic.Verbs.svipta : VerbCaseFrame

svipta 'deprive' — NAD frame ([Thr07] ex. 4.65a). Lögreglan svipti hann ökuleyfinu. 'Police-the(N) deprived him(A) driver's-licence-the(D).'

Equations

• Icelandic.Verbs.svipta = { form := "svipta", gloss := "deprive", subjectCase := Case.nom, firstObject := some Case.acc, secondObject := some Case.dat }

def Icelandic.Verbs.leyna : VerbCaseFrame

leyna 'conceal' — NAD frame ([Thr07] ex. 4.65b). Þeir leyndu hana sannleikanum. 'They(N) concealed her(A) truth-the(D).'

Equations

• Icelandic.Verbs.leyna = { form := "leyna", gloss := "conceal", subjectCase := Case.nom, firstObject := some Case.acc, secondObject := some Case.dat }

def Icelandic.Verbs.lofa : VerbCaseFrame

lofa 'promise' — NDD frame ([Thr07] ex. 4.72a). Ég lofaði henni því. 'I(N) promised her(D) it(D).'

Equations

• Icelandic.Verbs.lofa = { form := "lofa", gloss := "promise", subjectCase := Case.nom, firstObject := some Case.dat, secondObject := some Case.dat }

def Icelandic.Verbs.skila : VerbCaseFrame

skila 'return' — NDD frame ([Thr07] ex. 4.72b). Hún skilaði mér bókinni. 'She(N) returned me(D) book-the(D).'

Equations

• Icelandic.Verbs.skila = { form := "skila", gloss := "return", subjectCase := Case.nom, firstObject := some Case.dat, secondObject := some Case.dat }

def Icelandic.Verbs.spyrja : VerbCaseFrame

spyrja 'ask' — NAG frame ([Thr07] ex. 4.70a). Þeir spurðu hana margra spurninga. 'They(N) asked her(A) many questions(G).'

Equations

• Icelandic.Verbs.spyrja = { form := "spyrja", gloss := "ask", subjectCase := Case.nom, firstObject := some Case.acc, secondObject := some Case.gen }

def Icelandic.Verbs.oska : VerbCaseFrame

óska 'wish' — NDG frame ([Thr07] ex. 4.69a). Ég óska þér velfarnaðar. 'I(N) wish you(D) well-being(G).'

Equations

• Icelandic.Verbs.oska = { form := "óska", gloss := "wish", subjectCase := Case.nom, firstObject := some Case.dat, secondObject := some Case.gen }

def Icelandic.Verbs.kosta : VerbCaseFrame

kosta 'cost' — NAA frame ([Thr07] ex. 4.74). Maturinn kostaði mig fjóra dollara. 'Food-the(N) cost me(A) four dollars(A).' Extremely rare pattern (~2 verbs).

Equations

• Icelandic.Verbs.kosta = { form := "kosta", gloss := "cost", subjectCase := Case.nom, firstObject := some Case.acc, secondObject := some Case.acc }

inductive Icelandic.Verbs.SubjectDiagnostic : Type

The 10 standard subject diagnostics for Icelandic ([Thr07] §4.1.1, [ZMT85]).

• defaultPosition : SubjectDiagnostic
• yesNoInversion : SubjectDiagnostic
• blockExpletive : SubjectDiagnostic
• reflexiveBinding : SubjectDiagnostic
• longDistanceReflexive : SubjectDiagnostic
• conjunctionReduction : SubjectDiagnostic
• ecmEmbedding : SubjectDiagnostic
• proControl : SubjectDiagnostic
• extraction : SubjectDiagnostic
• verbAgreement : SubjectDiagnostic

@[implicit_reducible]

instance Icelandic.Verbs.instDecidableEqSubjectDiagnostic : DecidableEq SubjectDiagnostic

Equations

• Icelandic.Verbs.instDecidableEqSubjectDiagnostic x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[implicit_reducible]

instance Icelandic.Verbs.instReprSubjectDiagnostic : Repr SubjectDiagnostic

Equations

• Icelandic.Verbs.instReprSubjectDiagnostic = { reprPrec := Icelandic.Verbs.instReprSubjectDiagnostic.repr }

def Icelandic.Verbs.instReprSubjectDiagnostic.repr : SubjectDiagnostic → ℕ → Std.Format

Equations

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

def Icelandic.Verbs.SubjectDiagnostic.passedByQuirkySubject : SubjectDiagnostic → Bool

Does a quirky (non-nominative) subject pass this diagnostic? Quirky subjects pass all diagnostics EXCEPT verb agreement ([Thr07] §4.1.2.1).

Equations

• Icelandic.Verbs.SubjectDiagnostic.verbAgreement.passedByQuirkySubject = false
• x✝.passedByQuirkySubject = true

inductive Icelandic.Verbs.AgreementTarget : Type

Which argument does the finite verb agree with? In Icelandic, the verb agrees with the nominative argument, regardless of whether it is the subject or the object ([Thr07] §4.1.2.1, ex. 4.47). When no nominative argument is present, default 3sg appears.

• nominativeArg : AgreementTarget
• default3sg : AgreementTarget

@[implicit_reducible]

instance Icelandic.Verbs.instDecidableEqAgreementTarget : DecidableEq AgreementTarget

Equations

• Icelandic.Verbs.instDecidableEqAgreementTarget x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[implicit_reducible]

instance Icelandic.Verbs.instReprAgreementTarget : Repr AgreementTarget

Equations

• Icelandic.Verbs.instReprAgreementTarget = { reprPrec := Icelandic.Verbs.instReprAgreementTarget.repr }

def Icelandic.Verbs.instReprAgreementTarget.repr : AgreementTarget → ℕ → Std.Format

Equations

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

def Icelandic.Verbs.VerbCaseFrame.agreementTarget (v : VerbCaseFrame) : AgreementTarget

Determine the agreement target for a verb's case frame. If any argument is nominative, the verb agrees with it. Otherwise, default 3sg.

Equations

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

def Icelandic.Verbs.nomSubjectVerbs : List VerbCaseFrame

Dyadic verbs with nominative subjects.

Equations

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

def Icelandic.Verbs.quirkySubjectVerbs : List VerbCaseFrame

Dyadic verbs with quirky (non-nominative) subjects.

Equations

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

def Icelandic.Verbs.allDyadicVerbs : List VerbCaseFrame

All dyadic verb entries.

Equations

• Icelandic.Verbs.allDyadicVerbs = Icelandic.Verbs.nomSubjectVerbs ++ Icelandic.Verbs.quirkySubjectVerbs

def Icelandic.Verbs.ditransitiveVerbs : List VerbCaseFrame

Ditransitive verb entries.

Equations

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

def Icelandic.Verbs.productiveDyadicPatterns : List (Case × Case)

The 5 productive dyadic case patterns in Icelandic ([Thr07] §4.1.2.2, [YMJ87]). Out of 16 logically possible combinations (4 cases × 4 cases), 7 do not occur (DA, DD, DG, GA, GD, GG, transitive NN) and 4 are very rare (AN, AG, GN, NN-copular).

Equations

• Icelandic.Verbs.productiveDyadicPatterns = [(Case.nom, Case.acc), (Case.nom, Case.dat), (Case.nom, Case.gen), (Case.dat, Case.nom), (Case.acc, Case.acc)]

theorem Icelandic.Verbs.five_of_sixteen_productive : productiveDyadicPatterns.length = 5

theorem Icelandic.Verbs.all_verbs_use_attested_pattern : have attested := productiveDyadicPatterns ++ [(Case.acc, Case.nom), (Case.gen, Case.nom)]; (allDyadicVerbs.all fun (v : VerbCaseFrame) => match v.firstObject with | some o => attested.contains (v.subjectCase, o) | none => false) = true

Every verb in the fragment uses one of the 7 attested patterns (5 productive + AN + GN).

theorem Icelandic.Verbs.quirky_verbs_are_quirky : (quirkySubjectVerbs.all fun (x : VerbCaseFrame) => x.quirkySubject) = true

All verbs in the quirky list have non-nominative subjects.

theorem Icelandic.Verbs.nom_verbs_not_quirky : (nomSubjectVerbs.all fun (v : VerbCaseFrame) => !v.quirkySubject) = true

No verb in the nominative-subject list has a quirky subject.

theorem Icelandic.Verbs.quirky_subjects_are_fixed : (quirkySubjectVerbs.all fun (v : VerbCaseFrame) => v.subjectCaseAssignment == Features.CaseAssignment.fixed) = true

Quirky subjects have fixed (lexical) case assignment.

theorem Icelandic.Verbs.nom_subjects_are_derived : (nomSubjectVerbs.all fun (v : VerbCaseFrame) => v.subjectCaseAssignment == Features.CaseAssignment.derived) = true

Nominative subjects have derived (structural) case assignment.

theorem Icelandic.Verbs.na_agrees_with_subject : elska.agreementTarget = AgreementTarget.nominativeArg

NA verbs: agreement target is the nominative subject.

theorem Icelandic.Verbs.dn_agrees_with_object : lika.agreementTarget = AgreementTarget.nominativeArg ∧ batna.agreementTarget = AgreementTarget.nominativeArg ∧ leidastCF.agreementTarget = AgreementTarget.nominativeArg

DN verbs: agreement target is the nominative OBJECT (not the dative subject). This is the key quirky-case agreement fact.

theorem Icelandic.Verbs.aa_default_agreement : vanta.agreementTarget = AgreementTarget.default3sg ∧ dreyma.agreementTarget = AgreementTarget.default3sg ∧ bresta.agreementTarget = AgreementTarget.default3sg

AA verbs (no nominative argument): default 3sg agreement.

theorem Icelandic.Verbs.an_agrees_with_object : syfja.agreementTarget = AgreementTarget.nominativeArg

AN verbs: agreement target is the nominative object.

theorem Icelandic.Verbs.quirky_with_nom_object_agrees : ((List.filter (fun (v : VerbCaseFrame) => v.firstObject == some Case.nom) quirkySubjectVerbs).all fun (v : VerbCaseFrame) => v.agreementTarget == AgreementTarget.nominativeArg) = true

Comprehensive: quirky verbs with NOM objects agree with that object.

theorem Icelandic.Verbs.quirky_without_nom_defaults : ((List.filter (fun (v : VerbCaseFrame) => v.firstObject != some Case.nom) quirkySubjectVerbs).all fun (v : VerbCaseFrame) => v.agreementTarget == AgreementTarget.default3sg) = true

Comprehensive: quirky verbs without any NOM argument default to 3sg.

theorem Icelandic.Verbs.quirky_passes_nine : have diagnostics := [SubjectDiagnostic.defaultPosition, SubjectDiagnostic.yesNoInversion, SubjectDiagnostic.blockExpletive, SubjectDiagnostic.reflexiveBinding, SubjectDiagnostic.longDistanceReflexive, SubjectDiagnostic.conjunctionReduction, SubjectDiagnostic.ecmEmbedding, SubjectDiagnostic.proControl, SubjectDiagnostic.extraction, SubjectDiagnostic.verbAgreement]; (List.filter SubjectDiagnostic.passedByQuirkySubject diagnostics).length = 9

Quirky subjects pass 9 of 10 diagnostics.

theorem Icelandic.Verbs.quirky_fails_only_agreement : SubjectDiagnostic.verbAgreement.passedByQuirkySubject = false ∧ SubjectDiagnostic.defaultPosition.passedByQuirkySubject = true ∧ SubjectDiagnostic.reflexiveBinding.passedByQuirkySubject = true ∧ SubjectDiagnostic.extraction.passedByQuirkySubject = true

Verb agreement is the only diagnostic quirky subjects fail.

theorem Icelandic.Verbs.ditrans_nom_subjects : (ditransitiveVerbs.all fun (v : VerbCaseFrame) => v.subjectCase == Case.nom) = true

All ditransitive verbs have nominative subjects.

theorem Icelandic.Verbs.six_ditrans_patterns : have patterns := List.map (fun (v : VerbCaseFrame) => (v.firstObject, v.secondObject)) ditransitiveVerbs; patterns.contains (some Case.dat, some Case.acc) = true ∧ patterns.contains (some Case.acc, some Case.dat) = true ∧ patterns.contains (some Case.dat, some Case.dat) = true ∧ patterns.contains (some Case.dat, some Case.gen) = true ∧ patterns.contains (some Case.acc, some Case.gen) = true ∧ patterns.contains (some Case.acc, some Case.acc) = true

All 6 attested ditransitive object patterns are represented.

theorem Icelandic.Verbs.dyadic_verb_count : allDyadicVerbs.length = 16

theorem Icelandic.Verbs.ditransitive_verb_count : ditransitiveVerbs.length = 9

theorem Icelandic.Verbs.leidast_is_quirky_dn : leidastCF.subjectCase = Case.dat ∧ leidastCF.firstObject = some Case.nom ∧ leidastCF.quirkySubject = true ∧ leidastCF.subjectCaseAssignment = Features.CaseAssignment.fixed

leiðast 'be bored' is both an -st verb AND a quirky-subject verb (DAT-NOM frame). The form and gloss match between this fragment and Predicates.lean — verified by inspection (structural link requires a study file that imports both).