Neg-raising as O→E pragmatic strengthening

Neg-raising interprets the negation of an attitude verb as the attitude applied to the negated complement — "I don't think it's raining" ≈ "I think it's not raining", ¬Bel(p) strengthened to Bel(¬p) ([Hor01]). On the doxastic square of opposition (doxasticSquare: A = Bel(p), E = Bel(¬p), I = ◇p, O = ¬Bel(p)) this is O→E strengthening, available exactly because belief and disbelief are contraries: the agent may be undecided, so ¬Bel(p) leaves a gap. [Gaj07]'s excluded-middle premise — the agent is Opinionated about the prejacent — closes the gap by disjunctive syllogism (negRaisesAt_of_opinionated). Being opinionated about every prejacent is the decided/subsingleton limit of the shared Homogeneity core (forall_opinionated_iff_subsingleton).

Neg-raising is available for believe and think but not know: for a veridical predicate, ¬know(p) includes the case that p is false, so strengthening to know(¬p) would smuggle in a factual claim (negRaisingAvailable).

The doxastic square

def NegRaising.doxasticSquare {W : Type u_1} {E : Type u_2} (R : E → W → W → Prop) (agent : E) (worlds : List W) (p : W → Prop) : Aristotelian.Square (W → Prop)

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 NegRaising.doxasticSquare_contradAO {W : Type u_1} {E : Type u_2} (R : E → W → W → Prop) (agent : E) (worlds : List W) (p : W → Prop) (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 NegRaising.doxasticSquare_contradEI {W : Type u_1} {E : Type u_2} (R : E → W → W → Prop) (agent : E) (worlds : List W) (p : W → Prop) (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 DiamondAt is the dual of BoxAt: ◇p = ¬□¬p. We prove this from the definitions.

Neg-raising and the excluded-middle premise

def NegRaising.NegRaisesAt {W : Type u_1} {E : Type u_2} (R : E → W → W → Prop) (agent : E) (worlds : List W) (p : W → Prop) (w : W) : Prop

Neg-raising: the O→E inference ¬Bel(p) → Bel(¬p) at a world.

Equations

• NegRaising.NegRaisesAt R agent worlds p w = (¬Doxastic.BoxAt R agent w worlds p → Doxastic.BoxAt R agent w worlds fun (w' : W) => ¬p w')

def NegRaising.Opinionated {W : Type u_1} {E : Type u_2} (R : E → W → W → Prop) (agent : E) (worlds : List W) (p : W → Prop) (w : W) : Prop

The excluded-middle premise: the agent is opinionated about p, believing p or believing ¬p — [Gaj07]'s neg-raising presupposition.

Equations

• NegRaising.Opinionated R agent worlds p w = (Doxastic.BoxAt R agent w worlds p ∨ Doxastic.BoxAt R agent w worlds fun (w' : W) => ¬p w')

theorem NegRaising.negRaisesAt_of_opinionated {W : Type u_1} {E : Type u_2} (R : E → W → W → Prop) (agent : E) (worlds : List W) (p : W → Prop) (w : W) : Opinionated R agent worlds p w → NegRaisesAt R agent worlds p w

Opinionatedness about p licenses the O→E strengthening by disjunctive syllogism: neg-raising is this inference run on the pragmatically presupposed excluded-middle premise, not a semantic entailment.

def NegRaising.accessibleSet {W : Type u_1} {E : Type u_2} (R : E → W → W → Prop) (agent : E) (worlds : List W) (w : W) : Set W

The accessible-worlds set at w; BoxAt … p is ∀ w' ∈ accessibleSet, p w'.

Equations

• NegRaising.accessibleSet R agent worlds w = {w' : W | w' ∈ worlds ∧ R agent w w'}

theorem NegRaising.boxAt_iff_forall_accessibleSet {W : Type u_1} {E : Type u_2} (R : E → W → W → Prop) (agent : E) (worlds : List W) (p : W → Prop) (w : W) : Doxastic.BoxAt R agent w worlds p ↔ ∀ w' ∈ accessibleSet R agent worlds w, p w'

theorem NegRaising.forall_opinionated_iff_subsingleton {W : Type u_1} {E : Type u_2} (R : E → W → W → Prop) (agent : E) (worlds : List W) (w : W) : (∀ (p : W → Prop), Opinionated R agent worlds p w) ↔ (accessibleSet R agent worlds w).Subsingleton

The agent is opinionated about every prejacent — neg-raising then holds as a validity — iff the accessible state is decided, a subsingleton: the doxastic instance of the shared Homogeneity core.

def NegRaising.negRaisingAvailable (v : Features.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

• NegRaising.negRaisingAvailable Features.Veridicality.nonVeridical = true
• NegRaising.negRaisingAvailable Features.Veridicality.veridical = false

Veridicality and square lemmas

theorem NegRaising.negRaising_iff_nonVeridical (v : Features.Veridicality) : negRaisingAvailable v = true ↔ v = Features.Veridicality.nonVeridical

Neg-raising availability aligns with non-veridicality.