Documentation

Linglib.Theories.Semantics.Attitudes.Monotonicity

Attitude Verb Monotonicity #

Classifies attitude verb complement positions using EntailmentSig from Core/NaturalLogic.lean — the same 9-element lattice used for quantifier determiners. This makes the parallel between quantifier monotonicity and attitude monotonicity explicit: both are instances of the same algebraic classification.

Per-verb monotonicity data lives on VerbCore.complementSig in the fragment lexicon (Fragments/English/Predicates/Verbal.lean), not here. This file provides only the derivation logic: given an EntailmentSig, what follows about conjunction distribution and neg-raising?

Key contributions #

@cite{bondarenko-elliott-2026}

  1. Conjunction distribution derived from EntailmentSig: An attitude verb distributes over conjunction iff its complement signature refines .mono.

  2. Neg-raising from monotonicity + EMP: Bondarenko & Elliott derive neg-raising from upward monotonicity plus an excluded-middle presupposition (EMP), NOT from veridicality (as in NegRaising.lean). Both derivations agree on standard doxastic verbs.

  3. Mereological grounding: The conjunction distribution theorem (mono_att_distrib_and_iff in Truthmaker.Basic) proves that the distribution follows from the SemilatticeSup structure of states.

source
def Semantics.Attitudes.Monotonicity.distribOverConj (sig : Core.NaturalLogic.EntailmentSig) :
Bool

An attitude distributes over conjunction iff its complement signature refines .mono (upward monotone). This includes: .all, .addMult, .additive, .mult, and .mono itself.

Note: .mult (multiplicative) distributes over ∧ by definition — f(A ∧ B) = f(A) ∧ f(B). The .mono refinement captures this.

Equations
Instances For
    source
    def Semantics.Attitudes.Monotonicity.hasEMP (sig : Core.NaturalLogic.EntailmentSig) :
    Bool

    Excluded-Middle Presupposition (EMP). An attitude verb has EMP if it presupposes that the agent either holds the attitude toward p or toward ¬p. EMP(V, x, p) := V(x, p) ∨ V(x, ¬p)

    Under EMP, ¬V(p) → V(¬p) is immediate (disjunctive syllogism). This is neg-raising.

    The Bondarenko & Elliott insight: EMP is motivated by monotonicity. Upward-monotone verbs have a "gapless" information state — the state either contains a verifier for p or for ¬p (no undecided gap). This is a presupposition, not a semantic entailment.

    Equations
    Instances For
      source
      def Semantics.Attitudes.Monotonicity.negRaisingFromMono (sig : Core.NaturalLogic.EntailmentSig) (v : Doxastic.Veridicality) :
      Bool

      Neg-raising available via monotonicity + EMP. This is an alternative to NegRaising.negRaisingAvailable, which derives neg-raising from veridicality. Both are correct derivations that agree on all standard verbs but have different theoretical underpinnings.

      Bondarenko & Elliott: monotonicity + EMP → neg-raising @cite{horn-2001}: non-veridicality → neg-raising

      Equations
      Instances For
        source
        theorem Semantics.Attitudes.Monotonicity.negRaising_accounts_agree (v : Doxastic.Veridicality) :
        negRaisingFromMono Core.NaturalLogic.EntailmentSig.mono v = NegRaising.negRaisingAvailable v

        The veridicality and monotonicity accounts agree on all standard doxastic verbs: both predict neg-raising for non-veridical monotone verbs and no neg-raising for veridical ones.

        They could diverge for hypothetical verbs that are:

        • Non-monotone but non-veridical → veridicality allows, monotonicity blocks

        Currently both routes agree because all non-veridical doxastic verbs in the lexicon are also monotone.

        source
        theorem Semantics.Attitudes.Monotonicity.conjunction_distribution_grounded (S : Type u_1) (E : Type u_2) [SemilatticeSup S] (σ : E → S) (p q : Truthmaker.TMProp S) (x : E) :
        Truthmaker.attHolds σ (Truthmaker.tmAnd p q) x ↔ Truthmaker.attHolds σ p x ∧ Truthmaker.attHolds σ q x

        The truthmaker conjunction distribution theorem (Truthmaker.mono_att_distrib_and_iff) provides the semantic why for the monotonicity classification.

        This re-export makes the connection explicit: the EntailmentSig classification of attitude verbs is grounded in the SemilatticeSup structure of propositional content via truthmaker semantics.