Belnap (1970): Conditional Assertion and Restricted Quantification

Belnap reads "if p then q" as a conditional assertion, the assertion of q on the condition p, which is assertive only where p is true and is as if never made elsewhere. At a world a sentence is true, false or nonassertive (p. 3), and so has a trivalent value. Combining conditional assertion (3) with universal quantification (10) derives restricted quantification (11): "All crows are black" becomes "Consider the crows: each one is black", assertive only if there are crows.

Main statements

• restrictedForall_eq_zero_iff: the restricted forms (11)–(12) are nonassertive exactly when nothing satisfies the restrictor, which is Strawson's existential presupposition, here derived rather than stipulated.
• belnap_forall_content_eq_every, restrictedExists_eq_one_iff: when assertive, the restricted forms assert every and GQ.some.
• contentSquare_eq_square, content_square_relations: where the forms are assertive their contents are the quantifier square at the restrictor, so they stand in all six relations of the square.
• i_conversion_equitrue, i_conversion_not_equiassertive, barbara: conversion preserves truth but not assertiveness, and Barbara's major does all the implying (pp. 8–9).

Implementation notes

The conditional assertion (A/B) of (3) is the indicator {w | A w}.indicator fun w ↦ SignType.ofProp (B w), a categorical atom (6) is fun w ↦ SignType.ofProp (A w), negation (7) is -, which preserves assertiveness, conjunction (8) and disjunction (9) are SignType.meetBelnap and SignType.joinBelnap, assertive iff some operand is, and the quantifiers (10) are Trivalent.forallHaug and Trivalent.existsHaug. The restricted forms are evaluated in a single model, where what a sentence asserts is represented by its truth value, so the propositional implication between contents that Belnap appeals to is read as implication between truth values.

References

• [Bel70]
• [Qui50]
• [Str52]

noncomputable def Belnap1970.restrictedForall {E : Type} (C B : E → Prop) : SignType

Restricted universal quantification ∀x(Cx/Bx) (11) is the universal quantifier (10) over the conditional assertions (Cx/Bx) (3), the A-form All crows are black read as a claim about each crow.

Equations

• Belnap1970.restrictedForall C B = Trivalent.forallHaug ({x : E | C x}.indicator fun (x : E) => SignType.ofProp (B x))

noncomputable def Belnap1970.restrictedExists {E : Type} (C B : E → Prop) : SignType

Restricted existential quantification ∃x(Cx/Bx) (12) is the existential quantifier (10) over the conditional assertions (Cx/Bx) (3).

Equations

• Belnap1970.restrictedExists C B = Trivalent.existsHaug ({x : E | C x}.indicator fun (x : E) => SignType.ofProp (B x))

Assertiveness and content

@[simp]

theorem Belnap1970.restrictedForall_eq_zero_iff {E : Type} {C B : E → Prop} : restrictedForall C B = 0 ↔ ∀ (x : E), ¬C x

∀x(Cx/Bx) is nonassertive exactly when nothing satisfies C. This is the existential presupposition of universals, which Strawson stipulated and Belnap derives.

@[simp]

theorem Belnap1970.restrictedForall_eq_one_iff {E : Type} {C B : E → Prop} : restrictedForall C B = 1 ↔ (∃ (x : E), C x) ∧ Quantifier.GQ.every C B

∀x(Cx/Bx) is true when something satisfies C and every such thing satisfies B.

@[simp]

theorem Belnap1970.restrictedForall_eq_neg_one_iff {E : Type} {C B : E → Prop} : restrictedForall C B = -1 ↔ ¬Quantifier.GQ.every C B

∀x(Cx/Bx) is false when something satisfying C fails B.

@[simp]

theorem Belnap1970.restrictedExists_eq_zero_iff {E : Type} {C B : E → Prop} : restrictedExists C B = 0 ↔ ∀ (x : E), ¬C x

∃x(Cx/Bx) is nonassertive exactly when nothing satisfies C.

@[simp]

theorem Belnap1970.restrictedExists_eq_one_iff {E : Type} {C B : E → Prop} : restrictedExists C B = 1 ↔ Quantifier.GQ.some C B

∃x(Cx/Bx) is true exactly when something satisfies both C and B, so what (12) asserts, when assertive, is exactly GQ.some.

@[simp]

theorem Belnap1970.restrictedExists_eq_neg_one_iff {E : Type} {C B : E → Prop} : restrictedExists C B = -1 ↔ (∃ (x : E), C x) ∧ ¬Quantifier.GQ.some C B

∃x(Cx/Bx) is false when something satisfies C and nothing satisfies both.

theorem Belnap1970.belnap_forall_content_eq_every {E : Type} {C B : E → Prop} (h : restrictedForall C B ≠ 0) : restrictedForall C B = 1 ↔ Quantifier.GQ.every C B

What (11) asserts, when assertive, is exactly every.

The square of opposition

noncomputable def Belnap1970.belnapSquare {E : Type} (C B : E → Prop) : Aristotelian.Square SignType

The four Aristotelian forms as restricted quantifications make up a square, since "semantic relations between these forms turn out ... to constitute what is pretty much a good old fashioned square of opposition" (p. 8).

Equations

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

theorem Belnap1970.square_equiassertive {E : Type} {C B : E → Prop} : ((belnapSquare C B).A = 0 ↔ (belnapSquare C B).E = 0) ∧ ((belnapSquare C B).A = 0 ↔ (belnapSquare C B).I = 0) ∧ ((belnapSquare C B).A = 0 ↔ (belnapSquare C B).O = 0)

All four forms share one assertiveness condition, ∃xCx, so the square's relations are as strong as possible, with equi-assertiveness on top of the content relations (p. 8).

def Belnap1970.contentSquare {E : Type} (C : E → Prop) : Aristotelian.Square ((E → Prop) → Prop)

Abstracting over the scope, the truth conditions of the four forms make up a square in the Boolean algebra (E → Prop) → Prop.

Equations

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

theorem Belnap1970.contentSquare_eq_square {E : Type} {C : E → Prop} (hC : ∃ (x : E), C x) : contentSquare C = Quantifier.GQ.square C

Where the forms are assertive, a form is true exactly when what it asserts is, and the content square is the square of every, no, some and not every at the restrictor C.

theorem Belnap1970.content_square_relations {E : Type} {C : E → Prop} (hR : ∃ (x : E), C x) : Aristotelian.SquareRelations (contentSquare C)

The content square satisfies SquareRelations when the restrictor is non-empty, which is Belnap's assertiveness condition, so the relations hold exactly where the forms are assertive.

Obversion, I-conversion, Barbara

theorem Belnap1970.obversion {E : Type} {C B : E → Prop} : (restrictedForall C fun (x : E) => ¬¬B x) = restrictedForall C B

Obversion is a strong equivalence (p. 8), since ∀x(Cx/¬¬Bx) and ∀x(Cx/Bx) are equi-assertive with identical content.

theorem Belnap1970.i_conversion_equitrue {E : Type} {C B : E → Prop} : restrictedExists C B = 1 ↔ restrictedExists B C = 1

I-conversion is equitrue, in that "truth is preserved in passing from one to the other" (p. 8), although "their propositional contents are unrelated".

theorem Belnap1970.i_conversion_not_equiassertive {E : Type} [Nonempty E] : ∃ (C : E → Prop) (B : E → Prop), restrictedExists C B ≠ 0 ∧ restrictedExists B C = 0

I-conversion is not equi-assertive, since "'Some unicorns are animals' is nonassertive while 'Some animals are unicorns' is just plain false" (p. 8). In any nonempty domain, a restrictor true of everything and one true of nothing separate the two conditions.

theorem Belnap1970.barbara_assertive {E : Type} (A C B : E → Prop) (hMinor : restrictedForall A C = 1) : restrictedForall C B ≠ 0 ∧ restrictedForall A B ≠ 0

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

theorem Belnap1970.barbara {E : Type} (A C B : E → Prop) (hMinor : restrictedForall A C = 1) : restrictedForall C B = 1 → restrictedForall A B = 1

When Barbara's minor is true her major implies her conclusion, and "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" (p. 9).

Contraposition and confirmation (§6)

theorem Belnap1970.contrapositive_different_assertiveness {E : Type} {C B : E → Prop} : (restrictedForall C B ≠ 0 ↔ ∃ (x : E), C x) ∧ ((restrictedForall (fun (x : E) => ¬B x) fun (x : E) => ¬C x) ≠ 0 ↔ ∃ (x : E), ¬B x)

The contrapositive ∀x(¬Bx/¬Cx) is assertive when there are nonblack things, and ∀x(Cx/Bx) when there are crows. Reports that something is not a crow support the contrapositive but are "evidentially irrelevant" to the original (p. 10), so the confirmation paradox dissolves because the two are not the same conditional assertion.