Possessor extraction and categorical subject in Tseltalan

Aissen and Polian argue that a Tseltalan possessor never Ā-subextracts: nominal opacity, a Keine horizon at N⁰ for the wh-probe on C⁰, forces an extracted possessor to A-move first to Spec,TP or Spec,ApplP, where Attract Closest over DPs decides whether it can — a specific possessive's D layer, an agent, a specific subject or theme, or an occupied Spec,ApplP stops it. Hence only non-specific possessums strand, and the possessor that reaches Spec,TP is the ψ-subject of a categorical judgment.

Nominal opacity is the profile nominalOpacity read through Invisible, Attract Closest is isClosestGoalIn over D leaves on the paper's structures, judgment reads the judgment type off the same search, and the paper's examples are the rows, over which stranding_iff, piedPiping_specific and psi_no_piedPiping hold.

References

• [AP25]
• [Kei19]
• [Kur72]
• [Lit20a]
• [Pol13a]
• [Gav00]
• [Ais96]
• [CBL21]
• [HD03]

Probes

def AissenPolian2025.nominalOpacity : Minimalist.Probe.Profile

Nominal opacity: the wh-probe on C⁰ has every node in the extended projection of N⁰ as its horizon, [wh]C⁰ ⊣‖ N.

Equations

• AissenPolian2025.nominalOpacity = { probeHead := Minimalist.Cat.C, horizon := some Minimalist.Cat.N }

def AissenPolian2025.dProbeT : Minimalist.Probe.Profile

The [EPP:D] probe on T⁰, without horizon.

Equations

• AissenPolian2025.dProbeT = { probeHead := Minimalist.Cat.T, horizon := none }

def AissenPolian2025.dProbeAppl : Minimalist.Probe.Profile

The [EPP:D] probe on Appl⁰, without horizon.

Equations

• AissenPolian2025.dProbeAppl = { probeHead := Minimalist.Cat.Appl, horizon := none }

def AissenPolian2025.secondaryWh : Minimalist.Probe.Profile

The [EPP:WH] probe on D⁰ that drives pied-piping with inversion, without horizon.

Equations

• AissenPolian2025.secondaryWh = { probeHead := Minimalist.Cat.D, horizon := none }

def AissenPolian2025.Invisible (p : Minimalist.Probe.Profile) (root probe target : Minimalist.SyntacticObject) : Prop

target is invisible to a probe with profile p sitting at probe when it lies behind the profile's horizon.

Equations

• AissenPolian2025.Invisible p root probe target = ∃ h ∈ p.horizon, root.behindHorizonIn probe target h

theorem AissenPolian2025.invisible_iff_behindHorizon (h : Minimalist.Cat) (root probe target : Minimalist.SyntacticObject) {p : Minimalist.Probe.Profile} (hp : p.horizon = some h) : Invisible p root probe target ↔ root.behindHorizonIn probe target h

theorem AissenPolian2025.not_invisible_of_horizon_none (root probe target : Minimalist.SyntacticObject) {p : Minimalist.Probe.Profile} (hp : p.horizon = none) : ¬Invisible p root probe target

A probe without horizon sees everything in its domain.

theorem AissenPolian2025.dProbe_sees_through (root probe target : Minimalist.SyntacticObject) : ¬Invisible dProbeT root probe target ∧ ¬Invisible dProbeAppl root probe target ∧ ¬Invisible secondaryWh root probe target

The structures

def AissenPolian2025.C₀ : Minimalist.PlanarSyntacticObject

Equations

• AissenPolian2025.C₀ = ↑{ item := Minimalist.LexicalItem.of Minimalist.Cat.C [], id := 1 }

def AissenPolian2025.T₀ : Minimalist.PlanarSyntacticObject

Equations

• AissenPolian2025.T₀ = ↑{ item := Minimalist.LexicalItem.of Minimalist.Cat.T [], id := 2 }

def AissenPolian2025.V₀ : Minimalist.PlanarSyntacticObject

Equations

• AissenPolian2025.V₀ = ↑{ item := Minimalist.LexicalItem.of Minimalist.Cat.V [], id := 3 }

def AissenPolian2025.v₀ : Minimalist.PlanarSyntacticObject

Equations

• AissenPolian2025.v₀ = ↑{ item := Minimalist.LexicalItem.of Minimalist.Cat.v [], id := 4 }

def AissenPolian2025.Appl₀ : Minimalist.PlanarSyntacticObject

Equations

• AissenPolian2025.Appl₀ = ↑{ item := Minimalist.LexicalItem.of Minimalist.Cat.Appl [], id := 5 }

def AissenPolian2025.P₀ : Minimalist.PlanarSyntacticObject

Equations

• AissenPolian2025.P₀ = ↑{ item := Minimalist.LexicalItem.of Minimalist.Cat.P [], id := 6 }

def AissenPolian2025.Psr : Minimalist.PlanarSyntacticObject

Equations

• AissenPolian2025.Psr = ↑{ item := Minimalist.LexicalItem.of Minimalist.Cat.D [], id := 7 }

def AissenPolian2025.Psm : Minimalist.PlanarSyntacticObject

Equations

• AissenPolian2025.Psm = ↑{ item := Minimalist.LexicalItem.of Minimalist.Cat.N [], id := 8 }

def AissenPolian2025.D₀ : Minimalist.PlanarSyntacticObject

Equations

• AissenPolian2025.D₀ = ↑{ item := Minimalist.LexicalItem.of Minimalist.Cat.D [], id := 9 }

def AissenPolian2025.Agt : Minimalist.PlanarSyntacticObject

Equations

• AissenPolian2025.Agt = ↑{ item := Minimalist.LexicalItem.of Minimalist.Cat.D [], id := 10 }

def AissenPolian2025.SubjD : Minimalist.PlanarSyntacticObject

Equations

• AissenPolian2025.SubjD = ↑{ item := Minimalist.LexicalItem.of Minimalist.Cat.D [], id := 11 }

def AissenPolian2025.SubjN : Minimalist.PlanarSyntacticObject

Equations

• AissenPolian2025.SubjN = ↑{ item := Minimalist.LexicalItem.of Minimalist.Cat.N [], id := 12 }

def AissenPolian2025.ThemeD : Minimalist.PlanarSyntacticObject

Equations

• AissenPolian2025.ThemeD = ↑{ item := Minimalist.LexicalItem.of Minimalist.Cat.D [], id := 13 }

def AissenPolian2025.ThemeN : Minimalist.PlanarSyntacticObject

Equations

• AissenPolian2025.ThemeN = ↑{ item := Minimalist.LexicalItem.of Minimalist.Cat.N [], id := 14 }

def AissenPolian2025.Pivot : Minimalist.PlanarSyntacticObject

Equations

• AissenPolian2025.Pivot = ↑{ item := Minimalist.LexicalItem.of Minimalist.Cat.N [], id := 15 }

def AissenPolian2025.PossP : Minimalist.PlanarSyntacticObject

A non-specific possessive, {Psr, Psm}.

Equations

• AissenPolian2025.PossP = {AissenPolian2025.Psr, AissenPolian2025.Psm}

def AissenPolian2025.DP : Minimalist.PlanarSyntacticObject

A specific possessive, {D⁰, PossP}.

Equations

• AissenPolian2025.DP = {AissenPolian2025.D₀, AissenPolian2025.PossP}

def AissenPolian2025.PP : Minimalist.PlanarSyntacticObject

A locative PP over a non-specific possessive, {P, PossP}.

Equations

• AissenPolian2025.PP = {AissenPolian2025.P₀, AissenPolian2025.PossP}

def AissenPolian2025.unaccPossP : Minimalist.PlanarSyntacticObject

(9c) with a non-specific possessive S_O.

Equations

• AissenPolian2025.unaccPossP = {AissenPolian2025.T₀, {AissenPolian2025.V₀, AissenPolian2025.PossP}}

def AissenPolian2025.unaccDP : Minimalist.PlanarSyntacticObject

(9c) with a specific possessive S_O.

Equations

• AissenPolian2025.unaccDP = {AissenPolian2025.T₀, {AissenPolian2025.V₀, AissenPolian2025.DP}}

def AissenPolian2025.transPossP : Minimalist.PlanarSyntacticObject

(9a) with a non-specific possessive O.

Equations

• AissenPolian2025.transPossP = {AissenPolian2025.T₀, {AissenPolian2025.Agt, {AissenPolian2025.v₀, {AissenPolian2025.V₀, AissenPolian2025.PossP}}}}

def AissenPolian2025.raisingAppl : Minimalist.PlanarSyntacticObject

(29) the raising applicative under T⁰.

Equations

• AissenPolian2025.raisingAppl = {AissenPolian2025.T₀, {AissenPolian2025.Agt, {AissenPolian2025.v₀, {AissenPolian2025.Appl₀, {AissenPolian2025.V₀, AissenPolian2025.PossP}}}}}

def AissenPolian2025.unerg (subj : Minimalist.PlanarSyntacticObject) : Minimalist.PlanarSyntacticObject

(9b) with a locative PP, for a specific or a non-specific S_A.

Equations

• AissenPolian2025.unerg subj = {AissenPolian2025.T₀, {subj, {AissenPolian2025.v₀, {AissenPolian2025.V₀, AissenPolian2025.PP}}}}

def AissenPolian2025.themeLoc (theme : Minimalist.PlanarSyntacticObject) : Minimalist.PlanarSyntacticObject

(71) theme over locative, for a specific or a non-specific theme: path verbs, locative existentials and locative copulas.

Equations

• AissenPolian2025.themeLoc theme = {AissenPolian2025.T₀, {AissenPolian2025.V₀, {theme, AissenPolian2025.PP}}}

def AissenPolian2025.experiencer : Minimalist.PlanarSyntacticObject

(83) the experiencer PP merged above the theme.

Equations

• AissenPolian2025.experiencer = {AissenPolian2025.T₀, {AissenPolian2025.PP, {AissenPolian2025.V₀, AissenPolian2025.ThemeD}}}

def AissenPolian2025.existential : Minimalist.PlanarSyntacticObject

(40a) an existential with a bare pivot.

Equations

• AissenPolian2025.existential = {AissenPolian2025.T₀, {AissenPolian2025.V₀, AissenPolian2025.Pivot}}

def AissenPolian2025.cp (tp : Minimalist.PlanarSyntacticObject) : Minimalist.PlanarSyntacticObject

The clause under C⁰.

Equations

• AissenPolian2025.cp tp = {AissenPolian2025.C₀, tp}

Nominal opacity

theorem AissenPolian2025.psr_invisible_dp : Invisible nominalOpacity ↑(cp unaccDP) ↑C₀ ↑Psr

The possessor of a specific S_O is invisible to C⁰'s wh-probe.

theorem AissenPolian2025.psr_invisible_possP : Invisible nominalOpacity ↑(cp unaccPossP) ↑C₀ ↑Psr

So is the possessor of a non-specific S_O: opacity does not depend on size.

theorem AissenPolian2025.psr_invisible_pp : Invisible nominalOpacity ↑(cp (themeLoc ThemeN)) ↑C₀ ↑Psr

And the possessor inside a locative PP: PP islands follow from nominal opacity.

theorem AissenPolian2025.dHead_visible : ¬Invisible nominalOpacity ↑(cp unaccDP) ↑C₀ ↑D₀

The D head of a specific possessive is visible, so the whole DP can be pied-piped.

Attract Closest

theorem AissenPolian2025.unacc_possP_psr_closest : (↑unaccPossP).isClosestGoalIn (↑T₀) (↑Psr) (Minimalist.SyntacticObject.isLeafOf Minimalist.Cat.D)

The possessor of a non-specific S_O is T⁰'s closest D-goal: it raises to Spec,TP and can strand the possessum.

theorem AissenPolian2025.unacc_dp_dHead_closest : (↑unaccDP).isClosestGoalIn (↑T₀) (↑D₀) (Minimalist.SyntacticObject.isLeafOf Minimalist.Cat.D) ∧ ¬(↑unaccDP).isClosestGoalIn (↑T₀) (↑Psr) (Minimalist.SyntacticObject.isLeafOf Minimalist.Cat.D)

In a specific S_O the D layer is the closer goal: the whole DP raises and the possessor is shielded.

theorem AissenPolian2025.trans_agt_closest : (↑transPossP).isClosestGoalIn (↑T₀) (↑Agt) (Minimalist.SyntacticObject.isLeafOf Minimalist.Cat.D) ∧ ¬(↑transPossP).isClosestGoalIn (↑T₀) (↑Psr) (Minimalist.SyntacticObject.isLeafOf Minimalist.Cat.D)

The agent of a transitive is the closer goal, so the possessor of O cannot reach Spec,TP.

theorem AissenPolian2025.appl_psr_closest : (↑raisingAppl).isClosestGoalIn (↑Appl₀) (↑Psr) (Minimalist.SyntacticObject.isLeafOf Minimalist.Cat.D)

In the raising applicative the possessor of O is Appl⁰'s closest D-goal: it externalizes to Spec,ApplP.

theorem AissenPolian2025.unerg_specific_blocks : (↑(unerg SubjD)).isClosestGoalIn (↑T₀) (↑SubjD) (Minimalist.SyntacticObject.isLeafOf Minimalist.Cat.D) ∧ ¬(↑(unerg SubjD)).isClosestGoalIn (↑T₀) (↑Psr) (Minimalist.SyntacticObject.isLeafOf Minimalist.Cat.D)

A specific unergative subject stops T⁰ before the possessor inside the locative PP.

theorem AissenPolian2025.unerg_nonspecific_psr_closest : (↑(unerg SubjN)).isClosestGoalIn (↑T₀) (↑Psr) (Minimalist.SyntacticObject.isLeafOf Minimalist.Cat.D)

A non-specific unergative subject is no DP, so the possessor is the closest goal.

theorem AissenPolian2025.theme_specific_blocks : (↑(themeLoc ThemeD)).isClosestGoalIn (↑T₀) (↑ThemeD) (Minimalist.SyntacticObject.isLeafOf Minimalist.Cat.D) ∧ ¬(↑(themeLoc ThemeD)).isClosestGoalIn (↑T₀) (↑Psr) (Minimalist.SyntacticObject.isLeafOf Minimalist.Cat.D)

A specific theme c-commanding the locative PP raises instead of the possessor.

theorem AissenPolian2025.theme_nonspecific_psr_closest : (↑(themeLoc ThemeN)).isClosestGoalIn (↑T₀) (↑Psr) (Minimalist.SyntacticObject.isLeafOf Minimalist.Cat.D)

A non-specific theme lets T⁰ reach the possessor inside the PP.

theorem AissenPolian2025.experiencer_both_closest : (↑experiencer).isClosestGoalIn (↑T₀) (↑Psr) (Minimalist.SyntacticObject.isLeafOf Minimalist.Cat.D) ∧ (↑experiencer).isClosestGoalIn (↑T₀) (↑ThemeD) (Minimalist.SyntacticObject.isLeafOf Minimalist.Cat.D)

With the experiencer PP merged above the theme, neither c-commands the other and both are closest goals; the experiential reading requires the experiencer to raise.

Judgment type

inductive AissenPolian2025.JudgmentType : Type

Categorical judgments have a subject of predication, thetic ones present a situation.

• categorical : JudgmentType
• thetic : JudgmentType

@[instance_reducible]

instance AissenPolian2025.instDecidableEqJudgmentType : DecidableEq JudgmentType

Equations

• AissenPolian2025.instDecidableEqJudgmentType x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def AissenPolian2025.instReprJudgmentType.repr : JudgmentType → ℕ → Std.Format

Equations

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

@[instance_reducible]

instance AissenPolian2025.instReprJudgmentType : Repr JudgmentType

Equations

• AissenPolian2025.instReprJudgmentType = { reprPrec := AissenPolian2025.instReprJudgmentType.repr }

@[instance_reducible]

instance AissenPolian2025.instDecidableExistsSyntacticObjectAndMemMultisetTermsIsClosestGoalInIsLeafOfD_studies (root probe : Minimalist.SyntacticObject) : Decidable (∃ g ∈ root.terms, root.isClosestGoalIn probe g (Minimalist.SyntacticObject.isLeafOf Minimalist.Cat.D))

Equations

• AissenPolian2025.instDecidableExistsSyntacticObjectAndMemMultisetTermsIsClosestGoalInIsLeafOfD_studies root probe = Multiset.decidableExistsMultiset

def AissenPolian2025.judgment (root probe : Minimalist.SyntacticObject) : JudgmentType

A clause is categorical when T⁰'s [EPP:D] probe finds a goal to raise to Spec,TP — the ψ-subject — and thetic when it finds none.

Equations

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

theorem AissenPolian2025.existential_thetic : judgment ↑existential ↑T₀ = JudgmentType.thetic

An existential with a bare pivot contains no DP: the clause is thetic.

theorem AissenPolian2025.possession_categorical : judgment ↑unaccPossP ↑T₀ = JudgmentType.categorical

Predicative possession is categorical, with the possessor as ψ-subject.

The paper's examples

theorem AissenPolian2025.stranding_iff (row : Datum) : row ∈ Examples.all → row.feature? "strategy" = some "stranding" → (row.judgment = Judgment.acceptable ↔ row.feature? "possessum" = some "nonSpecific" ∧ row.feature? "intervener" = some "none")

Stranding succeeds exactly when the possessum is non-specific and no DP or occupied external position stands between the possessor and its probe (Table 4).

theorem AissenPolian2025.piedPiping_specific (row : Datum) : row ∈ Examples.all → row.feature? "strategy" = some "piedPiping" → row.judgment = Judgment.acceptable → row.feature? "possessum" = some "specific"

Pied-piping succeeds only with a specific possessum, since only a DP can be wh-moved.

theorem AissenPolian2025.psi_no_piedPiping (row : Datum) : row ∈ Examples.all → row.feature? "strategy" = some "piedPiping" → row.feature? "construction" = some "predicativePossession" ∨ row.feature? "construction" = some "experientialCollocation" → row.judgment ≠ Judgment.acceptable

In predicative possession and experiential collocations possessor and possessum form no constituent, so pied-piping is out.