Béjar and Rezac 2003: person licensing and the Person Case Constraint

Béjar and Rezac derive the Person Case Constraint, that the direct object of two weak objects cannot be 1st or 2nd person, from the Person Licensing Condition, that an interpretable 1st/2nd person feature must enter an Agree relation with a functional category. A φ/Case head probes for person and then for number, each search halting at the closest nominal and Agreeing with it only if its Case is unvalued. A dative, whose Case its own preposition has valued, absorbs the person probe and displaces, so the number probe reaches the theme and values its Case while the theme's person goes unlicensed. Every repair adds a person probe: a theme above a prepositional dative, or in a dative–nominative construction the projection of T, once the nominative's φ-features have risen above the dative, as in French and Spanish but not in Icelandic.

Main definitions

• BejarRezac2003.Nominal: a φ-goal with whether its person feature is licensed.
• BejarRezac2003.Head: a φ/Case head, with the Case it assigns, its EPP, and whether its nominative's φ-features rise as a head.
• BejarRezac2003.Head.derive: the derivation of a head's domain.
• BejarRezac2003.PLC: the Person Licensing Condition.

Main results

• BejarRezac2003.applicative_derive: a dative is what its own preposition's derivation yields.
• BejarRezac2003.doc_plc_iff: the constraint in a double object construction.
• BejarRezac2003.pp_plc: the prepositional construction escapes it.
• BejarRezac2003.dnc_plc_iff: a dative–nominative construction obeys it iff the dative satisfies the EPP and the nominative's φ-features stay below it.

Implementation notes

The number probe values Case after the projection's person probe has searched, where the paper orders it before: valued Case would make the nominative inactive for that later search, which (17) requires to reach it, and in every configuration of the paper the number probe finds the same nominal either way. The displacement of the nominal that absorbs the person probe is taken as given, so the crash of (4), where the dative cannot displace, is not modelled. The prose on p. 55 swaps the two constructions of (11); the diagram, which agrees with the low prepositional dative of §2, is followed.

TODO

The general form of the conclusion, that a nominal with unvalued Case is licensed iff it is the closest match of the head's first or reprojected person probe, is stated only configuration by configuration. Causatives and restructuring (2), nominalizations, and focused pronouns (§4) are not modelled.

References

• [BR03]
• [Bon91]
• [Cho00]
• [Ana03]
• [HR02]
• [ZMT85]
• [Tar95]
• [Sig96]

structure BejarRezac2003.Nominalextends Minimalist.PhiGoal : Type

A nominal in the domain of a φ/Case head is a φ-goal together with whether its person feature has entered an Agree relation with a functional category.

• valuedCase : Option Case
• cell : Agreement.Bundle
• licensed : Bool

def BejarRezac2003.instDecidableEqNominal.decEq (x✝ x✝¹ : Nominal) : Decidable (x✝ = x✝¹)

Equations

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

@[instance_reducible]

instance BejarRezac2003.instDecidableEqNominal : DecidableEq Nominal

Equations

• BejarRezac2003.instDecidableEqNominal = BejarRezac2003.instDecidableEqNominal.decEq

def BejarRezac2003.instReprNominal.repr : Nominal → ℕ → Std.Format

Equations

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

@[instance_reducible]

instance BejarRezac2003.instReprNominal : Repr Nominal

Equations

• BejarRezac2003.instReprNominal = { reprPrec := BejarRezac2003.instReprNominal.repr }

def BejarRezac2003.Nominal.caseless (c : Agreement.Bundle) : Nominal

Nominal.caseless c is a nominal with φ-cell c, unvalued Case, and unlicensed person.

Equations

• BejarRezac2003.Nominal.caseless c = { toPhiGoal := Minimalist.PhiGoal.unvalued c, licensed := false }

def BejarRezac2003.Nominal.dat (c : Agreement.Bundle) : Nominal

Nominal.dat c is a dative, whose Case and person its own preposition has valued and licensed (§4).

Equations

• BejarRezac2003.Nominal.dat c = { toPhiGoal := Minimalist.PhiGoal.valued Case.dat c, licensed := true }

@[simp]

theorem BejarRezac2003.Nominal.isActive_caseless (c : Agreement.Bundle) : (caseless c).isActive = true

@[simp]

theorem BejarRezac2003.Nominal.isActive_dat (c : Agreement.Bundle) : (dat c).isActive = false

@[simp]

theorem BejarRezac2003.Nominal.cell_caseless (c : Agreement.Bundle) : (caseless c).cell = c

@[simp]

theorem BejarRezac2003.Nominal.cell_dat (c : Agreement.Bundle) : (dat c).cell = c

@[simp]

theorem BejarRezac2003.Nominal.licensed_caseless (c : Agreement.Bundle) : (caseless c).licensed = false

@[simp]

theorem BejarRezac2003.Nominal.licensed_dat (c : Agreement.Bundle) : (dat c).licensed = true

Agree

def BejarRezac2003.phiProbe : Minimalist.Probe Nominal

The person and the number probe of a φ/Case head halt at the closest nominal, since every nominal bears person and number ((8)), and Agree with it iff its Case is unvalued (§2).

Equations

• BejarRezac2003.phiProbe = Minimalist.Probe.ofInt fun (x : BejarRezac2003.Nominal) => x.isActive

def BejarRezac2003.agreeWith (f : Nominal → Nominal) (ns : List Nominal) : List Nominal

agreeWith f ns applies f to the goal phiProbe Agrees with in ns, the closest nominal if its Case is unvalued; an inactive closest nominal absorbs the probe ((9)).

Equations

• BejarRezac2003.agreeWith f ns = List.modifyHead (fun (n : BejarRezac2003.Nominal) => if n.isActive = true then f n else n) ns

theorem BejarRezac2003.agreeWith_eq (f : Nominal → Nominal) (ns : List Nominal) : agreeWith f ns = match phiProbe.agree ns with | some n => f n :: ns.tail | none => ns

agreeWith f updates exactly the goal phiProbe Agrees with.

def BejarRezac2003.piAgree : List Nominal → List Nominal

Agree for person licenses its goal's person feature.

Equations

• BejarRezac2003.piAgree = BejarRezac2003.agreeWith fun (n : BejarRezac2003.Nominal) => { toPhiGoal := n.toPhiGoal, licensed := true }

def BejarRezac2003.numAgree (c : Case) : List Nominal → List Nominal

Agree for number values its goal's Case with c. The inactive nominal that absorbed the person probe has displaced, cliticized or raised, and the number probe looks past its trace ((10), (16b)).

Equations

• One or more equations did not get rendered due to their size.
• BejarRezac2003.numAgree c [] = []

def BejarRezac2003.raise (can : Nominal → Bool) (ns : List Nominal) : List Nominal

raise can ns moves the closest nominal of ns satisfying can to the top (§5).

Equations

• BejarRezac2003.raise can ns = ((Minimalist.Probe.relativized can).search ns).toList ++ List.eraseP can ns

Heads and their derivations

structure BejarRezac2003.Head : Type

A φ/Case head assigns a Case, may bear an EPP feature satisfied by the closest nominal for which epp holds, and, in a language with pro-drop, has a nominative whose φ-features rise as a head above everything else (§5, §6).

• case : Case
• epp : Option (Nominal → Bool)
• agrX0 : Bool

def BejarRezac2003.Head.derive (F : Head) (ns : List Nominal) : List Nominal

The derivation of a head's domain. The person probe searches the base order; if the head has an EPP feature, the nominal satisfying it raises, a rising nominative φ-head raises above it, and the projection of the head probes again for person; the number probe values the head's Case last ((8)–(10), (16)–(17), (25)).

Equations

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

def BejarRezac2003.PLC (ns : List Nominal) : Prop

The Person Licensing Condition holds of a domain when every nominal with an interpretable 1st/2nd person feature has had it licensed (§3).

Equations

• BejarRezac2003.PLC ns = ∀ n ∈ ns, n.cell.IsParticipant → n.licensed = true

@[instance_reducible]

instance BejarRezac2003.instDecidablePredListNominalPLC : DecidablePred PLC

Equations

• BejarRezac2003.instDecidablePredListNominalPLC ns = BejarRezac2003.instDecidablePredListNominalPLC._aux_1 ns

def BejarRezac2003.applicative : Head

The applicative preposition assigns dative to its complement (§4).

Equations

• BejarRezac2003.applicative = { case := Case.dat }

def BejarRezac2003.v : Head

v assigns accusative (§3).

Equations

• BejarRezac2003.v = { case := Case.acc }

def BejarRezac2003.icelandicT : Head

Icelandic T has an EPP feature that a dative can satisfy (§5).

Equations

• BejarRezac2003.icelandicT = { case := Case.nom, epp := some fun (x : BejarRezac2003.Nominal) => true }

def BejarRezac2003.frenchT : Head

French T has an EPP feature that a dative cannot satisfy (§5).

Equations

• BejarRezac2003.frenchT = { case := Case.nom, epp := some fun (x : BejarRezac2003.Nominal) => x.valuedCase != some Case.dat }

def BejarRezac2003.spanishT : Head

Spanish T has an EPP feature that a dative can satisfy, and its nominative's φ-features rise as a head above the dative (§6).

Equations

• BejarRezac2003.spanishT = { case := Case.nom, epp := some fun (x : BejarRezac2003.Nominal) => true, agrX0 := true }

The preposition's own domain

theorem BejarRezac2003.applicative_derive (c : Agreement.Bundle) : applicative.derive [Nominal.caseless c] = [Nominal.dat c]

A dative is the nominal its own preposition's derivation yields, inherent Case being structural Case valued under Agree with the preposition (§4).

The double object and prepositional constructions

theorem BejarRezac2003.v_derive_doc (cd ca : Agreement.Bundle) : v.derive [Nominal.dat cd, Nominal.caseless ca] = [Nominal.dat cd, { toPhiGoal := Minimalist.PhiGoal.valued Case.acc ca, licensed := false }]

In a double object construction the dative absorbs v's person probe and the number probe values accusative on the theme, whose person stays unlicensed ((8)–(10)).

theorem BejarRezac2003.doc_plc_iff (cd ca : Agreement.Bundle) : PLC (v.derive [Nominal.dat cd, Nominal.caseless ca]) ↔ ¬ca.IsParticipant

The double object construction obeys the condition iff its theme is 3rd person, whatever the dative ((1), (7)).

theorem BejarRezac2003.v_derive_pp (ct cg : Agreement.Bundle) : v.derive [Nominal.caseless ct, Nominal.dat cg] = [{ toPhiGoal := Minimalist.PhiGoal.valued Case.acc ct, licensed := true }, Nominal.dat cg]

In the prepositional construction the theme is v's closest nominal and both its probes reach it ((11a)).

theorem BejarRezac2003.pp_plc (ct cg : Agreement.Bundle) : PLC (v.derive [Nominal.caseless ct, Nominal.dat cg])

The prepositional construction obeys the condition whatever the theme's person ((3)).

Dative–nominative constructions

theorem BejarRezac2003.icelandicT_derive (cd cn : Agreement.Bundle) : icelandicT.derive [Nominal.dat cd, Nominal.caseless cn] = [Nominal.dat cd, { toPhiGoal := Minimalist.PhiGoal.valued Case.nom cn, licensed := false }]

In Icelandic the dative stays the highest φ-bearer, absorbing both of T's person probes, and the nominative gets only T's number ((12), (25c)).

theorem BejarRezac2003.frenchT_derive (cd cn : Agreement.Bundle) : frenchT.derive [Nominal.dat cd, Nominal.caseless cn] = [{ toPhiGoal := Minimalist.PhiGoal.valued Case.nom cn, licensed := true }, Nominal.dat cd]

In French the nominative moves over the dative to Spec,TP, and the projection of T licenses its person ((16), (17), (25b)).

theorem BejarRezac2003.spanishT_derive (cd cn : Agreement.Bundle) : spanishT.derive [Nominal.dat cd, Nominal.caseless cn] = [{ toPhiGoal := Minimalist.PhiGoal.valued Case.nom cn, licensed := true }, Nominal.dat cd]

In Spanish the dative is in Spec,TP, but the nominative's φ-features rise as a head above it and the projection of T licenses its person ((25a)).

theorem BejarRezac2003.dnc_plc_iff (can : Nominal → Bool) (hcan : ∀ (c : Agreement.Bundle), can (Nominal.caseless c) = true) (x0 : Bool) (cd cn : Agreement.Bundle) : PLC ({ case := Case.nom, epp := some can, agrX0 := x0 }.derive [Nominal.dat cd, Nominal.caseless cn]) ↔ can (Nominal.dat cd) = true ∧ x0 = false → ¬cn.IsParticipant

A dative–nominative construction obeys the condition iff its nominative is 3rd person or the nominative's φ-features end up above the dative, because the dative cannot satisfy the EPP or the φ-features rise as a head (§5, §6).