Indefinites in Negated Intensional Contexts @cite{mirrazi-2024}

Semantics & Pragmatics 17, Article 7: 1–44.

The Scope Paradox

Farsi indefinites under negated intensional operators (think, necessary, can) yield "wide pseudo-scope de dicto" readings. The indefinite appears to take wide scope over negation but narrow scope (de dicto) under the intensional operator:

(1) Rodica does not think that Carl read some of the books. Attested: think ≫ INDEF ≫ ¬ = Rodica thinks there are some books Carl didn't read (but she doesn't know which ones)

This is paradoxical: there is no syntactic position that is simultaneously above negation and below think. Under movement-based approaches, the indefinite would have to move above negation, but any such landing site unavoidably outscopes the intensional operator — yielding a de re (not de dicto) construal. This is the "fourth reading" problem (@cite{percus-2000}, @cite{von-fintel-heim-2011}, @cite{keshet-schwarz-2019}).

Choice Functions Solve It

In-situ choice function accounts separate the existential quantification (∃f) from the descriptive content. The ∃-closure over the choice function sits above negation (giving wide scope), while the CF's world variable, bound by the intensional operator, keeps the restrictor de dicto.

World-Skolemized Choice Functions

Standard intensional CFs (@cite{heim-1994}, @cite{winter-1997}) run into the fixed-set problem: when the NP extension is rigid across worlds, f(⟨s, ⟨e,t⟩⟩) returns the same individual everywhere. World-skolemized CFs f(w', NP(w')) solve this: the CF takes a world argument, so it can pick different individuals in different worlds even from the same set.

Cross-Linguistic Variation

Wide pseudo-scope de dicto is available in Farsi and Japanese, marginal in English, and absent in German and French. @cite{schwarz-2012} proposes that determiners vary in whether they carry an independent world variable. Farsi indefinites (ye, čand-ta, do-ta) carry one; German/French do not.

Indefinite/Universal Asymmetry

Universal quantifiers (hame "all") under the same negated intensional operators do NOT get wide pseudo-scope de dicto readings. This follows because universal quantifiers are genuine scope-takers (GQs), not choice functions — they cannot separate their quantificational force from their descriptive content.

inductive Mirrazi2024.ScopeConfig : Type

The three logically possible scope configurations for an indefinite under a negated intensional operator: ¬ INT_OP [INDEF VP].

• narrow : ScopeConfig

  NEG ≫ INT ≫ INDEF: narrow scope (under both).

• wideDeRe : ScopeConfig

  INDEF ≫ NEG ≫ INT: wide scope de re (above both).

• widePseudoDeDicto : ScopeConfig

  INT ≫ INDEF ≫ NEG: wide pseudo-scope de dicto.

@[implicit_reducible]

instance Mirrazi2024.instDecidableEqScopeConfig : DecidableEq ScopeConfig

Equations

• Mirrazi2024.instDecidableEqScopeConfig x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[implicit_reducible]

instance Mirrazi2024.instReprScopeConfig : Repr ScopeConfig

Equations

• Mirrazi2024.instReprScopeConfig = { reprPrec := Mirrazi2024.instReprScopeConfig.repr }

def Mirrazi2024.instReprScopeConfig.repr : ScopeConfig → ℕ → Std.Format

Equations

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

inductive Mirrazi2024.ScopeTakerKind : Type

The kind of scope-taker.

• indefinite : ScopeTakerKind

  An indefinite (choice function semantics).

• universal : ScopeTakerKind

  A genuine generalized quantifier (every, all).

@[implicit_reducible]

instance Mirrazi2024.instDecidableEqScopeTakerKind : DecidableEq ScopeTakerKind

Equations

• Mirrazi2024.instDecidableEqScopeTakerKind x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Mirrazi2024.instReprScopeTakerKind.repr : ScopeTakerKind → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance Mirrazi2024.instReprScopeTakerKind : Repr ScopeTakerKind

Equations

• Mirrazi2024.instReprScopeTakerKind = { reprPrec := Mirrazi2024.instReprScopeTakerKind.repr }

structure Mirrazi2024.NegRaisingCounterargument : Type

Under neg-raising, ¬THINK(p) is strengthened to THINK(¬p).

@cite{mirrazi-2024} §1.2 ex. (5)–(6): if neg-raising applies to (1), the resulting interpretation is THINK(¬[Carl read some of the books]). This puts the indefinite UNDER negation (inside the think-complement), giving think ≫ ¬ ≫ INDEF — NOT the attested think ≫ INDEF ≫ ¬.

Moreover, the same readings arise with non-neg-raising predicates (necessary, can), so neg-raising cannot be the explanation.

• negRaising_wrong_scope : ScopeConfig

  A neg-raising predicate produces think ≫ ¬ ≫ INDEF, not the attested think ≫ INDEF ≫ ¬. The indefinite ends up below negation.

• nonNegRaiser_also_works : Bool

  Non-neg-raising predicates (necessary, can) also yield the reading, so neg-raising is neither necessary nor sufficient.

def Mirrazi2024.negRaisingFails : NegRaisingCounterargument

The neg-raising hypothesis yields the wrong scope configuration. Under neg-raising: ¬think(p) → think(¬p), and the indefinite stays inside ¬p, giving narrow scope — the opposite of what's attested. @cite{mirrazi-2024} §1.2 exx. (5)–(10).

Equations

• Mirrazi2024.negRaisingFails = { negRaising_wrong_scope := Mirrazi2024.ScopeConfig.narrow, nonNegRaiser_also_works := true }

theorem Mirrazi2024.negRaising_yields_narrow : negRaisingFails.negRaising_wrong_scope = ScopeConfig.narrow

Neg-raising yields the wrong scope order for the indefinite.

theorem Mirrazi2024.nonNegRaiser_suffices : negRaisingFails.nonNegRaiser_also_works = true

Neg-raising is not needed: non-neg-raising operators also yield wide pseudo-scope de dicto.

theorem Mirrazi2024.think_does_neg_raise {W : Type u_1} {E : Type u_2} (R : Semantics.Attitudes.Doxastic.AccessRel W E) (agent : E) (worlds : List W) (p : W → Prop) (w : W) (hNeg : ¬Semantics.Attitudes.Doxastic.boxAt R agent w worlds p) (hExclMiddle : Semantics.Attitudes.NegRaising.negRaisesAt R agent worlds p w) : Semantics.Attitudes.Doxastic.boxAt R agent w worlds fun (w' : W) => ¬p w'

Structural verification: think supports neg-raising via the doxastic infrastructure. This connects to the library's negRaisesAt without claiming neg-raising explains the scope paradox.

def Mirrazi2024.widePseudoDeDictoTC (W : Type u_1) (E : Type u_2) (f : Semantics.Quantification.ChoiceFunction.SkolemCF W E) (R : Semantics.Attitudes.Doxastic.AccessRel W E) (agent : E) (worlds : List W) (nounProp : W → E → Prop) (vp : E → W → Prop) (w₀ : W) : Prop

The truth conditions for the wide pseudo-scope de dicto reading, derived from CF semantics.

@cite{mirrazi-2024} ex. (44): ∀w'' ∈ Beliefs(Rodica,w₀): ¬read_{w''}(Carl, f(w'', book(w'')))

The ∃f sits above negation (wide scope), while f's world argument is bound by the attitude verb (de dicto). The accessibility relation R connects to the doxastic infrastructure in Attitudes.Doxastic.

Equations

• Mirrazi2024.widePseudoDeDictoTC W E f R agent worlds nounProp vp w₀ = ∀ w' ∈ worlds, R agent w₀ w' → ¬vp (f w' (nounProp w')) w'

def Mirrazi2024.wideDeReTC (W : Type u_1) (E : Type u_2) (f : Semantics.Quantification.ChoiceFunction.SkolemCF W E) (R : Semantics.Attitudes.Doxastic.AccessRel W E) (agent : E) (worlds : List W) (nounProp : W → E → Prop) (vp : E → W → Prop) (w₀ : W) : Prop

The truth conditions for the genuine wide scope de re reading.

@cite{mirrazi-2024} ex. (41): ∀w'' ∈ Beliefs(Rodica,w₀): ¬read_{w''}(Carl, f(book_{w₀}))

The CF's world variable is free (evaluated at w₀): the individual is fixed across belief worlds.

Equations

• Mirrazi2024.wideDeReTC W E f R agent worlds nounProp vp w₀ = ∀ w' ∈ worlds, R agent w₀ w' → ¬vp (f w₀ (nounProp w₀)) w'

theorem Mirrazi2024.deRe_eq_pseudoDeDicto_when_rigid (W : Type u_1) (E : Type u_2) (f : Semantics.Quantification.ChoiceFunction.SkolemCF W E) (R : Semantics.Attitudes.Doxastic.AccessRel W E) (agent : E) (worlds : List W) (nounProp : W → E → Prop) (vp : E → W → Prop) (w₀ : W) (hRigidNP : ∀ (w : W), nounProp w = nounProp w₀) (hRigidCF : ∀ (w : W), f w = f w₀) : widePseudoDeDictoTC W E f R agent worlds nounProp vp w₀ ↔ wideDeReTC W E f R agent worlds nounProp vp w₀

The key structural fact: de re and pseudo-de dicto differ exactly in whether the CF's world argument is bound (varies with w') or free (fixed at w₀). When nounProp is world-invariant and f is world-invariant, they collapse — the two readings become equivalent.

This is the formal content of the fixed-set problem: when there is no cross-world variation, world-skolemization adds nothing, and the "pseudo-de dicto" reading reduces to plain de re.

theorem Mirrazi2024.movement_above_neg_forces_deRe {W : Type u_1} {E : Type u_2} (f : Semantics.Quantification.ChoiceFunction.SkolemCF W E) (R : Semantics.Attitudes.Doxastic.AccessRel W E) (agent : E) (worlds : List W) (nounProp : W → E → Prop) (vp : E → W → Prop) (w₀ : W) : (∀ w' ∈ worlds, R agent w₀ w' → ¬vp (f w₀ (nounProp w₀)) w') ↔ wideDeReTC W E f R agent worlds nounProp vp w₀

Under movement-based accounts, a DP that moves above an intensional operator is necessarily interpreted de re (at its landing site).

@cite{mirrazi-2024} §2.2, citing @cite{percus-2000}, @cite{von-fintel-heim-2011}, @cite{keshet-schwarz-2019}:

"According to all of these theories, a DP can only get a de dicto reading when it is under the scope of an intensional operator. If a DP moves in order to take wide scope with respect to the intensional operator, it can no longer be construed de dicto."

This means: to scope above negation, the indefinite must move to a position above NEG — but any such position is also above the intensional operator, forcing de re. There is no landing site that is simultaneously above NEG and below the intensional operator (since NEG is syntactically below the operator).

theorem Mirrazi2024.fixedSet_no_variation {W : Type u_1} {E : Type u_2} (f : Semantics.Quantification.ChoiceFunction.CF E) (nounProp : E → Prop) : ∀ (x x✝ : W), f nounProp = f nounProp

The fixed-set problem: when the NP extension is rigid across worlds, a non-world-skolemized CF returns the same individual everywhere.

@cite{mirrazi-2024} §3: Consider a course on Covid-19 with exactly 5 books {A,B,C,D,E}. The extension of "book Carl has to read" is the same set in every belief world. A plain intensional CF f(⟨s,⟨e,t⟩⟩) applied to this rigid intension always returns the same book.

theorem Mirrazi2024.worldSkolem_allows_variation {W : Type u_1} {E : Type u_2} (f : Semantics.Quantification.ChoiceFunction.SkolemCF W E) (P : E → Prop) (w₁ w₂ : W) (hVary : f w₁ P ≠ f w₂ P) : ∃ (x : W) (x : W), f w₁ P ≠ f w₂ P

World-skolemization solves the fixed-set problem: f(w', P) can pick different individuals at different worlds because f varies with w'.

@cite{mirrazi-2024} ex. (45): f(w₁, {A,B,C,D,E}) = A, f(w₂, {A,B,C,D,E}) = C, f(w₃, {A,B,C,D,E}) = E.

Wide pseudo-scope de dicto requires CF semantics + world variable.

@cite{mirrazi-2024} §1.3: universal quantifiers (hame "all") under the same negated intensional operators do NOT get wide pseudo-scope de dicto readings. This follows because universals are genuine GQs — they cannot separate quantificational force from their descriptive content.

The prediction is DERIVED from IndefType.canPseudoDeDicto:

• Indefinite (CF + world var): ✓
• Universal (GQ): ✗ regardless of world variable

theorem Mirrazi2024.existential_never_pseudo (b : Bool) : Semantics.Quantification.ChoiceFunction.IndefType.existential.canPseudoDeDicto b = false

∃-quantifiers never yield pseudo-de dicto, regardless of world variable. This is structural: ∃-quantifiers cannot separate their quantificational force from their descriptive content, so there is no mechanism to place ∃ above negation while keeping the restrictor below the intensional operator.

Cross-linguistic parameter: whether wide pseudo-scope de dicto is available depends on whether the language's indefinite determiners carry a world variable AND use CF semantics.

@cite{mirrazi-2024} §3.1, @cite{schwarz-2012}:

| Language | CF | World var | canPseudoDeDicto |
|----------|-----------|-----------|-----------------|
| Farsi    | ✓         | ✓         | ✓               |
| Japanese | ✓         | ✓         | ✓               |
| English  | ✓         | ✓/✗       | marginal        |
| German   | ?         | ✗         | ✗               |
| French   | ?         | ✗         | ✗               |

These two structural theorems derive the full typological pattern
from `canPseudoDeDicto`. 

theorem Mirrazi2024.worldVar_necessary_for_pseudo : Semantics.Quantification.ChoiceFunction.IndefType.choiceFunction.canPseudoDeDicto false = false

The world variable is necessary: without it, even CF indefinites cannot get pseudo-de dicto (the CF has no world argument to bind).

theorem Mirrazi2024.worldVar_sufficient_for_pseudo : Semantics.Quantification.ChoiceFunction.IndefType.choiceFunction.canPseudoDeDicto true = true

The world variable is sufficient (given CF): with it, the CF's world argument can be bound by the intensional operator, yielding de dicto construal while ∃-closure sits above negation.

theorem Mirrazi2024.plainIndef_pseudo_de_dicto (entry : Fragments.Farsi.Determiners.PlainIndefiniteEntry) (hCF : entry.indefType = Semantics.Quantification.ChoiceFunction.IndefType.choiceFunction) (hWV : entry.hasWorldVar = true) : entry.indefType.canPseudoDeDicto entry.hasWorldVar = true

Any PlainIndefiniteEntry that is a choice function with a world variable is predicted to support wide pseudo-scope de dicto. This is the structurally general version — it applies to ye, čand-ta, do-ta, and any future entry with the same properties.