Neg-Raising as O→E Pragmatic Strengthening

@cite{gajewski-2007} @cite{horn-2001}

Neg-raising is the phenomenon where the negation of an attitude verb is interpreted as the attitude applied to the negated complement:

"I don't think it's raining" ≈ "I think it's not raining" ¬Bel(p) → Bel(¬p)

In terms of the Square of Opposition, this is strengthening from the O-corner (¬Bel(p)) to the E-corner (Bel(¬p)). This strengthening is available precisely because belief and disbelief are contraries: one can neither believe p nor believe ¬p (the "undecided" gap). The pragmatic inference fills this gap by assuming the agent has a settled opinion.

The Doxastic Square

        contraries
  Bel(p) ────────── Bel(¬p)
    │ │
    │ │
    │ │
  ◇p ──────────────── ¬Bel(p)
       subcontraries

• A = Bel(p): agent believes p
• E = Bel(¬p): agent believes not-p (disbelieves p)
• I = ◇p: agent's beliefs are compatible with p
• O = ¬Bel(p): agent doesn't believe p

Neg-raising is available for believe and think (non-veridical: there is a gap between ¬Bel(p) and Bel(¬p)) but NOT for know (veridical: ¬know(p) includes cases where p is false, so strengthening to know(¬p) would require ¬p to be true, which is a factual claim the speaker may not intend).

def Semantics.Attitudes.NegRaising.doxasticSquare {W : Type u_1} {E : Type u_2} (R : Doxastic.AccessRel W E) (agent : E) (worlds : List W) (p : W → Bool) : Core.SquareOfOpposition.Square (W → Bool)

The doxastic square for a belief predicate.

Given an accessibility relation, agent, and proposition, produce the four corners of the doxastic square of opposition:

• A = Bel(p): all doxastic alternatives satisfy p
• E = Bel(¬p): all doxastic alternatives satisfy ¬p
• I = ◇p: some doxastic alternative satisfies p
• O = ¬Bel(p): not all doxastic alternatives satisfy p

Equations

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

theorem Semantics.Attitudes.NegRaising.doxasticSquare_contradAO {W : Type u_1} {E : Type u_2} (R : Doxastic.AccessRel W E) (agent : E) (worlds : List W) (p : W → Bool) (w : W) : (doxasticSquare R agent worlds p).A w = !(doxasticSquare R agent worlds p).O w

The doxastic square satisfies the A–O contradiction diagonal.

theorem Semantics.Attitudes.NegRaising.doxasticSquare_contradEI {W : Type u_1} {E : Type u_2} (R : Doxastic.AccessRel W E) (agent : E) (worlds : List W) (p : W → Bool) (w : W) : (doxasticSquare R agent worlds p).E w = !(doxasticSquare R agent worlds p).I w

The doxastic square satisfies the E–I contradiction diagonal.

This requires that diaAt is the dual of boxAt: ◇p = ¬□¬p. We prove this from the definitions.

structure Semantics.Attitudes.NegRaising.NegRaisingPredicate (W : Type u_1) (E : Type u_2) extends Semantics.Attitudes.Doxastic.DoxasticPredicate W E : Type (max u_1 u_2)

A neg-raising predicate is a doxastic predicate whose negation is pragmatically strengthened from O (¬Bel(p)) to E (Bel(¬p)).

The negRaises field indicates whether the predicate supports this inference. Structurally, neg-raising is available when the predicate is non-veridical (belief, not knowledge).

• name : String
• access : AccessRel W E
• veridicality : Veridicality
• createsOpaqueContext : Bool
• negRaises : Bool

  Whether negation of this predicate raises into the complement.

def Semantics.Attitudes.NegRaising.negRaisesAt {W : Type u_1} {E : Type u_2} (R : Doxastic.AccessRel W E) (agent : E) (worlds : List W) (p : W → Bool) (w : W) : Prop

Neg-raising is the pragmatic inference from O to E: ¬V(p) is strengthened to V(¬p).

This is the "excluded middle of belief": when a speaker says "I don't think p", they implicate they have a settled opinion, namely Bel(¬p).

Equations

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

def Semantics.Attitudes.NegRaising.negRaisingAvailable (v : Doxastic.Veridicality) : Bool

Neg-raising is available exactly when the predicate admits a gap between ¬Bel(p) and Bel(¬p) — i.e., when the O→E strengthening is a genuine pragmatic move (not a semantic entailment).

For non-veridical predicates, ¬Bel(p) does NOT semantically entail Bel(¬p) — there is a gap (the agent might be undecided). Neg-raising fills this gap pragmatically.

For veridical predicates (know), ¬know(p) could mean either: (a) p is true but agent doesn't know it, or (b) p is false Strengthening to know(¬p) would require (b), which is a factual claim beyond pragmatic strengthening.

Equations

• Semantics.Attitudes.NegRaising.negRaisingAvailable Semantics.Attitudes.Doxastic.Veridicality.nonVeridical = true
• Semantics.Attitudes.NegRaising.negRaisingAvailable Semantics.Attitudes.Doxastic.Veridicality.veridical = false

def Semantics.Attitudes.NegRaising.believeNR {W : Type u_1} {E : Type u_2} (R : Doxastic.AccessRel W E) : NegRaisingPredicate W E

"believe" supports neg-raising. "I don't believe it's raining" ≈ "I believe it's not raining".

Equations

• Semantics.Attitudes.NegRaising.believeNR R = { toDoxasticPredicate := Semantics.Attitudes.Doxastic.believeTemplate R, negRaises := true }

def Semantics.Attitudes.NegRaising.thinkNR {W : Type u_1} {E : Type u_2} (R : Doxastic.AccessRel W E) : NegRaisingPredicate W E

"think" supports neg-raising. "I don't think it's raining" ≈ "I think it's not raining".

Equations

• Semantics.Attitudes.NegRaising.thinkNR R = { toDoxasticPredicate := Semantics.Attitudes.Doxastic.thinkTemplate R, negRaises := true }

def Semantics.Attitudes.NegRaising.knowNR {W : Type u_1} {E : Type u_2} (R : Doxastic.AccessRel W E) : NegRaisingPredicate W E

"know" does NOT support neg-raising. "I don't know it's raining" ≠ "I know it's not raining".

Equations

• Semantics.Attitudes.NegRaising.knowNR R = { toDoxasticPredicate := Semantics.Attitudes.Doxastic.knowTemplate R, negRaises := false }

theorem Semantics.Attitudes.NegRaising.negRaising_iff_nonVeridical (v : Doxastic.Veridicality) : negRaisingAvailable v = true ↔ v = Doxastic.Veridicality.nonVeridical

Neg-raising availability aligns with non-veridicality.

theorem Semantics.Attitudes.NegRaising.believe_negRaises {W : Type u_1} {E : Type u_2} (R : Doxastic.AccessRel W E) : (believeNR R).negRaises = true

"believe" is classified as neg-raising.

theorem Semantics.Attitudes.NegRaising.think_negRaises {W : Type u_1} {E : Type u_2} (R : Doxastic.AccessRel W E) : (thinkNR R).negRaises = true

"think" is classified as neg-raising.

theorem Semantics.Attitudes.NegRaising.know_not_negRaises {W : Type u_1} {E : Type u_2} (R : Doxastic.AccessRel W E) : (knowNR R).negRaises = false

"know" is NOT classified as neg-raising.

theorem Semantics.Attitudes.NegRaising.negRaising_implies_nonVeridical {W : Type u_1} {E : Type u_2} (V : NegRaisingPredicate W E) (hNR : V.negRaises = true) (hAlign : V.negRaises = negRaisingAvailable V.veridicality) : V.veridicality = Doxastic.Veridicality.nonVeridical

Neg-raising predicates are non-veridical.

theorem Semantics.Attitudes.NegRaising.believe_square_contradictions {W : Type u_1} {E : Type u_2} (R : Doxastic.AccessRel W E) (agent : E) (worlds : List W) (p : W → Bool) (w : W) : (doxasticSquare R agent worlds p).A w = !(doxasticSquare R agent worlds p).O w ∧ (doxasticSquare R agent worlds p).E w = !(doxasticSquare R agent worlds p).I w

The doxastic square for "believe" satisfies the contradiction diagonals.