Jeretič et al. 2025 — Anti-duality of tous

@cite{jeretic-bassi-gonzalez-yatsushiro-meyer-sauerland-2025}

Cross-linguistic anti-duality of universal and other quantifiers:

The English universal quantifiers all and every are 'anti-dual', i.e. cannot be used if their domain is known to contain only two individuals. Instead, the dual universal quantifier both can be used in those contexts […] French tous is also anti-dual. But French does not have a lexical item for 'both'.

The paper's resolution distinguishes three theoretical entities (paper §4.3, Fig. 1):

1. The lexicalized dual item (English both, German beide) — competes with universal all/alle via standard MP (@cite{percus-2006}, @cite{sauerland-2008}).
2. The unpronounceable dual structure (tous les NP.dual) — generated by the grammar via the dual core concept and blocked from pronunciation by Avoid Ambiguity (paper eq 37).
3. The indirect alternative (French les deux NP) — a pronounceable surrogate equivalent in meaning to (2) and at most as complex (Katzir node count); its existence licenses (2) to count as MP competitor.

The Competitor type below faithfully tracks all three, rather than collapsing (2) and (3) into one bin.

Cross-linguistic predictions (paper §5)

We reproduce only the (language, quantifier) cells the paper actually discusses. Per-cell paper-section citations are attached to each datum. The prediction is computed via:

• Lexicalizes lex realizes Id.dual for Competitor.lexicalDual (paper §3, English all via both; §5.2 no via neither)
• A pronounceable expression at-most-as-complex equivalent to the unpronounceable dual structure for Competitor.indirectAlternative (paper §4.1 French tous via les deux; §5.4 English always via both times)
• Competitor.none if neither obtains (paper §5.2 French aucun, German keine; §5.4 French toujours)

Connection to linglib infrastructure

• Features.Number.dualPredOnLattice is the predicate-modification denotation of DUAL (paper eq 39 / §8 eq 98b), grounded in the existing Harbour dualF = ⟨−atomic, +minimal⟩ and bridged via Features.Number.dualPredOnLattice_eq_via_features.
• Alternatives.Indirect.indirectFrom lifts an indirect alternative into an AlternativeSource, plugging into the Alternatives.Structural.violatesMP competition operator.
• Pragmatics.AvoidAmbiguity.Blocked formalizes paper eq 37 as the blocking principle that renders tous les NP.dual unpronounceable.
• The paper's MP-via-indirect-alts is a refinement of the MP-via-direct-alts machinery already in linglib via Phenomena/Plurals/Studies/Sauerland2003.lean (sg/pl/dual phi-MP); Sauerland's account works for English both but not French tous, which is exactly the gap this paper fills.

Theoretical alternatives the paper rejects

§6.1 considers BOTH as the universal core concept (rather than just DUAL) and rejects it; we do not formalize this counter-proposal but note that the choice between MP-based accounts of anti-duality (@cite{percus-2006}, @cite{sauerland-2008}) and obligatory-implicature accounts (@cite{magri-2009}) is real. This file commits to MP.

inductive Phenomena.Presupposition.Studies.JereticEtAl2025.Language : Type

Languages discussed in the paper, plus Slovenian as the discriminating prediction (paper §4.2.1, §5: dual morphologically realized → no anti-duality of universal).

• english : Language
• french : Language
• german : Language
• japanese : Language
• icelandic : Language
• slovenian : Language

@[implicit_reducible]

instance Phenomena.Presupposition.Studies.JereticEtAl2025.instDecidableEqLanguage : DecidableEq Language

Equations

• Phenomena.Presupposition.Studies.JereticEtAl2025.instDecidableEqLanguage x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[implicit_reducible]

instance Phenomena.Presupposition.Studies.JereticEtAl2025.instReprLanguage : Repr Language

Equations

• Phenomena.Presupposition.Studies.JereticEtAl2025.instReprLanguage = { reprPrec := Phenomena.Presupposition.Studies.JereticEtAl2025.instReprLanguage.repr }

def Phenomena.Presupposition.Studies.JereticEtAl2025.instReprLanguage.repr : Language → ℕ → Std.Format

Equations

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

inductive Phenomena.Presupposition.Studies.JereticEtAl2025.QSlot : Type

Quantifier slots discussed in the paper.

• universal : QSlot

  Universal: English all, French tous, German alle.

• negative : QSlot

  Negative: English no, French aucun, German keine.

• which : QSlot

  Interrogative: English which, French quel, Japanese dono.

• each : QSlot

  Distributive: English each, French chaque, Japanese each.

• one : QSlot

  Existential: English one, French un, Japanese one.

• always : QSlot

  Temporal universal: English always, French toujours.

@[implicit_reducible]

instance Phenomena.Presupposition.Studies.JereticEtAl2025.instDecidableEqQSlot : DecidableEq QSlot

Equations

• Phenomena.Presupposition.Studies.JereticEtAl2025.instDecidableEqQSlot x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Phenomena.Presupposition.Studies.JereticEtAl2025.instReprQSlot.repr : QSlot → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance Phenomena.Presupposition.Studies.JereticEtAl2025.instReprQSlot : Repr QSlot

Equations

• Phenomena.Presupposition.Studies.JereticEtAl2025.instReprQSlot = { reprPrec := Phenomena.Presupposition.Studies.JereticEtAl2025.instReprQSlot.repr }

inductive Phenomena.Presupposition.Studies.JereticEtAl2025.Competitor : Type

Three-way classification (paper §4.3, Fig. 1):

• lexicalDual: a single lexical item realizes the dual core concept, e.g. English both, German beide, Japanese dotti. Competes via standard MP.
• unpronounceableWithIndirectAlt: the dual structure exists in the grammar but is silent (blocked by Avoid Ambiguity). A pronounceable surrogate at no greater complexity (the indirect alternative) makes the silent structure count as MP competitor. E.g. French les deux surrogates tous les NP.dual; English both times surrogates all+ways DUAL times; German beide Male surrogates immer + DUAL.
• noCompetitor: the dual structure exists but no pronounceable surrogate at sufficient simplicity exists, so MP does not fire. E.g. French aucun (would-be surrogates aucun des deux / ni l'un ni l'autre are too complex); German keine; French toujours.

• lexicalDual : Competitor
• unpronounceableWithIndirectAlt : Competitor
• noCompetitor : Competitor

@[implicit_reducible]

instance Phenomena.Presupposition.Studies.JereticEtAl2025.instDecidableEqCompetitor : DecidableEq Competitor

Equations

• Phenomena.Presupposition.Studies.JereticEtAl2025.instDecidableEqCompetitor x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[implicit_reducible]

instance Phenomena.Presupposition.Studies.JereticEtAl2025.instReprCompetitor : Repr Competitor

Equations

• Phenomena.Presupposition.Studies.JereticEtAl2025.instReprCompetitor = { reprPrec := Phenomena.Presupposition.Studies.JereticEtAl2025.instReprCompetitor.repr }

def Phenomena.Presupposition.Studies.JereticEtAl2025.instReprCompetitor.repr : Competitor → ℕ → Std.Format

Equations

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

inductive Phenomena.Presupposition.Studies.JereticEtAl2025.Acceptability : Type

Acceptability strength reported in the paper. The Boolean distinction "anti-dual yes/no" loses the marginality contrast between Japanese dono (categorical #) and Icelandic hvaða (marginal ?). We track three values to preserve the paper's gradient judgment data.

• hash : Acceptability

  # — categorically infelicitous in dual contexts (anti-dual).

• question : Acceptability

  ? — marginal/degraded in dual contexts.

• ok : Acceptability

  ✓ — felicitous in dual contexts (NOT anti-dual).

@[implicit_reducible]

instance Phenomena.Presupposition.Studies.JereticEtAl2025.instDecidableEqAcceptability : DecidableEq Acceptability

Equations

• Phenomena.Presupposition.Studies.JereticEtAl2025.instDecidableEqAcceptability x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[implicit_reducible]

instance Phenomena.Presupposition.Studies.JereticEtAl2025.instReprAcceptability : Repr Acceptability

Equations

• Phenomena.Presupposition.Studies.JereticEtAl2025.instReprAcceptability = { reprPrec := Phenomena.Presupposition.Studies.JereticEtAl2025.instReprAcceptability.repr }

def Phenomena.Presupposition.Studies.JereticEtAl2025.instReprAcceptability.repr : Acceptability → ℕ → Std.Format

Equations

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

structure Phenomena.Presupposition.Studies.JereticEtAl2025.Datum : Type

An empirical datum: a (language, quantifier-slot) cell the paper explicitly discusses, with the paper-reported acceptability and a human-readable section reference.

• language : Language
• slot : QSlot
• observed : Acceptability

  Paper-reported acceptability of the universal/negative/etc. with a 2-element domain. .hash and .question are anti-dual; .ok is not.

• paperRef : String

  Paper section/example reference, for audit.

def Phenomena.Presupposition.Studies.JereticEtAl2025.instReprDatum.repr : Datum → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance Phenomena.Presupposition.Studies.JereticEtAl2025.instReprDatum : Repr Datum

Equations

• Phenomena.Presupposition.Studies.JereticEtAl2025.instReprDatum = { reprPrec := Phenomena.Presupposition.Studies.JereticEtAl2025.instReprDatum.repr }

def Phenomena.Presupposition.Studies.JereticEtAl2025.paperData : List Datum

The paper's empirical claims. Every entry corresponds to an explicit paragraph or example in Jeretič et al. 2025. Cells the paper does not discuss are omitted rather than extrapolated.

Coverage: English (all 6 slots), French (all 6 slots), German (universal/negative/always — §5.2 fn 2 and §5.4 only), Japanese (which/each/one/always — §5.1.1, §5.1.2, §5.4 only), Icelandic (which only — §5.1.1), Slovenian (universal — §4.2.1 ex. 36).

Total: 21 paper-licensed data points.

Equations

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

def Phenomena.Presupposition.Studies.JereticEtAl2025.Acceptability.isAntiDual : Acceptability → Bool

Whether the paper-reported acceptability counts as anti-dual.

Equations

• Phenomena.Presupposition.Studies.JereticEtAl2025.Acceptability.hash.isAntiDual = true
• Phenomena.Presupposition.Studies.JereticEtAl2025.Acceptability.question.isAntiDual = true
• Phenomena.Presupposition.Studies.JereticEtAl2025.Acceptability.ok.isAntiDual = false

def Phenomena.Presupposition.Studies.JereticEtAl2025.lexiconCompetitor : Language → QSlot → Competitor

For each (language, quantifier-slot) cell, what does the language provide for the dual reading? This is the typological input the theory consumes — derived from per-language Fragment data where it exists, hand-encoded for languages whose Fragment is not yet in linglib. Where Fragment data is available (English, French), the encoding here is consistent with it.

Justification per cell:

• English all → .lexicalDual because Fragments.English.Determiners.both has numberRestriction := some .du (see both_neither_dual_marked).
• English no → .lexicalDual via neither.
• French tous → .unpronounceableWithIndirectAlt because Fragments.French.Determiners.les_deux has numberRestriction := some .du and is no more complex than tous les NP.
• French aucun → .noCompetitor because no Fragment entry has both qforce = .negative and numberRestriction = some .du and no surrogate at sufficient simplicity exists (paper §5.2).
• German alle → .lexicalDual via beide (Fragment not yet built).
• German keine → .noCompetitor per paper §5.2 (no German neither).
• German immer → .unpronounceableWithIndirectAlt per paper §5.4: immer decomposes as the suppleted all+ways DUAL, with beide Male as the indirect alternative (NOT a lexical dual).
• Japanese dono etc. → .lexicalDual via the dotti indeterminate; paper §5.1.1, §5.1.2 (one morpheme realizes the dual core concept across which/each/one slots).
• Japanese itu-mo → .unpronounceableWithIndirectAlt per paper §5.4 fn 22: ni-kai-tomo ('two-times-with-foc') as the surrogate, weakly.
• Icelandic hvaða → .lexicalDual via hvor (paper §5.1.1).
• Slovenian vsi → .noCompetitor: dual is morphologically OVERT (paper §4.2.1 ex. 36 računalnika sta pokvarjena), so AA doesn't block the dual structure → it remains pronounceable as a direct alternative, not as an indirect one. The "indirect alternative" machinery doesn't fire because there is no unpronounceable witness.

Equations

• One or more equations did not get rendered due to their size.
• Phenomena.Presupposition.Studies.JereticEtAl2025.lexiconCompetitor x✝¹ x✝ = Phenomena.Presupposition.Studies.JereticEtAl2025.Competitor.noCompetitor

def Phenomena.Presupposition.Studies.JereticEtAl2025.predictedAntiDual (lang : Language) (q : QSlot) : Bool

The theoretical prediction (paper §4–5): a quantifier is anti-dual iff the language provides EITHER a lexical dual competitor OR an indirect alternative for the (silent) dual structure.

Equations

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

Connect lexiconCompetitor to the actual per-language Fragment data where it exists. These are not stipulations about the typology but checks: if Fragments.English.Determiners.both were not .du-marked, the theorem would fail and the typological encoding would be exposed as out of sync with the lexicon.

def Phenomena.Presupposition.Studies.JereticEtAl2025.englishRealizesDual : Prop

English realizes the dual core concept iff some entry in the lexicon carries numberRestriction = some .du. For English this is witnessed by both and neither.

Equations

• Phenomena.Presupposition.Studies.JereticEtAl2025.englishRealizesDual = ∃ q ∈ Fragments.English.Determiners.allQuantifiers, q.numberRestriction = some Number.du

theorem Phenomena.Presupposition.Studies.JereticEtAl2025.english_realizes_dual : englishRealizesDual

def Phenomena.Presupposition.Studies.JereticEtAl2025.frenchHasDualOnDefinite : Prop

French does NOT lexicalize a universal dual quantifier (no French both); it does have les_deux realizing the dual core concept on the definite slot. This is the paper's central observation: French has the dual concept but lacks its universal lexicalization.

Equations

• Phenomena.Presupposition.Studies.JereticEtAl2025.frenchHasDualOnDefinite = (Fragments.French.Determiners.les_deux.numberRestriction = some Number.du)

theorem Phenomena.Presupposition.Studies.JereticEtAl2025.french_dual_on_definite : frenchHasDualOnDefinite

theorem Phenomena.Presupposition.Studies.JereticEtAl2025.french_tous_not_lexical_dual : Fragments.French.Determiners.tous.numberRestriction ≠ some Number.du

French tous is plural-restricted, NOT dual — the gap the paper explains via Indirect Alternatives.

theorem Phenomena.Presupposition.Studies.JereticEtAl2025.english_universal_competitor_grounded : lexiconCompetitor Language.english QSlot.universal = Competitor.lexicalDual ∧ ∃ q ∈ Fragments.English.Determiners.allQuantifiers, q.qforce = Theories.Semantics.Quantification.Lexicon.QForce.universal ∧ q.numberRestriction = some Number.du

The grounding bridge: lexiconCompetitor .english .universal = .lexicalDual is consistent with English having a .du-marked quantifier with qforce = .universal (which is both).

theorem Phenomena.Presupposition.Studies.JereticEtAl2025.french_universal_competitor_grounded : lexiconCompetitor Language.french QSlot.universal = Competitor.unpronounceableWithIndirectAlt ∧ Fragments.French.Determiners.tous.qforce = Theories.Semantics.Quantification.Lexicon.QForce.universal ∧ Fragments.French.Determiners.tous.numberRestriction ≠ some Number.du ∧ Fragments.French.Determiners.les_deux.numberRestriction = some Number.du

The grounding bridge for French: lexiconCompetitor .french .universal = .unpronounceableWithIndirectAlt is consistent with French lacking a .du-marked universal AND having les deux realizing dual on the definite slot (the indirect alternative).

theorem Phenomena.Presupposition.Studies.JereticEtAl2025.theory_matches_data : (paperData.all fun (d : Datum) => predictedAntiDual d.language d.slot == d.observed.isAntiDual) = true

For each cell the paper discusses, the prediction matches the reported acceptability.

This is the headline result. Unlike a data = data theorem over two parallel stipulated tables, here predictedAntiDual is computed from lexiconCompetitor (typological input) and Acceptability.isAntiDual extracts a Boolean from the paper's gradient judgment. The prediction shape (lexical dual OR indirect alternative → anti-dual) is the theory; the per-cell lexiconCompetitor value reads the language; the agreement with paperData.observed.isAntiDual is the substantive empirical claim.

theorem Phenomena.Presupposition.Studies.JereticEtAl2025.slovenian_universal_not_anti_dual : predictedAntiDual Language.slovenian QSlot.universal = false

Discriminating prediction for Slovenian (paper §4.2.1 ex. 36): because Slovenian morphologically realizes the dual, the unpronounceable structure of the analysis becomes pronounceable, no indirect-alternative competition is needed, and the universal is NOT anti-dual. This is the empirical leverage of the Indirect Alternative account: it explains why dual-marking languages do not show anti-duality of the universal in the way French/English do.

Bridge to Phenomena/Plurals/Studies/Sauerland2003.lean

@cite{sauerland-2003} formalizes MP competition over phi-features (sg/pl/dual) via direct alternatives — the standard @cite{percus-2006}, @cite{sauerland-2008} mechanism. That account correctly predicts:

• English all anti-dual via direct competition with both (lexicalized phi-feature alternative).

It cannot predict:

• French tous anti-dual (no direct alternative — no French both).
• English always anti-dual (no direct alternative — both times is not a phi-feature alternative to always but a phrasal one).

This paper extends the account by introducing indirect alternatives: when the direct phi-feature alternative is unpronounceable, a phrasal surrogate at no greater complexity counts as competitor. The two accounts agree on lexicalDual cases and diverge on unpronounceableWithIndirectAlt cases — Sauerland 2003 predicts no anti-duality where Jeretič et al. 2025 predict anti-duality. The empirical evidence (French tous, English always) favors the extended account.

def Phenomena.Presupposition.Studies.JereticEtAl2025.directAltAgrees : Language → QSlot → Bool

Cells where Sauerland 2003's direct-alts MP and Jeretič et al. 2025's indirect-alts MP make the same prediction (lexical dual).

Equations

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

def Phenomena.Presupposition.Studies.JereticEtAl2025.directAltDiverges : Language → QSlot → Bool

The cells where the two accounts diverge — exactly the unpronounceableWithIndirectAlt cells.

Equations

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

theorem Phenomena.Presupposition.Studies.JereticEtAl2025.accounts_diverge : directAltDiverges Language.french QSlot.universal = true ∧ directAltDiverges Language.english QSlot.always = true

Divergence is non-empty: there are paper-cited cells where the two accounts make different predictions. This is the empirical content of the paper's contribution over Sauerland 2003.

A worked end-to-end example: French tous les verres

The typological table above asserts that French tous is anti-dual via an indirect alternative. This section exercises the typeclass infrastructure end-to-end on a minimal sentence pair, demonstrating that AlternativeSource / Pronounceability / indirectFrom / Alternatives.Structural.violatesMP compose correctly: each component plugs into the next and the final violatesMP predicate fires on real parse trees.

We use a deliberately shallow tree structure — a single NP with two Det-substitutable terminals — so the proofs go through by decide and a single Katzir substitution step. The sentence pair is paper §4.1 ex. 25 (tous les verres sont pleins / les deux verres sont pleins), collapsed to its essential head structure: tous V / les_deux V, with the silent witness tous_DUAL V.

inductive Phenomena.Presupposition.Studies.JereticEtAl2025.WorldEx : Type

Two domains: a 2-cup world (w2) and a 3-cup world (w3). The dual presupposition is satisfied only in w2.

• w2 : WorldEx
• w3 : WorldEx

@[implicit_reducible]

instance Phenomena.Presupposition.Studies.JereticEtAl2025.instDecidableEqWorldEx : DecidableEq WorldEx

Equations

• Phenomena.Presupposition.Studies.JereticEtAl2025.instDecidableEqWorldEx x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Phenomena.Presupposition.Studies.JereticEtAl2025.instReprWorldEx.repr : WorldEx → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance Phenomena.Presupposition.Studies.JereticEtAl2025.instReprWorldEx : Repr WorldEx

Equations

• Phenomena.Presupposition.Studies.JereticEtAl2025.instReprWorldEx = { reprPrec := Phenomena.Presupposition.Studies.JereticEtAl2025.instReprWorldEx.repr }

theorem Phenomena.Presupposition.Studies.JereticEtAl2025.tous_violatesMP_via_indirect : Alternatives.Structural.violatesMP Phenomena.Presupposition.Studies.JereticEtAl2025.frenchIndirectSrc✝ Phenomena.Presupposition.Studies.JereticEtAl2025.presupFn✝ Phenomena.Presupposition.Studies.JereticEtAl2025.assertionFn✝ Phenomena.Presupposition.Studies.JereticEtAl2025.tousVerres✝ fun (x : Core.Tree.Tree Core.Tree.Cat String) => true

Headline theorem of §7: tous V violates Maximize Presupposition via competition with the indirect alternative les deux V, which is licensed by the silent witness tous_DUAL V.

This is the end-to-end demonstration that the AlternativeSource / Pronounceability / indirectFrom / Alternatives.Structural.violatesMP infrastructure is wired correctly: the abstract pragmatic-competition operator fires on a real tree-based example with a real silent witness via a real indirect alternative, deriving the paper's anti-duality of tous (paper §4.1 ex. 25, paper Fig. 1).