Gajewski (2007): Neg-Raising and Polarity

Gajewski gives a presuppositional account of neg-raising and argues for it from the licensing of strict negative polarity items. Following Bartsch, a neg-raising predicate such as think presupposes that its subject is settled about the complement, so its negation entails the negated complement: Bill doesn't think Mary is here entails Bill thinks Mary is not here. Strict NPIs such as punctual until and in years need an anti-additive environment, as Zwarts proposes, and the presupposition makes a negated neg-raising predicate anti-additive where a negated universal is not. Since the presupposition of a complement projects into the subject's beliefs whatever the attitude, the negation lowers through think into the complement of want but not through want into the complement of think, the asymmetry of stacked neg-raising predicates that Horn reports.

Main results

• nrp_eq_neg_one_iff, nrp_self_eq_neg_one_iff: a negated neg-raising predicate asserts the negated complement throughout its modal base, and passes through to the negated complement when its heritage base is its modal base.
• isAntiAdditive_negNR, not_isAntiAdditive_negUniversal: a negated neg-raising predicate is anti-additive and a negated universal is not.
• isAntiAdditive_noOneNR: no one thinks is anti-additive under universal projection.
• isAntiAdditive_negStack_self, not_isAntiAdditive_negStack: not think want is anti-additive and not want think is not.
• strawsonAntiAdditive_not_sufficient: Strawson anti-additivity does not characterize the licensers of strict NPIs.
• rows_licensed: the paper's judgments follow the anti-additivity of their environments, with the superlatives the exception the paper records (superlative_exception) and a finite clause boundary degrading the remaining case (finite_boundary).

Implementation notes

• nrp is the neg-raising predicate of Appendix 2, over a modal base and a heritage base, and Env lists the environments of the paper's strict NPIs.
• Propositions are sets of worlds and attitudes relational boxes (ModalLogic.Box). An environment is the truth set of its sentence, presupposition included, as a function of the proposition in the NPI's clause, and its anti-additivity is NaturalLogic.IsAntiAdditive of that function: standard entailment, which Appendix 1 argues is the relevant notion.
• Sentences are trivalent propositions W → SignType. The excluded middle of nrp is stated with the complement's full meaning, φ u ≠ 1 rather than φ u = -1, as in Appendix 2, so that a complement's own presupposition is cancelled inside it and projects only through the heritage base.
• The stressed reading without neg-raising cancels the presupposition with Beaver and Krahmer's assertion operator, so it negates fun w ↦ SignType.ofProp (p w = 1).
• No one thinks is the negated Weak Kleene existential Trivalent.existsWeak over the subtype of people, which projects the excluded middle universally, and negated know is the substrate's two-dimensional ConventionalImplicature.TwoDim.negFactive over a presuppositionless complement.

TODO

• The appendix to §2 explains why it's not true that fails to license: true cancels the complement's presupposition, and disjunction projects presuppositions as in Karttunen and Peters. Formalizing it needs complements with presuppositions, and the paper calls the explanation technical and incomplete.
• The Romance n-words of A.3 are not formalized.

References

• [Gaj07]
• [Bar73]
• [Zwa98]
• [vF99a]
• [Hor78]
• [KP79]
• [Hei83]
• [Hei92]
• [BK01]

Neg-raising predicates ((59)–(61), Appendix 2)

noncomputable def Gajewski2007.nrp {W : Type u_1} (R H : SetRel W W) (φ : W → SignType) : W → SignType

A neg-raising predicate over the modal base R ((59), Appendix 2 (1)–(2)) presupposes that the complement is settled throughout the modal base and that the complement's presupposition holds throughout the heritage base H, and asserts the complement throughout the modal base. Think has its beliefs as both bases, want its desires as modal base and its beliefs as heritage base.

Equations

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

theorem Gajewski2007.nrp_eq_neg_one_iff {W : Type u_1} {R H : SetRel W W} {φ : W → SignType} {w : W} : nrp R H φ w = -1 ↔ ModalLogic.Box H (fun (x : W) => φ x ≠ 0) w ∧ (∃ (u : W), (w, u) ∈ R) ∧ ModalLogic.Box R (fun (x : W) => φ x ≠ 1) w

A neg-raising predicate is false, and its negation true, exactly when the complement's presupposition holds throughout the heritage base, the modal base is nonempty, and the complement fails throughout it ((60)–(61)).

theorem Gajewski2007.nrp_self_eq_neg_one_iff {W : Type u_1} {R : SetRel W W} {φ : W → SignType} {w : W} : nrp R R φ w = -1 ↔ (∃ (u : W), (w, u) ∈ R) ∧ ModalLogic.Box R (fun (x : W) => φ x = -1) w

When the complement's presupposition projects into the predicate's own modal base, as with think, the negation passes through the predicate onto the complement (§3.3.1).

Anti-additivity ((50)–(56))

def Gajewski2007.every {W : Type u_1} (R : SetRel W W) (s : Set W) : Set W

The EVERY of (92) and (110) is universal quantification with existential import over the successors of a world, as a function on propositions.

Equations

• Gajewski2007.every R s = {w : W | (∃ (u : W), (w, u) ∈ R) ∧ ModalLogic.Box R (fun (x : W) => x ∈ s) w}

theorem Gajewski2007.isAntiAdditive_every {W : Type u_1} {R : SetRel W W} {V : Type u_2} {g : Set V → Set W} (hg : NaturalLogic.IsAntiAdditive g) : NaturalLogic.IsAntiAdditive (every R ∘ g)

Universal quantification over an anti-additive environment is anti-additive (92a).

def Gajewski2007.negNR {W : Type u_1} (R H : SetRel W W) (p : Set W) : Set W

The environment of a negated neg-raising predicate.

Equations

• Gajewski2007.negNR R H p = Trivalent.posExt (-Gajewski2007.nrp R H fun (u : W) => SignType.ofProp (u ∈ p))

theorem Gajewski2007.negNR_eq {W : Type u_1} (R H : SetRel W W) (p : Set W) : negNR R H p = every R pᶜ

A negated neg-raising predicate is the universal over the negated complement (61).

theorem Gajewski2007.negNR_subset {W : Type u_1} (R H : SetRel W W) (p : Set W) : negNR R H p ⊆ {w : W | ModalLogic.Box R (fun (x : W) => x ∉ p) w}

Bill doesn't think Mary is here entails Bill thinks Mary is not here (1).

theorem Gajewski2007.isAntiAdditive_negNR {W : Type u_1} (R H : SetRel W W) : NaturalLogic.IsAntiAdditive (negNR R H)

A negated neg-raising predicate is anti-additive ((62)–(64)).

def Gajewski2007.negUniversal {W : Type u_1} (R : SetRel W W) (p : Set W) : Set W

The environment of a negated universal without neg-raising, as in didn't claim, not every, not required and not certain.

Equations

• Gajewski2007.negUniversal R p = {w : W | ¬ModalLogic.Box R (fun (x : W) => x ∈ p) w}

theorem Gajewski2007.not_negUniversal_subset : ¬∀ (W : Type) (R : SetRel W W) (p : Set W), negUniversal R p ⊆ {w : W | ModalLogic.Box R (fun (x : W) => x ∉ p) w}

Bill didn't say that Mary is here does not entail Bill said that Mary isn't here (2).

theorem Gajewski2007.not_isAntiAdditive_negUniversal : ¬NaturalLogic.IsAntiAdditive (negUniversal Set.univ)

A negated universal is not anti-additive ((51b), (53), (65)).

def Gajewski2007.negExistential {W : Type u_1} (R : SetRel W W) (p : Set W) : Set W

The environment of a negated existential, as in not a single, not allowed and can't.

Equations

• Gajewski2007.negExistential R p = {w : W | ¬ModalLogic.Diamond R (fun (x : W) => x ∈ p) w}

theorem Gajewski2007.isAntiAdditive_negExistential {W : Type u_1} (R : SetRel W W) : NaturalLogic.IsAntiAdditive (negExistential R)

A negated existential is anti-additive ((51a), (52), (71)).

def Gajewski2007.negNRStressed {W : Type u_1} (R : SetRel W W) (p : Set W) : Set W

The environment of a neg-raising predicate under stressed negation, where the assertion operator cancels the excluded middle (fn. 7 (ii)).

Equations

• Gajewski2007.negNRStressed R p = Trivalent.posExt fun (w : W) => -SignType.ofProp (Gajewski2007.nrp R R (fun (u : W) => SignType.ofProp (u ∈ p)) w = 1)

theorem Gajewski2007.negNRStressed_eq {W : Type u_1} (R : SetRel W W) : negNRStressed R = negUniversal R

Without its presupposition a negated neg-raising predicate is a negated universal (§2.1.3).

def Gajewski2007.negKnow {W : Type u_1} (R : SetRel W W) (p : Set W) : Set W

The environment of negated know, a factive universal without neg-raising, built from the substrate's negated factive.

Equations

• Gajewski2007.negKnow R p = Trivalent.posExt ((pure fun (x : W) => x ∈ p).negFactive (ModalLogic.Box R)).toTrivalent

theorem Gajewski2007.not_isAntiAdditive_negKnow : ¬NaturalLogic.IsAntiAdditive (negKnow Set.univ)

Negated know is not anti-additive (58b).

Negative quantifiers (§3.1)

def Gajewski2007.noOneNR {W : Type u_1} {E : Type u_2} (O : Set E) (B : E → SetRel W W) (p : Set W) : Set W

No one thinks p (83) has the excluded middle projecting universally from the scope of the quantifier ([Hei83]).

Equations

• Gajewski2007.noOneNR O B p = Trivalent.posExt fun (w : W) => -Trivalent.existsWeak fun (x : ↑O) => Gajewski2007.nrp (B ↑x) (B ↑x) (fun (u : W) => SignType.ofProp (u ∈ p)) w

theorem Gajewski2007.noOneNR_eq {W : Type u_1} {E : Type u_2} (O : Set E) (B : E → SetRel W W) (p : Set W) : noOneNR O B p = {w : W | ∀ x ∈ O, w ∈ every (B x) pᶜ}

No one thinks p is everyone thinks not-p ((87)–(89)).

theorem Gajewski2007.isAntiAdditive_noOneNR {W : Type u_1} {E : Type u_2} (O : Set E) (B : E → SetRel W W) : NaturalLogic.IsAntiAdditive (noOneNR O B)

No one thinks is anti-additive (90).

Stacked neg-raising predicates (§3.2–3.3)

def Gajewski2007.negStack {W : Type u_1} (R₁ H₁ R₂ H₂ : SetRel W W) (p : Set W) : Set W

The environment of a negated neg-raising predicate over another.

Equations

• Gajewski2007.negStack R₁ H₁ R₂ H₂ p = Trivalent.posExt (-Gajewski2007.nrp R₁ H₁ (Gajewski2007.nrp R₂ H₂ fun (u : W) => SignType.ofProp (u ∈ p)))

theorem Gajewski2007.negStack_self_eq {W : Type u_1} (R₁ R₂ H₂ : SetRel W W) (p : Set W) : negStack R₁ R₁ R₂ H₂ p = every R₁ (every R₂ pᶜ)

Under a predicate whose heritage base is its modal base, such as think, the negation goes all the way down ((107)–(110)).

theorem Gajewski2007.negStack_self_subset {W : Type u_1} (R₁ R₂ H₂ : SetRel W W) (p : Set W) : negStack R₁ R₁ R₂ H₂ p ⊆ {w : W | ModalLogic.Box R₁ (ModalLogic.Box R₂ fun (x : W) => x ∉ p) w}

I don't believe Bill wanted Harry to die entails I believe Bill wanted Harry not to die (95).

theorem Gajewski2007.isAntiAdditive_negStack_self {W : Type u_1} (R₁ R₂ H₂ : SetRel W W) : NaturalLogic.IsAntiAdditive (negStack R₁ R₁ R₂ H₂)

Not think want is anti-additive (97a).

theorem Gajewski2007.negStack_eq {W : Type u_1} (R₁ H₁ R₂ : SetRel W W) (p : Set W) : negStack R₁ H₁ R₂ R₂ p = {w : W | (∀ (u : W), (w, u) ∈ H₁ → ModalLogic.Box R₂ (fun (x : W) => x ∈ p) u ∨ ModalLogic.Box R₂ (fun (x : W) => x ∉ p) u) ∧ (∃ (u : W), (w, u) ∈ R₁) ∧ ModalLogic.Box R₁ (fun (u : W) => ¬ModalLogic.Box R₂ (fun (x : W) => x ∈ p) u) w}

When the inner predicate's heritage base is its modal base, the negated stack holds exactly when the inner subject is settled throughout the outer heritage base, the outer modal base is nonempty, and the inner predicate fails throughout it ((111)–(113)).

A frame for John doesn't want Fred to think: John's desire world 0 has Fred considering the worlds 2 and 3 possible, and at John's belief world 1 Fred is settled, considering only 4.

@[reducible, inline]

abbrev Gajewski2007.desJohn : SetRel (Fin 5) (Fin 5)

John's desire alternatives in the frame.

Equations

• Gajewski2007.desJohn = {p : Fin 5 × Fin 5 | p.1 = 0 ∧ p.2 = 0}

@[reducible, inline]

abbrev Gajewski2007.belJohn : SetRel (Fin 5) (Fin 5)

John's belief alternatives in the frame.

Equations

• Gajewski2007.belJohn = {p : Fin 5 × Fin 5 | p.1 = 0 ∧ p.2 = 1}

@[reducible, inline]

abbrev Gajewski2007.belFred : SetRel (Fin 5) (Fin 5)

Fred's belief alternatives in the frame.

Equations

• Gajewski2007.belFred = {p : Fin 5 × Fin 5 | p.1 = 0 ∧ (p.2 = 2 ∨ p.2 = 3) ∨ p.1 = 1 ∧ p.2 = 4}

theorem Gajewski2007.not_negStack_subset : ¬negStack desJohn belJohn belFred belFred {2} ⊆ {w : Fin 5 | ModalLogic.Box desJohn (ModalLogic.Box belFred fun (x : Fin 5) => x ∉ {2}) w}

I don't want Bill to believe Harry died does not entail I want Bill to believe Harry didn't die ((96), (114)).

theorem Gajewski2007.not_isAntiAdditive_negStack : ¬NaturalLogic.IsAntiAdditive (negStack desJohn belJohn belFred belFred)

Not want think is not anti-additive (97b). John wants Fred not to think p and not to think q, and yet Fred thinks p or q at John's desire world.

The environments of the paper's strict NPIs

inductive Gajewski2007.Env : Type

The environments in which the paper places a strict NPI.

• positive : Env

  No licenser, (12a), (13a).

• negation : Env

  Sentential negation, (12b), (13b).

• notSome : Env

  A negated existential, as in not a single, not allowed, can't and not possible.

• notEvery : Env

  A negated universal, as in not every, didn't claim, not required and not certain.

• notThink : Env

  A negated neg-raising predicate, as in doesn't think and doesn't believe.

• notThinkStressed : Env

  A neg-raising predicate under stressed negation, fn. 7 (ii).

• notKnow : Env

  Negated know, (58b).

• noOneThinks : Env

  A negative quantifier over a neg-raising predicate, (83).

• notThinkWant : Env

  A negated doxastic neg-raising predicate over another, as in don't believe … wanted.

• notWantThink : Env

  A negated bouletic or deontic neg-raising predicate over a doxastic one, as in don't want … believe and shouldn't think.

• only : Env

  Only DP, (123).

• adversative : Env

  An adversative attitude, (126).

• conditional : Env

  A conditional antecedent, (127).

• superlative : Env

  The relative clause of a superlative, (132).

@[instance_reducible]

instance Gajewski2007.instDecidableEqEnv : DecidableEq Env

Equations

• Gajewski2007.instDecidableEqEnv x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[instance_reducible]

instance Gajewski2007.instReprEnv : Repr Env

Equations

• Gajewski2007.instReprEnv = { reprPrec := Gajewski2007.instReprEnv.repr }

def Gajewski2007.instReprEnv.repr : Env → ℕ → Std.Format

Equations

• One or more equations did not get rendered due to their size.
• Gajewski2007.instReprEnv.repr Gajewski2007.Env.positive prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Gajewski2007.Env.positive")).group prec✝
• Gajewski2007.instReprEnv.repr Gajewski2007.Env.negation prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Gajewski2007.Env.negation")).group prec✝
• Gajewski2007.instReprEnv.repr Gajewski2007.Env.notSome prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Gajewski2007.Env.notSome")).group prec✝
• Gajewski2007.instReprEnv.repr Gajewski2007.Env.notEvery prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Gajewski2007.Env.notEvery")).group prec✝
• Gajewski2007.instReprEnv.repr Gajewski2007.Env.notThink prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Gajewski2007.Env.notThink")).group prec✝
• Gajewski2007.instReprEnv.repr Gajewski2007.Env.notKnow prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Gajewski2007.Env.notKnow")).group prec✝
• Gajewski2007.instReprEnv.repr Gajewski2007.Env.only prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Gajewski2007.Env.only")).group prec✝

def Gajewski2007.Env.AntiAdditive : Env → Prop

An environment is anti-additive in every frame.

Equations

• One or more equations did not get rendered due to their size.
• Gajewski2007.Env.positive.AntiAdditive = ∀ (W : Type), NaturalLogic.IsAntiAdditive id
• Gajewski2007.Env.negation.AntiAdditive = ∀ (W : Type), NaturalLogic.IsAntiAdditive compl
• Gajewski2007.Env.notSome.AntiAdditive = ∀ (W : Type) (R : SetRel W W), NaturalLogic.IsAntiAdditive (Gajewski2007.negExistential R)
• Gajewski2007.Env.notEvery.AntiAdditive = ∀ (W : Type) (R : SetRel W W), NaturalLogic.IsAntiAdditive (Gajewski2007.negUniversal R)
• Gajewski2007.Env.notThink.AntiAdditive = ∀ (W : Type) (R H : SetRel W W), NaturalLogic.IsAntiAdditive (Gajewski2007.negNR R H)
• Gajewski2007.Env.notThinkStressed.AntiAdditive = ∀ (W : Type) (R : SetRel W W), NaturalLogic.IsAntiAdditive (Gajewski2007.negNRStressed R)
• Gajewski2007.Env.notKnow.AntiAdditive = ∀ (W : Type) (R : SetRel W W), NaturalLogic.IsAntiAdditive (Gajewski2007.negKnow R)
• Gajewski2007.Env.noOneThinks.AntiAdditive = ∀ (W E : Type) (O : Set E) (B : E → SetRel W W), NaturalLogic.IsAntiAdditive (Gajewski2007.noOneNR O B)
• Gajewski2007.Env.notThinkWant.AntiAdditive = ∀ (W : Type) (B R H : SetRel W W), NaturalLogic.IsAntiAdditive (Gajewski2007.negStack B B R H)
• Gajewski2007.Env.notWantThink.AntiAdditive = ∀ (W : Type) (D B R : SetRel W W), NaturalLogic.IsAntiAdditive (Gajewski2007.negStack D B R R)
• Gajewski2007.Env.only.AntiAdditive = ∀ (W ι : Type) (x : ι), NaturalLogic.IsAntiAdditive fun (P : ι → Set W) => Trivalent.posExt (NaturalLogic.only x P)

theorem Gajewski2007.Env.antiAdditive_iff (e : Env) : e.AntiAdditive ↔ e ∈ [negation, notSome, notThink, noOneThinks, notThinkWant]

Of the paper's environments, sentential negation, the negated existentials, the negated neg-raising predicates, no one thinks and not think want are anti-additive.

@[instance_reducible]

instance Gajewski2007.instDecidablePredEnvAntiAdditive : DecidablePred Env.AntiAdditive

Equations

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

theorem Gajewski2007.strawsonAntiAdditive_not_sufficient : (∀ (W ι : Type) (x : ι), NaturalLogic.IsStrawsonAntiAdditive (NaturalLogic.only x)) ∧ (∀ (W : Type) (dox base : W → Set W) (g : W → Set (W → Prop)), NaturalLogic.IsStrawsonAntiAdditive (Desire.BestWorlds.regret dox base g)) ∧ (∀ (W : Type) (horizon : W → Set W) (q : Set W), NaturalLogic.IsStrawsonAntiAdditive fun (x : Set W) => Conditional.horizonCounterfactual horizon x q) ∧ (∀ (W ι D : Type) [inst : Preorder D] (μ : ι → D) (a : ι), NaturalLogic.IsStrawsonAntiAdditive fun (x : W → Set ι) => Degree.superlative μ x a) ∧ ∀ e ∈ [Env.only, Env.adversative, Env.conditional, Env.superlative], ¬e.AntiAdditive

Only DP, the adversatives, conditional antecedents and superlatives are all Strawson anti-additive, and none is anti-additive ((122)–(131)).

The paper's judgments

def Gajewski2007.envTable : List (String × Env)

The environments of the rows, keyed as in Data/Examples/Gajewski2007.json.

Equations

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

structure Gajewski2007.Row : Type

A sentence with a strict NPI records its environment and its judgment.

• env : Env

  The environment of the strict NPI.

• judgment : Judgment

  The paper's judgment.

def Gajewski2007.instDecidableEqRow.decEq (x✝ x✝¹ : Row) : Decidable (x✝ = x✝¹)

Equations

• Gajewski2007.instDecidableEqRow.decEq { env := a, judgment := a_1 } { env := b, judgment := b_1 } = if h : a = b then h ▸ if h : a_1 = b_1 then h ▸ isTrue ⋯ else isFalse ⋯ else isFalse ⋯

@[instance_reducible]

instance Gajewski2007.instDecidableEqRow : DecidableEq Row

Equations

• Gajewski2007.instDecidableEqRow = Gajewski2007.instDecidableEqRow.decEq

@[instance_reducible]

instance Gajewski2007.instReprRow : Repr Row

Equations

• Gajewski2007.instReprRow = { reprPrec := Gajewski2007.instReprRow.repr }

def Gajewski2007.instReprRow.repr : Row → ℕ → Std.Format

Equations

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

def Gajewski2007.Row.ofDatum (ex : Datum) : Option Row

The row of an example.

Equations

• Gajewski2007.Row.ofDatum ex = do let __do_lift ← ex.parse? "environment" Gajewski2007.envTable pure { env := __do_lift, judgment := ex.judgment }

theorem Gajewski2007.row_ofDatum_isSome (ex : Datum) : ex ∈ Examples.all → (Row.ofDatum ex).isSome = true

Every example of the paper parses to a row.

def Gajewski2007.rows : List Row

The paper's sentences with strict NPIs.

Equations

• Gajewski2007.rows = List.filterMap Gajewski2007.Row.ofDatum Gajewski2007.Examples.all

theorem Gajewski2007.rows_licensed (r : Row) : r ∈ rows → r.env ≠ Env.superlative → (r.judgment = Judgment.acceptable → r.env.AntiAdditive) ∧ (r.judgment = Judgment.ungrammatical → ¬r.env.AntiAdditive)

A strict NPI is acceptable in an anti-additive environment and unacceptable elsewhere, the superlatives aside (55).

theorem Gajewski2007.superlative_exception (r : Row) : r ∈ rows → r.env = Env.superlative → r.judgment = Judgment.acceptable ∧ ¬r.env.AntiAdditive

Strict NPIs are acceptable in superlative relative clauses, which are Strawson anti-additive but not anti-additive, the exception the paper leaves open (132).

theorem Gajewski2007.finite_boundary (ex : Datum) : ex ∈ Examples.all → ∀ e ∈ ex.parse? "environment" envTable, e.AntiAdditive → ex.judgment ≠ Judgment.acceptable → ex.feature? "clause" = some "finite"

Where a strict NPI in an anti-additive environment is not acceptable, a finite clause boundary separates it from its licenser, the room the paper leaves for a locality condition ((73)–(74)).