Documentation

Linglib.Phenomena.Focus.Studies.IppolitoKissWilliams2022

Ippolito, Kiss & Williams 2022: Discourse Function of Adversative Conjunction #

@cite{ippolito-kiss-williams-2022}

The Sinn und Bedeutung 26 paper that introduces the doxastic-evidential notions of SUPPORT, AGREEMENT, and DISAGREEMENT which the follow-up paper @cite{ippolito-kiss-williams-2025} reuses for discourse only. The 2022 paper itself targets adversative but; the SUPPORT / AGREE / DISAGREE apparatus is the part of that account both papers share.

This file currently formalizes only the shared apparatus — the but analysis itself is not yet formalized. The recap below follows the conceptual statement that @cite{ippolito-kiss-williams-2025} §4 (p. 225) gives explicitly: "Following Ippolito et al. (2022) we define the notion of AGREEMENT (and DISAGREEMENT) and the notion of SUPPORT, on which the former notion is based."

SUPPORT #

A sentence S supports a proposition r (in context c) iff some alternative q ∈ ⟦S⟧ is doxastically grounded for the speaker (dox_sp ⊆ q) and provides evidence for r. The doxastic anchor is what derives the @cite{ippolito-kiss-williams-2025} §5.2 interrogative-left-argument restriction: a speaker who doesn't believe any alternative cannot use the sentence to support anything.

Project-canonical refinement. The original 2022 statement leaves "q provides evidence for r" deliberately informal. We formalize it as IsPositiveEvidence q r μ (Bayesian conditional-probability shift, see Theories/Semantics/Questions/Probabilistic.lean). This is a strengthening; the §5.2 architectural derivations carry over but rest on the strengthened relation. A flavor-agnostic version parameterized by an abstract evidence relation could be added if a sibling theory needs it.

AGREEMENT / DISAGREEMENT #

Two sentences agree on a QUD if they support a common alternative; they disagree if each supports some alternative but no shared one witnesses agreement. Both relations are symmetric in their S/S' arguments.

SUPPORT (paper ex. (13) of @cite{ippolito-kiss-williams-2025}, #

restating the 2022 definition)
source
def Phenomena.Focus.Studies.IppolitoKissWilliams2022.Supports {W : Type u_1} (dox : Set W) (S : Core.Question W) (r : Set W) (μ : PMF W) :
Prop

S supports r from doxastic state dox under prior μ: some alternative q ∈ alt S is doxastically grounded (dox ⊆ q) and provides positive evidence for r.

Refines the 2022 informal "q provides evidence for r" as IsPositiveEvidence (conditional-probability shift).

Equations
Instances For
    source
    theorem Phenomena.Focus.Studies.IppolitoKissWilliams2022.Supports.of_no_belief_fails {W : Type u_1} {dox : Set W} {S : Core.Question W} {r : Set W} {μ : PMF W} (h : ∀ q ∈ S.alt, ¬dox ⊆ q) :
    ¬Supports dox S r μ

    An info-seeking speaker — one who doesn't believe any alternative of S — cannot use S to support anything. The architectural derivation of @cite{ippolito-kiss-williams-2025} §5.2's interrogative-left-argument restriction: the failure isn't a clause-type filter but a doxastic consequence of Supports.

    source
    theorem Phenomena.Focus.Studies.IppolitoKissWilliams2022.Supports.exists_dox_alt {W : Type u_1} {dox : Set W} {S : Core.Question W} {r : Set W} {μ : PMF W} (h : Supports dox S r μ) :
    ∃ p ∈ S.alt, dox ⊆ p

    Supports dox S r μ exposes a doxastically-grounded alternative of S containing dox. The bridge from probabilistic support to pure inquisitive Resolves-style witnesses.

    AGREEMENT and DISAGREEMENT (paper ex. (14) of #

    @cite{ippolito-kiss-williams-2025}, restating the 2022 definitions)
    source
    def Phenomena.Focus.Studies.IppolitoKissWilliams2022.Agree {W : Type u_1} (dox : Set W) (S S' Q : Core.Question W) (μ : PMF W) :
    Prop

    Two sentences S and S' agree on QUD Q from doxastic state dox iff some alternative α ∈ alt Q is supported by both.

    Equations
    • One or more equations did not get rendered due to their size.
    Instances For
      source
      def Phenomena.Focus.Studies.IppolitoKissWilliams2022.Disagree {W : Type u_1} (dox : Set W) (S S' Q : Core.Question W) (μ : PMF W) :
      Prop

      Two sentences S and S' disagree on QUD Q from doxastic state dox iff each supports some answer but no shared alternative witnesses agreement.

      Equations
      • One or more equations did not get rendered due to their size.
      Instances For
        source
        theorem Phenomena.Focus.Studies.IppolitoKissWilliams2022.Agree.symm {W : Type u_1} {dox : Set W} {S S' Q : Core.Question W} {μ : PMF W} (h : Agree dox S S' Q μ) :
        Agree dox S' S Q μ

        Agree is symmetric in its S/S' arguments.

        source
        theorem Phenomena.Focus.Studies.IppolitoKissWilliams2022.Disagree.symm {W : Type u_1} {dox : Set W} {S S' Q : Core.Question W} {μ : PMF W} (h : Disagree dox S S' Q μ) :
        Disagree dox S' S Q μ

        Disagree is symmetric in its S/S' arguments.