Cariani, Santorio and Wellwood (2024): Confidence Reports

Cariani, Santorio and Wellwood give adjectival confident and nominal confidence one denotation, a property of confidence states. Each state carries a proposition as its theme, and a background ordering ranks a holder's states. σ is confident that p says that some state of σ's with theme p lies at or above a contrast state, and certain is the same ordering with the contrast state at the top. The comparative instead compares degrees, assigned by a measure that preserves the strict ordering. This is the two-component analysis of Semantics/Degree/Background.lean, and the file sorts the paper's inferences by whether they use the ordering or the degree scale.

Main statements

• exists_conjunctionFallacy, image_Ici_ne_ge_over: confidence in a conjunction without confidence in its conjunct is consistent with the semantics, and with no threshold on a probability measure.
• image_Ici_subset_image_Ici_iff_isMax: confident entails certain exactly when its contrast state is maximal.
• not_maxComparative_of_isMax: nothing is more confident than a certainty, when the measure also respects ties.

Implementation notes

• A holder's confidence states form a type S with its background preorder, and θ : S → Set W assigns themes; the states of all holders are the disjoint sum Σ a, S a.
• The positive form is p ∈ θ '' Set.Ici c for a contrast state c, certain is p ∈ θ '' {s | IsMax s}, and the comparative is Degree.MaxComparative .gt (θ · = p) (θ · = q) μ for StrictMono μ.
• Totality of the ordering is a hypothesis of the theorems that use it.
• The paper states no semantics for doubt, so (63c) is not formalized.

TODO

• The conditional (59) under a contrast that maps a proposition to its negation, and the two objections to it, (60) and fn. 31. With the weak positive form (40) the entailment needs the p-state strictly above the ¬p-state, since a tie satisfies (59a) and refutes (59b); the paper's gloss ("ranked higher") reads the contrast strictly.
• Conditional confidence (61), (62), with the ordering indexed by an information state.

References

• [CSW24]
• [CSW23]
• [Wel15]
• [TK83]
• [Las17a]

The comparative and the positive form

theorem CarianiSantorioWellwood2024.maxComparative_theme_iff {S : Type u_1} {W : Type u_2} {D : Type u_3} [Preorder D] {θ : S → Set W} {μ : S → D} (hθ : Function.Injective θ) (s t : S) : Degree.MaxComparative Degree.Comparison.gt (fun (x : S) => θ x = θ s) (fun (x : S) => θ x = θ t) μ ↔ μ t < μ s

With one state per theme, the comparative (47) compares the two states' measures, so σ's confidence that p exceeds the than-clause degree (37).

The conjunction fallacy (52)

theorem CarianiSantorioWellwood2024.exists_conjunctionFallacy {W : Type u_2} {φ ψ : Set W} (h : ¬φ ⊆ ψ) : ∃ (θ : Bool → Set W), φ ∩ ψ ∈ θ '' Set.Ici true ∧ φ ∉ θ '' Set.Ici true

(52a) John is not confident that Linda is a bankteller and (52b) John is confident that Linda is a feminist bankteller are true together. Whenever φ ∩ ψ differs from φ, a two-state total ordering with the φ ∩ ψ-state above the φ-state and the contrast state at the top makes the holder confident of the conjunction but not of the conjunct.

theorem CarianiSantorioWellwood2024.image_Ici_ne_ge_over {S : Type u_1} {W : Type u_2} [Preorder S] {θ : S → Set W} [MeasurableSpace W] (P : MeasureTheory.Measure W) (t : ENNReal) {c : S} {φ ψ : Set W} (h₁ : φ ∩ ψ ∈ θ '' Set.Ici c) (h₂ : φ ∉ θ '' Set.Ici c) : θ '' Set.Ici c ≠ ⇑P ⁻¹' Set.Ici t

A holder confident of a conjunction but not of its conjunct is confident of no set of propositions that the threshold account of §2 (7) delivers. Whatever the threshold, the propositions whose probability meets it are closed under conjunction elimination, since a measure is monotone.

Certain and confident (§5.2)

theorem CarianiSantorioWellwood2024.image_Ici_subset_image_Ici_of_isMax {S : Type u_1} {W : Type u_2} [Preorder S] {θ : S → Set W} [Std.Total fun (x1 x2 : S) => x1 ≤ x2] {m : S} (hm : IsMax m) (c : S) : θ '' Set.Ici m ⊆ θ '' Set.Ici c

Certain entails confident (65b), (66b). The paper's reason is that certain picks out a smaller segment of the ordering than confident, which is Ici_subset_Ici once confident's contrast state lies below certain's; on a total ordering that holds of every contrast state once certain's is maximal.

theorem CarianiSantorioWellwood2024.not_image_Ici_subset_image_Ici {S : Type u_1} {W : Type u_2} [Preorder S] {θ : S → Set W} (hθ : Function.Injective θ) {c m : S} (hmc : ¬m ≤ c) : ¬θ '' Set.Ici c ⊆ θ '' Set.Ici m

The entailment is asymmetric (65a), (66a). When confident's contrast state c is not above certain's m, the holder is confident but not certain of c's theme.

theorem CarianiSantorioWellwood2024.image_Ici_subset_image_Ici_iff_isMax {S : Type u_1} {W : Type u_2} [Preorder S] {θ : S → Set W} [Std.Total fun (x1 x2 : S) => x1 ≤ x2] (hθ : Function.Injective θ) {m : S} (hm : IsMax m) {c : S} : θ '' Set.Ici c ⊆ θ '' Set.Ici m ↔ IsMax c

Confident entails certain exactly when its contrast state is itself maximal, so (65a) is consistent only on a contrast state below the top. Confident measures on an ordering with maximal elements (69) without taking them as its standard.

theorem CarianiSantorioWellwood2024.Ici_eq_setOf_isMax {S : Type u_1} [Preorder S] [Std.Total fun (x1 x2 : S) => x1 ≤ x2] {m : S} (hm : IsMax m) : Set.Ici m = {s : S | IsMax s}

On a total ordering the region above a maximal contrast state (71) is the set of maximal states, what certain denotes in Figure 3.

theorem CarianiSantorioWellwood2024.not_maxComparative_of_isMax {S : Type u_1} {W : Type u_2} {D : Type u_3} [Preorder S] [Preorder D] {θ : S → Set W} {μ : S → D} [Std.Total fun (x1 x2 : S) => x1 ≤ x2] (hμ : Monotone μ) {s : S} (hs : IsMax s) {p q : Set W} (hsp : θ s = p) : ¬Degree.MaxComparative Degree.Comparison.gt (fun (x : S) => θ x = q) (fun (x : S) => θ x = p) μ

Nothing is more confident than a certainty (68). If σ is certain that p, σ is not more confident of any q than of p. Admissibility (21) is not enough, since it leaves tied maximal states free to be measured apart; the measure must also be monotone.

theorem CarianiSantorioWellwood2024.maxComparative_of_isMax {S : Type u_1} {W : Type u_2} {D : Type u_3} [Preorder S] [Preorder D] {θ : S → Set W} {μ : S → D} (hθ : Function.Injective θ) {s t : S} (hs : IsMax s) (hlt : μ s < μ t) : θ s ∈ θ '' {s : S | IsMax s} ∧ Degree.MaxComparative Degree.Comparison.gt (fun (x : S) => θ x = θ t) (fun (x : S) => θ x = θ s) μ

Under admissibility alone (68) fails, since a maximal state measured below another state makes σ certain of its theme and more confident of the other's.