Cross-Linguistic Typology of the Two-Until Distinction

@cite{giannakidou-2002} @cite{karttunen-1974}

Languages employ four strategies for expressing the durative/eventive distinction in temporal connectives:

1. Three-way lexicalization (Greek): separate lexemes for before (prin), durative until (mexri), and eventive NPI-until (para monon).

2. Two-way lexicalization (Icelandic, Finnish): separate lexemes for durative until (flanga til, kunnes) and eventive NPI-until (fyrr en, ennenkuin). Before may or may not be one of the until forms.

3. Ambiguity (English): a single lexeme until is ambiguous between durative (positive contexts) and eventive/NPI (negative contexts).

4. PPI replacement (Dutch, German): durative until (tot, bis) cannot co-occur with negation. A separate PPI (pas, erst) supplies the 'not before' meaning without negation.

The typology is organized by how many surface forms a language uses and what polarity properties they have, not by geographic or genetic affiliation. The aspect parameter (overt vs covert perfective/imperfective marking) is orthogonal: Icelandic has no overt aspect but still lexicalizes the distinction.

inductive Phenomena.TemporalConnectives.Typology.UntilStrategy : Type

How a language handles the durative/eventive until distinction.

• threeWay : UntilStrategy

  Three distinct lexemes: before, durative until, eventive NPI-until. Greek: prin, mexri, para monon.

• twoWay : UntilStrategy

  Two distinct lexemes: durative until and eventive NPI-until. Icelandic: flanga til, fyrr en. Finnish: kunnes, ennenkuin.

• ambiguous : UntilStrategy

  Single ambiguous lexeme, disambiguated by negation context. English: until.

• ppiReplacement : UntilStrategy

  Durative until blocked under negation; PPI replaces NPI-until. Dutch: tot, pas. German: bis, erst.

instance Phenomena.TemporalConnectives.Typology.instDecidableEqUntilStrategy : DecidableEq UntilStrategy

Equations

• Phenomena.TemporalConnectives.Typology.instDecidableEqUntilStrategy x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Phenomena.TemporalConnectives.Typology.instReprUntilStrategy.repr : UntilStrategy → ℕ → Std.Format

Equations

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

instance Phenomena.TemporalConnectives.Typology.instReprUntilStrategy : Repr UntilStrategy

Equations

• Phenomena.TemporalConnectives.Typology.instReprUntilStrategy = { reprPrec := Phenomena.TemporalConnectives.Typology.instReprUntilStrategy.repr }

def Phenomena.TemporalConnectives.Typology.instBEqUntilStrategy.beq : UntilStrategy → UntilStrategy → Bool

Equations

• Phenomena.TemporalConnectives.Typology.instBEqUntilStrategy.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

instance Phenomena.TemporalConnectives.Typology.instBEqUntilStrategy : BEq UntilStrategy

Equations

• Phenomena.TemporalConnectives.Typology.instBEqUntilStrategy = { beq := Phenomena.TemporalConnectives.Typology.instBEqUntilStrategy.beq }

structure Phenomena.TemporalConnectives.Typology.UntilTypologyEntry : Type

A language's strategy for the two-until distinction, with evidence linking to fragment entries and NegationData.

• language : String
• strategy : UntilStrategy
• durativeForm : String

  Surface form for durative until

• eventiveForm : String

  Surface form for eventive until (NPI or PPI)

• eventiveMorphBeforeBased : Bool

  Is the eventive form morphologically built on before?

• hasOvertAspect : Bool

  Does the language have overt perfective/imperfective marking?

def Phenomena.TemporalConnectives.Typology.instReprUntilTypologyEntry.repr : UntilTypologyEntry → ℕ → Std.Format

Equations

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

instance Phenomena.TemporalConnectives.Typology.instReprUntilTypologyEntry : Repr UntilTypologyEntry

Equations

• Phenomena.TemporalConnectives.Typology.instReprUntilTypologyEntry = { reprPrec := Phenomena.TemporalConnectives.Typology.instReprUntilTypologyEntry.repr }

def Phenomena.TemporalConnectives.Typology.greek : UntilTypologyEntry

Equations

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

def Phenomena.TemporalConnectives.Typology.icelandic : UntilTypologyEntry

Equations

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

def Phenomena.TemporalConnectives.Typology.finnish : UntilTypologyEntry

Equations

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

def Phenomena.TemporalConnectives.Typology.english : UntilTypologyEntry

Equations

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

def Phenomena.TemporalConnectives.Typology.dutch : UntilTypologyEntry

Equations

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

def Phenomena.TemporalConnectives.Typology.german : UntilTypologyEntry

Equations

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

def Phenomena.TemporalConnectives.Typology.typology : List UntilTypologyEntry

The full typological sample.

Equations

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

theorem Phenomena.TemporalConnectives.Typology.all_distinguish_durative_eventive (e : UntilTypologyEntry) : e ∈ typology → e.durativeForm ≠ e.eventiveForm

Every language in the sample uses distinct surface forms for durative and eventive until (even the ambiguous strategy uses the same form in different syntactic contexts, disambiguated by negation).

theorem Phenomena.TemporalConnectives.Typology.before_morphology_attested : icelandic.eventiveMorphBeforeBased = true ∧ finnish.eventiveMorphBeforeBased = true

The two-way and three-way strategies both have morphologically before-based eventive forms in at least one language, confirming @cite{karttunen-1974}'s identity NPI-until = ¬before.

theorem Phenomena.TemporalConnectives.Typology.aspect_not_required : icelandic.hasOvertAspect = false ∧ icelandic.strategy = UntilStrategy.twoWay ∧ finnish.hasOvertAspect = false ∧ finnish.strategy = UntilStrategy.twoWay

Overt aspect marking is NOT required for lexicalization of the two-until distinction. Icelandic and Finnish lack overt verbal aspect but still lexicalize two untils.

theorem Phenomena.TemporalConnectives.Typology.greek_confirmed : Fragments.Greek.TemporalConnectives.mexri.form ≠ Fragments.Greek.TemporalConnectives.paraMonon.form ∧ Fragments.Greek.TemporalConnectives.mexri.form ≠ Fragments.Greek.TemporalConnectives.prin.form ∧ Fragments.Greek.TemporalConnectives.paraMonon.form ≠ Fragments.Greek.TemporalConnectives.prin.form

Greek strategy confirmed by fragment: three distinct forms.

theorem Phenomena.TemporalConnectives.Typology.icelandic_confirmed : Fragments.Icelandic.TemporalConnectives.flangaTil.form ≠ Fragments.Icelandic.TemporalConnectives.fyrrEn.form ∧ Fragments.Icelandic.TemporalConnectives.flangaTil.complementVeridical = true ∧ Fragments.Icelandic.TemporalConnectives.fyrrEn.complementVeridical = false

Icelandic strategy confirmed by fragment: two distinct forms with veridicality split.

theorem Phenomena.TemporalConnectives.Typology.dutch_confirmed : Fragments.Dutch.TemporalConnectives.tot.form ≠ Fragments.Dutch.TemporalConnectives.pas.form ∧ Fragments.Dutch.TemporalConnectives.tot.complementVeridical = true ∧ Fragments.Dutch.TemporalConnectives.pas.complementVeridical = false

Dutch strategy confirmed by fragment: two distinct forms with veridicality split.

theorem Phenomena.TemporalConnectives.Typology.actualization_universal : NegationData.greek_mexri.actualizationStatus = NegationData.ActualizationStatus.implicature ∧ NegationData.english_dur_until.actualizationStatus = NegationData.ActualizationStatus.implicature ∧ NegationData.greek_para_monon.actualizationStatus = NegationData.ActualizationStatus.entailment ∧ NegationData.english_npi_until.actualizationStatus = NegationData.ActualizationStatus.entailment

The NegationData three-way actualization split is consistent with the typological strategies: all strategies preserve the semantic distinction between durative (implicature) and eventive (entailment) actualization.

theorem Phenomena.TemporalConnectives.Typology.english_greek_eventive_agree : NegationData.english_npi_until.semanticType = NegationData.greek_para_monon.semanticType

English NPI-until and Greek para monon agree on semantic type: both are eventive (not before-type). This was previously inconsistent in the data file.