Greenberg 1963: Implicational Universals on Basic Word Order

[Gre63] [DH13a]

[Gre63] 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 ImplicationalUniversal predicate (every P-language is also Q) is defined study-locally below. 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.

def Greenberg1963.ImplicationalUniversal {α : Type u_1} (P Q : α → Prop) (s : Finset α) : Prop

A Greenbergian implicational universal: every language in sample s with property P also has Q (the "no P-but-not-Q counterexample" claim, [Gre63]).

Equations

• Greenberg1963.ImplicationalUniversal P Q s = ∀ l ∈ s, P l → Q l

@[implicit_reducible]

instance Greenberg1963.instDecidableImplicationalUniversalOfDecidablePred {α : Type u_1} (P Q : α → Prop) (s : Finset α) [DecidablePred P] [DecidablePred Q] : Decidable (ImplicationalUniversal P Q s)

Equations

• Greenberg1963.instDecidableImplicationalUniversalOfDecidablePred P Q s = Finset.decidableDforallFinset

structure 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 : WordOrder.WordOrderProfile
• adposition : Adposition.AdpositionOrder

@[implicit_reducible]

instance Greenberg1963.instReprSampleEntry : Repr SampleEntry

Equations

• Greenberg1963.instReprSampleEntry = { reprPrec := Greenberg1963.instReprSampleEntry.repr }

def Greenberg1963.instReprSampleEntry.repr : SampleEntry → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance Greenberg1963.instDecidableEqSampleEntry : DecidableEq SampleEntry

Equations

• Greenberg1963.instDecidableEqSampleEntry = Greenberg1963.instDecidableEqSampleEntry.decEq

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

Equations

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

def 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 Greenberg1963.isVSO (p : SampleEntry) : Prop

Language has WALS basic order VSO.

Equations

• Greenberg1963.isVSO p = p.wordOrder.basicOrder.IsVSO

@[reducible, inline]

abbrev Greenberg1963.isSOV (p : SampleEntry) : Prop

Language has WALS basic order SOV.

Equations

• Greenberg1963.isSOV p = p.wordOrder.basicOrder.IsSOV

@[reducible, inline]

abbrev Greenberg1963.isSubjectBeforeObject (p : SampleEntry) : Prop

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

Equations

• Greenberg1963.isSubjectBeforeObject p = p.wordOrder.basicOrder.IsSubjectBeforeObject

@[reducible, inline]

abbrev Greenberg1963.isObjectBeforeSubject (p : SampleEntry) : Prop

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

Equations

• Greenberg1963.isObjectBeforeSubject p = p.wordOrder.basicOrder.IsObjectBeforeSubject

@[reducible, inline]

abbrev Greenberg1963.isPrepositional (p : SampleEntry) : Prop

Language is classified as prepositional in WALS Ch 85.

Equations

• Greenberg1963.isPrepositional p = p.adposition.IsPrepositional

@[reducible, inline]

abbrev Greenberg1963.isPostpositional (p : SampleEntry) : Prop

Language is classified as postpositional in WALS Ch 85.

Equations

• Greenberg1963.isPostpositional p = p.adposition.IsPostpositional

@[reducible, inline]

abbrev Greenberg1963.isOV (p : SampleEntry) : Prop

Language is OV (object precedes verb) per WALS Ch 83. [Dry92]'s primary classification under BDT.

Equations

• Greenberg1963.isOV p = p.wordOrder.ovOrder.IsOV

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

[Gre63] 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 Greenberg1963.greenberg_universal_3 : ImplicationalUniversal isVSO isPrepositional fragmentSample

[Gre63] 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 Greenberg1963.greenberg_universal_4 : ImplicationalUniversal isSOV isPostpositional fragmentSample

[Gre63] 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 Greenberg1963.dryer_bdt_ov_postp : ImplicationalUniversal isOV isPostpositional fragmentSample

[Dry92]'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 WordOrder's module docstring.