Jeretič et al. (2025): Core concepts and indirect alternatives

This file formalizes Jeretič, Bassi, Gonzalez, Yatsushiro, Meyer and Sauerland's account of the anti-duality of French tous. English all and every are unusable in a domain known to hold two individuals because Maximize Presupposition prefers both (Percus, Sauerland); tous is anti-dual too although French has no word for both, the puzzle of Chemla taken by Buccola, Križ and Chemla to show a conceptual alternative at work. The account posits a dual number feature in every language, syncretic with the plural in French, so that the string tous les NP is ambiguous between a plural and a dual parse; Avoid Ambiguity (BarredByAmbiguity) bars the dual parse from pronunciation because les deux NP realizes its meaning at no greater node count, and that expression, an indirect alternative (indirectFrom), licenses the Maximize Presupposition competition the silent parse cannot enter on its own. The worked example runs this on (25): the dual parse is barred, pronounceability is thereby derived rather than stipulated, and tous violates Maximize Presupposition through les deux (tous_blocked_via_indirect), so that it is used in the domain of three cups and not in the domain of two (unblocked_tous).

Across languages and quantifier slots a plain quantifier is predicted anti-dual exactly when a dual competitor exists, a lexical dual item or a pronounceable dual expression at most as complex as the plain one, which Slot.competitor derives from the paper's forms and their node counts; theory_matches_data checks the prediction against the judgments the paper reports, as rows: English no and always anti-dual, French aucun and toujours not, Japanese which, each, and one anti-dual by the lexical dual dotti where English and French are not. An account with direct alternatives only, Sauerland's, predicts anti-duality from lexical duals alone and so misses the indirect cells. The combination tous les deux, the domain restriction of Avoid Ambiguity, and the alternatives the paper rejects are not formalized.

Implementation notes

• Node counts follow the paper: three heads each for tous les NP and les deux NP (38), two morphemes for always as all plus ways, for toujours, for suppletive immer, for itu-mo, and for ni-kai, four for ni-kai-to-mo and the English partitives, three for the French partitives; where the paper names no dual expression the list is empty.
• The English lexical duals are read from the fragment, their lexical status being their dual number restriction; French les deux is the fragment's entry, a two-word expression.

References

• [JBG+25]
• [Che07a]
• [BKC18]
• [Per06]
• [Sau08a]
• [Sau03]

The typology

inductive JereticEtAl2025.Language : Type

The languages with reported judgments.

• 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

The quantifier slots are universal, negative, interrogative, distributive, existential, and the temporal universal always.

• universal : QSlot
• negative : QSlot
• which : QSlot
• each : QSlot
• one : QSlot
• always : QSlot

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

structure JereticEtAl2025.DualForm : Type

A dual expression a language offers for a slot records its form, whether it is a single lexical item, and its node count.

• form : String
• lexical : Bool
• size : ℕ

@[instance_reducible]

instance JereticEtAl2025.instDecidableEqDualForm : DecidableEq DualForm

Equations

• JereticEtAl2025.instDecidableEqDualForm = JereticEtAl2025.instDecidableEqDualForm.decEq

def JereticEtAl2025.instDecidableEqDualForm.decEq (x✝ x✝¹ : DualForm) : Decidable (x✝ = x✝¹)

Equations

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

@[instance_reducible]

instance JereticEtAl2025.instReprDualForm : Repr DualForm

Equations

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

def JereticEtAl2025.instReprDualForm.repr : DualForm → ℕ → Std.Format

Equations

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

def JereticEtAl2025.lexicalDual (form : String) (restriction : Option Number) : DualForm

A lexical dual item of a fragment is a quantifier whose number restriction is the dual.

Equations

• JereticEtAl2025.lexicalDual form restriction = { form := form, lexical := decide (restriction = some Number.dual), size := 1 }

structure JereticEtAl2025.Slot : Type

The plain expression of a slot with its node count and the dual expressions the language offers for it.

• plain : String
• size : ℕ
• duals : List DualForm

@[instance_reducible]

instance JereticEtAl2025.instDecidableEqSlot : DecidableEq Slot

Equations

• JereticEtAl2025.instDecidableEqSlot = JereticEtAl2025.instDecidableEqSlot.decEq

def JereticEtAl2025.instDecidableEqSlot.decEq (x✝ x✝¹ : Slot) : Decidable (x✝ = x✝¹)

Equations

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

def JereticEtAl2025.instReprSlot.repr : Slot → ℕ → Std.Format

Equations

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

@[instance_reducible]

instance JereticEtAl2025.instReprSlot : Repr Slot

Equations

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

inductive JereticEtAl2025.Competitor : Type

The dual competitor a slot provides is a lexical dual item, the standard Maximize Presupposition competitor; or a pronounceable dual expression at most as complex as the plain one, which blocks the silent dual parse and stands in for it as an indirect alternative; or nothing simple enough.

• lexicalDual : Competitor
• indirect : Competitor
• none : 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.

def JereticEtAl2025.Slot.competitor (s : Slot) : Competitor

The competitor a slot provides, from its dual expressions.

Equations

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

def JereticEtAl2025.typology : Language → QSlot → Option Slot

Each of the paper's cells records the plain expression, its node count, and the dual expressions of the language with their counts.

Equations

• One or more equations did not get rendered due to their size.
• JereticEtAl2025.typology JereticEtAl2025.Language.english JereticEtAl2025.QSlot.which = some { plain := "which", size := 1, duals := [{ form := "which of the two", lexical := false, size := 4 }] }
• JereticEtAl2025.typology JereticEtAl2025.Language.english JereticEtAl2025.QSlot.each = some { plain := "each", size := 1, duals := [{ form := "each of the two", lexical := false, size := 4 }] }
• JereticEtAl2025.typology JereticEtAl2025.Language.english JereticEtAl2025.QSlot.one = some { plain := "one", size := 1, duals := [{ form := "one of the two", lexical := false, size := 4 }] }
• JereticEtAl2025.typology JereticEtAl2025.Language.english JereticEtAl2025.QSlot.always = some { plain := "always", size := 2, duals := [{ form := "both times", lexical := false, size := 2 }] }
• JereticEtAl2025.typology JereticEtAl2025.Language.french JereticEtAl2025.QSlot.which = some { plain := "quel", size := 1, duals := [] }
• JereticEtAl2025.typology JereticEtAl2025.Language.french JereticEtAl2025.QSlot.each = some { plain := "chaque", size := 1, duals := [] }
• JereticEtAl2025.typology JereticEtAl2025.Language.french JereticEtAl2025.QSlot.one = some { plain := "un", size := 1, duals := [] }
• JereticEtAl2025.typology JereticEtAl2025.Language.french JereticEtAl2025.QSlot.always = some { plain := "toujours", size := 2, duals := [{ form := "les deux fois", lexical := false, size := 3 }] }
• JereticEtAl2025.typology JereticEtAl2025.Language.german JereticEtAl2025.QSlot.negative = some { plain := "keine", size := 1, duals := [] }
• JereticEtAl2025.typology JereticEtAl2025.Language.german JereticEtAl2025.QSlot.always = some { plain := "immer", size := 2, duals := [{ form := "beide Male", lexical := false, size := 2 }] }
• JereticEtAl2025.typology JereticEtAl2025.Language.japanese JereticEtAl2025.QSlot.which = some { plain := "dono", size := 1, duals := [{ form := "dotti", lexical := true, size := 1 }] }
• JereticEtAl2025.typology JereticEtAl2025.Language.japanese JereticEtAl2025.QSlot.each = some { plain := "dono ... mo", size := 1, duals := [{ form := "dotti ... mo", lexical := true, size := 1 }] }
• JereticEtAl2025.typology JereticEtAl2025.Language.japanese JereticEtAl2025.QSlot.one = some { plain := "dono ... ka", size := 1, duals := [{ form := "dotti ... ka", lexical := true, size := 1 }] }
• JereticEtAl2025.typology JereticEtAl2025.Language.icelandic JereticEtAl2025.QSlot.which = some { plain := "hvaða", size := 1, duals := [{ form := "hvor", lexical := true, size := 1 }] }
• JereticEtAl2025.typology x✝¹ x✝ = none

theorem JereticEtAl2025.universal_competitors : Option.map Slot.competitor (typology Language.english QSlot.universal) = some Competitor.lexicalDual ∧ Option.map Slot.competitor (typology Language.french QSlot.universal) = some Competitor.indirect

In the headline contrast, English all and French tous are anti-dual by different routes, a lexical dual and an indirect alternative.

The judgments

def JereticEtAl2025.cellRow (r : Datum) : Option (Language × QSlot × Bool)

A reported judgment on a plain quantifier records its language, its slot, and whether it is anti-dual, degraded in a domain of two.

Equations

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

def JereticEtAl2025.cells : List (Language × QSlot × Bool)

The paper's judgments on plain quantifiers in a domain of two.

Equations

• JereticEtAl2025.cells = List.filterMap JereticEtAl2025.cellRow JereticEtAl2025.Examples.all

theorem JereticEtAl2025.theory_matches_data (c : Language × QSlot × Bool) : c ∈ cells → ∀ s ∈ typology c.1 c.2.1, s.competitor ≠ Competitor.none ↔ c.2.2 = true

On every reported cell a plain quantifier is anti-dual exactly when its slot provides a competitor.

theorem JereticEtAl2025.direct_account_misses_indirect (c : Language × QSlot × Bool) : c ∈ cells → ∀ s ∈ typology c.1 c.2.1, s.competitor = Competitor.indirect → c.2.2 = true

An account with direct alternatives only predicts anti-duality from lexical duals alone, so it misses the cells whose competitor is indirect, where the paper finds anti-duality.

Avoid Ambiguity

(37): if a string is ambiguous between two parses and a string at most as complex realizes the meaning of the first parse but has no parse equivalent to the second, the string cannot realize the first parse; complexity is node count (38). The paper restricts the principle's domain of application; BarredByAmbiguity 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.BarredByAmbiguity {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

Under Avoid Ambiguity (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.BarredByAmbiguity.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 : BarredByAmbiguity parses meaning size s p₁) : IsAmbiguous parses meaning s

Only ambiguous strings block, so unambiguous synonyms never compete under Avoid Ambiguity.

@[instance_reducible]

instance JereticEtAl2025.instDecidableBarredByAmbiguityOfDecidableEqOfFintype {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 (BarredByAmbiguity parses meaning size s p₁)

Equations

• JereticEtAl2025.instDecidableBarredByAmbiguityOfDecidableEqOfFintype = id inferInstance

Indirect alternatives

def JereticEtAl2025.indirectFrom {S : Type u_1} {M : Type u_2} (base : S → Set S) (pron : S → Prop) (meaning : S → M) (size : S → ℕ) : S → Set S

The indirect alternatives of s (43) are the pronounceable expressions s' at most as complex as s that mean what some unpronounceable alternative sₓ ∈ base s means.

Equations

• JereticEtAl2025.indirectFrom base pron meaning size s = {s' : S | pron s' ∧ size s' ≤ size s ∧ ∃ sₓ ∈ base s, ¬pron sₓ ∧ meaning s' = meaning sₓ}

@[simp]

theorem JereticEtAl2025.mem_indirectFrom {S : Type u_1} {M : Type u_2} {base : S → Set S} {pron : S → Prop} {meaning : S → M} {size : S → ℕ} {s s' : S} : s' ∈ indirectFrom base pron meaning size s ↔ pron s' ∧ size s' ≤ size s ∧ ∃ sₓ ∈ base s, ¬pron sₓ ∧ meaning s' = meaning sₓ

theorem JereticEtAl2025.indirectFrom_eq_empty_of_forall_pron {S : Type u_1} {M : Type u_2} {base : S → Set S} {pron : S → Prop} {meaning : S → M} {size : S → ℕ} {s : S} (h : ∀ x ∈ base s, pron x) : indirectFrom base pron meaning size s = ∅

An expression all of whose alternatives are pronounceable has no indirect alternative.

The worked example (25)

Tous les verres sont pleins against les deux verres sont pleins, collapsed to head structure: tous V, les deux V, and the silent witness tous_DUAL V. Trees are shallow, one NP over two terminals, so every step is a decide or one Katzir substitution.

inductive JereticEtAl2025.WorldEx : Type

The two evaluation contexts are a domain of two cups and a domain of three; the dual presupposition is satisfied only in the first.

• 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 : PhraseStructure.Tree PhraseStructure.Cat String

The universal tous.

Equations

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

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

The silent dual-bearing realization of tous, of the same category and so Katzir-substitutable for tousLex.

Equations

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

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

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

Equations

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

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

The common noun verres.

Equations

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

def JereticEtAl2025.frenchLex : Finset (PhraseStructure.Tree PhraseStructure.Cat String)

The lexicon of the worked example.

Equations

• JereticEtAl2025.frenchLex = {JereticEtAl2025.tousLex, JereticEtAl2025.tousDualLex, JereticEtAl2025.lesDeuxLex, JereticEtAl2025.verresLex}

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

tous V, the surface universal.

Equations

• JereticEtAl2025.tousVerres = PhraseStructure.Tree.node PhraseStructure.Cat.N [JereticEtAl2025.tousLex, JereticEtAl2025.verresLex]

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

tous_DUAL V, the silent witness, one Katzir substitution from tousVerres at the same size.

Equations

• JereticEtAl2025.tousDualVerres = PhraseStructure.Tree.node PhraseStructure.Cat.N [JereticEtAl2025.tousDualLex, JereticEtAl2025.verresLex]

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

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

Equations

• JereticEtAl2025.lesDeuxVerres = PhraseStructure.Tree.node PhraseStructure.Cat.N [JereticEtAl2025.lesDeuxLex, JereticEtAl2025.verresLex]

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

Whether a tree contains the silent dual marker.

Equations

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

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

Whether a tree contains les deux.

Equations

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

@[reducible, inline]

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

Under French pronounceability, trees containing the silent dual marker are silent. Stipulated here and derived from Avoid Ambiguity in frenchPron_iff_not_barred.

Equations

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

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

In the toy semantics tous V asserts that all cups are full with a trivial presupposition; the dual variants, silent or les deux, presuppose exactly two cups and are defined only in the two-cup domain.

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

inductive JereticEtAl2025.Str : Type

The two surface strings of (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 (PhraseStructure.Tree PhraseStructure.Cat String)

The parses of each string, where tous les verres is ambiguous between the plural and the dual parse by syncretism and 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 is the maximal node count over the string's parses, uniform here.

Equations

• JereticEtAl2025.strSize s = List.foldr max 0 (List.map RoseTree.numNodes (JereticEtAl2025.strParses s))

theorem JereticEtAl2025.tousDual_barred : BarredByAmbiguity strParses meaning strSize Str.tousV tousDualVerres

The dual parse of tous les verres is barred by (37), witnessed by les deux verres.

theorem JereticEtAl2025.tousPl_not_barred : ¬BarredByAmbiguity strParses meaning strSize Str.tousV tousVerres

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

theorem JereticEtAl2025.frenchPron_iff_not_barred (st : Str) (p : PhraseStructure.Tree PhraseStructure.Cat String) : p ∈ strParses st → (frenchPron p ↔ ¬BarredByAmbiguity strParses meaning strSize st p)

Pronounceability is Avoid Ambiguity, since on the strings of the example a parse is pronounceable iff (37) does not block it, which derives the predicate the indirect-alternative source consumes.

def JereticEtAl2025.presupFn (t : PhraseStructure.Tree PhraseStructure.Cat String) : Set WorldEx

The presupposition is the set of worlds where the sentence is defined.

Equations

• JereticEtAl2025.presupFn t = {w : JereticEtAl2025.WorldEx | JereticEtAl2025.meaning t w = true}

def JereticEtAl2025.assertionFn : PhraseStructure.Tree PhraseStructure.Cat String → Set WorldEx

The at-issue assertion, uniform across the three sentences, which differ only in presupposition.

Equations

• JereticEtAl2025.assertionFn x✝ = Set.univ

def JereticEtAl2025.frenchIndirectSrc : PhraseStructure.Tree PhraseStructure.Cat String → Set (PhraseStructure.Tree PhraseStructure.Cat String)

The indirect-alternative source (43) filters Katzir alternatives by pronounceability and meaning-equivalence to a silent witness, with complexity measured by RoseTree.numNodes.

Equations

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

theorem JereticEtAl2025.tousDual_katzir_alt : tousDualVerres ∈ PhraseStructure.Tree.structuralAlternatives frenchLex tousVerres

tous_DUAL V is a Katzir alternative of tous V, by substituting the dual determiner.

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 (43).

theorem JereticEtAl2025.lesDeux_mem_sameAssertion : lesDeuxVerres ∈ Competition.sameAssertion frenchIndirectSrc assertionFn tousVerres

les deux V competes with tous V as an indirect alternative with the same assertion.

theorem JereticEtAl2025.presupFn_lesDeux_ssubset_tous : presupFn lesDeuxVerres ⊂ presupFn tousVerres

The dual presupposition of les deux V is strictly stronger than the trivial one of tous V.

theorem JereticEtAl2025.tous_blocked_via_indirect : Competition.Blocked (Competition.sameAssertion frenchIndirectSrc assertionFn) presupFn tousVerres

tous V violates Maximize Presupposition through the indirect alternative les deux V, licensed by the silent witness.

theorem JereticEtAl2025.unblocked_tous : Competition.unblocked (Competition.sameAssertion frenchIndirectSrc assertionFn) presupFn tousVerres = {WorldEx.w3}

tous V is used exactly in the domain of three cups, the paper's derivation of its anti-duality: in the domain of two the dual presupposition of les deux V holds and blocks it, and every competitor defined in the domain of three presupposes nothing.