@cite{pylkkanen-2008} — Introducing Arguments

@cite{pylkkanen-2008} @cite{cuervo-2003} @cite{barss-lasnik-1986}

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 @cite{barss-lasnik-1986} 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 Theories/Syntax/Minimalism/ApplicativeDiagnostics.lean.

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.

def Pylkkanen2008.voice_ag_t : Minimalist.SyntacticObject

Equations

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

def Pylkkanen2008.appl_low_t : Minimalist.SyntacticObject

Equations

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

def Pylkkanen2008.appl_high_t : Minimalist.SyntacticObject

Equations

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

def Pylkkanen2008.V_sent_t : Minimalist.SyntacticObject

Equations

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

def Pylkkanen2008.V_eat_t : Minimalist.SyntacticObject

Equations

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

def Pylkkanen2008.DP_john_t : Minimalist.SyntacticObject

Equations

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

def Pylkkanen2008.DP_mary_t : Minimalist.SyntacticObject

Equations

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

def Pylkkanen2008.DP_letter_t : Minimalist.SyntacticObject

Equations

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

def Pylkkanen2008.DP_wife_t : Minimalist.SyntacticObject

Equations

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

def Pylkkanen2008.DP_food_t : Minimalist.SyntacticObject

Equations

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

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 @cite{barss-lasnik-1986} asymmetry that IO asymmetrically c-commands DO.

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.cCommandsIn ditransitiveTree DP_john_t DP_mary_t

Agent c-commands goal.

theorem Pylkkanen2008.ditransitive_agent_ccommands_theme : Minimalist.cCommandsIn ditransitiveTree DP_john_t DP_letter_t

Agent c-commands theme.

theorem Pylkkanen2008.ditransitive_goal_ccommands_theme : Minimalist.cCommandsIn ditransitiveTree DP_mary_t DP_letter_t

Goal c-commands theme — the @cite{barss-lasnik-1986} asymmetry derived structurally from V selecting ApplP.

theorem Pylkkanen2008.ditransitive_theme_not_ccommands_goal : ¬Minimalist.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.cCommandsIn benefactiveTree DP_wife_t DP_food_t

Benefactive c-commands theme.

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

Theme does NOT c-command benefactive.

theorem Pylkkanen2008.send_is_low_appl : Minimalist.contains ditransitiveTree appl_low_t

Low applicative marks the ditransitive.

theorem Pylkkanen2008.eat_is_high_appl : Minimalist.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 Theories/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.

@cite{pylkkanen-2008} 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 Minimalist.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 Minimalist.ApplDiagnosticBundle; classification records Pylkkänen's analytical conclusion.

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

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

@[implicit_reducible]

instance Pylkkanen2008.instReprLangApplProfile : Repr LangApplProfile

Equations

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

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

Equations

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

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 "depictives" can also modify implicit external arguments and DPs inside PPs, so they don't qualify as English-style depictives — 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 : Minimalist.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 : Minimalist.classifyByDiagnostics luganda_appl.diagnostics = some Minimalist.ApplType.high

theorem Pylkkanen2008.hebrew_classification_derives_to_low : Minimalist.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.

@cite{larson-1988}'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 : Minimalist.cCommandsIn Larson1988.docDativeShift.final Larson1988.DP_mary Larson1988.DP_letter ∧ ¬Minimalist.cCommandsIn Larson1988.docDativeShift.final Larson1988.DP_letter Larson1988.DP_mary ∧ Minimalist.cCommandsIn ditransitiveTree DP_mary_t DP_letter_t ∧ ¬Minimalist.cCommandsIn ditransitiveTree DP_letter_t DP_mary_t

@cite{larson-1988}'s DOC and the modern Voice + low-Appl derivation produce the same c-command hierarchy: IO asymmetrically c-commands DO.

This proves that @cite{larson-1988} and @cite{pylkkanen-2008}, despite different decompositions, converge on the same structural prediction for @cite{barss-lasnik-1986} asymmetries.

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

(@cite{pylkkanen-2008} Ch. 3 §3.2 + Ch. 4 §4.2)

@cite{pylkkanen-2008}'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 @cite{kratzer-1996}. 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 Theories/Syntax/Minimalism/VoiceProjection.lean. The other view, defended by @cite{collins-2005} and @cite{storment-2026}, treats Voice as a structural head (the smuggling projection) and assigns external-argument introduction to v instead. The two views are orthogonal — see VoiceProjection.lean for the substantive contrast.

theorem Pylkkanen2008.voice_introduces_external_arg_pylkkanen : Minimalist.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

(@cite{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 (@cite{pylkkanen-2008} 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 (eq. 19–25) 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.

Formalizing the bieventive vs. θ-role contrast at the level of detail Pylkkänen offers requires event semantics infrastructure beyond this study file's scope; the substantive claim is recorded here for cross-reference.

§10. Hebrew possessor datives as low source applicatives

(@cite{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 (@cite{pylkkanen-2008} §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 @cite{pylkkanen-2008}; not yet in linglib bib) diagnostics, reanalyzed in
@cite{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 @cite{pylkkanen-2008}; not yet in linglib bib)'s; @cite{pylkkanen-2008}'s contribution is the reanalysis as a low-source vs. high applicative typology. Both share the -rare- morphology, but only the gapless type carries an obligatory adversative entailment (Kubo's 1992 work (cited by @cite{pylkkanen-2008}; not yet in linglib bib)). 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 (@cite{pylkkanen-2008} §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 (@cite{cuervo-2003},

discussed in @cite{pylkkanen-2008} §2.1.4.2)

@cite{cuervo-2003}'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 @cite{cuervo-2003}'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, §3.4)

Pylkkänen Table 3.1 (§3.4) 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 @cite{song-1996}'s expression-style typology in Phenomena/Causation/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

@cite{pylkkanen-2008} §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

@cite{pylkkanen-2008} §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

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

Equations

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

@[implicit_reducible]

instance Pylkkanen2008.instDecidableEqCausativeCell : DecidableEq CausativeCell

Equations

• Pylkkanen2008.instDecidableEqCausativeCell = Pylkkanen2008.instDecidableEqCausativeCell.decEq

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? Only phase-selecting Cause can.

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 = false ∧ 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 Theories/Syntax/Minimalism/VoiceProjection.lean, 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 Theories/Syntax/Minimalism/Voice.lean: which Voice flavors do introduce external arguments?

theorem Pylkkanen2008.pylkkanen_view_partitions_voice_flavors : Minimalist.IsExternalArgIntroducer Minimalist.voiceAgent ∧ Minimalist.IsExternalArgIntroducer Minimalist.voiceCauser ∧ Minimalist.IsExternalArgIntroducer Minimalist.voiceReflexive ∧ Minimalist.IsExternalArgIntroducer Minimalist.voiceExperiencer ∧ ¬Minimalist.IsExternalArgIntroducer Minimalist.voiceMiddle ∧ ¬Minimalist.IsExternalArgIntroducer Minimalist.voiceImpersonal ∧ ¬Minimalist.IsExternalArgIntroducer Minimalist.voiceAnticausative ∧ ¬Minimalist.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

(@cite{pylkkanen-2008} Diagnostic 1; semantic argument at eq. 103 /
p. 55; -- UNVERIFIED: eq. 17 number)

Pylkkänen's predicted generalization (book Ch. 2 §2.1.1, Diagnostic 1): "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 (Carlson, Parsons).

Status of this formalization: The composition predicate below uses Core.Verbs.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). The composition theorem is structural — it does not re-derive the type clash from event-semantic λ-calculus (that requires the compositional type-driven semantics in Theories/Semantics/Composition/, not yet wired in here). The substantive content captured: "low Appl needs a theme; unergative provides none; composition fails."

def Pylkkanen2008.hasUnsaturatedTheme (objectProfile : Option Semantics.ArgumentStructure.EntailmentProfile.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 Semantics.ArgumentStructure.EntailmentProfile.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 Semantics.ArgumentStructure.EntailmentProfile.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 Theories/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 : Semantics.ArgumentStructure.EntailmentProfile.EntailmentProfile

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

Equations

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

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).

§16. Voice × Appl licensing matrix

(`Theories/Syntax/Minimalism/Applicative.lean.licensedWith`)

ApplHead.licensedWith (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 @cite{pylkkanen-2008}'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 @cite{pylkkanen-2008} Appl typology in a single matrix.

theorem Pylkkanen2008.voice_appl_licensing_matrix : Minimalist.applHigh.licensedWith Minimalist.voiceAgent = true ∧ Minimalist.applHigh.licensedWith Minimalist.voiceCauser = true ∧ Minimalist.applLowRecipient.licensedWith Minimalist.voiceAgent = true ∧ Minimalist.applLowRecipient.licensedWith Minimalist.voicePassive = true ∧ Minimalist.applLowSource.licensedWith Minimalist.voiceAnticausative = true

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 : Phenomena.ArgumentStructure.Studies.Polinsky2013.english.applicative = Typology.ArgumentStructure.ApplicativeType.noApplicative ∧ english_appl.classification = Minimalist.ApplType.lowRecipient

WALS Ch 109 (per Studies/Polinsky2013.lean's english.applicative) and Pylkkänen's analysis (english_appl.classification) make contradictory predictions about English: WALS says no applicative, Pylkkänen says low recipient. Same for Japanese. The disagreement is about the criterion for "applicative," not about the data.

theorem Pylkkanen2008.wals_pylkkanen_diverge_on_japanese : Phenomena.ArgumentStructure.Studies.Polinsky2013.japanese.applicative = Typology.ArgumentStructure.ApplicativeType.noApplicative ∧ japanese_appl.classification = Minimalist.ApplType.lowRecipient