Marantz (1991): Case and Licensing

Marantz develops a theory of morphological case. Noun phrases are licensed by projection and the requirement that clauses have subjects, and case is read off the finished structure afterwards. A case affix takes the first case it is eligible for in a disjunctive hierarchy: a case determined by a lexical head, then a dependent case, then the unmarked case of its environment, then a default. The dependent cases are accusative and ergative. The verb with its inflection assigns one to a position it governs when another position it governs holds a distinct chain that no lexical head has marked, the accusative downward to the object and the ergative upward to the subject.

Case goes to chains, not to positions. A subject that has moved from the object position is one chain with its trace, so there is no second chain for a dependent case to be assigned against. This one fact covers both what Burzio's generalization says about the accusative and what the paper calls the ergative generalization, that a derived subject is never ergative. Whether the subject position is thematic plays no part: a raised subject over a distinct object, as with strike, leaves the object accusative. An unergative clause has an unfilled object position, and languages differ in whether it counts as a position to assign the ergative against: Georgian and Basque always count it, Hindi may, Inuktitut never does.

The split ergativity of Georgian follows. The inflection of the first series assigns dependent case downward and that of the second upward, while the agreement on the inflection finds its controller in the same way in both, taking the subject unless a lexical head has marked it and the object otherwise.

Main declarations

• Clause: a clause as the case rules see it, by what its subject and object positions hold; Clause.chains lists its chains.
• Clause.subject, Clause.object: the case of the two chains under given rules.
• Setting: the rules of an inflection, the visibility of unfilled positions and the names the language gives the cases; georgian, hindi, basque, inuktitut.
• Clause.agr: the position the agreement of the paper's (31) takes its features from.

Main results

• Clause.subject_dependent_iff, Clause.object_dependent_iff: when each position has dependent case, the paper's (30).
• Clause.ergative_generalization: a subject moved from the object position has no dependent case, whatever the rules.
• Clause.not_burzio: a clause with a non-thematic subject position and an accusative object.
• subject_rows, object_rows: the cases of the paper's Georgian, Hindi and Basque examples.
• georgian_subject_eq_pattern, georgian_object_eq_pattern, georgian_agr: the rules derive the case marking and the Set A agreement of the Georgian fragment in the first two series.
• ecm: the embedded subject and object of an exceptional case marking clause are both accusative.

Implementation notes

The argument that *It arrived the man fails for want of a subject and not for want of Case, and the residue of Case theory that governs PRO, are not formalized. Default case is not modelled apart from unmarked case. The rules of Syntax/Case/Dependent.lean count a noun phrase as a competitor while it is caseless, where the paper asks only that no lexical head has marked it; the two agree when the domains of a sentence are run from the lowest up, as they are in ecm. The third series of Georgian is outside the paper.

References

• [Mar91]

Clauses and their chains

inductive Marantz1991.ObjectPosition : Type

What the object position governed by the verb and its inflection holds.

• chain (lexicalCase : Option Case) : ObjectPosition

  A chain distinct from the subject's, with any case a lexical head determines on it.

• trace : ObjectPosition

  A link of the subject's chain, the subject having moved from here.

• unfilled : ObjectPosition

  Nothing, as in an unergative clause.

def Marantz1991.instDecidableEqObjectPosition.decEq (x✝ x✝¹ : ObjectPosition) : Decidable (x✝ = x✝¹)

Equations

• Marantz1991.instDecidableEqObjectPosition.decEq (Marantz1991.ObjectPosition.chain a) (Marantz1991.ObjectPosition.chain b) = if h : a = b then h ▸ isTrue ⋯ else isFalse ⋯
• Marantz1991.instDecidableEqObjectPosition.decEq (Marantz1991.ObjectPosition.chain lexicalCase) Marantz1991.ObjectPosition.trace = isFalse ⋯
• Marantz1991.instDecidableEqObjectPosition.decEq (Marantz1991.ObjectPosition.chain lexicalCase) Marantz1991.ObjectPosition.unfilled = isFalse ⋯
• Marantz1991.instDecidableEqObjectPosition.decEq Marantz1991.ObjectPosition.trace (Marantz1991.ObjectPosition.chain lexicalCase) = isFalse ⋯
• Marantz1991.instDecidableEqObjectPosition.decEq Marantz1991.ObjectPosition.trace Marantz1991.ObjectPosition.trace = isTrue ⋯
• Marantz1991.instDecidableEqObjectPosition.decEq Marantz1991.ObjectPosition.trace Marantz1991.ObjectPosition.unfilled = isFalse Marantz1991.instDecidableEqObjectPosition.decEq._proof_7
• Marantz1991.instDecidableEqObjectPosition.decEq Marantz1991.ObjectPosition.unfilled (Marantz1991.ObjectPosition.chain lexicalCase) = isFalse ⋯
• Marantz1991.instDecidableEqObjectPosition.decEq Marantz1991.ObjectPosition.unfilled Marantz1991.ObjectPosition.trace = isFalse Marantz1991.instDecidableEqObjectPosition.decEq._proof_9
• Marantz1991.instDecidableEqObjectPosition.decEq Marantz1991.ObjectPosition.unfilled Marantz1991.ObjectPosition.unfilled = isTrue ⋯

@[instance_reducible]

instance Marantz1991.instDecidableEqObjectPosition : DecidableEq ObjectPosition

Equations

• Marantz1991.instDecidableEqObjectPosition = Marantz1991.instDecidableEqObjectPosition.decEq

@[instance_reducible]

instance Marantz1991.instReprObjectPosition : Repr ObjectPosition

Equations

• Marantz1991.instReprObjectPosition = { reprPrec := Marantz1991.instReprObjectPosition.repr }

def Marantz1991.instReprObjectPosition.repr : ObjectPosition → ℕ → Std.Format

Equations

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

structure Marantz1991.Clause : Type

A clause as the case rules see it.

• thematicSubject : Bool

  The subject position is thematic, so that an argument is projected into it.

• subjectCase : Option Case

  The case a lexical head determines on the chain in subject position.

• object : ObjectPosition

  What the object position holds.

@[instance_reducible]

instance Marantz1991.instDecidableEqClause : DecidableEq Clause

Equations

• Marantz1991.instDecidableEqClause = Marantz1991.instDecidableEqClause.decEq

def Marantz1991.instDecidableEqClause.decEq (x✝ x✝¹ : Clause) : Decidable (x✝ = x✝¹)

Equations

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

@[instance_reducible]

instance Marantz1991.instReprClause : Repr Clause

Equations

• Marantz1991.instReprClause = { reprPrec := Marantz1991.instReprClause.repr }

def Marantz1991.instReprClause.repr : Clause → ℕ → Std.Format

Equations

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

def Marantz1991.Clause.transitive : Clause

A transitive clause.

Equations

• Marantz1991.Clause.transitive = { thematicSubject := true, subjectCase := none, object := Marantz1991.ObjectPosition.chain none }

def Marantz1991.Clause.unergative : Clause

An unergative clause.

Equations

• Marantz1991.Clause.unergative = { thematicSubject := true, subjectCase := none, object := Marantz1991.ObjectPosition.unfilled }

def Marantz1991.Clause.unaccusative : Clause

An unaccusative or passive clause, whose subject has moved from the object position.

Equations

• Marantz1991.Clause.unaccusative = { thematicSubject := false, subjectCase := none, object := Marantz1991.ObjectPosition.trace }

def Marantz1991.Clause.psych (c : Case) : Clause

A clause whose subject is derived from inside the verb phrase and bears a lexical case, over an object, as with the dative-subject psychological verbs of Georgian.

Equations

• Marantz1991.Clause.psych c = { thematicSubject := false, subjectCase := some c, object := Marantz1991.ObjectPosition.chain none }

def Marantz1991.Clause.raising : Clause

A clause whose non-thematic subject position is filled by a chain distinct from the object's, as in Elmer struck her as being too stubborn.

Equations

• Marantz1991.Clause.raising = { thematicSubject := false, subjectCase := none, object := Marantz1991.ObjectPosition.chain none }

def Marantz1991.Clause.chains (c : Clause) (v : Bool) : List (Option Case)

The chains with a link in a position the verb and its inflection govern, highest first, each given by the case a lexical head has valued on it, if any. An unfilled object position is listed when the language sees it.

Equations

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

def Marantz1991.Clause.subject (c : Clause) (r : DependentCase.Rules) (v : Bool) : Option (Case × Case.Mechanism)

The case of the subject's chain, with what valued it.

Equations

• c.subject r v = (List.map (fun (x : Option Case × Option (Case × Case.Mechanism)) => x.2) (r.assign id (c.chains v))).headD none

def Marantz1991.Clause.object? (c : Clause) (r : DependentCase.Rules) (v : Bool) : Option (Case × Case.Mechanism)

The case of the object's chain, with what valued it, where there is one.

Equations

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

theorem Marantz1991.Clause.subject_of_lexical (c : Clause) (r : DependentCase.Rules) (v : Bool) {l : Case} (h : c.subjectCase = some l) : c.subject r v = some (l, Case.Mechanism.lexical)

A case a lexical head determines is kept, under any rules.

theorem Marantz1991.Clause.subject_dependent_iff (c : Clause) (r : DependentCase.Rules) (v : Bool) : Option.map (fun (x : Case × Case.Mechanism) => x.2) (c.subject r v) = some Case.Mechanism.dependent ↔ c.subjectCase = none ∧ r.high.isSome = true ∧ (c.object = ObjectPosition.chain none ∨ c.object = ObjectPosition.unfilled ∧ v = true)

The subject has dependent case exactly when no lexical head has marked it, the rules assign a dependent case upward, and the object position holds a distinct unmarked chain or is unfilled and seen.

theorem Marantz1991.Clause.object_dependent_iff (c : Clause) (r : DependentCase.Rules) (v : Bool) : Option.map (fun (x : Case × Case.Mechanism) => x.2) (c.object? r v) = some Case.Mechanism.dependent ↔ c.subjectCase = none ∧ c.object = ObjectPosition.chain none ∧ r.low.isSome = true

The object has dependent case exactly when it is a distinct chain no lexical head has marked, the subject's chain is unmarked too, and the rules assign a dependent case downward.

theorem Marantz1991.Clause.ergative_generalization (c : Clause) (r : DependentCase.Rules) (v : Bool) (h : c.object = ObjectPosition.trace) : Option.map (fun (x : Case × Case.Mechanism) => x.2) (c.subject r v) ≠ some Case.Mechanism.dependent

The ergative generalization holds under any rules, since a subject moved from the object position has no dependent case.

theorem Marantz1991.Clause.not_burzio (v : Bool) : raising.thematicSubject = false ∧ raising.object? (DependentCase.Rules.ofAlignment Alignment.AlignmentType.accusative) v = some (Case.acc, Case.Mechanism.dependent)

Burzio's generalization does not hold of case, since the object of a clause with a non-thematic subject position is accusative when the subject's chain is distinct from it.

Settings of a language

inductive Marantz1991.Visibility : Type

Whether a language sees an unfilled object position as a position to assign dependent case against.

• always : Visibility
• optionally : Visibility
• never : Visibility

@[instance_reducible]

instance Marantz1991.instDecidableEqVisibility : DecidableEq Visibility

Equations

• Marantz1991.instDecidableEqVisibility x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Marantz1991.instReprVisibility.repr : Visibility → ℕ → Std.Format

Equations

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

@[instance_reducible]

instance Marantz1991.instReprVisibility : Repr Visibility

Equations

• Marantz1991.instReprVisibility = { reprPrec := Marantz1991.instReprVisibility.repr }

def Marantz1991.Visibility.settings : Visibility → Finset Bool

The ways a language may treat the unfilled position of a given clause.

Equations

• Marantz1991.Visibility.always.settings = {true}
• Marantz1991.Visibility.optionally.settings = {true, false}
• Marantz1991.Visibility.never.settings = {false}

structure Marantz1991.Setting : Type

A setting is what decides the case of the chains of a clause, namely the rules of its inflection, the visibility of unfilled positions, and the names the language gives the cases.

• rules : DependentCase.Rules
• unfilled : Visibility
• spellOut : Case → Case

def Marantz1991.Setting.subjectCases (g : Setting) (c : Clause) : Finset (Option Case)

The cases the subject may have.

Equations

• g.subjectCases c = Finset.image (fun (v : Bool) => Option.map (fun (x : Case × Case.Mechanism) => g.spellOut x.1) (c.subject g.rules v)) g.unfilled.settings

def Marantz1991.Setting.objectCases (g : Setting) (c : Clause) : Finset (Option Case)

The cases the object may have.

Equations

• g.objectCases c = Finset.image (fun (v : Bool) => Option.map (fun (x : Case × Case.Mechanism) => g.spellOut x.1) (c.object? g.rules v)) g.unfilled.settings

def Marantz1991.alignment : Georgian.Series → Alignment.AlignmentType

The direction in which the inflection of a Georgian series assigns dependent case, downward in the first series and upward in the second. The paper does not treat the third series, which is given the value of the first.

Equations

• Marantz1991.alignment Georgian.Series.aorist = Alignment.AlignmentType.ergative
• Marantz1991.alignment Georgian.Series.present = Alignment.AlignmentType.accusative
• Marantz1991.alignment Georgian.Series.perfect = Alignment.AlignmentType.accusative

def Marantz1991.georgian (s : Georgian.Series) : Setting

Georgian always sees an unfilled position. Its dative is what the accusative has fallen together with, and its nominative is the unmarked case under either direction.

Equations

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

def Marantz1991.hindi (a : Aspect.Perfectivity) : Setting

Hindi sees an unfilled position optionally, and its unmarked case is the nominative.

Equations

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

def Marantz1991.basque : Setting

Basque assigns the ergative in every tense and always sees an unfilled position.

Equations

• Marantz1991.basque = { rules := DependentCase.Rules.ofAlignment Alignment.AlignmentType.ergative, unfilled := Marantz1991.Visibility.always }

def Marantz1991.inuktitut : Setting

Inuktitut assigns the ergative and never sees an unfilled position.

Equations

• Marantz1991.inuktitut = { rules := DependentCase.Rules.ofAlignment Alignment.AlignmentType.ergative, unfilled := Marantz1991.Visibility.never }

theorem Marantz1991.unergative_subjectCases : basque.subjectCases Clause.unergative = {some Case.erg} ∧ (hindi Aspect.Perfectivity.perfective).subjectCases Clause.unergative = {some Case.erg, some Case.nom} ∧ inuktitut.subjectCases Clause.unergative = {some Case.abs}

The subject of an unergative clause is ergative in Basque, ergative or not in the Hindi perfect, and never ergative in Inuktitut.

The examples

def Marantz1991.setting? (e : Datum) : Option Setting

The setting of an example, by its language and the inflection the paper notes.

Equations

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

def Marantz1991.clause? (e : Datum) : Option Clause

The clause of an example.

Equations

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

def Marantz1991.case? (e : Datum) (key : String) : Option Case

The case an example shows on its subject or object.

Equations

• Marantz1991.case? e key = e.parse? key [("NOM", Case.nom), ("ERG", Case.erg), ("DAT", Case.dat), ("ABS", Case.abs)]

theorem Marantz1991.subject_rows (e : Datum) : e ∈ Examples.all → ∃ g ∈ setting? e, ∃ c ∈ clause? e, ∃ s ∈ case? e "subject", e.judgment = Judgment.acceptable ↔ some s ∈ g.subjectCases c

An example is acceptable exactly when the case of its subject is one the setting of its language gives the subject of its clause. This covers the ergative on Georgian and Basque unergatives, its optionality in Hindi, and its absence from unaccusatives in all three.

theorem Marantz1991.object_rows (e : Datum) : e ∈ Examples.all → ∀ o ∈ case? e "object", ∃ g ∈ setting? e, ∃ c ∈ clause? e, g.objectCases c = {some o}

The case of the object of an example is the one its setting gives.

Georgian

def Marantz1991.clause : Georgian.VerbClass → Clause

The clause of each Georgian verb class. The intransitives have derived subjects, the medials are unergative, and the indirect verbs have a derived dative subject over an object.

Equations

• Marantz1991.clause Georgian.VerbClass.transitive = Marantz1991.Clause.transitive
• Marantz1991.clause Georgian.VerbClass.intransitive = Marantz1991.Clause.unaccusative
• Marantz1991.clause Georgian.VerbClass.medial = Marantz1991.Clause.unergative
• Marantz1991.clause Georgian.VerbClass.indirect = Marantz1991.Clause.psych Case.dat

def Marantz1991.series : List Georgian.Series

The two series the paper treats.

Equations

• Marantz1991.series = [Georgian.Series.present, Georgian.Series.aorist]

theorem Marantz1991.georgian_subject_eq_pattern (v : Georgian.VerbClass) (s : Georgian.Series) : s ∈ series → (georgian s).subjectCases (clause v) = {some (Georgian.pattern v s).subject.case.label}

The rules derive the subject case of the Fragment for every class in both series.

theorem Marantz1991.georgian_object_eq_pattern (v : Georgian.VerbClass) : v ∈ [Georgian.VerbClass.transitive, Georgian.VerbClass.indirect] → ∀ s ∈ series, (georgian s).objectCases (clause v) = {some (Georgian.pattern v s).directObject.case.label}

The rules derive the object case of the Fragment for the two classes with an object.

Agreement across the split

inductive Marantz1991.Position : Type

The positions the verb and its inflection govern.

• subject : Position
• object : Position

@[instance_reducible]

instance Marantz1991.instDecidableEqPosition : DecidableEq Position

Equations

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

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

Equations

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

@[instance_reducible]

instance Marantz1991.instReprPosition : Repr Position

Equations

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

def Marantz1991.Clause.agr (c : Clause) : Option Position

The position the agreement of the paper's (31) takes its features from, or none for the default third person singular. Dependent agreement upward and unmarked agreement both pass over a chain a lexical head has marked, so the agreement goes to the subject unless it is so marked, and then to the object. The direction of dependent case plays no part.

Equations

• c.agr = if c.subjectCase = none then some Marantz1991.Position.subject else if c.object = Marantz1991.ObjectPosition.chain none then some Marantz1991.Position.object else none

theorem Marantz1991.georgian_agr (v : Georgian.VerbClass) (s : Georgian.Series) : s ∈ series → ((Georgian.pattern v s).subject.affixes = some Georgian.AffixSet.A ↔ (clause v).agr = some Position.subject) ∧ ((Georgian.pattern v s).directObject.affixes = some Georgian.AffixSet.A ↔ (clause v).agr = some Position.object)

The Fragment's Set A, the suffixal agreement, marks the argument the agreement of (31) picks in both series, which is the nominative subject, the ergative subject, or the nominative object of a verb with a dative subject.

Exceptional case marking

inductive Marantz1991.ECMArgument : Type

The noun phrases of I consider him to have discovered her.

• matrixSubject : ECMArgument
• embeddedSubject : ECMArgument
• embeddedObject : ECMArgument

@[instance_reducible]

instance Marantz1991.instDecidableEqECMArgument : DecidableEq ECMArgument

Equations

• Marantz1991.instDecidableEqECMArgument x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Marantz1991.instReprECMArgument.repr : ECMArgument → ℕ → Std.Format

Equations

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

@[instance_reducible]

instance Marantz1991.instReprECMArgument : Repr ECMArgument

Equations

• Marantz1991.instReprECMArgument = { reprPrec := Marantz1991.instReprECMArgument.repr }

theorem Marantz1991.ecm : have r := DependentCase.Rules.ofAlignment Alignment.AlignmentType.accusative; List.map (fun (x : ECMArgument × Option (Case × Case.Mechanism)) => Option.map (fun (x : Case × Case.Mechanism) => x.1) x.2) (r.unmarkedPass (fun (x : ECMArgument) => true) (r.dependentPass (fun (x : ECMArgument) => decide (x ≠ ECMArgument.embeddedObject)) (r.dependentPass (fun (x : ECMArgument) => decide (x ≠ ECMArgument.matrixSubject)) (Case.lexicalValuation (fun (x : ECMArgument) => none) [ECMArgument.matrixSubject, ECMArgument.embeddedSubject, ECMArgument.embeddedObject])))) = [some Case.nom, some Case.acc, some Case.acc]

The embedded subject is accusative against the matrix subject and the embedded object against the embedded subject, so an accusative does not depend on a nominative having been assigned in its clause.