Implicational universals and 2×2 contingency tables

@cite{greenberg-1963} @cite{dryer-1992}

A Greenbergian implicational universal of the form "if a language is φ then it is also ψ" is the claim that the Type IV cell of a 2×2 contingency table (φ ∧ ¬ψ) is empty over the relevant language sample. This file gives the minimal, sample-polymorphic API for stating, computing, and bridging implicational universals to their tetrachoric form.

Design

• ImplicationalUniversal P Q s : Prop — the universal claim "every l ∈ s with property P also has property Q" over a Finset sample.
• ContingencyTable — named-field 2×2 cell counts (pp pn np nn : ℕ), preferred over an opaque Fin 4 → ℕ.
• Finset.contingency — derive a ContingencyTable from a sample by counting elements that satisfy each combination of P and Q.
• implicational_iff_no_typeIV — the bridge: ImplicationalUniversal P Q s holds iff the table's Type IV cell (pn) is zero. The load-bearing theorem that keeps tetrachoric and propositional formulations in sync.

The language type is left abstract (α); concrete samples instantiate it to the appropriate Fragment-derived profile type (Typology.WordOrder.WordOrderProfile, etc.).

Decidability over literal samples

decide on ImplicationalUniversal P Q {a, b, …} routes through Finset.decidableBAll → Multiset → Quot.mk and may exhaust kernel recursion depth on samples larger than a handful. Two mathlib-blessed fixes for consumers:

• simp only [Finset.forall_mem_insert, Finset.forall_mem_empty] <;> decide — structural decomposition into a conjunction of per-language goals.
• set_option maxRecDepth N in theorem ... — brute-force; mathlib uses this idiom for similar Finset.decide sites.

structure Typology.ContingencyTable : Type

A 2×2 tetrachoric contingency table.

Cells are named for whether the two predicates hold (p) or fail (n):

cell	row P	column Q
pp	true	true
pn	true	false
np	false	true
nn	false	false

For an implication P → Q, the Type IV cell is pn: languages that have P but lack Q are the counterexamples.

• pp : ℕ

  Both predicates hold.

• pn : ℕ

  P holds, Q fails — the Type IV (counterexample) cell.

• np : ℕ

  P fails, Q holds.

• nn : ℕ

  Both predicates fail.

def Typology.instReprContingencyTable.repr : ContingencyTable → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance Typology.instReprContingencyTable : Repr ContingencyTable

Equations

• Typology.instReprContingencyTable = { reprPrec := Typology.instReprContingencyTable.repr }

def Typology.instDecidableEqContingencyTable.decEq (x✝ x✝¹ : ContingencyTable) : Decidable (x✝ = x✝¹)

Equations

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

@[implicit_reducible]

instance Typology.instDecidableEqContingencyTable : DecidableEq ContingencyTable

Equations

• Typology.instDecidableEqContingencyTable = Typology.instDecidableEqContingencyTable.decEq

def Typology.ContingencyTable.total (t : ContingencyTable) : ℕ

Total number of languages tabulated.

Equations

• t.total = t.pp + t.pn + t.np + t.nn

def Typology.ContingencyTable.rowP (t : ContingencyTable) : ℕ

Marginal count of languages with P.

Equations

• t.rowP = t.pp + t.pn

def Typology.ContingencyTable.colQ (t : ContingencyTable) : ℕ

Marginal count of languages with Q.

Equations

• t.colQ = t.pp + t.np

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

Greenbergian implicational universal: every language in sample s that satisfies P also satisfies Q. The "no Type IV gap" formulation, (Finset.contingency s P Q).pn = 0, is logically equivalent (see implicational_iff_no_typeIV).

Equations

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

@[implicit_reducible]

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

Equations

• Typology.instDecidableImplicationalUniversalOfDecidablePred P Q s = Finset.decidableDforallFinset

def Finset.contingency {α : Type u} (s : Finset α) (P Q : α → Prop) [DecidablePred P] [DecidablePred Q] : Typology.ContingencyTable

Build a 2×2 contingency table by counting elements of s that satisfy each combination of P and Q.

Equations

• s.contingency P Q = { pp := {l ∈ s | P l ∧ Q l}.card, pn := {l ∈ s | P l ∧ ¬Q l}.card, np := {l ∈ s | ¬P l ∧ Q l}.card, nn := {l ∈ s | ¬P l ∧ ¬Q l}.card }

theorem Typology.implicational_iff_no_typeIV {α : Type u} (s : Finset α) (P Q : α → Prop) [DecidablePred P] [DecidablePred Q] : ImplicationalUniversal P Q s ↔ (s.contingency P Q).pn = 0

Bridge between the propositional and tetrachoric formulations: an implicational universal holds iff its Type IV cell is empty.

@cite{greenberg-1963}'s reformulation of "P implies Q" as "no language is P-but-not-Q" — same content, expressed once as a universal statement and once as a count-zero claim.