Confidence and certainty as gradable attitudes

Gradable attitude adjectives like confident, certain, sure, and doubtful denote properties of confidence states, following Cariani, Santorio & Wellwood ([CSW24]; henceforth CSW). Unlike accessibility-based attitudes (Doxastic.lean: believe, know) and preference-based attitudes (Preference.lean: hope, fear), these are gradable properties of states with propositional themes — a third kind of attitude semantics.

Core Structure

A confidence state has a holder (the attitude bearer) and a theme (the proposition the holder is confident about). Confidence states for a given holder are ordered by a ConfidenceOrdering, which extends Preorder (ConfidenceState E W) with a holder field.

Key features:

• Per-holder ordering: Ann's confidence ordering differs from Bob's (CSW §4.1). CSW's ordering is domain-restricted to the holder's own states; on the total-type preorder this is rendered by holder_consistent — distinct comparable states belong to the holder, foreign states sit as isolated reflexive points.
• Not per-theme: the ordering ranks states across themes, not within one theme
• Not probabilistic: the ordering need not respect conjunction — there is no conjunction-monotonicity axiom; the divergence witness is CarianiSantorioWellwood2024.conjunction_fallacy_predicted (CSW (52))
• Bounded above (for ordinary holders): certain picks out the maximal elements (CSW §5.2). The maximality assumption is supplied per-theorem via h_top, not baked into the structure — CSW p.19 hedges with "for ordinary individuals."

Logic of Confidence (CSW §4.6)

The ordering validates:

• Transitivity of comparative confidence (CSW (54))
• Antisymmetry of equative confidence (CSW (55))
• Upward monotonicity: confident(p) ∧ more_confident(q, p) → confident(q) (CSW (53))

It does NOT validate:

• Probabilistic conjunction: confident(p ∧ q) → confident(p) (CSW (52))
• Connectedness (CSW are agnostic, §4.6 discussion of (58))

Confidence states

structure Confidence.ConfidenceState (E : Type u_1) (W : Type u_2) : Type (max u_1 u_2)

A confidence state: a state with a holder and a propositional theme.

CSW §4.1: "there are three states of confidence such that Mary is the holder of all three. These states have as themes, respectively, the propositions that it's snowing, that Regina is in Saskatchewan, and that Brazil will win the World Cup."

Every ordinary person is the holder of a large number of confidence states. The holder field is the Neodavidsonian HOLDER role (ThematicRoles.lean); the theme is the propositional THEME.

• holder : E

  The attitude bearer

• theme : W → Prop

  The proposition the holder is confident about

Holder-relativized confidence ordering

structure Confidence.ConfidenceOrdering (E : Type u_1) (W : Type u_2) extends Preorder (Confidence.ConfidenceState E W) : Type (max u_1 u_2)

A holder-relativized confidence ordering (CSW §4.1).

Extends mathlib's Preorder with a holder field and a consistency constraint that distinct comparable states belong to that holder — the total-type rendering of CSW's domain-restricted ⟨D^ho, ≿⟩, with other holders' states as isolated reflexive points. (Reflexivity forces le s s for every state, so constraining all related pairs would make the structure uninhabited as soon as two holders exist.) The preorder is at least reflexive and transitive; CSW §4.6 are explicitly agnostic about connectedness (totality), which is why Preorder (not LinearOrder or PartialOrder) is the right base — it permits CSW's discussion of (58) where some propositions are incomparable.

Each holder has their own ordering: orderings vary from holder to holder but NOT from theme to theme (CSW p.19).

• le : Confidence.ConfidenceState E W → Confidence.ConfidenceState E W → Prop
• lt : Confidence.ConfidenceState E W → Confidence.ConfidenceState E W → Prop
• le_refl (a : Confidence.ConfidenceState E W) : a ≤ a
• le_trans (a b c : Confidence.ConfidenceState E W) : a ≤ b → b ≤ c → a ≤ c
• lt_iff_le_not_ge (a b : Confidence.ConfidenceState E W) : a < b ↔ a ≤ b ∧ ¬b ≤ a
• holder : E

  The attitude bearer whose ordering this is

• holder_consistent (s₁ s₂ : ConfidenceState E W) : s₁ ≤ s₂ → s₁ ≠ s₂ → s₁.holder = self.holder ∧ s₂.holder = self.holder

  Distinct comparable states belong to this holder

Confident, certain, and doubts as contrast points

confident, certain, and doubts share a ConfidenceOrdering and differ only in a contrast point on it (CSW Figures 2–3: same background ordering, different cut-offs). The lexical entries are POS-free (CSW §3.3): the positive form is co.le contrastPt s directly on the preorder — no covert pos morpheme, no degree, and (post substrate dissolution) no entry struct: a CSW lexical entry IS its contrast point. certain's point is maximal for ordinary holders (CSW §5.2, hedged per-theorem via h_top); doubts is negative-polarity, holding of states below its point.

theorem Confidence.certain_entails_confident {E : Type u_1} {W : Type u_2} (co : ConfidenceOrdering E W) (confPt maxPt : ConfidenceState E W) (h_top : ∀ (s : ConfidenceState E W), s ≤ maxPt) (s : ConfidenceState E W) (h_certain : maxPt ≤ s) : confPt ≤ s

certain entails confident (CSW (65)/(66)).

Given that maxPt is the top of the ordering (CSW's "ordinary holder" assumption), the certainty contrast point dominates any confidence contrast point, so every state in the certainty region is also in the confidence region.

theorem Confidence.confident_not_entails_certain {E : Type u_1} {W : Type u_2} (co : ConfidenceOrdering E W) (confPt maxPt : ConfidenceState E W) (h_strict : ¬maxPt ≤ confPt) : ∃ (s : ConfidenceState E W), confPt ≤ s ∧ ¬maxPt ≤ s

The entailment is asymmetric (CSW (65b)/(66b)): confidence does NOT entail certainty whenever the ordering admits a state strictly above the confidence contrast point that is not in the certainty region.

Concretely: if confPt sits strictly below the certainty point (¬co.le maxPt confPt), the state confPt itself witnesses confidence without certainty.

Logic of confidence reports

theorem Confidence.comparative_transitive {E : Type u_1} {W : Type u_2} {D : Type u_3} [LinearOrder D] (μ : ConfidenceState E W → D) (s_p s_q s_r : ConfidenceState E W) (h_pq : μ s_q < μ s_p) (h_qr : μ s_r < μ s_q) : μ s_r < μ s_p

Comparative confidence is transitive (CSW (54)/(57)): "more confident of p than q" ∧ "more confident of q than r" → "more confident of p than r".

This is lt_trans on the linearly-ordered measure type. The ConfidenceOrdering doesn't enter the proof, but the named lemma documents that this is the prediction CSW make for confidence comparatives. CSW (57) is contradictory because asserting the negation of (54)'s consequent contradicts this generic fact.

theorem Confidence.comparative_antisymmetric {E : Type u_1} {W : Type u_2} {D : Type u_3} [LinearOrder D] (μ : ConfidenceState E W → D) (s_p s_q : ConfidenceState E W) (h₁ : μ s_q ≤ μ s_p) (h₂ : μ s_p ≤ μ s_q) : μ s_p = μ s_q

Comparative confidence is antisymmetric (CSW (55)): "at least as confident of p as q" ∧ "at least as confident of q as p" → "equally confident of p and q".

theorem Confidence.confidence_upward_monotone {E : Type u_1} {W : Type u_2} (co : ConfidenceOrdering E W) (contrastPt s_p s_q : ConfidenceState E W) (h_conf : contrastPt ≤ s_p) (h_more : s_p ≤ s_q) : contrastPt ≤ s_q

Upward monotonicity of the positive form (CSW (53)): "σ is confident that p" ∧ "σ is more confident of q than of p" → "σ is confident that q".

If s_p is in the positive region and s_q is ranked at least as high as s_p in the confidence ordering, then s_q is also in the positive region — by transitivity through the contrast point.

theorem Confidence.confident_excludes_doubts {E : Type u_1} {W : Type u_2} (co : ConfidenceOrdering E W) (confPt doubtPt : ConfidenceState E W) (h_strict : ¬confPt ≤ doubtPt) (s : ConfidenceState E W) : ¬(confPt ≤ s ∧ s ≤ doubtPt)

CSW (63a)/(63c): confident and doubts are mutually exclusive.

No confidence state is simultaneously in the confidence region (above the confidence contrast point) and the doubt region (below the doubt contrast point), provided the doubt contrast point is strictly below the confidence contrast point. This is the substantive content of CSW's claim that "Ann doubts that the dress is blue" is inconsistent with "Ann is confident / has confidence that the dress is blue".

Combined with certain_entails_confident, this gives CSW's full inferential triangle: certain(p) → confident(p), confident(p) ⊥ doubts(p), so certain(p) ⊥ doubts(p).

Conjunction-fallacy compatibility (CSW (52))

Confidence orderings need not respect logical conjunction: it is consistent to be confident that (p ∧ q) without being confident that p (CSW (52), [TK83]). In this substrate that is not a theorem but the absence of a constraint — the background Preorder carries no conjunction-monotonicity axiom, unlike a probability measure.

The genuine witness that this diverges from a probabilistic account — a non-monotone credence ranking a consistent conjunction above a conjunct, which no probability measure can do — is CarianiSantorioWellwood2024.conjunction_fallacy_predicted; the packaged cross-framework refutation is CarianiSantorioWellwood2024.states_vs_threshold_on_conjunction_fallacy. (Earlier a vacuous conjunction_fallacy_compatible : ∃ a b c : ℕ, a ≤ b ∧ ¬ a ≤ c stood here; it encoded nothing about confidence or conjunction and was removed.)

Bridge to Neo-Davidsonian event semantics

CSW (44) and (47) are the compositional logical forms for positive and comparative confidence reports respectively. The substrate exposes both via confidenceLogicalForm (presupposition-flattened) and comparativeConfidenceLogicalForm (under unique-state simplification — CSW fn. 25 explicitly reject this, but it is convenient as a working form; the faithful max-quantified (47) is confidenceComparative below, via Degree.maxComparative, with the unique-state collapse provided by Degree.maxComparative_unique).

def Confidence.confidenceLogicalForm {E : Type u_1} {W : Type u_2} (co : ConfidenceOrdering E W) (contrastPt : ConfidenceState E W) (holder : E) (p : W → Prop) : Prop

Truth-conditional content of CSW (44) (presupposition flattened).

CSW (44) restricts the existential to states in Dom(⟨D^ho(s)_conf, ≿⟩); the substrate version drops the domain restriction and lets membership in ConfidenceState E W stand in for it. For the substrate's truth-conditional purposes this is sufficient; for presupposition bookkeeping a separate domain-restricted variant would be needed.

Equations

• Confidence.confidenceLogicalForm co contrastPt holder p = ∃ (s : Confidence.ConfidenceState E W), s.holder = holder ∧ contrastPt ≤ s ∧ s.theme = p

def Confidence.comparativeConfidenceLogicalForm {E : Type u_1} {W : Type u_2} (co : ConfidenceOrdering E W) {D : Type u_3} [LinearOrder D] (μ : ConfidenceState E W → D) (holder : E) (p q : W → Prop) : Prop

Schematic comparative content under the unique-state simplification.

The actual CSW (47) abstracts a max(λd. ...) over the than-clause; this version requires only that some q-themed state has a strictly smaller measure than the p-themed state. CSW fn. 25 explicitly reject the unique-state assumption ("This is not the picture we adopt"), but the simplification is useful for theorem statements that don't need the full max-quantification. The faithful maximality version is confidenceComparative below; this is its unique-state reduction.

Equations

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

Faithful comparative (CSW (47)) and the admissibility spine

def Confidence.confidenceComparative {E : Type u_1} {W : Type u_2} {D : Type u_3} [Preorder D] (μ : ConfidenceState E W → D) (holder : E) (p q : W → Prop) : Prop

Comparative confidence (CSW (47)): "A is more confident that p than that q" — Degree.maxComparative with the holder/theme predicates as the matrix (p) and than-clause (q) restrictions. The max-quantified than-clause does not assume a unique state per theme (CSW fn 25), unlike comparativeConfidenceLogicalForm, which is its unique-state reduction. It is measure-based and contrast-blind, so the confident/certain scale-mate equivalence (CSW (72)) holds by construction.

Equations

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

theorem Confidence.confidence_more_of_ordering {E : Type u_1} {W : Type u_2} {D : Type u_3} [Preorder D] (co : ConfidenceOrdering E W) (μ : ConfidenceState E W → D) {s_p s_q : ConfidenceState E W} : Degree.admissibleMeasure μ → s_q < s_p → Degree.comparativeSem μ s_p s_q Core.Order.ScalePolarity.positive

The admissibility spine (CSW (21)/(31)): when the measure μ is admissible (StrictMono w.r.t. the holder's confidence ordering), the ordering entails the comparative — if s_q ≺ s_p then A is more confident of s_p than s_q. This ties the measure-comparative to the ConfidenceOrdering, the constraint the free-μ comparative_transitive/comparative_antisymmetric lack. (Over a Preorder, only this forward direction holds — CSW's ordering need not be connected.)