Icelandic Case Fragment

@cite{thrainsson-2007} @cite{yip-maling-jackendoff-1987} @cite{zaenen-maling-thrainsson-1985}

Icelandic has 4 morphological cases: NOM, ACC, DAT, GEN. The signature phenomenon is quirky case: non-nominative subjects (DAT, ACC, rarely GEN) that pass virtually all standard subject diagnostics except verb agreement.

Case Frames (@cite{thrainsson-2007} §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 (@cite{yip-maling-jackendoff-1987}): 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 (@cite{thrainsson-2007} §4.1.2.1)

Oblique subjects pass 9 of 10 subject diagnostics (@cite{zaenen-maling-thrainsson-1985}, @cite{thrainsson-2007} §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 (@cite{thrainsson-2007} ex. 4.47).

Triadic (Ditransitive) Frames (@cite{thrainsson-2007} §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 (@cite{zaenen-maling-thrainsson-1985})

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 Core.Case.

def Fragments.Icelandic.Case.caseInventory : List Core.Case

Icelandic 4-case inventory (@cite{thrainsson-2007} §4.1).

Equations

• Fragments.Icelandic.Case.caseInventory = [Core.Case.nom, Core.Case.acc, Core.Case.gen, Core.Case.dat]

theorem Fragments.Icelandic.Case.inventory_valid : Core.validInventory caseInventory = true

Contiguous on Blake's hierarchy (ranks 6, 6, 5, 4).

structure Fragments.Icelandic.Case.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). @cite{thrainsson-2007} §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 : Core.Case

  Case of the subject (first argument)

• firstObject : Option Core.Case

  Case of the first post-verbal argument, if any

• secondObject : Option Core.Case

  Case of the second post-verbal argument, if any

• subjectCaseAssignment : Core.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.

def Fragments.Icelandic.Case.instReprVerbCaseFrame.repr : VerbCaseFrame → Nat → Std.Format

Equations

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

instance Fragments.Icelandic.Case.instReprVerbCaseFrame : Repr VerbCaseFrame

Equations

• Fragments.Icelandic.Case.instReprVerbCaseFrame = { reprPrec := Fragments.Icelandic.Case.instReprVerbCaseFrame.repr }

instance Fragments.Icelandic.Case.instBEqVerbCaseFrame : BEq VerbCaseFrame

Equations

• Fragments.Icelandic.Case.instBEqVerbCaseFrame = { beq := Fragments.Icelandic.Case.instBEqVerbCaseFrame.beq }

def Fragments.Icelandic.Case.instBEqVerbCaseFrame.beq : VerbCaseFrame → VerbCaseFrame → Bool

Equations

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

def Fragments.Icelandic.Case.VerbCaseFrame.quirkySubject (v : VerbCaseFrame) : Bool

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

Equations

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

def Fragments.Icelandic.Case.elska : VerbCaseFrame

elska 'love' — NA frame (@cite{thrainsson-2007} ex. 4.56a). Hann elskar hana. 'He(N) loves her(A).'

Equations

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

def Fragments.Icelandic.Case.lesa : VerbCaseFrame

lesa 'read' — NA frame (@cite{thrainsson-2007} ex. 4.56b). Hún las bókina. 'She(N) read book-the(A).'

Equations

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

def Fragments.Icelandic.Case.hjalpa : VerbCaseFrame

hjálpa 'help' — ND frame (@cite{thrainsson-2007} ex. 4.57a). Hún hjálpaði honum. 'She(N) helped him(D).'

Equations

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

def Fragments.Icelandic.Case.strauka : VerbCaseFrame

strauka 'pet' — ND frame (@cite{thrainsson-2007} ex. 4.57b). Ég strauk kettinum. 'I(N) petted cat-the(D).'

Equations

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

def Fragments.Icelandic.Case.kasta : VerbCaseFrame

kasta 'throw' — ND frame (@cite{thrainsson-2007} ex. 4.57c). Hann kastaði boltanum. 'He(N) threw ball-the(D).'

Equations

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

def Fragments.Icelandic.Case.sakna : VerbCaseFrame

sakna 'miss' — NG frame (@cite{thrainsson-2007} ex. 4.58a). Hann saknar hennar. 'He(N) misses her(G).'

Equations

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

def Fragments.Icelandic.Case.krefja : VerbCaseFrame

krefja 'demand' — NG frame (@cite{thrainsson-2007} ex. 4.58b). Ég krefst bóta. 'I(N) demand compensation(G).'

Equations

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

def Fragments.Icelandic.Case.lika : VerbCaseFrame

líka 'like' — DN frame (@cite{thrainsson-2007} 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

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

def Fragments.Icelandic.Case.batna : VerbCaseFrame

batna 'get better' — DN frame (@cite{thrainsson-2007} ex. 4.61c). Barninu batnaði veikin. 'Child-the(D) got-better sickness(N).'

Equations

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

def Fragments.Icelandic.Case.leidastCF : VerbCaseFrame

leiðast 'be bored' — DN frame (@cite{thrainsson-2007} ex. 4.61d). Stráknum leiddust kennararnir. 'Boy-the(D) bored(pl.) teachers-the(Npl.).' Also an -st verb (see Predicates.lean).

Equations

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

def Fragments.Icelandic.Case.askotnast : VerbCaseFrame

áskotnast 'get by luck' — DN frame (@cite{thrainsson-2007} ex. 4.61a). Mér áskotnuðust peningar. 'Me(D) lucked-onto(pl.) money(Npl.).'

Equations

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

def Fragments.Icelandic.Case.vanta : VerbCaseFrame

vanta 'lack/need' — AA frame (@cite{thrainsson-2007} ex. 4.60a). Hana vantar vinnu. 'Her(A) lacks work(A).'

Equations

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

def Fragments.Icelandic.Case.dreyma : VerbCaseFrame

dreyma 'dream' — AA frame (@cite{thrainsson-2007} ex. 4.60b). Mig dreymdi draum. 'Me(A) dreamt dream(A).'

Equations

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

def Fragments.Icelandic.Case.bresta : VerbCaseFrame

bresta 'fail (of courage)' — AA frame (@cite{thrainsson-2007} ex. 4.60c). Harald brast kjark. 'Harold(A) failed courage(A).'

Equations

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

def Fragments.Icelandic.Case.syfja : VerbCaseFrame

ACC-NOM impersonal — extremely rare, possibly one construction (@cite{thrainsson-2007} 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

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

def Fragments.Icelandic.Case.vera_kostur : VerbCaseFrame

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

Equations

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

def Fragments.Icelandic.Case.gefa : VerbCaseFrame

gefa 'give' — NDA frame (@cite{thrainsson-2007} ex. 4.63a). María gaf Haraldi bókina. 'Mary(N) gave Harold(D) book-the(A).' Most common ditransitive pattern (>220 verbs).

Equations

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

def Fragments.Icelandic.Case.segja : VerbCaseFrame

segja 'tell' — NDA frame (@cite{thrainsson-2007} ex. 4.62).

Equations

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

def Fragments.Icelandic.Case.svipta : VerbCaseFrame

svipta 'deprive' — NAD frame (@cite{thrainsson-2007} ex. 4.65a). Lögreglan svipti hann ökuleyfinu. 'Police-the(N) deprived him(A) driver's-licence-the(D).'

Equations

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

def Fragments.Icelandic.Case.leyna : VerbCaseFrame

leyna 'conceal' — NAD frame (@cite{thrainsson-2007} ex. 4.65b). Þeir leyndu hana sannleikanum. 'They(N) concealed her(A) truth-the(D).'

Equations

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

def Fragments.Icelandic.Case.lofa : VerbCaseFrame

lofa 'promise' — NDD frame (@cite{thrainsson-2007} ex. 4.72a). Ég lofaði henni því. 'I(N) promised her(D) it(D).'

Equations

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

def Fragments.Icelandic.Case.skila : VerbCaseFrame

skila 'return' — NDD frame (@cite{thrainsson-2007} ex. 4.72b). Hún skilaði mér bókinni. 'She(N) returned me(D) book-the(D).'

Equations

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

def Fragments.Icelandic.Case.spyrja : VerbCaseFrame

spyrja 'ask' — NAG frame (@cite{thrainsson-2007} ex. 4.70a). Þeir spurðu hana margra spurninga. 'They(N) asked her(A) many questions(G).'

Equations

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

def Fragments.Icelandic.Case.oska : VerbCaseFrame

óska 'wish' — NDG frame (@cite{thrainsson-2007} ex. 4.69a). Ég óska þér velfarnaðar. 'I(N) wish you(D) well-being(G).'

Equations

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

def Fragments.Icelandic.Case.kosta : VerbCaseFrame

kosta 'cost' — NAA frame (@cite{thrainsson-2007} 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

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

inductive Fragments.Icelandic.Case.SubjectDiagnostic : Type

The 10 standard subject diagnostics for Icelandic (@cite{thrainsson-2007} §4.1.1, @cite{zaenen-maling-thrainsson-1985}).

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

instance Fragments.Icelandic.Case.instDecidableEqSubjectDiagnostic : DecidableEq SubjectDiagnostic

Equations

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

instance Fragments.Icelandic.Case.instBEqSubjectDiagnostic : BEq SubjectDiagnostic

Equations

• Fragments.Icelandic.Case.instBEqSubjectDiagnostic = { beq := Fragments.Icelandic.Case.instBEqSubjectDiagnostic.beq }

def Fragments.Icelandic.Case.instBEqSubjectDiagnostic.beq : SubjectDiagnostic → SubjectDiagnostic → Bool

Equations

• Fragments.Icelandic.Case.instBEqSubjectDiagnostic.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

def Fragments.Icelandic.Case.instReprSubjectDiagnostic.repr : SubjectDiagnostic → Nat → Std.Format

Equations

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

instance Fragments.Icelandic.Case.instReprSubjectDiagnostic : Repr SubjectDiagnostic

Equations

• Fragments.Icelandic.Case.instReprSubjectDiagnostic = { reprPrec := Fragments.Icelandic.Case.instReprSubjectDiagnostic.repr }

def Fragments.Icelandic.Case.SubjectDiagnostic.passedByQuirkySubject : SubjectDiagnostic → Bool

Does a quirky (non-nominative) subject pass this diagnostic? Quirky subjects pass all diagnostics EXCEPT verb agreement (@cite{thrainsson-2007} §4.1.2.1).

Equations

• Fragments.Icelandic.Case.SubjectDiagnostic.verbAgreement.passedByQuirkySubject = false
• x✝.passedByQuirkySubject = true

inductive Fragments.Icelandic.Case.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 (@cite{thrainsson-2007} §4.1.2.1, ex. 4.47). When no nominative argument is present, default 3sg appears.

• nominativeArg : AgreementTarget
• default3sg : AgreementTarget

instance Fragments.Icelandic.Case.instDecidableEqAgreementTarget : DecidableEq AgreementTarget

Equations

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

instance Fragments.Icelandic.Case.instBEqAgreementTarget : BEq AgreementTarget

Equations

• Fragments.Icelandic.Case.instBEqAgreementTarget = { beq := Fragments.Icelandic.Case.instBEqAgreementTarget.beq }

def Fragments.Icelandic.Case.instBEqAgreementTarget.beq : AgreementTarget → AgreementTarget → Bool

Equations

• Fragments.Icelandic.Case.instBEqAgreementTarget.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

instance Fragments.Icelandic.Case.instReprAgreementTarget : Repr AgreementTarget

Equations

• Fragments.Icelandic.Case.instReprAgreementTarget = { reprPrec := Fragments.Icelandic.Case.instReprAgreementTarget.repr }

def Fragments.Icelandic.Case.instReprAgreementTarget.repr : AgreementTarget → Nat → Std.Format

Equations

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

def Fragments.Icelandic.Case.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 Fragments.Icelandic.Case.nomSubjectVerbs : List VerbCaseFrame

Dyadic verbs with nominative subjects.

Equations

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

def Fragments.Icelandic.Case.quirkySubjectVerbs : List VerbCaseFrame

Dyadic verbs with quirky (non-nominative) subjects.

Equations

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

def Fragments.Icelandic.Case.allDyadicVerbs : List VerbCaseFrame

All dyadic verb entries.

Equations

• Fragments.Icelandic.Case.allDyadicVerbs = Fragments.Icelandic.Case.nomSubjectVerbs ++ Fragments.Icelandic.Case.quirkySubjectVerbs

def Fragments.Icelandic.Case.ditransitiveVerbs : List VerbCaseFrame

Ditransitive verb entries.

Equations

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

def Fragments.Icelandic.Case.productiveDyadicPatterns : List (Core.Case × Core.Case)

The 5 productive dyadic case patterns in Icelandic (@cite{thrainsson-2007} §4.1.2.2, @cite{yip-maling-jackendoff-1987}). 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

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

theorem Fragments.Icelandic.Case.five_of_sixteen_productive : productiveDyadicPatterns.length = 5

theorem Fragments.Icelandic.Case.all_verbs_use_attested_pattern : have attested := productiveDyadicPatterns ++ [(Core.Case.acc, Core.Case.nom), (Core.Case.gen, Core.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 Fragments.Icelandic.Case.icelandic_has_four_cases : caseInventory.length = 4

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

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

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

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

theorem Fragments.Icelandic.Case.quirky_subjects_are_fixed : (quirkySubjectVerbs.all fun (v : VerbCaseFrame) => v.subjectCaseAssignment == Core.CaseAssignment.fixed) = true

Quirky subjects have fixed (lexical) case assignment.

theorem Fragments.Icelandic.Case.nom_subjects_are_derived : (nomSubjectVerbs.all fun (v : VerbCaseFrame) => v.subjectCaseAssignment == Core.CaseAssignment.derived) = true

Nominative subjects have derived (structural) case assignment.

theorem Fragments.Icelandic.Case.na_agrees_with_subject : elska.agreementTarget = AgreementTarget.nominativeArg

NA verbs: agreement target is the nominative subject.

theorem Fragments.Icelandic.Case.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 Fragments.Icelandic.Case.aa_default_agreement : vanta.agreementTarget = AgreementTarget.default3sg ∧ dreyma.agreementTarget = AgreementTarget.default3sg ∧ bresta.agreementTarget = AgreementTarget.default3sg

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

theorem Fragments.Icelandic.Case.an_agrees_with_object : syfja.agreementTarget = AgreementTarget.nominativeArg

AN verbs: agreement target is the nominative object.

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

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

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

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

theorem Fragments.Icelandic.Case.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 Fragments.Icelandic.Case.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 Fragments.Icelandic.Case.ditrans_nom_subjects : (ditransitiveVerbs.all fun (v : VerbCaseFrame) => v.subjectCase == Core.Case.nom) = true

All ditransitive verbs have nominative subjects.

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

All 6 attested ditransitive object patterns are represented.

theorem Fragments.Icelandic.Case.dyadic_verb_count : allDyadicVerbs.length = 16

theorem Fragments.Icelandic.Case.ditransitive_verb_count : ditransitiveVerbs.length = 9

theorem Fragments.Icelandic.Case.leidast_is_quirky_dn : leidastCF.subjectCase = Core.Case.dat ∧ leidastCF.firstObject = some Core.Case.nom ∧ leidastCF.quirkySubject = true ∧ leidastCF.subjectCaseAssignment = Core.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).