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

[JBG+25]

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 ([Per06], [Sau08]).
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

• 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 Number.dualPredOnLattice_eq_via_features.
• Alternatives.indirectFrom lifts an indirect alternative into an Alternatives.Source, plugging into the Alternatives.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 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 ([Per06], [Sau08]) and obligatory-implicature accounts ([Mag09]) is real. This file commits to MP.

Core-concept registry

A core concept is a conceptual primitive universally available to every language's grammar, regardless of whether any lexical item realizes it. From [Che07a] (anti-duality of French tous despite French lacking a lexical both), generalized to "conceptual alternatives" by [BKC18]; this paper refines it: core concepts feed competition only when an indirect alternative — a pronounceable expression equivalent to the unpronounceable core-concept structure — is available (Alternatives.indirectFrom). Denotations live where their semantic content does (e.g. dualPredOnLattice in Features/Number.lean for dual).

inductive JereticEtAl2025.CoreConcept.Id : Type

The registered core concepts: conceptual primitives independently motivated in the literature, with denotations defined elsewhere in linglib.

• dual : Id

  Number-feature dual: predicate-modifier "and has exactly 2 atomic parts"; denotation in Number.dualPredOnLattice.

• trial : Id

  Number-feature trial. Mentioned in [Har14a] as morphologically stable but rare. Denotation TBD.

• universal : Id

  Universal quantifier core concept. Lexicalized as all/tous cross-linguistically.

• existential : Id

  Existential quantifier core concept. Lexicalized as some/ quelques.

@[implicit_reducible]

instance JereticEtAl2025.CoreConcept.instDecidableEqId : DecidableEq Id

Equations

• JereticEtAl2025.CoreConcept.instDecidableEqId x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def JereticEtAl2025.CoreConcept.instReprId.repr : Id → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance JereticEtAl2025.CoreConcept.instReprId : Repr Id

Equations

• JereticEtAl2025.CoreConcept.instReprId = { reprPrec := JereticEtAl2025.CoreConcept.instReprId.repr }

def JereticEtAl2025.CoreConcept.Lexicalizes {Tok : Type} (lex : List Tok) (realizes : Tok → Id → Prop) (c : Id) : Prop

A lexicon (any list of lexical tokens of type Tok) lexicalizes a core concept iff some entry realizes it. The realization relation realizes is supplied by the caller — typically a per-language predicate that inspects the lexical entry's denotation: English realizes both Id.dual = True, French realizes _ Id.dual = False.

Equations

• JereticEtAl2025.CoreConcept.Lexicalizes lex realizes c = ∃ tok ∈ lex, realizes tok c

inductive 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 JereticEtAl2025.instDecidableEqLanguage : DecidableEq Language

Equations

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

def JereticEtAl2025.instReprLanguage.repr : Language → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance JereticEtAl2025.instReprLanguage : Repr Language

Equations

• JereticEtAl2025.instReprLanguage = { reprPrec := JereticEtAl2025.instReprLanguage.repr }

inductive 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 JereticEtAl2025.instDecidableEqQSlot : DecidableEq QSlot

Equations

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

@[implicit_reducible]

instance JereticEtAl2025.instReprQSlot : Repr QSlot

Equations

• JereticEtAl2025.instReprQSlot = { reprPrec := JereticEtAl2025.instReprQSlot.repr }

def JereticEtAl2025.instReprQSlot.repr : QSlot → ℕ → Std.Format

Equations

• One or more equations did not get rendered due to their size.
• JereticEtAl2025.instReprQSlot.repr JereticEtAl2025.QSlot.one prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "JereticEtAl2025.QSlot.one")).group prec✝

inductive 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 JereticEtAl2025.instDecidableEqCompetitor : DecidableEq Competitor

Equations

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

def JereticEtAl2025.instReprCompetitor.repr : Competitor → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance JereticEtAl2025.instReprCompetitor : Repr Competitor

Equations

• JereticEtAl2025.instReprCompetitor = { reprPrec := JereticEtAl2025.instReprCompetitor.repr }

inductive 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 JereticEtAl2025.instDecidableEqAcceptability : DecidableEq Acceptability

Equations

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

def JereticEtAl2025.instReprAcceptability.repr : Acceptability → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance JereticEtAl2025.instReprAcceptability : Repr Acceptability

Equations

• JereticEtAl2025.instReprAcceptability = { reprPrec := JereticEtAl2025.instReprAcceptability.repr }

structure 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 JereticEtAl2025.instReprDatum.repr : Datum → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance JereticEtAl2025.instReprDatum : Repr Datum

Equations

• JereticEtAl2025.instReprDatum = { reprPrec := JereticEtAl2025.instReprDatum.repr }

def 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 JereticEtAl2025.Acceptability.isAntiDual : Acceptability → Bool

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

Equations

• JereticEtAl2025.Acceptability.hash.isAntiDual = true
• JereticEtAl2025.Acceptability.question.isAntiDual = true
• JereticEtAl2025.Acceptability.ok.isAntiDual = false

def 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 English.Determiners.both has numberRestriction := some .dual.
• English no → .lexicalDual via neither.
• French tous → .unpronounceableWithIndirectAlt because French.Determiners.les_deux has numberRestriction := some .dual and is no more complex than tous les NP.
• French aucun → .noCompetitor because no Fragment entry is both negative and numberRestriction = some .dual 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

• JereticEtAl2025.lexiconCompetitor JereticEtAl2025.Language.english JereticEtAl2025.QSlot.universal = JereticEtAl2025.Competitor.lexicalDual
• JereticEtAl2025.lexiconCompetitor JereticEtAl2025.Language.english JereticEtAl2025.QSlot.negative = JereticEtAl2025.Competitor.lexicalDual
• JereticEtAl2025.lexiconCompetitor JereticEtAl2025.Language.english JereticEtAl2025.QSlot.which = JereticEtAl2025.Competitor.noCompetitor
• JereticEtAl2025.lexiconCompetitor JereticEtAl2025.Language.english JereticEtAl2025.QSlot.each = JereticEtAl2025.Competitor.noCompetitor
• JereticEtAl2025.lexiconCompetitor JereticEtAl2025.Language.english JereticEtAl2025.QSlot.one = JereticEtAl2025.Competitor.noCompetitor
• JereticEtAl2025.lexiconCompetitor JereticEtAl2025.Language.english JereticEtAl2025.QSlot.always = JereticEtAl2025.Competitor.unpronounceableWithIndirectAlt
• JereticEtAl2025.lexiconCompetitor JereticEtAl2025.Language.french JereticEtAl2025.QSlot.universal = JereticEtAl2025.Competitor.unpronounceableWithIndirectAlt
• JereticEtAl2025.lexiconCompetitor JereticEtAl2025.Language.french JereticEtAl2025.QSlot.negative = JereticEtAl2025.Competitor.noCompetitor
• JereticEtAl2025.lexiconCompetitor JereticEtAl2025.Language.french JereticEtAl2025.QSlot.which = JereticEtAl2025.Competitor.noCompetitor
• JereticEtAl2025.lexiconCompetitor JereticEtAl2025.Language.french JereticEtAl2025.QSlot.each = JereticEtAl2025.Competitor.noCompetitor
• JereticEtAl2025.lexiconCompetitor JereticEtAl2025.Language.french JereticEtAl2025.QSlot.one = JereticEtAl2025.Competitor.noCompetitor
• JereticEtAl2025.lexiconCompetitor JereticEtAl2025.Language.french JereticEtAl2025.QSlot.always = JereticEtAl2025.Competitor.noCompetitor
• JereticEtAl2025.lexiconCompetitor JereticEtAl2025.Language.german JereticEtAl2025.QSlot.universal = JereticEtAl2025.Competitor.lexicalDual
• JereticEtAl2025.lexiconCompetitor JereticEtAl2025.Language.german JereticEtAl2025.QSlot.negative = JereticEtAl2025.Competitor.noCompetitor
• JereticEtAl2025.lexiconCompetitor JereticEtAl2025.Language.german JereticEtAl2025.QSlot.always = JereticEtAl2025.Competitor.unpronounceableWithIndirectAlt
• JereticEtAl2025.lexiconCompetitor JereticEtAl2025.Language.japanese JereticEtAl2025.QSlot.which = JereticEtAl2025.Competitor.lexicalDual
• JereticEtAl2025.lexiconCompetitor JereticEtAl2025.Language.japanese JereticEtAl2025.QSlot.each = JereticEtAl2025.Competitor.lexicalDual
• JereticEtAl2025.lexiconCompetitor JereticEtAl2025.Language.japanese JereticEtAl2025.QSlot.one = JereticEtAl2025.Competitor.lexicalDual
• JereticEtAl2025.lexiconCompetitor JereticEtAl2025.Language.japanese JereticEtAl2025.QSlot.always = JereticEtAl2025.Competitor.unpronounceableWithIndirectAlt
• JereticEtAl2025.lexiconCompetitor JereticEtAl2025.Language.icelandic JereticEtAl2025.QSlot.which = JereticEtAl2025.Competitor.lexicalDual
• JereticEtAl2025.lexiconCompetitor JereticEtAl2025.Language.slovenian JereticEtAl2025.QSlot.universal = JereticEtAl2025.Competitor.noCompetitor
• JereticEtAl2025.lexiconCompetitor x✝¹ x✝ = JereticEtAl2025.Competitor.noCompetitor

def 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 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 JereticEtAl2025.englishRealizesDual : Prop

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

Equations

• JereticEtAl2025.englishRealizesDual = ∃ q ∈ English.Determiners.allQuantifiers, q.numberRestriction = some Number.dual

theorem JereticEtAl2025.english_realizes_dual : englishRealizesDual

def 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

• JereticEtAl2025.frenchHasDualOnDefinite = (French.Determiners.les_deux.numberRestriction = some Number.dual)

theorem JereticEtAl2025.french_dual_on_definite : frenchHasDualOnDefinite

theorem JereticEtAl2025.french_tous_not_lexical_dual : French.Determiners.tous.numberRestriction ≠ some Number.dual

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

theorem JereticEtAl2025.english_universal_competitor_grounded : lexiconCompetitor Language.english QSlot.universal = Competitor.lexicalDual ∧ ∃ q ∈ English.Determiners.allQuantifiers, q.numberRestriction = some Number.dual

The grounding bridge: lexiconCompetitor .english .universal = .lexicalDual is consistent with English having a .du-marked universal quantifier — both (numberRestriction = some Number.dual; its universal denotation is both_sem = every_sem ∧ |R| ≥ 2, no longer a stored qforce field after the marked-Quantifier migration).

theorem JereticEtAl2025.french_universal_competitor_grounded : lexiconCompetitor Language.french QSlot.universal = Competitor.unpronounceableWithIndirectAlt ∧ French.Determiners.tous.numberRestriction = some Number.plural ∧ French.Determiners.tous.numberRestriction ≠ some Number.dual ∧ French.Determiners.les_deux.numberRestriction = some Number.dual

The grounding bridge for French: lexiconCompetitor .french .universal = .unpronounceableWithIndirectAlt is consistent with French tous being plural-restricted (not .dual-marked) AND les deux realizing dual on the definite slot (the indirect alternative). tous's universal force is a fact about its denotation, no longer a stored qforce field after the marked-Quantifier migration.

theorem 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 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 Studies/Sauerland2003.lean

[Sau03] formalizes MP competition over phi-features (sg/pl/dual) via direct alternatives — the standard [Per06], [Sau08] 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 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

• JereticEtAl2025.directAltAgrees x✝¹ x✝ = match JereticEtAl2025.lexiconCompetitor x✝¹ x✝ with | JereticEtAl2025.Competitor.lexicalDual => true | x => false

def JereticEtAl2025.directAltDiverges : Language → QSlot → Bool

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

Equations

• JereticEtAl2025.directAltDiverges x✝¹ x✝ = match JereticEtAl2025.lexiconCompetitor x✝¹ x✝ with | JereticEtAl2025.Competitor.unpronounceableWithIndirectAlt => true | x => false

theorem 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 Alternatives.Source / indirectFrom / Alternatives.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 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 JereticEtAl2025.instDecidableEqWorldEx : DecidableEq WorldEx

Equations

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

def JereticEtAl2025.instReprWorldEx.repr : WorldEx → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance JereticEtAl2025.instReprWorldEx : Repr WorldEx

Equations

• JereticEtAl2025.instReprWorldEx = { reprPrec := JereticEtAl2025.instReprWorldEx.repr }

theorem JereticEtAl2025.tous_violatesMP_via_indirect : Alternatives.violatesMP JereticEtAl2025.frenchIndirectSrc✝ JereticEtAl2025.presupFn✝ JereticEtAl2025.assertionFn✝ JereticEtAl2025.tousVerres✝ fun (x : Syntax.Tree Syntax.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 Alternatives.Source / indirectFrom / Alternatives.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).