Greenberg 1963: Implicational Universals on Basic Word Order

@cite{greenberg-1963} @cite{dryer-haspelmath-2013}

@cite{greenberg-1963} stated 45 cross-linguistic implicational universals on basic constituent order, adposition order, and related construction-pair correlations. This file formalises three of the most cited, tested over a curated 15-language Fragment-derived sample:

• Universal 1: subject-before-object orders (SOV + SVO + VSO) dominate over object-before-subject orders (VOS + OVS + OSV).
• Universal 3: VSO languages are prepositional.
• Universal 4: SOV languages are postpositional (with overwhelmingly greater than chance frequency).

All three are tested over fragmentSample, a 15-language Fragment-derived sample. The substrate type ImplicationalUniversal lives in Linglib/Typology/Universal.lean. WALS-aggregate distributional claims (SOV-most-common, SV-dominates-VS, etc.) live in Studies/DryerHaspelmath2013.lean.

The 15-language sample bundles each language's Fragment-sourced WordOrderProfile (Ch 81/82/83) and Option AdpositionOrder (Ch 85). Per- language data lives in Fragments/{Lang}/{WordOrder,Adposition}.lean; the sample just bundles them with an ISO code and a human-readable name. Sample shape is hand-curated to span the four major basic-order classes — Tzotzil (VOS) and Hixkaryana (OVS) are deliberately included so U1's "object- initial languages exist but are rare" statistical character can be tested non-vacuously.

structure Phenomena.WordOrder.Studies.Greenberg1963.SampleEntry : Type

A sample-language entry for the Greenberg / cross-chapter theorems: Fragment-sourced word-order profile plus adposition order.

• iso : String
• name : String
• wordOrder : Typology.WordOrder.WordOrderProfile
• adposition : Typology.Adposition.AdpositionOrder

def Phenomena.WordOrder.Studies.Greenberg1963.instReprSampleEntry.repr : SampleEntry → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance Phenomena.WordOrder.Studies.Greenberg1963.instReprSampleEntry : Repr SampleEntry

Equations

• Phenomena.WordOrder.Studies.Greenberg1963.instReprSampleEntry = { reprPrec := Phenomena.WordOrder.Studies.Greenberg1963.instReprSampleEntry.repr }

@[implicit_reducible]

instance Phenomena.WordOrder.Studies.Greenberg1963.instDecidableEqSampleEntry : DecidableEq SampleEntry

Equations

• Phenomena.WordOrder.Studies.Greenberg1963.instDecidableEqSampleEntry = Phenomena.WordOrder.Studies.Greenberg1963.instDecidableEqSampleEntry.decEq

def Phenomena.WordOrder.Studies.Greenberg1963.instDecidableEqSampleEntry.decEq (x✝ x✝¹ : SampleEntry) : Decidable (x✝ = x✝¹)

Equations

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

def Phenomena.WordOrder.Studies.Greenberg1963.fragmentSample : Finset SampleEntry

Hand-verified 15-language sample spanning the four major basic-order classes (SOV, SVO, VSO, plus a couple non-SVO entries) with adposition data attested in WALS. Used for stating cross-linguistic Greenbergian universals via Typology.ImplicationalUniversal.

Equations

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

@[reducible, inline]

abbrev Phenomena.WordOrder.Studies.Greenberg1963.isVSO (p : SampleEntry) : Prop

Language has WALS basic order VSO.

Equations

• Phenomena.WordOrder.Studies.Greenberg1963.isVSO p = p.wordOrder.basicOrder.IsVSO

@[reducible, inline]

abbrev Phenomena.WordOrder.Studies.Greenberg1963.isSOV (p : SampleEntry) : Prop

Language has WALS basic order SOV.

Equations

• Phenomena.WordOrder.Studies.Greenberg1963.isSOV p = p.wordOrder.basicOrder.IsSOV

@[reducible, inline]

abbrev Phenomena.WordOrder.Studies.Greenberg1963.isSubjectBeforeObject (p : SampleEntry) : Prop

Subject-before-object basic orders (SOV, SVO, VSO).

Equations

• Phenomena.WordOrder.Studies.Greenberg1963.isSubjectBeforeObject p = p.wordOrder.basicOrder.IsSubjectBeforeObject

@[reducible, inline]

abbrev Phenomena.WordOrder.Studies.Greenberg1963.isObjectBeforeSubject (p : SampleEntry) : Prop

Object-before-subject basic orders (VOS, OVS, OSV).

Equations

• Phenomena.WordOrder.Studies.Greenberg1963.isObjectBeforeSubject p = p.wordOrder.basicOrder.IsObjectBeforeSubject

@[reducible, inline]

abbrev Phenomena.WordOrder.Studies.Greenberg1963.isPrepositional (p : SampleEntry) : Prop

Language is classified as prepositional in WALS Ch 85.

Equations

• Phenomena.WordOrder.Studies.Greenberg1963.isPrepositional p = p.adposition.IsPrepositional

@[reducible, inline]

abbrev Phenomena.WordOrder.Studies.Greenberg1963.isPostpositional (p : SampleEntry) : Prop

Language is classified as postpositional in WALS Ch 85.

Equations

• Phenomena.WordOrder.Studies.Greenberg1963.isPostpositional p = p.adposition.IsPostpositional

@[reducible, inline]

abbrev Phenomena.WordOrder.Studies.Greenberg1963.isOV (p : SampleEntry) : Prop

Language is OV (object precedes verb) per WALS Ch 83. @cite{dryer-1992}'s primary classification under BDT.

Equations

• Phenomena.WordOrder.Studies.Greenberg1963.isOV p = p.wordOrder.ovOrder.IsOV

theorem Phenomena.WordOrder.Studies.Greenberg1963.greenberg_universal_1 : (Finset.filter isSubjectBeforeObject fragmentSample).card > (Finset.filter isObjectBeforeSubject fragmentSample).card * 4

@cite{greenberg-1963} Universal 1: in declarative sentences with nominal subject and object, the subject almost always precedes the object. Tested over fragmentSample: subject-before-object entries (SOV + SVO + VSO) outnumber object-before-subject entries (VOS + OVS + OSV) by more than 4×. The sample's three object-initial languages (Tzotzil VOS, Hixkaryana OVS, K'iche' VOS) give a non-trivial margin; the multiplier is sample-dependent (Greenberg's claim is "almost always", not a specific ratio).

theorem Phenomena.WordOrder.Studies.Greenberg1963.greenberg_universal_3 : Typology.ImplicationalUniversal isVSO isPrepositional fragmentSample

@cite{greenberg-1963} Universal 3: "Languages with dominant VSO order are always prepositional." Tested over fragmentSample; antecedent is triggered by Arabic, Welsh, Irish, all of which are prepositional.

theorem Phenomena.WordOrder.Studies.Greenberg1963.greenberg_universal_4 : Typology.ImplicationalUniversal isSOV isPostpositional fragmentSample

@cite{greenberg-1963} Universal 4: "With overwhelmingly greater than chance frequency, languages with normal SOV order are postpositional." Tested over fragmentSample; antecedent triggers Japanese, Korean, Turkish, Hindi, and Basque — all postpositional in WALS.

theorem Phenomena.WordOrder.Studies.Greenberg1963.dryer_bdt_ov_postp : Typology.ImplicationalUniversal isOV isPostpositional fragmentSample

@cite{dryer-1992}'s Branching Direction Theory primary correlation, stated as an implicational universal: in the sample, every OV (object-precedes-verb) language is postpositional.

Greenbergian U4 above commits to BasicOrder.IsSOV (SOV-specific) as the antecedent; Dryer's BDT primary commits to OVOrder.IsOV (covers SOV + OVS + OSV under one head-direction predicate). Both hold over the curated sample; they would diverge on a language with BasicOrder.noDominant Ch 81 + dominant .ov Ch 83 — exactly the Greenbergian-vs-Dryerian primacy choice flagged in Typology.WordOrder's module docstring.