[Pyl08] — Introducing Arguments

[Pyl08] [Cue03] [BL86]

Linguistic Inquiry Monographs 49. MIT Press.

Core Claims

1. High vs Low Applicatives: Applicative heads come in two semantic types. Low Appl merges below V, relating the applied argument to the theme (transfer-of-possession): [VP V [ApplP goal [Appl theme]]]. High Appl merges above VP, relating the applied argument to the event (benefactive): [VoiceP agent [Voice [ApplP benef [Appl [VP V theme]]]]].

2. Semantic type distinction: High Appl denotes an individual-event relation λx.λe. Appl(x,e). Low Appl denotes an individual-individual relation λx.λy.λf.λe. f(e,x) & theme(e,x) & to-the-possession(x,y).

3. Low recipient vs low source: Low applicatives split into recipient (ApplTo: transfer to applied arg) and source (ApplFrom: transfer from applied arg). English DOC is low recipient; Korean theft constructions and Hebrew possessor datives are low source.

4. C-command asymmetries: In both configurations, the applied argument asymmetrically c-commands the theme. This derives the [BL86] binding asymmetries structurally.

5. Cross-linguistic variation: English, Japanese, and Korean have LOW Appl; Bantu languages (Chaga, Luganda, Venda) and Albanian have HIGH Appl.

Diagnostics (Table 2.1, p. 33)

Test	High	Low
1. Can unergatives be applicativized?	Yes	No
2. Can static verbs be applicativized?	Yes	No
3. (If language has English-style depictives) is the
applied argument available for depictive modification?	Yes	No

Test 3 is conditional on the language having depictive secondary predicates with the English distribution. Korean lacks them entirely, and Venda/Albanian have too-broad depictives — in those languages Test 3 is inapplicable, not "fails." See ApplDiagnosticResult in the "Applicative diagnostics" section below.

Cross-references

• Studies/Larson1988.lean: VP shell predecessor — same c-command hierarchy (IO > DO) derived differently. Bridge theorem below proves convergence.
• Studies/Kratzer1996.lean Part III: Voice-based tree derivations (transitive, anticausative) using the same infrastructure.

Voice projection (relocated from Minimalist/VoiceProjection.lean)

What is Voice? Two competing views

[Kra96] [Pyl08] [Col05] [Sto26c]

A formalizer-side meta-bridge surfacing a substantive theoretical disagreement neither paper sets up directly: what is the job of the syntactic head called Voice?

The two views

Pylkkänen / Kratzer view ([Kra96], [Pyl08]): Voice is the head that introduces the external argument. Its job is thematic — it bears a θ-relation between the external argument and the event described by the verb (Event Identification, [Kra96] eq. 10). All argument-structure theory follows from where Voice projects and what it bundles with (Cause-Voice bundling, [Pyl08] Ch. 3 §3.3). Without Voice, no external argument is introduced at all.

Collins / Storment view ([Col05], [Sto26c]): Voice is the smuggling projection. Its job is structural — it provides the landing site (Spec,VoiceP) into which a constituent can move, licensing A-movement past an in-situ external argument. The external argument itself is introduced by v, not Voice ([Sto26c] §4.3). Voice's status as a non-phase head is what permits smuggling. The voice-as-smuggling-projection conception is "a notable departure from the view of Voice⁰ as an applicative head that introduces the external argument" ([Sto26c], §4.3).

The disagreement is partly substantive, partly terminological

The two camps do not disagree about the empirical phenomena. They disagree about which functional head does which job. Pylkkänen attributes external-argument introduction to Voice and structural licensing to higher functional projections (T⁰, Infl). Collins attributes external-argument introduction to v and structural licensing (Case + smuggling) to Voice. The label "Voice" denotes different positions in the two systems.

The orthogonality of the two predicates IsExternalArgIntroducer and IsSmugglingProjection (defined below) reflects this: a VoiceHead instance can satisfy one, both, or neither. Linglib's VoiceHead structure encodes both axes (assignsTheta and permitsSmuggling) independently, accommodating both views simultaneously.

Where this meta-bridge sits

Per the CLAUDE.md cross-theory-meta-bridges convention, this is a formalizer-side synthesis (neither Pylkkänen nor Collins/Storment formulates the contrast in these exact terms). Both views are pure-theory positions about a syntactic head, with no specific empirical phenomenon at stake.

Two predicates over Voice heads

The Pylkkänen view and the Collins/Storment view make different claims about what makes a Voice head "well-formed Voice."

def Pylkkanen2008.IsExternalArgIntroducer (v : Minimalist.VoiceHead) : Prop

Pylkkänen / Kratzer view: a Voice head is "doing its job" iff it introduces an external argument (assigns external θ). [Kra96]: Voice = the head bearing the θ-relation.

Equations

• Pylkkanen2008.IsExternalArgIntroducer v = v.AssignsTheta

@[implicit_reducible]

instance Pylkkanen2008.instDecidableIsExternalArgIntroducer (v : Minimalist.VoiceHead) : Decidable (IsExternalArgIntroducer v)

Equations

• Pylkkanen2008.instDecidableIsExternalArgIntroducer v = id inferInstance

def Pylkkanen2008.IsSmugglingProjection (v : Minimalist.VoiceHead) : Prop

Collins / Storment view: a Voice head is "doing its job" iff it permits smuggling (it is the structural landing site for a constituent moving past an in-situ external argument). [Col05], [Sto26c].

Equations

• Pylkkanen2008.IsSmugglingProjection v = (v.permitsSmuggling = true)

@[implicit_reducible]

instance Pylkkanen2008.instDecidableIsSmugglingProjection (v : Minimalist.VoiceHead) : Decidable (IsSmugglingProjection v)

Equations

• Pylkkanen2008.instDecidableIsSmugglingProjection v = id inferInstance

The two views are orthogonal

Linglib's VoiceHead already encodes both axes. The question is whether they coincide for the canonical Voice instances. Answer: they don't. A Voice head can satisfy either one, both, or neither — the four corners of the orthogonality square.

theorem Pylkkanen2008.voiceAgent_pylkkanen_yes_collins_no : IsExternalArgIntroducer Minimalist.voiceAgent ∧ ¬IsSmugglingProjection Minimalist.voiceAgent

voiceAgent satisfies the Pylkkänen view (it introduces the agent external argument) but fails the Collins/Storment view (agentive Voice is a strong phase head; smuggling is blocked).

theorem Pylkkanen2008.voicePassive_collins_yes_pylkkanen_no : IsSmugglingProjection Minimalist.voicePassive ∧ ¬IsExternalArgIntroducer Minimalist.voicePassive

voicePassive satisfies the Collins view (it is the smuggling landing site) but fails the Pylkkänen view (it does not introduce an external argument — the external arg is in Spec,vP per [Col05] §2 UTAH). The passive Voice head is puzzling on Pylkkänen's view: a Voice head with no θ-role to assign.

theorem Pylkkanen2008.voiceAnticausative_collins_yes_pylkkanen_no : IsSmugglingProjection Minimalist.voiceAnticausative ∧ ¬IsExternalArgIntroducer Minimalist.voiceAnticausative

voiceAnticausative similarly fits the Collins view (smuggling target for the unaccusative-like derivation Storment uses for QI and LI) and fails the Pylkkänen view (no external argument).

theorem Pylkkanen2008.views_not_equivalent : ¬∀ (v : Minimalist.VoiceHead), IsExternalArgIntroducer v ↔ IsSmugglingProjection v

The two views are not equivalent: there exist Voice heads distinguishing them (in fact, the canonical instances above all do).

What the disagreement amounts to

In Pylkkänen's framework, every Voice head should be an IsExternalArgIntroducer. The fact that linglib's voicePassive and voiceAnticausative are not means Pylkkänen would not call these "Voice" — she would attribute the structural-licensing function to a different (perhaps unnamed) head.

In Collins/Storment's framework, every Voice head should be an IsSmugglingProjection. The fact that linglib's voiceAgent is not means Collins/Storment would not call this "Voice" — they would call it v (which voiceAgent's thematic role and phase status more closely match in their system).

The disagreement is therefore partly labeling: which functional head gets the name "Voice." But it is also partly substantive: whether the same syntactic position can simultaneously introduce an external argument and serve as a smuggling target. Pylkkänen's framework requires Voice to do (a); Collins/Storment's framework requires Voice to do (b); and the two functions are made structurally incompatible by the phase/θ-role correlations Storment defends in §4 of his paper.

theorem Pylkkanen2008.views_jointly_unsatisfiable_for_canonical_voices : ¬(IsExternalArgIntroducer Minimalist.voiceAgent ∧ IsSmugglingProjection Minimalist.voiceAgent) ∧ ¬(IsExternalArgIntroducer Minimalist.voicePassive ∧ IsSmugglingProjection Minimalist.voicePassive) ∧ ¬(IsExternalArgIntroducer Minimalist.voiceAnticausative ∧ IsSmugglingProjection Minimalist.voiceAnticausative)

The substantive incompatibility: a Voice head cannot simultaneously satisfy both views. (Equivalently: introducing an external argument requires being a phase head, which blocks smuggling.)

Applicative diagnostics (relocated from Minimalist/ApplicativeDiagnostics.lean)

Applicative diagnostics

[Pyl08]

Cluster-based diagnostic classifier for the high/low applicative distinction ([Pyl08], Table 2.1). Three diagnostics:

1. Can unergative verbs be applicativized? (Ch. 2 §2.1.2)
2. Can static verbs be applicativized? (Ch. 2 §2.1.2)
3. If the language has English-style depictive secondary predicates, is the applied argument available for depictive modification? (Ch. 2 §2.1.3)

Cluster-based classification

A high applicative passes all tests; a low applicative fails all tests. Test 3 is conditional — when a language lacks English-style depictives (e.g., Korean) or has too-broad depictives (Venda, Albanian), the test is inapplicable (.inapplicable), not "fails." The classifier ignores inapplicable tests and classifies on the cluster of applicable ones.

This is stricter than an OR-based classifier (which would misclassify a language passing one test by accident). Languages that don't pattern cleanly with either cluster yield none, requiring further investigation rather than a forced classification.

inductive Pylkkanen2008.ApplDiagnosticResult : Type

The result of running a single Pylkkänen diagnostic on a language.

• passes : ApplDiagnosticResult

  The diagnostic is applicable and the language passes (the construction in question is grammatical).

• fails : ApplDiagnosticResult

  The diagnostic is applicable and the language fails (the construction is ungrammatical).

• inapplicable : ApplDiagnosticResult

  The diagnostic is inapplicable in this language — e.g., Korean lacks English-style depictives entirely, so Test 3 cannot be run. Distinct from .fails: an inapplicable test contributes no classification evidence.

@[implicit_reducible]

instance Pylkkanen2008.instDecidableEqApplDiagnosticResult : DecidableEq ApplDiagnosticResult

Equations

• Pylkkanen2008.instDecidableEqApplDiagnosticResult x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[implicit_reducible]

instance Pylkkanen2008.instReprApplDiagnosticResult : Repr ApplDiagnosticResult

Equations

• Pylkkanen2008.instReprApplDiagnosticResult = { reprPrec := Pylkkanen2008.instReprApplDiagnosticResult.repr }

def Pylkkanen2008.instReprApplDiagnosticResult.repr : ApplDiagnosticResult → ℕ → Std.Format

Equations

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

structure Pylkkanen2008.ApplDiagnosticBundle : Type

A bundle of Pylkkänen Table 2.1's three diagnostic results for a given language. Test 3's inapplicable value handles the language-conditional cases (Korean lacks depictives; Venda and Albanian have too-broad depictives to test).

• unergative : ApplDiagnosticResult

  Test 1: can unergative verbs be applicativized?

• staticVerb : ApplDiagnosticResult

  Test 2: can static verbs be applicativized?

• depictive : ApplDiagnosticResult

  Test 3: depictive modification of applied argument (conditional on language having English-style depictives).

def Pylkkanen2008.instReprApplDiagnosticBundle.repr : ApplDiagnosticBundle → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance Pylkkanen2008.instReprApplDiagnosticBundle : Repr ApplDiagnosticBundle

Equations

• Pylkkanen2008.instReprApplDiagnosticBundle = { reprPrec := Pylkkanen2008.instReprApplDiagnosticBundle.repr }

def Pylkkanen2008.ApplDiagnosticBundle.results (b : ApplDiagnosticBundle) : List ApplDiagnosticResult

The list of diagnostic results in a bundle, for cluster checks.

Equations

• b.results = [b.unergative, b.staticVerb, b.depictive]

def Pylkkanen2008.ApplDiagnosticBundle.applicableResults (b : ApplDiagnosticBundle) : List ApplDiagnosticResult

The applicable (non-.inapplicable) results in a bundle.

Equations

• b.applicableResults = List.filter (fun (x : Pylkkanen2008.ApplDiagnosticResult) => decide (x ≠ Pylkkanen2008.ApplDiagnosticResult.inapplicable)) b.results

def Pylkkanen2008.classifyByDiagnostics (b : ApplDiagnosticBundle) : Option Minimalist.ApplType

Cluster-based classification ([Pyl08], Table 2.1): a language has high applicatives iff every applicable diagnostic passes; low iff every applicable diagnostic fails; otherwise the pattern is mixed and the classifier returns none, requiring further investigation rather than forcing a classification.

Note: this returns Option ApplType collapsed to .high or .lowRecipient — distinguishing recipient from source low applicatives requires additional diagnostics (transfer directionality, §2.2 + §2.3) not in Table 2.1.

Equations

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

Soundness theorems

The classifier returns .high only on all-pass bundles, .lowRecipient only on all-fail bundles. Mixed bundles and empty/all-inapplicable bundles yield none. Soundness is checked structurally on the four canonical bundle shapes below.

theorem Pylkkanen2008.all_pass_classifies_high : classifyByDiagnostics { unergative := ApplDiagnosticResult.passes, staticVerb := ApplDiagnosticResult.passes, depictive := ApplDiagnosticResult.passes } = some Minimalist.ApplType.high

A bundle with all three results .passes classifies as high.

theorem Pylkkanen2008.all_fail_classifies_low : classifyByDiagnostics { unergative := ApplDiagnosticResult.fails, staticVerb := ApplDiagnosticResult.fails, depictive := ApplDiagnosticResult.fails } = some Minimalist.ApplType.lowRecipient

A bundle with all three results .fails classifies as low.

theorem Pylkkanen2008.mixed_does_not_classify : classifyByDiagnostics { unergative := ApplDiagnosticResult.passes, staticVerb := ApplDiagnosticResult.fails, depictive := ApplDiagnosticResult.fails } = none

A bundle with mixed results does not classify.

theorem Pylkkanen2008.all_inapplicable_does_not_classify : classifyByDiagnostics { unergative := ApplDiagnosticResult.inapplicable, staticVerb := ApplDiagnosticResult.inapplicable, depictive := ApplDiagnosticResult.inapplicable } = none

An all-inapplicable bundle does not classify.

theorem Pylkkanen2008.inapplicable_excluded : classifyByDiagnostics { unergative := ApplDiagnosticResult.passes, staticVerb := ApplDiagnosticResult.passes, depictive := ApplDiagnosticResult.inapplicable } = some Minimalist.ApplType.high

Inapplicable tests are excluded from the cluster: a bundle with one .inapplicable and two .passes still classifies as high.

theorem Pylkkanen2008.inapplicable_with_fails_classifies_low : classifyByDiagnostics { unergative := ApplDiagnosticResult.fails, staticVerb := ApplDiagnosticResult.fails, depictive := ApplDiagnosticResult.inapplicable } = some Minimalist.ApplType.lowRecipient

Inapplicable + all-fails still classifies as low.

def Pylkkanen2008.voice_ag_t : Minimalist.SO

Equations

• Pylkkanen2008.voice_ag_t = Minimalist.SO.mkLeafPhon Minimalist.Cat.Voice [Minimalist.Cat.V] "Voice[AG]" 400

def Pylkkanen2008.appl_low_t : Minimalist.SO

Equations

• Pylkkanen2008.appl_low_t = Minimalist.SO.mkLeafPhon Minimalist.Cat.Appl [Minimalist.Cat.D] "Appl[LOW]" 402

def Pylkkanen2008.appl_high_t : Minimalist.SO

Equations

• Pylkkanen2008.appl_high_t = Minimalist.SO.mkLeafPhon Minimalist.Cat.Appl [Minimalist.Cat.V] "Appl[HI]" 403

def Pylkkanen2008.V_sent_t : Minimalist.SO

Equations

• Pylkkanen2008.V_sent_t = Minimalist.SO.mkLeafPhon Minimalist.Cat.V [Minimalist.Cat.Appl] "sent" 404

def Pylkkanen2008.V_eat_t : Minimalist.SO

Equations

• Pylkkanen2008.V_eat_t = Minimalist.SO.mkLeafPhon Minimalist.Cat.V [Minimalist.Cat.D] "eat" 405

def Pylkkanen2008.DP_john_t : Minimalist.SO

Equations

• Pylkkanen2008.DP_john_t = Minimalist.SO.mkLeafPhon Minimalist.Cat.D [] "John" 406

def Pylkkanen2008.DP_mary_t : Minimalist.SO

Equations

• Pylkkanen2008.DP_mary_t = Minimalist.SO.mkLeafPhon Minimalist.Cat.D [] "Mary" 407

def Pylkkanen2008.DP_letter_t : Minimalist.SO

Equations

• Pylkkanen2008.DP_letter_t = Minimalist.SO.mkLeafPhon Minimalist.Cat.D [] "a letter" 408

def Pylkkanen2008.DP_wife_t : Minimalist.SO

Equations

• Pylkkanen2008.DP_wife_t = Minimalist.SO.mkLeafPhon Minimalist.Cat.D [] "wife" 409

def Pylkkanen2008.DP_food_t : Minimalist.SO

Equations

• Pylkkanen2008.DP_food_t = Minimalist.SO.mkLeafPhon Minimalist.Cat.D [] "food" 410

Planar leaf tokens, used to build the concrete trees the c-command theorems reason over (Merge SO.node is noncomputable; trees are built planar-first via SO.ofPlanar).

def Pylkkanen2008.ditransitiveTree : Minimalist.SyntacticObject

Ditransitive with low applicative: "John sent Mary a letter"

[VoiceP John [Voice' Voice_AG [VP sent [ApplP Mary [Appl' Appl_LOW [DP a letter]]]]]]

Low Appl merges below V: V takes ApplP as complement. The goal (Mary) is in Spec-ApplP, c-commanding the theme (a letter) in complement of Appl. This derives the [BL86] asymmetry that IO asymmetrically c-commands DO. Built planar-first so the c-command theorems decide.

Equations

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

def Pylkkanen2008.benefactiveTree : Minimalist.SyntacticObject

High applicative benefactive (Chaga pattern): "he ate food for wife"

[VoiceP John [Voice' Voice_AG [ApplP wife [Appl' Appl_HIGH [VP eat [DP food]]]]]]

High Appl merges above VP: Appl takes VP as complement. The benefactive (wife) is in Spec-ApplP, relating to the event (not the theme). High Appl is attested in Bantu languages (Chaga, Luganda, Venda) and Albanian, but NOT in English.

Equations

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

theorem Pylkkanen2008.ditransitive_agent_ccommands_goal : Minimalist.SO.cCommandsIn ditransitiveTree DP_john_t DP_mary_t

Agent c-commands goal.

theorem Pylkkanen2008.ditransitive_agent_ccommands_theme : Minimalist.SO.cCommandsIn ditransitiveTree DP_john_t DP_letter_t

Agent c-commands theme.

theorem Pylkkanen2008.ditransitive_goal_ccommands_theme : Minimalist.SO.cCommandsIn ditransitiveTree DP_mary_t DP_letter_t

Goal c-commands theme — the [BL86] asymmetry derived structurally from V selecting ApplP.

theorem Pylkkanen2008.ditransitive_theme_not_ccommands_goal : ¬Minimalist.SO.cCommandsIn ditransitiveTree DP_letter_t DP_mary_t

Theme does NOT c-command goal: the asymmetry is structural.

theorem Pylkkanen2008.benefactive_benef_ccommands_theme : Minimalist.SO.cCommandsIn benefactiveTree DP_wife_t DP_food_t

Benefactive c-commands theme.

theorem Pylkkanen2008.benefactive_theme_not_ccommands_benef : ¬Minimalist.SO.cCommandsIn benefactiveTree DP_food_t DP_wife_t

Theme does NOT c-command benefactive.

theorem Pylkkanen2008.send_is_low_appl : Minimalist.SO.contains ditransitiveTree appl_low_t

Low applicative marks the ditransitive.

theorem Pylkkanen2008.eat_is_high_appl : Minimalist.SO.contains benefactiveTree appl_high_t

High applicative marks the benefactive.

The lexical items appl_low_t and appl_high_t correspond to ApplHead instances from Syntax/Minimalism/Applicative.lean: the ditransitive uses applLowRecipient (English DOC = transfer to); the benefactive uses applHigh (Chaga = individual-event relation).

theorem Pylkkanen2008.ditransitive_uses_low_recipient : Minimalist.applLowRecipient.applType = Minimalist.ApplType.lowRecipient ∧ Minimalist.applLowRecipient.applType.IsLow

The ditransitive's applicative is low (recipient).

theorem Pylkkanen2008.benefactive_uses_high : Minimalist.applHigh.applType = Minimalist.ApplType.high ∧ ¬Minimalist.applHigh.applType.IsLow

The benefactive's applicative is high.

[Pyl08] tests the high/low distinction in six languages using three diagnostics (Table 2.1, p. 33). The diagnostics cluster into two groups, confirming the typological split. The classifier classifyByDiagnostics derives the high/low classification from the diagnostic results; we verify that for each language, the classifier output matches Pylkkänen's annotated classification.

structure Pylkkanen2008.LangApplProfile : Type

A language's diagnostic profile and Pylkkänen's annotated classification. The diagnostic results live in ApplDiagnosticBundle; classification records Pylkkänen's analytical conclusion.

• language : String
• diagnostics : ApplDiagnosticBundle
• classification : Minimalist.ApplType

  Pylkkänen's annotated classification (§2.1.2 conclusion).

def Pylkkanen2008.instReprLangApplProfile.repr : LangApplProfile → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance Pylkkanen2008.instReprLangApplProfile : Repr LangApplProfile

Equations

• Pylkkanen2008.instReprLangApplProfile = { reprPrec := Pylkkanen2008.instReprLangApplProfile.repr }

def Pylkkanen2008.LangApplProfile.DerivationConsistent (l : LangApplProfile) : Prop

Pylkkänen's analytical conclusion is derivable from the diagnostics: the cluster classifier returns the same result, modulo the recipient/source distinction (which Table 2.1's three tests don't make — separating low recipient from low source needs additional transfer-directionality diagnostics from §2.2/§2.3).

Equations

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

@[implicit_reducible]

instance Pylkkanen2008.instDecidablePredLangApplProfileDerivationConsistent : DecidablePred LangApplProfile.DerivationConsistent

Equations

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

def Pylkkanen2008.english_appl : LangApplProfile

English: low recipient. *I ran him (20a); *I held him the bag (20b); *John told Mary the news drunk (27e).

Equations

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

def Pylkkanen2008.japanese_appl : LangApplProfile

Japanese: low recipient. *Taroo-ga Hanako-ni hasit-ta (21a); *Taroo-ga Hanako-ni kanojo-no kaban-o mot-ta (21b); *Taroo-ga hadaka-de Hanako-ni hon-o yonda (40a).

Equations

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

def Pylkkanen2008.korean_appl : LangApplProfile

Korean: low recipient. *Mary-ka John-hanthey talli-ess-ta (22a); *John-i Mary-hanthey kabang-ul cap-ass-ta (22b). Korean lacks English-style depictives entirely (§2.1.3.2.2), so Test 3 is inapplicable.

Equations

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

def Pylkkanen2008.luganda_appl : LangApplProfile

Luganda: high. Mukasa ya-tambu-le-dde Katonga (23a); Katonga ya-kwaant-i-dde Mukasa ensawo (23b); Mustafa ya-ko-le-dde Katonga nga mulwadde (43a).

Equations

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

def Pylkkanen2008.venda_appl : LangApplProfile

Venda: high. Ndi-do-shum-el-a musadzi (24a); Nd-o-far-el-a Mukasa khali (24b). Venda postverbal APs have too broad a distribution to qualify as English-style depictives, so Test 3 is inapplicable (§2.1.3.2.4).

Equations

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

def Pylkkanen2008.albanian_appl : LangApplProfile

Albanian: high. I vrapova (25a); Agimi i mban Drites çanten time (25b). Albanian postverbal APs pattern like English ones (modifying internal and external but not implicit external arguments), except that — unlike English depictives — they can also easily modify DPs inside PPs. That extra breadth disqualifies them as English-style depictives, so Test 3 is inapplicable (§2.1.3.2.5).

Equations

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

def Pylkkanen2008.hebrew_appl : LangApplProfile

Hebrew possessor datives: low source applicative (book §2.2, eq. 82a). Hebrew possessor datives are low applicatives, so they fail Tests 1 and 2 by the same logic as English low recipient. Pylkkänen does not test depictive modification with Hebrew possessor datives in §2.1.3, so Test 3 is .inapplicable here. Note: Table 2.1's three tests don't distinguish recipient from source — derivationConsistent accepts the cluster classifier's .lowRecipient output for Hebrew's actual .lowSource classification (the recipient-vs-source distinction needs the additional transfer-directionality diagnostics from §2.2).

Equations

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

def Pylkkanen2008.allLanguages : List LangApplProfile

Equations

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

theorem Pylkkanen2008.seven_languages : allLanguages.length = 7

Seven languages classified (six from Table 2.1 + Hebrew from §2.2).

theorem Pylkkanen2008.all_classifications_derive_from_diagnostics (l : LangApplProfile) : l ∈ allLanguages → l.DerivationConsistent

For each language, Pylkkänen's annotated classification is derivable from the diagnostic results via the cluster-based classifier. The classification isn't stipulated and verified against itself — it's derived from the data and proved consistent with the analytical conclusion.

theorem Pylkkanen2008.english_classification_derives : classifyByDiagnostics english_appl.diagnostics = some Minimalist.ApplType.lowRecipient

Anchor verifications for the two clusters. The aggregate all_classifications_derive_from_diagnostics covers all seven languages; these two anchor the cluster behavior at each pole.

theorem Pylkkanen2008.luganda_classification_derives : classifyByDiagnostics luganda_appl.diagnostics = some Minimalist.ApplType.high

theorem Pylkkanen2008.hebrew_classification_derives_to_low : classifyByDiagnostics hebrew_appl.diagnostics = some Minimalist.ApplType.lowRecipient

Hebrew possessor datives are classified as .lowRecipient by Table 2.1's three tests (all-fail cluster), but Pylkkänen's actual classification is .lowSource. The two are both low; the recipient-vs-source distinction requires additional diagnostics not in Table 2.1. derivationConsistent accepts this case.

[Lar88]'s VP shell is the precursor of the modern Voice + Applicative decomposition. While the tree shapes differ (Larson uses one VP-shell layer; modern theory uses Voice and Appl heads), the c-command hierarchy among DP arguments is identical: agent > goal/IO > theme/DO.

theorem Pylkkanen2008.larson_modern_same_hierarchy : Larson1988.docDativeShiftTree.cCommandsIn Larson1988.DP_mary Larson1988.DP_letter ∧ ¬Larson1988.docDativeShiftTree.cCommandsIn Larson1988.DP_letter Larson1988.DP_mary ∧ Minimalist.SO.cCommandsIn ditransitiveTree DP_mary_t DP_letter_t ∧ ¬Minimalist.SO.cCommandsIn ditransitiveTree DP_letter_t DP_mary_t

[Lar88]'s DOC and the modern Voice + low-Appl derivation produce the same c-command hierarchy: IO asymmetrically c-commands DO.

This proves that [Lar88] and [Pyl08], despite different decompositions, converge on the same structural prediction for [BL86] asymmetries. (Larson's side is stated over docDativeShiftTree, the planar-built result tree of his Dative-Shift derivation; docDativeShift.final is noncomputable on the SO carrier.)

§7. Voice as the head that introduces the external argument

([pylkkanen-2008] Ch. 3 §3.2 + Ch. 4 §4.2)

[Pyl08]'s central claim about Voice (Ch. 4 §4.2, "Eliminating Linking"): the external argument is not projected by the verb itself but by a separate Voice head, following [Kra96]. Voice combines with VP via Event Identification (Event Identification, Ch. 1; -- UNVERIFIED: eq. number), introducing the external argument and relating it to the event described by the verb.

This is one of the two competing views of Voice surveyed in the "Voice projection" section above. The other view, defended by [Col05] and [Sto26c], treats Voice as a structural head (the smuggling projection) and assigns external-argument introduction to v instead. The two views are orthogonal — see the "Voice projection" section for the substantive contrast.

theorem Pylkkanen2008.voice_introduces_external_arg_pylkkanen : IsExternalArgIntroducer Minimalist.voiceAgent

Pylkkänen's view applied to the canonical agentive Voice: it satisfies IsExternalArgIntroducer (it does the job Pylkkänen attributes to Voice).

§8. Voice-bundling for the English zero-causative

([pylkkanen-2008] Ch. 3 §3.3; -- UNVERIFIED: eq. number)

A second contribution of Ch. 3: the difference between English (which lacks unaccusative causatives) and Japanese/Finnish (which have them) reduces to whether the language bundles Cause and Voice into a single morphological head. English bundles ([Cause, Voice]); Japanese and Finnish do not.

The VoiceBundlingChoice enum + CauseSelection axis + the full 2 × 3 typology cells (Pylkkänen Table 3.1) are defined in §13 below, since this is the only Pylkkänen-derived consumer in the codebase. The two canonical-instance affirmations (english_zero_is_bundled, japanese_lexical_is_independent) live alongside the cell definitions in §13.

§9. Cause is not a θ-role ([Pyl08] Ch. 3 §3.2)

Pylkkänen's other major Ch. 3 argument: the causative head Cause introduces a causing event, not a θ-role on the external argument. Evidence: Japanese adversity causatives (§3.2.2) have causative morphology and meaning but no external argument. The bieventive analysis (Cause = relation between two events) is required by such data; the θ-role analysis (Cause = relation between a causer and a caused event) cannot accommodate them.

The bieventive vs. θ-role contrast is formalized in Semantics/ArgumentStructure/ArgumentIntroduction.lean: causeBieventive_no_external_arg shows a causing event with no causer participant (the Japanese adversity causative), while causeThetaRole_forces_causer shows the θ-role denotation entails a causer — so only the bieventive analysis accommodates the data, derived from the denotations.

theorem Pylkkanen2008.cause_bieventive_admits_adversity_causative {Time : Type u_1} [LinearOrder Time] (cause : Event Time → Event Time → Prop) (caused : Event Time → Prop) (e e' : Event Time) (hc : caused e') (hcause : cause e e') : ArgumentStructure.causeBieventive cause caused e

[Pyl08] §3.2: the Japanese adversity causative — a causing event with no external argument — is admitted by the bieventive Cause denotation, which the θ-role analysis (forcing a causer) cannot model.

§10. Hebrew possessor datives as low source applicatives

([pylkkanen-2008] Ch. 2 §2.2, Table 2.2 p. 60)

The second major Chapter 2 contribution: possessor datives in Hebrew (and German, French, Korean) are low source applicatives — not double object constructions, not possessor-raising. The relation is reversed directionality: the dative argument is the source (former possessor) of the direct object, not the recipient.

Pylkkänen's Table 2.2 contrasts the predictions of the possessor- raising analysis (Landau 1999, Ura 1996, Kubo 1992) with the low applicative analysis on six properties. The contrast is the paper's own argument — Pylkkänen explicitly compares the two analyses.

inductive Pylkkanen2008.PossessorDativeAnalysis : Type

The two competing analyses of possessor dative constructions ([Pyl08] §2.2).

• possessorRaising : PossessorDativeAnalysis
• lowSourceApplicative : PossessorDativeAnalysis

@[implicit_reducible]

instance Pylkkanen2008.instDecidableEqPossessorDativeAnalysis : DecidableEq PossessorDativeAnalysis

Equations

• Pylkkanen2008.instDecidableEqPossessorDativeAnalysis x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[implicit_reducible]

instance Pylkkanen2008.instReprPossessorDativeAnalysis : Repr PossessorDativeAnalysis

Equations

• Pylkkanen2008.instReprPossessorDativeAnalysis = { reprPrec := Pylkkanen2008.instReprPossessorDativeAnalysis.repr }

def Pylkkanen2008.instReprPossessorDativeAnalysis.repr : PossessorDativeAnalysis → ℕ → Std.Format

Equations

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

inductive Pylkkanen2008.PossessorDativeProperty : Type

Property of possessor dative constructions tested in Table 2.2. quantifierBindingContrast is named to make the encoded property explicit: "qbind possible from DOC IO but NOT from possessor dative" (Landau's contrast claim).

• pseudopossessiveInterpretation : PossessorDativeProperty
• affectedness : PossessorDativeProperty
• lackOfAgentiveInterpretation : PossessorDativeProperty
• transitivityRestriction : PossessorDativeProperty
• quantifierBindingContrast : PossessorDativeProperty
• inabilityToControl : PossessorDativeProperty

@[implicit_reducible]

instance Pylkkanen2008.instDecidableEqPossessorDativeProperty : DecidableEq PossessorDativeProperty

Equations

• Pylkkanen2008.instDecidableEqPossessorDativeProperty x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[implicit_reducible]

instance Pylkkanen2008.instReprPossessorDativeProperty : Repr PossessorDativeProperty

Equations

• Pylkkanen2008.instReprPossessorDativeProperty = { reprPrec := Pylkkanen2008.instReprPossessorDativeProperty.repr }

def Pylkkanen2008.instReprPossessorDativeProperty.repr : PossessorDativeProperty → ℕ → Std.Format

Equations

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

inductive Pylkkanen2008.PredictsVerdict : Type

A 3-valued verdict for what an analysis says about a property: predicts (analysis says the property holds), antipredicts (analysis says the property does not hold), noCleanPrediction (analysis is silent or doesn't make a sharp claim).

• predicts : PredictsVerdict
• antipredicts : PredictsVerdict
• noCleanPrediction : PredictsVerdict

@[implicit_reducible]

instance Pylkkanen2008.instDecidableEqPredictsVerdict : DecidableEq PredictsVerdict

Equations

• Pylkkanen2008.instDecidableEqPredictsVerdict x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Pylkkanen2008.instReprPredictsVerdict.repr : PredictsVerdict → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance Pylkkanen2008.instReprPredictsVerdict : Repr PredictsVerdict

Equations

• Pylkkanen2008.instReprPredictsVerdict = { reprPrec := Pylkkanen2008.instReprPredictsVerdict.repr }

def Pylkkanen2008.PossessorDativeAnalysis.predicts : PossessorDativeAnalysis → PossessorDativeProperty → PredictsVerdict

Pylkkänen's Table 2.2 verdict: which analysis predicts each property. The qbind row is the most subtle: possessor-raising predicts the Landau contrast (qbind from possessor dative but not from DOC), while the low-applicative analysis predicts no contrast (both should permit qbind). Pylkkänen empirically vindicates the low-applicative side: "when pragmatics is controlled for, contrast disappears" (Ch. 2 §2.2.5, p. 56–57).

Equations

• Pylkkanen2008.PossessorDativeAnalysis.possessorRaising.predicts Pylkkanen2008.PossessorDativeProperty.pseudopossessiveInterpretation = Pylkkanen2008.PredictsVerdict.predicts
• Pylkkanen2008.PossessorDativeAnalysis.possessorRaising.predicts Pylkkanen2008.PossessorDativeProperty.affectedness = Pylkkanen2008.PredictsVerdict.antipredicts
• Pylkkanen2008.PossessorDativeAnalysis.possessorRaising.predicts Pylkkanen2008.PossessorDativeProperty.lackOfAgentiveInterpretation = Pylkkanen2008.PredictsVerdict.antipredicts
• Pylkkanen2008.PossessorDativeAnalysis.possessorRaising.predicts Pylkkanen2008.PossessorDativeProperty.transitivityRestriction = Pylkkanen2008.PredictsVerdict.predicts
• Pylkkanen2008.PossessorDativeAnalysis.possessorRaising.predicts Pylkkanen2008.PossessorDativeProperty.quantifierBindingContrast = Pylkkanen2008.PredictsVerdict.predicts
• Pylkkanen2008.PossessorDativeAnalysis.possessorRaising.predicts Pylkkanen2008.PossessorDativeProperty.inabilityToControl = Pylkkanen2008.PredictsVerdict.predicts
• Pylkkanen2008.PossessorDativeAnalysis.lowSourceApplicative.predicts Pylkkanen2008.PossessorDativeProperty.quantifierBindingContrast = Pylkkanen2008.PredictsVerdict.antipredicts
• Pylkkanen2008.PossessorDativeAnalysis.lowSourceApplicative.predicts x✝ = Pylkkanen2008.PredictsVerdict.predicts

def Pylkkanen2008.lowAnalysisPredictedProperties : List PossessorDativeProperty

The 5 properties where the low source analysis predicts the property holds. (Excludes quantifierBindingContrast, where LA antipredicts: it says no contrast exists — empirically vindicated in §2.2.5.)

Equations

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

theorem Pylkkanen2008.low_predicts_five_properties (p : PossessorDativeProperty) : p ∈ lowAnalysisPredictedProperties → PossessorDativeAnalysis.lowSourceApplicative.predicts p = PredictsVerdict.predicts

The low source applicative analysis predicts every property in lowAnalysisPredictedProperties.

theorem Pylkkanen2008.possessor_raising_misses_affectedness_and_agentivity : PossessorDativeAnalysis.possessorRaising.predicts PossessorDativeProperty.affectedness = PredictsVerdict.antipredicts ∧ PossessorDativeAnalysis.possessorRaising.predicts PossessorDativeProperty.lackOfAgentiveInterpretation = PredictsVerdict.antipredicts

The possessor-raising analysis fails on affectedness and lack of agentive interpretation — Pylkkänen's two key objections to the raising analysis (§2.2.2, §2.2.3).

theorem Pylkkanen2008.analyses_oppose_on_qbind : PossessorDativeAnalysis.possessorRaising.predicts PossessorDativeProperty.quantifierBindingContrast = PredictsVerdict.predicts ∧ PossessorDativeAnalysis.lowSourceApplicative.predicts PossessorDativeProperty.quantifierBindingContrast = PredictsVerdict.antipredicts

On the qbind row, the two analyses make opposing predictions. Pylkkänen's empirical argument (§2.2.5) is that the contrast Landau claimed disappears when pragmatics is controlled — so LA's .antipredicts (no contrast) wins, PR's .predicts (contrast exists) loses.

§11. Japanese adversity passives: high vs low split

(Kubo's 1992 work (cited by [pylkkanen-2008]; not yet in linglib bib) diagnostics, reanalyzed in
[pylkkanen-2008] Ch. 2 §2.3)

Japanese adversity passives split into gapped (low source applicative) and gapless (high applicative). The gapped/gapless distinction itself is Kubo's 1992 work (cited by [Pyl08]; not yet in linglib bib)'s; [Pyl08]'s contribution is the reanalysis as a low-source vs. high applicative typology. Both share the -rare- passive morphology; the distinguishing criterion is the possessive/transfer relation to the direct object — the gapped (low source) type requires it, the gapless (high malefactive) type bears a malefactive relation to the event and no necessary relation to the object. The diagnostic bundle distinguishing the two types is not formalized here; this section records the type-level split for cross-reference.

inductive Pylkkanen2008.JapaneseAdversityType : Type

The two types of Japanese adversity passive ([Pyl08] §2.3).

• gappedLowSource : JapaneseAdversityType

  Gapped: low source applicative. The affected DP is inside VP, with a transfer-of-possession relation to the underlying object.

• gaplessHigh : JapaneseAdversityType

  Gapless: high applicative. The affected DP is outside VP, relating to the event as a whole.

@[implicit_reducible]

instance Pylkkanen2008.instDecidableEqJapaneseAdversityType : DecidableEq JapaneseAdversityType

Equations

• Pylkkanen2008.instDecidableEqJapaneseAdversityType x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Pylkkanen2008.instReprJapaneseAdversityType.repr : JapaneseAdversityType → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance Pylkkanen2008.instReprJapaneseAdversityType : Repr JapaneseAdversityType

Equations

• Pylkkanen2008.instReprJapaneseAdversityType = { reprPrec := Pylkkanen2008.instReprJapaneseAdversityType.repr }

def Pylkkanen2008.JapaneseAdversityType.toApplType : JapaneseAdversityType → Minimalist.ApplType

The classification of an adversity passive type into the standard ApplType taxonomy.

Equations

• Pylkkanen2008.JapaneseAdversityType.gappedLowSource.toApplType = Minimalist.ApplType.lowSource
• Pylkkanen2008.JapaneseAdversityType.gaplessHigh.toApplType = Minimalist.ApplType.high

theorem Pylkkanen2008.gapped_is_low_source : JapaneseAdversityType.gappedLowSource.toApplType = Minimalist.ApplType.lowSource

theorem Pylkkanen2008.gapless_is_high : JapaneseAdversityType.gaplessHigh.toApplType = Minimalist.ApplType.high

§12. Spanish static low applicatives ([Cue03],

discussed in [pylkkanen-2008] §2.1.4.2)

[Cue03]'s thesis proposes a three-way split of low applicatives in Spanish: low-to (recipient, dynamic), low-from (source, dynamic), and low-AT (static possession). The static type is Cuervo's contribution; Pylkkänen briefly endorses it in §2.1.4.2 as compatible with her event-vs-state distinction. The static applicative combines with small clause predicates (e.g. Pablo le admira la paciencia a Valeria "Pablo admires Valeria's patience"), unlike English low recipients which require event-creating verbs.

inductive Pylkkanen2008.CuervoLowAppl : Type

Cuervo's three-way split of low applicatives. The third type (staticPossession) is [Cue03]'s extension; it is not in the canonical ApplType taxonomy because it requires static rather than dynamic semantics, and (per Cuervo) it specifically takes a small-clause complement.

• recipient : CuervoLowAppl
• source : CuervoLowAppl
• staticPossession : CuervoLowAppl

@[implicit_reducible]

instance Pylkkanen2008.instDecidableEqCuervoLowAppl : DecidableEq CuervoLowAppl

Equations

• Pylkkanen2008.instDecidableEqCuervoLowAppl x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Pylkkanen2008.instReprCuervoLowAppl.repr : CuervoLowAppl → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance Pylkkanen2008.instReprCuervoLowAppl : Repr CuervoLowAppl

Equations

• Pylkkanen2008.instReprCuervoLowAppl = { reprPrec := Pylkkanen2008.instReprCuervoLowAppl.repr }

def Pylkkanen2008.CuervoLowAppl.isDynamic : CuervoLowAppl → Bool

Both of Pylkkänen's two low types correspond to dynamic transfer; Cuervo's third is static.

Equations

• Pylkkanen2008.CuervoLowAppl.recipient.isDynamic = true
• Pylkkanen2008.CuervoLowAppl.source.isDynamic = true
• Pylkkanen2008.CuervoLowAppl.staticPossession.isDynamic = false

theorem Pylkkanen2008.static_not_dynamic : CuervoLowAppl.staticPossession.isDynamic = false

The static low applicative is not one of Pylkkänen's two types — it requires the event-vs-state generalization in §2.1.4.2.

§13. Causative typology (Pylkkänen Table 3.1, Ch. 3 intro p. 87)

Pylkkänen Table 3.1 (Chapter 3 introduction, p. 87 — not §3.4, which argues the three-way selection split and carries the separate Table 3.2) is a 2 × 3 typology of causative constructions parameterized by Voice-bundling × selection. The inventory (VoiceBundlingChoice, CauseSelection, MorphologyAccess, CausativeCell + 6 canonical instances + 4 prediction theorems) lives here; Pylkkanen2008 is the sole writer in the codebase, so substrate promotion is unwarranted (per CLAUDE.md "promote when ≥2 consumers").

Orthogonal to [Son96]'s expression-style typology in Studies/Song1996.lean: Song classifies the morphosyntactic packaging of a causative (compact / and / purp); Pylkkänen classifies the underlying syntactic configuration (Voice-bundled vs independent; selecting root, verb, or phase). A language is characterized along both axes (English is COMPACT in Song, bundled-root in Pylkkänen).

If Wood 2015 / Cuervo 2003 / Folli-Harley 2005 get formalized later as generative-side updates of this typology and re-use these cells, they should consume them from here. The earlier extracted-to-Causation/Typology plan was overengineering for n=1 writer; the file relocates here when the natural single home turns out to be the only home.

inductive Pylkkanen2008.VoiceBundlingChoice : Type

[Pyl08] §3.3: whether Cause and Voice are bundled into one morphological head. English bundles ([Cause, Voice]); Japanese and Finnish do not.

• bundled : VoiceBundlingChoice
• independent : VoiceBundlingChoice

@[implicit_reducible]

instance Pylkkanen2008.instDecidableEqVoiceBundlingChoice : DecidableEq VoiceBundlingChoice

Equations

• Pylkkanen2008.instDecidableEqVoiceBundlingChoice x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Pylkkanen2008.instReprVoiceBundlingChoice.repr : VoiceBundlingChoice → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance Pylkkanen2008.instReprVoiceBundlingChoice : Repr VoiceBundlingChoice

Equations

• Pylkkanen2008.instReprVoiceBundlingChoice = { reprPrec := Pylkkanen2008.instReprVoiceBundlingChoice.repr }

inductive Pylkkanen2008.CauseSelection : Type

[Pyl08] §3.4: what does Cause select for?

• root : CauseSelection

  Cause + √Root: causes a category-free root (English zero-causative).

• verb : CauseSelection

  Cause + v + √Root: causes a category-defined verb (Bemba -eshya, Finnish -tta).

• phase : CauseSelection

  Cause + (something at least as big as a phase, can include external args): causativizes unergatives and transitives (Luganda -sa, Venda -is).

@[implicit_reducible]

instance Pylkkanen2008.instDecidableEqCauseSelection : DecidableEq CauseSelection

Equations

• Pylkkanen2008.instDecidableEqCauseSelection x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Pylkkanen2008.instReprCauseSelection.repr : CauseSelection → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance Pylkkanen2008.instReprCauseSelection : Repr CauseSelection

Equations

• Pylkkanen2008.instReprCauseSelection = { reprPrec := Pylkkanen2008.instReprCauseSelection.repr }

inductive Pylkkanen2008.MorphologyAccess : Type

Three levels of root-Cause morpheme intervention. The three-way distinction is essential — collapsing to Bool would lose §3.4's central typological claim.

• none : MorphologyAccess
• categoryDefiningOnly : MorphologyAccess
• allMorphology : MorphologyAccess

@[implicit_reducible]

instance Pylkkanen2008.instDecidableEqMorphologyAccess : DecidableEq MorphologyAccess

Equations

• Pylkkanen2008.instDecidableEqMorphologyAccess x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Pylkkanen2008.instReprMorphologyAccess.repr : MorphologyAccess → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance Pylkkanen2008.instReprMorphologyAccess : Repr MorphologyAccess

Equations

• Pylkkanen2008.instReprMorphologyAccess = { reprPrec := Pylkkanen2008.instReprMorphologyAccess.repr }

structure Pylkkanen2008.CausativeCell : Type

A causative-typology cell: Voice-bundling × selection. bundling is Option because Pylkkänen Table 3.1 footnote a explicitly states the Voice-bundling properties of Bemba, Luganda, and Venda causatives are not known.

• bundling : Option VoiceBundlingChoice
• selection : CauseSelection

@[implicit_reducible]

instance Pylkkanen2008.instDecidableEqCausativeCell : DecidableEq CausativeCell

Equations

• Pylkkanen2008.instDecidableEqCausativeCell = Pylkkanen2008.instDecidableEqCausativeCell.decEq

def Pylkkanen2008.instDecidableEqCausativeCell.decEq (x✝ x✝¹ : CausativeCell) : Decidable (x✝ = x✝¹)

Equations

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

def Pylkkanen2008.instReprCausativeCell.repr : CausativeCell → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance Pylkkanen2008.instReprCausativeCell : Repr CausativeCell

Equations

• Pylkkanen2008.instReprCausativeCell = { reprPrec := Pylkkanen2008.instReprCausativeCell.repr }

def Pylkkanen2008.CausativeCell.permitsUnaccusativeCausative (c : CausativeCell) : PredictsVerdict

Table 3.1 prediction (1): can a language have unaccusative causatives? Bundled → no (Voice forces ext arg); independent → yes; unknown → no clean prediction. (Reuses the PredictsVerdict enum defined in §10 above for PossessorDativeAnalysis.predicts.)

Equations

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

def Pylkkanen2008.CausativeCell.permitsUnergativeAndTransitiveCausativization (c : CausativeCell) : Bool

Table 3.1 prediction (2): can the language causativize unergatives and transitives? Verb- and phase-selecting Cause can; only root-selecting Cause cannot. (Table 3.1's prediction (2) is identical across both Voice-bundling columns, so it turns on selection alone.)

Equations

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

def Pylkkanen2008.CausativeCell.morphologyAccess (c : CausativeCell) : MorphologyAccess

Table 3.1 prediction (3): what morphology can intervene between root and Cause?

Equations

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

def Pylkkanen2008.englishZeroCausative : CausativeCell

English zero-causative: Voice-bundling root-selecting.

Equations

• Pylkkanen2008.englishZeroCausative = { bundling := some Pylkkanen2008.VoiceBundlingChoice.bundled, selection := Pylkkanen2008.CauseSelection.root }

def Pylkkanen2008.japaneseLexicalCausative : CausativeCell

Japanese lexical causative: non-Voice-bundling root-selecting.

Equations

• Pylkkanen2008.japaneseLexicalCausative = { bundling := some Pylkkanen2008.VoiceBundlingChoice.independent, selection := Pylkkanen2008.CauseSelection.root }

def Pylkkanen2008.bembaEshyaCausative : CausativeCell

Bemba -eshya causative: verb-selecting; bundling unknown (Table 3.1 footnote a).

Equations

• Pylkkanen2008.bembaEshyaCausative = { bundling := none, selection := Pylkkanen2008.CauseSelection.verb }

def Pylkkanen2008.finnishTtaCausative : CausativeCell

Finnish -tta causative: non-Voice-bundling verb-selecting.

Equations

• Pylkkanen2008.finnishTtaCausative = { bundling := some Pylkkanen2008.VoiceBundlingChoice.independent, selection := Pylkkanen2008.CauseSelection.verb }

def Pylkkanen2008.lugandaSaCausative : CausativeCell

Luganda -sa causative: phase-selecting; bundling unknown.

Equations

• Pylkkanen2008.lugandaSaCausative = { bundling := none, selection := Pylkkanen2008.CauseSelection.phase }

def Pylkkanen2008.vendaIsCausative : CausativeCell

Venda -is causative: phase-selecting; bundling unknown.

Equations

• Pylkkanen2008.vendaIsCausative = { bundling := none, selection := Pylkkanen2008.CauseSelection.phase }

theorem Pylkkanen2008.english_zero_is_bundled : englishZeroCausative.bundling = some VoiceBundlingChoice.bundled

§11 Voice-bundling cross-references. English bundles, Japanese does not — the two canonical affirmations §11 promised live here alongside the Cell definitions they consume.

theorem Pylkkanen2008.japanese_lexical_is_independent : japaneseLexicalCausative.bundling = some VoiceBundlingChoice.independent

theorem Pylkkanen2008.english_zero_predictions : englishZeroCausative.permitsUnaccusativeCausative = PredictsVerdict.antipredicts ∧ englishZeroCausative.permitsUnergativeAndTransitiveCausativization = false ∧ englishZeroCausative.morphologyAccess = MorphologyAccess.none

theorem Pylkkanen2008.japanese_lexical_predictions : japaneseLexicalCausative.permitsUnaccusativeCausative = PredictsVerdict.predicts ∧ japaneseLexicalCausative.permitsUnergativeAndTransitiveCausativization = false ∧ japaneseLexicalCausative.morphologyAccess = MorphologyAccess.none

theorem Pylkkanen2008.finnish_tta_predictions : finnishTtaCausative.permitsUnaccusativeCausative = PredictsVerdict.predicts ∧ finnishTtaCausative.permitsUnergativeAndTransitiveCausativization = true ∧ finnishTtaCausative.morphologyAccess = MorphologyAccess.categoryDefiningOnly

theorem Pylkkanen2008.luganda_phase_predictions : lugandaSaCausative.permitsUnaccusativeCausative = PredictsVerdict.noCleanPrediction ∧ lugandaSaCausative.permitsUnergativeAndTransitiveCausativization = true ∧ lugandaSaCausative.morphologyAccess = MorphologyAccess.allMorphology

§14. Broader Voice taxonomy under Pylkkänen's view

Pylkkänen's Voice = external-argument introducer. Per the "Voice projection" section above, this is one of two competing views of Voice (the other being Collins/Storment's smuggling projection). Test Pylkkänen's view against the broader VoiceHead taxonomy in Syntax/Minimalism/Voice.lean: which Voice flavors do introduce external arguments?

theorem Pylkkanen2008.pylkkanen_view_partitions_voice_flavors : IsExternalArgIntroducer Minimalist.voiceAgent ∧ IsExternalArgIntroducer Minimalist.voiceCauser ∧ IsExternalArgIntroducer Minimalist.voiceReflexive ∧ IsExternalArgIntroducer Minimalist.voiceExperiencer ∧ ¬IsExternalArgIntroducer Minimalist.voiceMiddle ∧ ¬IsExternalArgIntroducer Minimalist.voiceImpersonal ∧ ¬IsExternalArgIntroducer Minimalist.voiceAnticausative ∧ ¬IsExternalArgIntroducer Minimalist.voicePassive

Pylkkänen's view of Voice tested against all 8 named canonical flavors: voiceAgent, voiceCauser, voiceReflexive, and voiceExperiencer introduce external arguments; voiceMiddle (expletive), voiceImpersonal, voiceAnticausative, and voicePassive do not. The Pylkkänen-coherent Voice flavors are exactly the θ-assigning ones. (.antipassive is defined as a flavor in the Voice taxonomy but lacks a canonical voiceAntipassive constant in Voice.lean.)

§15. Transitivity restriction grounded in EntailmentProfile

([pylkkanen-2008] Diagnostic 1 = eq. 17, p. 18; semantic
argument at eq. 103, p. 55)

Pylkkänen's predicted generalization (book Ch. 2 §2.1.1, Diagnostic 1, eq. 17, p. 18): "Only high applicative heads should be able to combine with unergatives. Since low applicative heads denote a relation between the direct object and the indirect object, a low applicative head cannot appear in a structure that lacks a direct object."

The semantic argument (eq. 103, p. 55): combining low Appl (λx.λy.λf.λe. f(e,x) ∧ theme(e,x) ∧ HAVE(x,y)) with an unergative VP (λe. agent(e, Mary) ∧ run(e)) yields agent(e, x) ∧ theme(e, x) when both arguments bind the same variable — a thematic-uniqueness contradiction.

Status of this formalization: The composition predicate below uses ArgumentStructure.EntailmentProfile.pPatientScore to check whether a verb has theme-like Proto-Patient entailments. An unergative has either no object profile (objectEntailments = none) or an empty one (pPatientScore = 0). This EntailmentProfile-based predicate is the structural surface; the event-semantic derivation of the eq. 103 type clash is now wired in via Semantics/ArgumentStructure/ArgumentIntroduction.lean and consumed in §15c below (low_appl_blocks_unergative_denotational, low_external_arg_clash).

def Pylkkanen2008.hasUnsaturatedTheme (objectProfile : Option ArgumentStructure.EntailmentProfile) : Prop

A verb has an unsaturated theme argument iff its object entailment profile (if any) carries Proto-Patient entailments. Unergatives have objectEntailments = none; transitives have pPatientScore ≥ 1.

Equations

• Pylkkanen2008.hasUnsaturatedTheme (some p) = (p.pPatientScore > 0)
• Pylkkanen2008.hasUnsaturatedTheme none = False

@[implicit_reducible]

instance Pylkkanen2008.instDecidableHasUnsaturatedTheme (op : Option ArgumentStructure.EntailmentProfile) : Decidable (hasUnsaturatedTheme op)

Equations

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

def Pylkkanen2008.applicativeComposition (a : Minimalist.ApplType) (objectProfile : Option ArgumentStructure.EntailmentProfile) : Prop

A composition of an applicative head with a verb's object profile is well-formed iff either the applicative doesn't require a theme (high) or the verb's object profile provides one (transitive).

Equations

• Pylkkanen2008.applicativeComposition a objectProfile = (¬a.RequiresThemeInComplement ∨ Pylkkanen2008.hasUnsaturatedTheme objectProfile)

theorem Pylkkanen2008.low_applicative_blocks_unergative (a : Minimalist.ApplType) (hLow : a.IsLow) : ¬applicativeComposition a none

Pylkkänen's Diagnostic 1: low applicatives cannot combine with unergative verbs (whose object profile is none). The composition theorem follows from ApplType.RequiresThemeInComplement for low types and the empty object profile of an unergative.

Note: this is structural, not a re-derivation of the eq. 103 type contradiction from event-semantic composition. The substantive semantic argument requires λ-calculus infrastructure not present in Semantics/Composition/ for applicatives. The theorem captures the empirical content (low + unergative fails) without proving it from event-semantic types.

theorem Pylkkanen2008.high_applicative_combines_with_unergative : applicativeComposition Minimalist.ApplType.high none

High applicatives can combine with unergatives — the empirical finding for Luganda/Venda/Albanian (PDF eq. 23a/24a/25a, all verified). Follows from ¬ ApplType.high.RequiresThemeInComplement.

def Pylkkanen2008.themeBearingProfile : ArgumentStructure.EntailmentProfile

A toy theme-bearing object profile: Proto-Patient with incrementalTheme set. Used to demonstrate transitive composition in the next two theorems.

Equations

• Pylkkanen2008.themeBearingProfile = { incrementalTheme := true }

theorem Pylkkanen2008.themeBearingProfile_has_unsaturated_theme : hasUnsaturatedTheme (some themeBearingProfile)

theorem Pylkkanen2008.low_recipient_combines_with_transitive : applicativeComposition Minimalist.ApplType.lowRecipient (some themeBearingProfile)

Low recipient applicatives can combine with verbs providing a theme — the canonical English DOC pattern (I baked him a cake).

theorem Pylkkanen2008.low_source_combines_with_transitive : applicativeComposition Minimalist.ApplType.lowSource (some themeBearingProfile)

Low source applicatives also combine with theme-providing verbs — Hebrew possessor datives (book §2.2).

§15c. Event-semantic grounding: the transitivity restriction derived

The applicativeComposition predicate above captures the empirical content structurally (via ApplType.RequiresThemeInComplement). The denotational derivation of [Pyl08]'s eq. 103 — the type clash that forces the transitivity restriction — lives in Semantics/ArgumentStructure/ArgumentIntroduction.lean. There the high/low contrast is IntroMode.toEvent/.toTheme, the two diagnostics are toTheme_blocks_unergative (Diagnostic 1, no internal argument) and toTheme_blocks_kimian (Diagnostic 2, no event argument — Kimian states, [Mol25]), and the thematic-uniqueness contradiction is low_external_arg_clash. We record the correspondence: Pylkkänen's ApplType projects to an IntroMode, and the empirical diagnostics are instances of the substrate theorems rather than restatements of the IsLow predicate.

def Pylkkanen2008.applIntroMode : Minimalist.ApplType → ArgumentStructure.IntroMode

Pylkkänen's high/low ApplType as a denotational introduction mode ([WM17]'s contextually-interpreted introducer).

Equations

• Pylkkanen2008.applIntroMode Minimalist.ApplType.high = ArgumentStructure.IntroMode.toEvent
• Pylkkanen2008.applIntroMode Minimalist.ApplType.lowRecipient = ArgumentStructure.IntroMode.toTheme
• Pylkkanen2008.applIntroMode Minimalist.ApplType.lowSource = ArgumentStructure.IntroMode.toTheme

theorem Pylkkanen2008.low_appl_blocks_unergative_denotational {Entity : Type u_1} {Time : Type u_2} [LinearOrder Time] (a : Minimalist.ApplType) (hLow : a.IsLow) (body : Event Time → Prop) : ¬(applIntroMode a).Licenses (ArgumentStructure.VerbDenot.unergative body)

The transitivity restriction, derived from the denotations: a low applicative (recipient or source) cannot license an unergative verb, because the low denotation has no event-internal theme to relate to. This is low_applicative_blocks_unergative re-grounded in the ArgumentIntroduction substrate rather than the IsLow alias.

theorem Pylkkanen2008.high_appl_licenses_unergative_denotational {Entity : Type u_1} {Time : Type u_2} [LinearOrder Time] (body : Event Time → Prop) : (applIntroMode Minimalist.ApplType.high).Licenses (ArgumentStructure.VerbDenot.unergative body)

High applicatives license unergatives, derived denotationally (Luganda/Venda/Albanian, PDF eq. 23a/24a/25a).

§16. Voice × Appl licensing matrix

(`Syntax/Minimalism/Applicative.lean.Licensed`)

ApplHead.Licensed (in Applicative.lean) checks whether a particular Appl head is licensed with a given Voice head: high applicatives require event-introducing Voice (hasSemantics = true); low applicatives are licensed with any Voice. Cross [Pyl08]'s high/low Appl typology with the VoiceHead taxonomy: which Voice flavors license high Appl, and which don't?

This connects §14's Pylkkänen-Voice partition with the [Pyl08] Appl typology in a single matrix.

theorem Pylkkanen2008.voice_appl_licensing_matrix : Minimalist.applHigh.Licensed Minimalist.voiceAgent ∧ Minimalist.applHigh.Licensed Minimalist.voiceCauser ∧ Minimalist.applLowRecipient.Licensed Minimalist.voiceAgent ∧ Minimalist.applLowRecipient.Licensed Minimalist.voicePassive ∧ Minimalist.applLowSource.Licensed Minimalist.voiceAnticausative

High Appl requires Voice with event semantics. The named Voice flavors split: voiceAgent/voiceCauser/voiceMiddle/ voiceImpersonal/voiceReflexive/voiceExperiencer carry event semantics and license high Appl; voiceAnticausative/voicePassive do not (they're event-semantically inert in this Voice taxonomy) and so don't license high Appl.

§17. WALS-vs-Pylkkänen divergence on English/Japanese applicatives

The WALS Ch 109 typology classifies English and Japanese as having "no applicative" (no overt valence-increasing morphology). Pylkkänen's analysis classifies the English double-object construction (DOC) and the Japanese -ni recipient construction as low recipient applicatives (structural Appl head merged below V relating recipient to theme).

The divergence is not empirical — both accounts agree on the same constructions. It is a methodological choice about what counts as an "applicative." WALS counts overt verbal applicative morphology; Pylkkänen counts the structural ApplP projection regardless of morphological exponent. The substrate is designed to make this kind of cross-framework editorial disagreement visible.

theorem Pylkkanen2008.wals_pylkkanen_diverge_on_english : Option.map (fun (x : Data.WALS.Datapoint Data.WALS.F109A.ApplicativeType) => x.value) (Data.WALS.F109A.lookupISO "eng") = some Data.WALS.F109A.ApplicativeType.noApplicative ∧ english_appl.classification = Minimalist.ApplType.lowRecipient

WALS Ch 109 codes English as .noApplicative (no overt valence-increasing morphology), while Pylkkänen's analysis (english_appl.classification) classifies the English double-object construction as .lowRecipient. The disagreement is about the criterion for "applicative," not the data.

theorem Pylkkanen2008.wals_pylkkanen_diverge_on_japanese : Option.map (fun (x : Data.WALS.Datapoint Data.WALS.F109A.ApplicativeType) => x.value) (Data.WALS.F109A.lookupISO "jpn") = some Data.WALS.F109A.ApplicativeType.noApplicative ∧ japanese_appl.classification = Minimalist.ApplType.lowRecipient