Brandom 1994: deontic scorekeeping

Brandom models assertion by deontic scorekeeping. Each interlocutor attributes commitments and entitlements to every interlocutor, and a claim's content is its role in committive inference, permissive inference and incompatibility, two claims being incompatible when commitment to one precludes entitlement to the other.

Represented by its incompatibles, a content is a concept of the incompatibility relation: the concept order is incompatibility entailment and a negation has the orthocomplement content. A scorecard records acknowledged commitments and prima facie entitlements, and the deontic statuses are its closure under a role. Read back off that scorekeeping, a role confers commitment entailment and preclusion. The role is coherent, so that entitlement passes along commitment entailment, exactly when the preclusion it confers is its own incompatibility.

Main definitions

• InferentialRole: committive inference, permissive inference and incompatibility.
• InferentialRole.content, InferentialRole.IsNegation: content and negation.
• Scorecard.Committed, Scorecard.Entitled: the deontic statuses a scorecard settles.
• InferentialRole.CommitmentEntails, InferentialRole.Precludes: the relations scorekeeping confers.
• Score, assert, challenge, defer, disavow: the scorekeeping moves.

Main statements

• Scorecard.Entitled.of_commitmentEntails: in a coherent role commitment entailment preserves entitlement.
• InferentialRole.coherent_iff_precludes_eq: coherence is incompatibility as scorekeeping confers it.
• InferentialRole.IsNegation.content_eq_compl: a negation's content is the orthocomplement.
• barn_entitled: entitlement to each of two incompatible claims, with commitment to neither.

Implementation notes

• Claims are an arbitrary type; InferentialRole.ofWorlds is a possible-worlds interpretation.
• Inferences have one premise; the auxiliary premises the book allows are not modelled.
• A scorecard stores outright attributions only, so a disavowal reinstates what it had defeated.

References

• [Bra94]
• [Bra83]

Inferential roles

structure Brandom1994.InferentialRole (P : Type u_2) : Type u_2

The broadly inferential role of claims consists of committive inference, permissive inference and incompatibility (pp. 168–169, 188). Incompatibility is assumed symmetric throughout (p. 674 n. 39).

• committive : P → P → Prop

  Commitment to the premise is commitment to the conclusion.

• permissive : P → P → Prop

  Entitlement to the premise entitles one to the conclusion unless an incompatible commitment defeats it.

• incompatible : P → P → Prop

  Commitment to the first claim precludes entitlement to the second.

• incompatible_symm : Std.Symm self.incompatible

  Incompatibility is mutual.

instance Brandom1994.InferentialRole.instSymmIncompatible {P : Type u_1} (R : InferentialRole P) : Std.Symm R.incompatible

@[reducible, inline]

abbrev Brandom1994.InferentialRole.content {P : Type u_1} (R : InferentialRole P) (p : P) : Concept P P R.incompatible

The content of a claim, represented by the claims incompatible with it (p. 160), is the concept of the incompatibility relation that the claim generates.

Equations

• R.content p = Concept.ofObject R.incompatible p

theorem Brandom1994.InferentialRole.content_le_iff {P : Type u_1} (R : InferentialRole P) {p : P} {c : Concept P P R.incompatible} : R.content p ≤ c ↔ p ∈ c

The content of p is the least concept containing p.

theorem Brandom1994.InferentialRole.mem_content_self {P : Type u_1} (R : InferentialRole P) (p : P) : p ∈ R.content p

theorem Brandom1994.InferentialRole.mem_content_iff {P : Type u_1} (R : InferentialRole P) {p q : P} : q ∈ R.content p ↔ ∀ ⦃r : P⦄, R.incompatible p r → R.incompatible q r

A claim is in the content of p when it incompatibility-entails p, that is, when everything incompatible with p is incompatible with it (p. 160).

theorem Brandom1994.InferentialRole.mem_compl_content_iff {P : Type u_1} (R : InferentialRole P) {p q : P} : q ∈ (R.content p)ᶜ ↔ R.incompatible p q

def Brandom1994.InferentialRole.Coherent {P : Type u_1} (R : InferentialRole P) : Prop

A role is coherent when committive inference is incompatibility entailment, so that if p commitment-entails q, anything incompatible with q is incompatible with p (p. 673 n. 27).

Equations

• R.Coherent = ∀ ⦃p q : P⦄, R.committive p q → R.content p ≤ R.content q

theorem Brandom1994.InferentialRole.Coherent.incompatible {P : Type u_1} {R : InferentialRole P} {p q r : P} (hR : R.Coherent) (hpq : R.committive p q) (hqr : R.incompatible q r) : R.incompatible p r

theorem Brandom1994.InferentialRole.Coherent.content_le {P : Type u_1} {R : InferentialRole P} {p q : P} (hR : R.Coherent) (h : Relation.ReflTransGen R.committive p q) : R.content p ≤ R.content q

def Brandom1994.InferentialRole.IsNegation {P : Type u_1} (R : InferentialRole P) (p n : P) : Prop

A negation of p is a minimal incompatible of p, a claim incompatible with p that everything incompatible with p commitment-entails (p. 673 n. 23).

Equations

• R.IsNegation p n = (R.incompatible p n ∧ ∀ ⦃r : P⦄, R.incompatible p r → Relation.ReflTransGen R.committive r n)

theorem Brandom1994.InferentialRole.IsNegation.content_eq_compl {P : Type u_1} {R : InferentialRole P} {p n : P} (hR : R.Coherent) (h : R.IsNegation p n) : R.content n = (R.content p)ᶜ

In a coherent role a negation has the orthocomplement of the claim's content.

theorem Brandom1994.InferentialRole.IsNegation.incompatible_iff {P : Type u_1} {R : InferentialRole P} {p r n : P} (hR : R.Coherent) (h : R.IsNegation p n) : R.incompatible p r ↔ R.content r ≤ R.content n

To be incompatible with a claim is to incompatibility-entail its negation.

theorem Brandom1994.InferentialRole.IsNegation.content_eq {P : Type u_1} {R : InferentialRole P} {p n : P} (hR : R.Coherent) {n' : P} (h : R.IsNegation p n) (h' : R.IsNegation p n') : R.content n = R.content n'

Negations of a claim agree in content, so a claim's negation is unique up to inferential equivalence.

Possible-worlds roles

def Brandom1994.InferentialRole.ofWorlds {P : Type u_1} {W : Type u_2} (ι : P → Set W) : InferentialRole P

A possible-worlds interpretation makes committive inference the inclusion of truth sets and incompatibility their disjointness (p. 169). Truth conditions alone license no merely permissive inference.

Equations

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

theorem Brandom1994.InferentialRole.coherent_ofWorlds {P : Type u_1} {W : Type u_2} (ι : P → Set W) : (ofWorlds ι).Coherent

theorem Brandom1994.InferentialRole.content_le_content_ofWorlds_id_iff {W : Type u_2} {p q : Set W} : (ofWorlds id).content p ≤ (ofWorlds id).content q ↔ p ⊆ q

On sets of worlds, incompatibility entailment is inclusion.

theorem Brandom1994.InferentialRole.isNegation_ofWorlds_id_compl {W : Type u_2} (p : Set W) : (ofWorlds id).IsNegation p pᶜ

On sets of worlds, the complement is the negation.

Scorecards

structure Brandom1994.Scorecard (P : Type u_2) : Type u_2

A scorecard records what one scorekeeper attributes to one interlocutor outright (pp. 190–191).

• acknowledged : Set P

  The commitments the interlocutor has acknowledged by avowing them.

• primaFacie : Set P

  The claims the interlocutor is entitled to without inference, by default or by deferral.

def Brandom1994.Scorecard.Committed {P : Type u_1} (R : InferentialRole P) (c : Scorecard P) (q : P) : Prop

An interlocutor is committed to whatever follows by committive inference from an acknowledged commitment, whether or not they acknowledge it (p. 194).

Equations

• Brandom1994.Scorecard.Committed R c q = ∃ p ∈ c.acknowledged, Relation.ReflTransGen R.committive p q

def Brandom1994.Scorecard.Precluded {P : Type u_1} (R : InferentialRole P) (c : Scorecard P) (q : P) : Prop

Entitlement to q is precluded by a commitment to something incompatible with it.

Equations

• Brandom1994.Scorecard.Precluded R c q = ∃ (r : P), Brandom1994.Scorecard.Committed R c r ∧ R.incompatible r q

inductive Brandom1994.Scorecard.Entitled {P : Type u_1} (R : InferentialRole P) (c : Scorecard P) : P → Prop

Entitlement is the closure the scorekeeping procedure prescribes (p. 191, p. 675 n. 44). It holds of the prima facie entitlements, their committive consequences, and the permissive consequences of entitled commitments, each unless precluded.

• primaFacie {P : Type u_1} {R : InferentialRole P} {c : Scorecard P} {p : P} : p ∈ c.primaFacie → ¬Precluded R c p → Entitled R c p
• committive {P : Type u_1} {R : InferentialRole P} {c : Scorecard P} {p q : P} : Entitled R c p → R.committive p q → ¬Precluded R c q → Entitled R c q
• permissive {P : Type u_1} {R : InferentialRole P} {c : Scorecard P} {p q : P} : Entitled R c p → Committed R c p → R.permissive p q → ¬Precluded R c q → Entitled R c q

def Brandom1994.Scorecard.avow {P : Type u_1} (c : Scorecard P) (p : P) : Scorecard P

Avowing p acknowledges the commitment and, by default, the entitlement (p. 177).

Equations

• c.avow p = { acknowledged := insert p c.acknowledged, primaFacie := insert p c.primaFacie }

theorem Brandom1994.Scorecard.committed_of_mem {P : Type u_1} {R : InferentialRole P} {c : Scorecard P} {p : P} (h : p ∈ c.acknowledged) : Committed R c p

theorem Brandom1994.Scorecard.Committed.of_committive {P : Type u_1} {R : InferentialRole P} {c : Scorecard P} {p q : P} (h : Committed R c p) (hpq : R.committive p q) : Committed R c q

Committive inference preserves commitment (p. 186).

theorem Brandom1994.Scorecard.Entitled.not_precluded {P : Type u_1} {R : InferentialRole P} {c : Scorecard P} {p : P} (h : Entitled R c p) : ¬Precluded R c p

theorem Brandom1994.Scorecard.not_entitled_of_incompatible {P : Type u_1} {R : InferentialRole P} {c : Scorecard P} {p r : P} (hr : Committed R c r) (h : R.incompatible r p) : ¬Entitled R c p

Commitment to one of two incompatible claims precludes entitlement to the other (p. 160).

theorem Brandom1994.Scorecard.Entitled.of_committive {P : Type u_1} {R : InferentialRole P} {c : Scorecard P} {p q : P} (hR : R.Coherent) (h : Entitled R c p) (hpq : R.committive p q) : Entitled R c q

In a coherent role committive inference preserves entitlement, since whatever precludes the conclusion precludes the premise (p. 673 n. 27, p. 674 n. 43).

theorem Brandom1994.Scorecard.Entitled.exists_primaFacie {P : Type u_1} {R : InferentialRole P} {c : Scorecard P} {p : P} (h : Entitled R c p) : ∃ q ∈ c.primaFacie, Relation.ReflTransGen (R.committive ⊔ R.permissive) q p

Inference spreads entitlement but does not originate it (p. 176), so every entitlement descends along committive and permissive inference from a prima facie one.

theorem Brandom1994.Scorecard.not_entitled_of_primaFacie_eq_empty {P : Type u_1} {R : InferentialRole P} {c : Scorecard P} {p : P} (h : c.primaFacie = ∅) : ¬Entitled R c p

theorem Brandom1994.Scorecard.entitled_avow_iff {P : Type u_1} {R : InferentialRole P} {c : Scorecard P} {p : P} : Entitled R (c.avow p) p ↔ ¬Precluded R (c.avow p) p

An avowal is attributed entitlement by default, unless an incompatible commitment defeats it (p. 177).

Conferral

def Brandom1994.InferentialRole.CommitmentEntails {P : Type u_1} (R : InferentialRole P) (p q : P) : Prop

Scorekeeping by R treats the inference from p to q as good, so that p commitment-entails q, when every scorecard committed to p is committed to q (p. 186).

Equations

• R.CommitmentEntails p q = ∀ (c : Brandom1994.Scorecard P), Brandom1994.Scorecard.Committed R c p → Brandom1994.Scorecard.Committed R c q

def Brandom1994.InferentialRole.Precludes {P : Type u_1} (R : InferentialRole P) (p q : P) : Prop

Scorekeeping by R treats commitment to p as precluding entitlement to q when every scorecard committed to p withholds entitlement to q (p. 186).

Equations

• R.Precludes p q = ∀ (c : Brandom1994.Scorecard P), Brandom1994.Scorecard.Committed R c p → ¬Brandom1994.Scorecard.Entitled R c q

theorem Brandom1994.InferentialRole.commitmentEntails_eq {P : Type u_1} (R : InferentialRole P) : R.CommitmentEntails = Relation.ReflTransGen R.committive

theorem Brandom1994.InferentialRole.precludes_eq {P : Type u_1} (R : InferentialRole P) : R.Precludes = Relation.Comp (Relation.ReflTransGen R.committive) R.incompatible

theorem Brandom1994.InferentialRole.coherent_iff_precludes_eq {P : Type u_1} (R : InferentialRole P) : R.Coherent ↔ R.Precludes = R.incompatible

A role is coherent exactly when its incompatibility is the one its own scorekeeping confers.

theorem Brandom1994.InferentialRole.Precludes.of_commitmentEntails {P : Type u_1} {R : InferentialRole P} {p q r : P} (hpq : R.CommitmentEntails p q) (hqr : R.Precludes q r) : R.Precludes p r

The relations scorekeeping confers are coherent, since whatever a commitment-consequence precludes, its premise precludes (p. 673 n. 27).

theorem Brandom1994.Scorecard.Entitled.of_commitmentEntails {P : Type u_1} {R : InferentialRole P} {c : Scorecard P} {p q : P} (hR : R.Coherent) (h : Entitled R c p) (hpq : R.CommitmentEntails p q) : Entitled R c q

In a coherent role entitlement is inherited by whatever a claim commitment-entails (p. 674 n. 43).

The barn

inductive Brandom1994.Barn : Type

The claims of the barn example (p. 675 n. 44).

• smoke : Barn
• rain : Barn
• fire : Barn
• noFire : Barn

def Brandom1994.barnRole : InferentialRole Barn

Smoke is inductive evidence of fire and rain of no fire; fire and no fire are incompatible.

Equations

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

def Brandom1994.barnCard : Scorecard Barn

Having observed smoke and rain, one acknowledges both, by default entitled.

Equations

• Brandom1994.barnCard = { acknowledged := {Brandom1994.Barn.smoke, Brandom1994.Barn.rain}, primaFacie := {Brandom1994.Barn.smoke, Brandom1994.Barn.rain} }

theorem Brandom1994.barn_entitled : Scorecard.Entitled barnRole barnCard Barn.fire ∧ Scorecard.Entitled barnRole barnCard Barn.noFire ∧ ¬Scorecard.Committed barnRole barnCard Barn.fire ∧ ¬Scorecard.Committed barnRole barnCard Barn.noFire ∧ ¬Scorecard.Entitled barnRole (barnCard.avow Barn.fire) Barn.noFire

One may be entitled to each of two incompatible claims while committed to neither (p. 675 n. 44); committing to one of them defeats entitlement to the other.

theorem Brandom1994.exists_entitled_committive_not_entitled : ∃ (R : InferentialRole Bool) (c : Scorecard Bool), Scorecard.Entitled R c true ∧ R.committive true false ∧ ¬Scorecard.Entitled R c false

Coherence cannot be dropped from Scorecard.Entitled.of_committive. Here true commits one to false, and the commitment to false precludes entitlement to it without precluding true.

Scorekeeping

@[reducible, inline]

abbrev Brandom1994.Score (I : Type u_2) (P : Type u_3) : Type (max u_2 u_3)

A score holds the scorecard s k i that each scorekeeper k keeps on each interlocutor i, so scorekeeping is doubly perspectival (p. 185).

Equations

• Brandom1994.Score I P = (I → I → Brandom1994.Scorecard P)

def Brandom1994.assert {P : Type u_1} {I : Type u_2} [DecidableEq I] (s : Score I P) (b : I) (p : P) : Score I P

When b asserts p, every scorekeeper attributes to b the commitment and, by default, entitlement to it (pp. 177, 186).

Equations

• Brandom1994.assert s b p k = Function.update (s k) b ((s k b).avow p)

def Brandom1994.challenge {P : Type u_1} {I : Type u_2} [DecidableEq I] (R : InferentialRole P) (s : Score I P) (a : I) (q : P) (b : I) (p : P) : Score I P

When a's claim q challenges b's claim p, a scorekeeper who takes a to be entitled to q withholds default entitlement to p from b and leaves the commitment standing (p. 193).

Equations

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

def Brandom1994.defer {P : Type u_1} {I : Type u_2} [DecidableEq I] (R : InferentialRole P) (s : Score I P) (a b : I) (p : P) : Score I P

When a defers to b concerning p, a acknowledges p, and a scorekeeper who takes b to be entitled to p takes a to inherit the entitlement by testimony (pp. 175, 192).

Equations

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

def Brandom1994.disavow {P : Type u_1} {I : Type u_2} [DecidableEq I] (s : Score I P) (b : I) (p : P) : Score I P

When b disavows p, scorekeepers cease to attribute to b the acknowledged commitment (p. 192).

Equations

• Brandom1994.disavow s b p k = Function.update (s k) b { acknowledged := (s k b).acknowledged \ {p}, primaFacie := (s k b).primaFacie }

@[simp]

theorem Brandom1994.assert_self {P : Type u_1} {I : Type u_2} [DecidableEq I] (s : Score I P) {b k : I} {p : P} : assert s b p k b = (s k b).avow p

@[simp]

theorem Brandom1994.acknowledged_challenge {P : Type u_1} {I : Type u_2} [DecidableEq I] (R : InferentialRole P) (s : Score I P) {a b k : I} {p q : P} (i : I) : (challenge R s a q b p k i).acknowledged = (s k i).acknowledged

A challenge leaves every commitment standing.

theorem Brandom1994.challenge_committed_not_entitled {P : Type u_1} {I : Type u_2} [DecidableEq I] (R : InferentialRole P) (s : Score I P) {a b k : I} {p q : P} (hb : (s k b).primaFacie = ∅) {q' : P} (ha : Scorecard.Entitled R (assert s b p k a) q) : Scorecard.Committed R (challenge R (assert s b p) a q b p k b) p ∧ ¬Scorecard.Entitled R (challenge R (assert s b p) a q b p k b) q'

A challenged assertion with no other support is a commitment without entitlement (pp. 177–178). Once a scorekeeper takes the challenger to be entitled to the challenge, it attributes to the asserter the commitment and no entitlement at all.

theorem Brandom1994.entitled_defer {P : Type u_1} {I : Type u_2} [DecidableEq I] (R : InferentialRole P) (s : Score I P) {a b k : I} {p : P} (hb : Scorecard.Entitled R (s k b) p) (hp : ¬Scorecard.Precluded R (defer R s a b p k a) p) : Scorecard.Entitled R (defer R s a b p k a) p

Deferral passes on the entitlement the scorekeeper attributes to the source (p. 175).

theorem Brandom1994.not_entitled_defer {P : Type u_1} {I : Type u_2} [DecidableEq I] (R : InferentialRole P) (s : Score I P) {a b k : I} {p q : P} (hb : ¬Scorecard.Entitled R (s k b) p) (ha : (s k a).primaFacie = ∅) : ¬Scorecard.Entitled R (defer R s a b p k a) q

Deferral to a source the scorekeeper takes to be unentitled confers no entitlement, since others cannot inherit an entitlement the asserter does not possess (p. 171).

theorem Brandom1994.committed_disavow {P : Type u_1} {I : Type u_2} [DecidableEq I] (R : InferentialRole P) (s : Score I P) {b k : I} {p q r : P} (hq : q ∈ (s k b).acknowledged) (hqp : q ≠ p) (h : Relation.ReflTransGen R.committive q r) : Scorecard.Committed R (disavow s b p k b) r

A disavowal of p fails while a premise committing b to p stays acknowledged (pp. 192–193).