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

[JBG+25]

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. […] French tous is also anti-dual. But French does not have a lexical item for 'both'.

The account (resolving [Che07a]'s puzzle via the conceptual alternatives of [BKC18]): dual number features are universally present — overt in Slovenian (paper (36)), in French syncretic with plural — so the string tous les NP is parse-ambiguous between plural and dual. Three entities drive the competition (paper §4, Fig. 1):

1. Lexicalized dual items (English both/neither, German beide, Japanese dotti, Icelandic hvor) — standard MP competitors ([Per06], [Sau08]).
2. The unpronounceable dual structure (tous les NP.dual) — generated by the grammar, blocked from pronunciation by Avoid Ambiguity (paper eq 37; Blocked below).
3. The indirect alternative (les deux NP) — pronounceable, meaning-equivalent to (2), at most as complex by node count; its existence licenses (2) as MP competitor (paper eq 43, Alternatives.indirectFrom).

paperData records the 19 (language, quantifier-slot) judgment cells the paper reports; theory_matches_data checks the prediction — anti-dual iff a lexical dual or an indirect alternative exists — on every cell. The worked example runs the pipeline on paper (25): Avoid Ambiguity blocks the dual parse (tousDual_blocked), pronounceability is thereby derived rather than stipulated (frenchPron_iff_not_blocked), and MP fires through the indirect alternative (tous_violatesMP_via_indirect). The DUAL denotation itself (paper eq 39) lives in Number.dualPredOnLattice (Features/Number/Decomposition.lean).

The account extends [Sau03]'s direct-alternative phi-feature MP; the two diverge exactly on the indirect-alternative cells (accounts_diverge). Not formalized: §4.4 (tous les deux), §4.5 (domain restrictions on Avoid Ambiguity), §6 (rejected alternatives, e.g. BOTH as the core concept).

Languages, quantifier slots, and competitor typology

inductive JereticEtAl2025.Language : Type

Languages with paper-reported judgment cells.

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

@[instance_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.

@[instance_reducible]

instance JereticEtAl2025.instReprLanguage : Repr Language

Equations

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

inductive JereticEtAl2025.QSlot : Type

Quantifier slots the paper discusses.

• 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.

• one : QSlot

  Existential: English one, French un.

• always : QSlot

  Temporal universal: English always, French toujours, German immer, Japanese itu-mo.

@[instance_reducible]

instance JereticEtAl2025.instDecidableEqQSlot : DecidableEq QSlot

Equations

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

@[instance_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

What a language provides as dual competitor for a quantifier slot (paper §4, Fig. 1): a lexicalized dual item (standard MP), a silent dual structure licensed by a pronounceable indirect alternative, or nothing sufficiently simple.

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

@[instance_reducible]

instance JereticEtAl2025.instDecidableEqCompetitor : DecidableEq Competitor

Equations

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

@[instance_reducible]

instance JereticEtAl2025.instReprCompetitor : Repr Competitor

Equations

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

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

Equations

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

inductive JereticEtAl2025.Acceptability : Type

Paper-reported acceptability in a two-element domain. Three values preserve the paper's gradient judgments: Japanese dono is categorical # where Icelandic hvaða is marginal ?.

• hash : Acceptability

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

• question : Acceptability

  ? — marginal in dual contexts.

• ok : Acceptability

  Felicitous in dual contexts (not anti-dual).

@[instance_reducible]

instance JereticEtAl2025.instDecidableEqAcceptability : DecidableEq Acceptability

Equations

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

@[instance_reducible]

instance JereticEtAl2025.instReprAcceptability : Repr Acceptability

Equations

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

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

Equations

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

def JereticEtAl2025.Acceptability.IsAntiDual (a : Acceptability) : Prop

Anti-dual means degraded in a two-element domain: # or ?.

Equations

• a.IsAntiDual = (a ≠ JereticEtAl2025.Acceptability.ok)

@[instance_reducible]

instance JereticEtAl2025.instDecidableIsAntiDual (a : Acceptability) : Decidable a.IsAntiDual

Equations

• JereticEtAl2025.instDecidableIsAntiDual a = JereticEtAl2025.instDecidableIsAntiDual._aux_1 a

structure JereticEtAl2025.Datum : Type

A (language, quantifier-slot) cell the paper explicitly reports, with its acceptability and paper location.

• language : Language
• slot : QSlot
• observed : Acceptability
• 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.

@[instance_reducible]

instance JereticEtAl2025.instReprDatum : Repr Datum

Equations

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

def JereticEtAl2025.paperData : List Datum

The paper's judgment cells; cells the paper does not report are omitted rather than extrapolated. In particular there is no German universal row (beide is asserted in §2/§5.2 prose, but no alle judgment is reported) and no Slovenian row ((36) shows overt dual morphology, not a quantifier judgment).

Equations

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

The theory

def JereticEtAl2025.lexiconCompetitor : Language → QSlot → Competitor

The typological input the theory reads: the dual competitor each language provides per slot. English and French values are checked against Fragment lexica below; the rest follow the paper:

• English both/neither are lexical duals (§1, §5.2); which of the two etc. are too complex for the other slots (§5.1); always decomposes as all+ways, so both times is an equally complex indirect alternative (§5.4).
• French les deux is the indirect alternative for tous (§4); aucun des deux, ni l'un ni l'autre, and les deux fois are all too complex to block (§5.2, §5.4).
• German has lexical beide (§2, §5.2 prose) but no neither counterpart for keine (§5.2); suppleted immer = all+ways competes with beide Male (§5.4).
• Japanese builds dual which/each/one on the indeterminate dotti (§2); bimorphemic ni-kai on its definite reading is the surrogate for itu-mo — ni-kai-to-mo is too complex (§5.4 (84)–(85)).
• Icelandic has dual hvor beside hvaða (§2 (7)).

Cells the paper does not discuss fall through to .noCompetitor and must not appear in paperData.

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.always = JereticEtAl2025.Competitor.unpronounceableWithIndirectAlt
• JereticEtAl2025.lexiconCompetitor JereticEtAl2025.Language.french JereticEtAl2025.QSlot.universal = JereticEtAl2025.Competitor.unpronounceableWithIndirectAlt
• JereticEtAl2025.lexiconCompetitor JereticEtAl2025.Language.german JereticEtAl2025.QSlot.universal = JereticEtAl2025.Competitor.lexicalDual
• 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 x✝¹ x✝ = JereticEtAl2025.Competitor.noCompetitor

def JereticEtAl2025.PredictsAntiDual (lang : Language) (q : QSlot) : Prop

The account's prediction (paper §4–5): a quantifier is anti-dual iff some dual competitor exists — lexical, or silent-but-licensed by an indirect alternative.

Equations

• JereticEtAl2025.PredictsAntiDual lang q = (JereticEtAl2025.lexiconCompetitor lang q ≠ JereticEtAl2025.Competitor.noCompetitor)

@[instance_reducible]

instance JereticEtAl2025.instDecidablePredictsAntiDual (lang : Language) (q : QSlot) : Decidable (PredictsAntiDual lang q)

Equations

• JereticEtAl2025.instDecidablePredictsAntiDual lang q = JereticEtAl2025.instDecidablePredictsAntiDual._aux_1 lang q

Fragment grounding

The English and French inputs derive from Fragment lexica: if both or les deux lost their dual restriction, or tous its plural one, these checks would fail and expose lexiconCompetitor as out of sync with the lexicon.

theorem JereticEtAl2025.english_universal_grounded : lexiconCompetitor Language.english QSlot.universal = Competitor.lexicalDual ∧ English.Determiners.both.numberRestriction = some Number.dual

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

Theory matches data

theorem JereticEtAl2025.theory_matches_data (d : Datum) : d ∈ paperData → (PredictsAntiDual d.language d.slot ↔ d.observed.IsAntiDual)

On every cell the paper reports, the prediction computed from lexiconCompetitor matches the reported judgment.

theorem JereticEtAl2025.accounts_diverge : lexiconCompetitor Language.french QSlot.universal = Competitor.unpronounceableWithIndirectAlt ∧ lexiconCompetitor Language.english QSlot.always = Competitor.unpronounceableWithIndirectAlt

Divergence from [Sau03]'s direct-alternative phi-MP, which derives anti-duality only from lexicalized duals (English both): it has no route for French tous or English always. The divergence cells are exactly the indirect-alternative ones; the observed judgments (rows "§1 (2)" and "§5.4 (80)" of paperData) favor this paper.

Avoid Ambiguity

Paper eq (37): "if a string S is ambiguous between two parses P1 and P2, and there is a string S′ with a parse P1′ whose meaning is semantically equivalent to P1, but no parse P2′ equivalent to P2, and S′ is structurally at most as complex as S, then string S cannot realize parse P1." Complexity is node count (paper (38)). The paper restricts the principle's domain of application (fn 11, §4.5: phase-bounded application, a broad non-synonymy condition); Blocked is the unrestricted (37).

def JereticEtAl2025.IsAmbiguous {S : Type u_1} {P : Type u_2} {M : Type u_3} (parses : S → List P) (meaning : P → M) (s : S) : Prop

A string is ambiguous iff it has two parses with distinct meanings.

Equations

• JereticEtAl2025.IsAmbiguous parses meaning s = ∃ p₁ ∈ parses s, ∃ p₂ ∈ parses s, meaning p₁ ≠ meaning p₂

def JereticEtAl2025.Blocked {S : Type u_1} {P : Type u_2} {M : Type u_3} (parses : S → List P) (meaning : P → M) (size : S → ℕ) (s : S) (p₁ : P) : Prop

Avoid Ambiguity (paper eq 37): s cannot realize its parse p₁ when s is ambiguous between p₁ and some p₂, and a string s' at most as complex realizes p₁'s meaning but has no parse equivalent to p₂.

Equations

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

theorem JereticEtAl2025.Blocked.isAmbiguous {S : Type u_1} {P : Type u_2} {M : Type u_3} {parses : S → List P} {meaning : P → M} {size : S → ℕ} {s : S} {p₁ : P} (h : Blocked parses meaning size s p₁) : IsAmbiguous parses meaning s

Only ambiguous strings block: eq (37)'s ambiguity premise is built in, so unambiguous synonyms never compete under Avoid Ambiguity.

@[instance_reducible]

instance JereticEtAl2025.instDecidableBlockedOfDecidableEqOfFintype {S : Type u_1} {P : Type u_2} {M : Type u_3} {parses : S → List P} {meaning : P → M} {size : S → ℕ} {s : S} {p₁ : P} [DecidableEq P] [DecidableEq M] [Fintype S] : Decidable (Blocked parses meaning size s p₁)

Equations

• JereticEtAl2025.instDecidableBlockedOfDecidableEqOfFintype = id inferInstance

Worked example: tous les verres (paper (25))

The pipeline end-to-end on paper (25) (tous les verres sont pleins vs les deux verres sont pleins), collapsed to essential head structure: tous V / les_deux V, with the silent witness tous_DUAL V. Trees are shallow — one NP over two terminals — so every step is a decide or a single Katzir substitution.

inductive JereticEtAl2025.WorldEx : Type

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

• w2 : WorldEx
• w3 : WorldEx

@[instance_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.

@[instance_reducible]

instance JereticEtAl2025.instReprWorldEx : Repr WorldEx

Equations

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

@[instance_reducible]

instance JereticEtAl2025.instFintypeWorldEx : Fintype WorldEx

Equations

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

def JereticEtAl2025.tousLex : Syntax.Tree Syntax.Cat String

The universal tous.

Equations

• JereticEtAl2025.tousLex = Syntax.Tree.terminal Syntax.Cat.Det "tous"

def JereticEtAl2025.tousDualLex : Syntax.Tree Syntax.Cat String

The silent dual-bearing realization of tous (paper §4.2.1); same category, so Katzir-substitutable for tousLex.

Equations

• JereticEtAl2025.tousDualLex = Syntax.Tree.terminal Syntax.Cat.Det "tous_DUAL"

def JereticEtAl2025.lesDeuxLex : Syntax.Tree Syntax.Cat String

The indirect alternative les deux, a portmanteau Det for minimality.

Equations

• JereticEtAl2025.lesDeuxLex = Syntax.Tree.terminal Syntax.Cat.Det "les_deux"

def JereticEtAl2025.verresLex : Syntax.Tree Syntax.Cat String

The common noun verres.

Equations

• JereticEtAl2025.verresLex = Syntax.Tree.terminal Syntax.Cat.N "verres"

def JereticEtAl2025.frenchLex : List (Syntax.Tree Syntax.Cat String)

The lexicon of the worked example.

Equations

• JereticEtAl2025.frenchLex = [JereticEtAl2025.tousLex, JereticEtAl2025.tousDualLex, JereticEtAl2025.lesDeuxLex, JereticEtAl2025.verresLex]

def JereticEtAl2025.tousVerres : Syntax.Tree Syntax.Cat String

tous V: the surface universal.

Equations

• JereticEtAl2025.tousVerres = Syntax.Tree.node Syntax.Cat.NP [JereticEtAl2025.tousLex, JereticEtAl2025.verresLex]

def JereticEtAl2025.tousDualVerres : Syntax.Tree Syntax.Cat String

tous_DUAL V: the silent witness — one Katzir substitution from tousVerres, identical size.

Equations

• JereticEtAl2025.tousDualVerres = Syntax.Tree.node Syntax.Cat.NP [JereticEtAl2025.tousDualLex, JereticEtAl2025.verresLex]

def JereticEtAl2025.lesDeuxVerres : Syntax.Tree Syntax.Cat String

les deux V: the indirect alternative, same size as tousVerres.

Equations

• JereticEtAl2025.lesDeuxVerres = Syntax.Tree.node Syntax.Cat.NP [JereticEtAl2025.lesDeuxLex, JereticEtAl2025.verresLex]

def JereticEtAl2025.hasDualMarker (t : Syntax.Tree Syntax.Cat String) : Bool

Whether a tree contains the silent dual marker.

Equations

• JereticEtAl2025.hasDualMarker t = t.subtrees.any fun (s : Syntax.Tree Syntax.Cat String) => match s with | Syntax.Tree.terminal a "tous_DUAL" => true | x => false

def JereticEtAl2025.hasLesDeux (t : Syntax.Tree Syntax.Cat String) : Bool

Whether a tree contains les_deux.

Equations

• JereticEtAl2025.hasLesDeux t = t.subtrees.any fun (s : Syntax.Tree Syntax.Cat String) => match s with | Syntax.Tree.terminal a "les_deux" => true | x => false

@[reducible, inline]

abbrev JereticEtAl2025.frenchPron : Syntax.Tree Syntax.Cat String → Prop

French pronounceability: trees containing tous_DUAL are silent. Stipulated here; derived from Avoid Ambiguity in frenchPron_iff_not_blocked below.

Equations

• JereticEtAl2025.frenchPron t = (JereticEtAl2025.hasDualMarker t = false)

def JereticEtAl2025.meaning (t : Syntax.Tree Syntax.Cat String) (w : WorldEx) : Bool

Toy semantics: tous V asserts "all cups full" with trivial presupposition; the dual variants (silent or les deux) additionally presuppose exactly two cups, so they are defined only in w2.

Equations

• JereticEtAl2025.meaning t JereticEtAl2025.WorldEx.w2 = if (JereticEtAl2025.hasDualMarker t || JereticEtAl2025.hasLesDeux t) = true then true else true
• JereticEtAl2025.meaning t JereticEtAl2025.WorldEx.w3 = if (JereticEtAl2025.hasDualMarker t || JereticEtAl2025.hasLesDeux t) = true then false else true

Avoid Ambiguity discharge (paper §4.2.2)

French dual is syncretic with plural, so the surface string tous les verres realizes both the plural parse and the silent dual parse, while les deux verres unambiguously realizes the dual meaning at equal node count. Eq (37) blocks exactly the dual parse.

inductive JereticEtAl2025.Str : Type

The two surface strings of paper (25).

• tousV : Str
• lesDeuxV : Str

@[instance_reducible]

instance JereticEtAl2025.instDecidableEqStr : DecidableEq Str

Equations

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

@[instance_reducible]

instance JereticEtAl2025.instFintypeStr : Fintype Str

Equations

• JereticEtAl2025.instFintypeStr = { elems := { val := ↑JereticEtAl2025.Str.enumList, nodup := JereticEtAl2025.Str.enumList_nodup }, complete := JereticEtAl2025.instFintypeStr._proof_1 }

def JereticEtAl2025.strParses : Str → List (Syntax.Tree Syntax.Cat String)

Parses per surface string: tous les verres is plural/dual ambiguous (syncretism, §4.2.1); les deux verres is unambiguous.

Equations

• JereticEtAl2025.strParses JereticEtAl2025.Str.tousV = [JereticEtAl2025.tousVerres, JereticEtAl2025.tousDualVerres]
• JereticEtAl2025.strParses JereticEtAl2025.Str.lesDeuxV = [JereticEtAl2025.lesDeuxVerres]

def JereticEtAl2025.strSize (s : Str) : ℕ

String complexity: maximal node count over the string's parses (uniform here, paper (38)).

Equations

• JereticEtAl2025.strSize s = List.foldr max 0 (List.map Syntax.Tree.size (JereticEtAl2025.strParses s))

theorem JereticEtAl2025.tousDual_blocked : Blocked strParses meaning strSize Str.tousV tousDualVerres

Paper §4.2.2: the dual parse of tous les verres is blocked by eq (37), witnessed by les deux verres.

theorem JereticEtAl2025.tousPl_not_blocked : ¬Blocked strParses meaning strSize Str.tousV tousVerres

The plural parse survives: les deux verres does not realize the plural meaning, and no other string is simple enough.

theorem JereticEtAl2025.frenchPron_iff_not_blocked (st : Str) (p : Syntax.Tree Syntax.Cat String) : p ∈ strParses st → (frenchPron p ↔ ¬Blocked strParses meaning strSize st p)

frenchPron is Avoid Ambiguity in disguise: on the example's strings, a parse is pronounceable iff eq (37) does not block it. This derives the pronounceability predicate the indirect-alternative source consumes below.

Maximize Presupposition via the indirect alternative

def JereticEtAl2025.presupFn : Syntax.Tree Syntax.Cat String → WorldEx → Prop

Presupposition: definedness of the sentence, meaning lifted to Prop for the violatesMP substrate.

Equations

• JereticEtAl2025.presupFn t w = (JereticEtAl2025.meaning t w = true)

def JereticEtAl2025.assertionFn : Syntax.Tree Syntax.Cat String → WorldEx → Prop

At-issue assertion, uniform across the three sentences: they differ only in presupposition, the precondition for MP.

Equations

• JereticEtAl2025.assertionFn x✝¹ x✝ = True

def JereticEtAl2025.frenchIndirectSrc : Alternatives.Source (Syntax.Tree Syntax.Cat String)

The indirect-alternative source (paper eq 43): Katzir alternatives filtered by pronounceability and meaning-equivalence to a silent witness, complexity measured by Tree.size.

Equations

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

theorem JereticEtAl2025.tousDual_katzir_alt : tousDualVerres ∈ Alternatives.Structural.katzirSource frenchLex tousVerres

tous_DUAL V is a Katzir alternative of tous V, by substituting tousDualLex for tousLex at the Det position.

theorem JereticEtAl2025.lesDeux_indirectAlt_tous : lesDeuxVerres ∈ frenchIndirectSrc tousVerres

les deux V is in the indirect-alternative source of tous V, witnessed by the silent tous_DUAL V (paper eq 43).

theorem JereticEtAl2025.tous_violatesMP_via_indirect : Alternatives.violatesMP frenchIndirectSrc presupFn assertionFn tousVerres fun (x : Syntax.Tree Syntax.Cat String) => True

tous V violates Maximize Presupposition via the indirect alternative les deux V, licensed by the silent witness tous_DUAL V (paper §4.1 (25), §4.3): the paper's derivation of the anti-duality of tous, end-to-end.