Belnap 1970: Conditional Assertion and Restricted Quantification

@cite{belnap-1970}

Nuel D. Belnap Jr. Conditional Assertion and Restricted Quantification. Noûs 4(1): 1–12, 1970.

Core idea

"If p then q" is not a truth-functional connective but a conditional assertion — the assertion of q on the condition p. When p is false, (p/q) is nonassertive: it asserts nothing. Belnap introduces four semantic concepts per sentence A at world w (p. 3):

1. A is true_w — standard sentential truth
2. A is false_w — standard sentential falsity
3. A is assertive_w — whether A asserts anything at w
4. A_w — what A asserts at w (a proposition = set of worlds)

We formalize this via PrProp (presup = assertive, assertion = content), showing that Belnap's system is isomorphic to linglib's existing partial proposition infrastructure.

Main result

Combining conditional assertion with universal quantification derives restricted quantification: ∀x(Cx/Bx) is assertive_w iff ∃xCx is true_w, and what it asserts = ⋀{Bt_w : Ct true_w}. "All crows are black" = "Consider the crows: each one is black."

Integration

• belnap_forall_content_eq_every: content of Belnap's restricted ∀ equals every_sem from generalized quantifier infrastructure
• belnap_exists_content_eq_some: same for restricted ∃
• subalternation_a_i (in Quantifier.lean): the non-empty-restrictor condition that Belnap derives is exactly what @cite{strawson-1952} stipulated as a presupposition of universals
• content_square_relations: concrete SquareRelations instance from Core.SquareOfOpposition, connecting to the abstract algebraic framework
• contrapositive_different_assertiveness: ∀x(Cx/Bx) and ∀x(¬Bx/¬Cx) have different assertiveness conditions — relevant to the confirmation paradox

Three Routes to Restricted Quantification

Belnap's derivation is one of three independent routes to restricted quantification in linglib:

1. Conditional assertion (this file): ∀x(Cx/Bx) = conditional assertion
   • universal quantification. @cite{belnap-1970}
2. Kratzer restrictor: if-clauses restrict modal bases, deriving restricted quantification from modality. @cite{kratzer-1986} See Theories/Semantics/Conditionals/Restrictor.lean.
3. Domain restriction: contextual predicates intersect the restrictor, deriving restricted quantification from pragmatics. @cite{von-fintel-1994} @cite{stanley-szab-2000} See Theories/Semantics/Lexical/Determiner/DomainRestriction.lean.

The convergence of three independent mechanisms on the same result suggests restricted quantification is a deep linguistic universal.

@[reducible, inline]

abbrev Phenomena.Conditionals.Studies.Belnap1970.condAssert {W : Type u_1} (A B : BProp W) : Core.Presupposition.PrProp W

Belnap's (3): conditional assertion (A/B).

"(A/B) is assertive_w just in case A is true_w. Provided (A/B) is assertive_w: (A/B)_w = B_w."

Equations

• Phenomena.Conditionals.Studies.Belnap1970.condAssert = Core.Presupposition.PrProp.condAssert

@[reducible, inline]

abbrev Phenomena.Conditionals.Studies.Belnap1970.atomic {W : Type u_1} (p : BProp W) : Core.Presupposition.PrProp W

Belnap's (6): atomic sentences are categorical — always assertive and always asserting the same proposition.

Equations

• Phenomena.Conditionals.Studies.Belnap1970.atomic = Core.Presupposition.PrProp.ofBProp

theorem Phenomena.Conditionals.Studies.Belnap1970.atomic_always_assertive {W : Type u_1} (p : BProp W) (w : W) : (atomic p).presup w = true

Atomic sentences are assertive at every world (Belnap's (6)).

theorem Phenomena.Conditionals.Studies.Belnap1970.neg_preserves_assertiveness {W : Type u_1} (p : Core.Presupposition.PrProp W) : p.neg.presup = p.presup

Belnap's (7): negation preserves assertiveness and negates content.

"~A is assertive_w just in case A is assertive_w. (A)_w = (A_w)." This is exactly PrProp.neg.

@[reducible, inline]

abbrev Phenomena.Conditionals.Studies.Belnap1970.belnapAnd {W : Type u_1} (p q : Core.Presupposition.PrProp W) : Core.Presupposition.PrProp W

Belnap's (8): conjunction under conditional assertion is PrProp.andBelnap, not classical PrProp.and.

Classical conjunction requires BOTH operands to be defined. Belnap's requires only ONE — undefined conjuncts are skipped.

Equations

• Phenomena.Conditionals.Studies.Belnap1970.belnapAnd = Core.Presupposition.PrProp.andBelnap

@[reducible, inline]

abbrev Phenomena.Conditionals.Studies.Belnap1970.belnapOr {W : Type u_1} (p q : Core.Presupposition.PrProp W) : Core.Presupposition.PrProp W

Belnap's (9): disjunction under conditional assertion.

Equations

• Phenomena.Conditionals.Studies.Belnap1970.belnapOr = Core.Presupposition.PrProp.orBelnap

def Phenomena.Conditionals.Studies.Belnap1970.restrictedForall {m : Semantics.Montague.Model} [Fintype m.Entity] (C B : m.Entity → Bool) : Core.Presupposition.PrProp Unit

Belnap's (11): restricted universal quantification.

∀x(Cx/Bx) is assertive_w iff ∃xCx is true_w. What it asserts = conjunction of Bt for all t such that Ct is true_w.

This derives restricted quantification from two independent mechanisms: conditional assertion (§2) and standard universal quantification (§4).

Equations

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

def Phenomena.Conditionals.Studies.Belnap1970.restrictedExists {m : Semantics.Montague.Model} [Fintype m.Entity] (C B : m.Entity → Bool) : Core.Presupposition.PrProp Unit

Belnap's (12): restricted existential quantification.

∃x(Cx/Bx) is assertive iff ∃xCx is true. What it asserts = disjunction of Bt for all t such that Ct is true.

Equations

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

theorem Phenomena.Conditionals.Studies.Belnap1970.belnap_forall_content_eq_every {m : Semantics.Montague.Model} [Fintype m.Entity] (C B : m.Entity → Bool) : (restrictedForall C B).assertion () = Semantics.Lexical.Determiner.Quantifier.every_sem m C B

Content bridge (∀): what Belnap's ∀x(Cx/Bx) asserts (when assertive) is exactly what every_sem computes.

Proof uses every_sem_extension: every_sem m C B = (elements.filter C).all B.

theorem Phenomena.Conditionals.Studies.Belnap1970.belnap_exists_content_eq_some {m : Semantics.Montague.Model} [Fintype m.Entity] (C B : m.Entity → Bool) : (restrictedExists C B).assertion () = Semantics.Lexical.Determiner.Quantifier.some_sem m C B

Content bridge (∃): what Belnap's ∃x(Cx/Bx) asserts (when assertive) is exactly what some_sem computes.

theorem Phenomena.Conditionals.Studies.Belnap1970.assertive_iff_restrictor_nonempty {m : Semantics.Montague.Model} [Fintype m.Entity] (C B : m.Entity → Bool) : (restrictedForall C B).presup () = decide (∃ (x : m.Entity), C x = true)

Assertiveness = existential presupposition: Belnap's assertiveness condition for ∀x(Cx/Bx) is exactly the existential presupposition of universal quantifiers.

@cite{strawson-1952} argued "All S are P" presupposes there are Ss. Belnap derives this: ∀x(Cx/Bx) is nonassertive when nothing satisfies C. See also subalternation_a_i in Quantifier.lean, which proves the consequence: every(R,S) entails some(R,S) when the restrictor is non-empty.

def Phenomena.Conditionals.Studies.Belnap1970.belnapSquare {m : Semantics.Montague.Model} [Fintype m.Entity] (C B : m.Entity → Bool) : Core.SquareOfOpposition.Square (Core.Presupposition.PrProp Unit)

The Belnap square: the four Aristotelian forms as Belnap restricted quantification, packaged as a Core.SquareOfOpposition.Square of partial propositions (PrProp Unit).

A: ∀x(Cx/Bx) "All C are B" E: ∀x(Cx/¬Bx) "No C are B" I: ∃x(Cx/Bx) "Some C are B" O: ∃x(Cx/¬Bx) "Some C are not B"

Belnap: "semantic relations between these forms turn out to be pretty much a good old fashioned square of opposition!"

Equations

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

theorem Phenomena.Conditionals.Studies.Belnap1970.square_equiassertive {m : Semantics.Montague.Model} [Fintype m.Entity] (C B : m.Entity → Bool) : (belnapSquare C B).A.presup = (belnapSquare C B).E.presup ∧ (belnapSquare C B).A.presup = (belnapSquare C B).I.presup ∧ (belnapSquare C B).A.presup = (belnapSquare C B).O.presup

All four forms share the same assertiveness condition: ∃xCx.

def Phenomena.Conditionals.Studies.Belnap1970.contentSquare {m : Semantics.Montague.Model} [Fintype m.Entity] (C B : m.Entity → Bool) : Core.SquareOfOpposition.Square (Unit → Bool)

The content square: extract the assertion-level content into a Square (Unit → Bool), suitable for constructing SquareRelations.

Equations

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

theorem Phenomena.Conditionals.Studies.Belnap1970.a_o_contradictory {m : Semantics.Montague.Model} [Fintype m.Entity] (C B : m.Entity → Bool) (w : Unit) : (contentSquare C B).A w = !(contentSquare C B).O w

A and O have contradictory content (when both assertive).

theorem Phenomena.Conditionals.Studies.Belnap1970.e_i_contradictory {m : Semantics.Montague.Model} [Fintype m.Entity] (C B : m.Entity → Bool) (w : Unit) : (contentSquare C B).E w = !(contentSquare C B).I w

E and I have contradictory content (when both assertive).

theorem Phenomena.Conditionals.Studies.Belnap1970.content_square_relations {m : Semantics.Montague.Model} [Fintype m.Entity] (C B : m.Entity → Bool) (hR : decide (∃ (x : m.Entity), C x = true) = true) : Core.SquareOfOpposition.SquareRelations (contentSquare C B)

The content square satisfies all six SquareRelations when the restrictor is non-empty. The non-empty condition is exactly Belnap's assertiveness condition — the square's relations hold precisely in the worlds where the forms are assertive.

theorem Phenomena.Conditionals.Studies.Belnap1970.obversion {m : Semantics.Montague.Model} [Fintype m.Entity] (C B : m.Entity → Bool) : restrictedForall C B = restrictedForall C fun (x : m.Entity) => !!B x

Obversion is a strong equivalence (p. 8): "All S are P" ↔ "No S are non-P". In Belnap's framework: ∀x(Cx/Bx) and ∀x(Cx/~~Bx) are equi-assertive and content-identical, since ~~B = B. This is trivially true but worth stating as Belnap explicitly mentions it.

theorem Phenomena.Conditionals.Studies.Belnap1970.i_conversion_content {m : Semantics.Montague.Model} [Fintype m.Entity] (C B : m.Entity → Bool) : (restrictedExists C B).assertion () = (restrictedExists B C).assertion ()

I-conversion preserves assertion content: ∃x(Cx/Bx) and ∃x(Bx/Cx) assert the same proposition (when assertive).

Both reduce to ∃x. C(x) ∧ B(x), which is symmetric in C and B. However, they are NOT equi-assertive: the first requires ∃xCx, the second requires ∃xBx.

theorem Phenomena.Conditionals.Studies.Belnap1970.i_conversion_equitrue {m : Semantics.Montague.Model} [Fintype m.Entity] (C B : m.Entity → Bool) (hTrue : (restrictedExists C B).assertion () = true) : (restrictedExists B C).presup () = true ∧ (restrictedExists B C).assertion () = true

I-conversion is equitrue (p. 8): "truth is preserved in passing from one to the other." If ∃x(Cx/Bx)'s assertion holds, then ∃x(Bx/Cx) is assertive and its assertion holds too.

Note: we prove the stronger result that assertion alone suffices — assertiveness is not needed as a hypothesis (it follows from assertion since any witness for the filter also witnesses ∃xBx).

Belnap: "But 'Some unicorns are animals' is nonassertive while 'Some animals are unicorns' is just plain false."

theorem Phenomena.Conditionals.Studies.Belnap1970.i_conversion_not_equiassertive : ∃ (m : Semantics.Montague.Model) (x : Fintype m.Entity) (C : m.Entity → Bool) (B : m.Entity → Bool), (restrictedExists C B).presup () ≠ (restrictedExists B C).presup ()

I-conversion is NOT equi-assertive in general.

theorem Phenomena.Conditionals.Studies.Belnap1970.barbara_assertive {m : Semantics.Montague.Model} [Fintype m.Entity] (A C B : m.Entity → Bool) (hMinorAssertive : (restrictedForall A C).presup () = true) (hMinorTrue : (restrictedForall A C).assertion () = true) : (restrictedForall C B).presup () = true ∧ (restrictedForall A B).presup () = true

Barbara: assertiveness propagation. When Barbara's minor premise is true (assertive and assertion holds), both her major and her conclusion are assertive.

Belnap (p. 9): "for every w in which Barbara's minor is true_w, both her major and her conclusion are assertive_w."

Proof: the minor's truth means every A-element is a C-element. Combined with its assertiveness (∃xAx), this gives ∃xCx (major is assertive) and ∃xAx (conclusion is assertive, same as minor).

theorem Phenomena.Conditionals.Studies.Belnap1970.barbara {m : Semantics.Montague.Model} [Fintype m.Entity] (A C B : m.Entity → Bool) (hMajor : (restrictedForall C B).assertion () = true) (hMinor : (restrictedForall A C).assertion () = true) : (restrictedForall A B).assertion () = true

Barbara: content implication. What Barbara's major asserts propositionally implies what her conclusion asserts.

Major: ∀x(Cx/Bx) "All crows are black" Minor: ∀x(Ax/Cx) "All of Alan's birds are crows" Concl: ∀x(Ax/Bx) "All of Alan's birds are black"

Belnap (p. 9): "it is her major alone which does any implying of her conclusion, a feature of the situation which doubtless explains the tradition according to which Barbara's major is major and her minor only minor."

theorem Phenomena.Conditionals.Studies.Belnap1970.contrapositive_different_assertiveness {m : Semantics.Montague.Model} [Fintype m.Entity] (C B : m.Entity → Bool) : (restrictedForall C B).presup () = decide (∃ (x : m.Entity), C x = true) ∧ (restrictedForall (fun (x : m.Entity) => !B x) fun (x : m.Entity) => !C x).presup () = decide (∃ (x : m.Entity), (!B x) = true)

The contrapositive ∀x(¬Bx/¬Cx) has a DIFFERENT assertiveness condition from the original ∀x(Cx/Bx).

Original: assertive iff ∃xCx (there are crows) Contrapositive: assertive iff ∃x¬Bx (there are nonblack things)

This is relevant to the confirmation paradox (p. 10): "reports that such and such is not a crow, although offering support for the contrapositive 'No nonblack things are noncrows' — ∀x(~Bx/~Cx) — when such and such is not black, is evidentially irrelevant to ∀x(Cx/Bx)."