Features.Attitudes

@cite{karttunen-1971} @cite{villalta-2008} @cite{anand-hacquard-2013} @cite{klecha-2016}

Per-verb-entry feature taxonomies for attitude verbs: veridicality (Karttunen lineage), evaluative valence (positive vs negative attitudes), preferential strategy (degree comparison vs uncertainty vs relevance), and the composed Attitude type combining doxastic and preferential dimensions.

Provenance

Bundled together (rather than 4 separate single-enum files) per the mathlib idiom of co-locating peer concepts that share theoretical context (cf. Mathlib/Order/RelClasses.lean bundling IsRefl/IsSymm/IsTrans). Moved from Core/Lexical/VerbClass.lean in the cleanup that dissolved Core/Lexical/.

Framework commitment

Each enum here is anchored on a specific theoretical lineage and not a pan-framework consensus:

• Veridicality (Veridicality): Karttunen lineage on factive vs non-factive complement-taking verbs (the Hooper 1975 On Assertive Predicates paper extends this to assertive predicates; not currently in references.bib). @cite{giannakidou-1998} critiques this binary as too coarse and proposes a 3-way veridical / nonveridical / antiveridical taxonomy; Schlenker (e.g., @cite{schlenker-2003}) on attitude-verb projection draws yet different cuts. The binary veridical/non-veridical carve-up here is the classical-DRT default, not a neutral substrate.

• AttitudeValence (AttitudeValence): positive/negative split underlies the TSP distribution literature (positive attitudes have TSP, negative don't) and "V whether" interpretive asymmetries. @cite{stalnaker-1984}-style "directedness" frameworks would parameterize this differently.

• Preferential (Preferential): three-way split between degree-comparison (@cite{villalta-2008}), uncertainty-based (@cite{anand-hacquard-2013} worry-class), and relevance-based. Note: "relevance-based" is linglib's coinage for qidai-type attitudes resisting both Villalta degree-comparison and A&H uncertainty analyses; not a published category. @cite{heim-1992} gradable-attitude analysis and @cite{lassiter-2017} expected-utility account carve the space differently. The C-distributivity and NVP-class derivations downstream depend on this specific 3-way split.

• Attitude (composed): unifies doxastic (Hintikka accessibility) with preferential (degree/uncertainty). Wholly framework-internal: not every attitude-verb taxonomy splits along the doxastic/preferential axis (Anand & Hacquard subdivide finer; Villalta lumps differently).

Out of scope

The current Attitude type covers doxastic and preferential cases. Bouletic verbs (want, wish) are typically slotted under preferential .degreeComparison .positive per the @cite{heim-1992} gradable-attitude analysis. Speech-act predicates (promise, demand, order) are not covered by this feature taxonomy and would need a parallel SpeechActPredicate type in Theories/Pragmatics/.

inductive Features.Veridicality : Type

A doxastic predicate is veridical if believing/knowing p entails p is true.

Veridical: know, realize, discover Non-veridical: believe, think, suspect

• veridical : Veridicality
• nonVeridical : Veridicality

@[implicit_reducible]

instance Features.instDecidableEqVeridicality : DecidableEq Veridicality

Equations

• Features.instDecidableEqVeridicality x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[implicit_reducible]

instance Features.instReprVeridicality : Repr Veridicality

Equations

• Features.instReprVeridicality = { reprPrec := Features.instReprVeridicality.repr }

def Features.instReprVeridicality.repr : Veridicality → Nat → Std.Format

Equations

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

inductive Features.AttitudeValence : Type

Evaluative valence of a preferential predicate.

• Positive: Expresses desire for the proposition (hope, wish, expect)
• Negative: Expresses aversion to the proposition (fear, worry, dread)

This distinction is crucial for:

1. TSP distribution (positive have TSP, negative don't)
2. Interpretive asymmetry in "V whether" constructions

• positive : AttitudeValence
• negative : AttitudeValence

@[implicit_reducible]

instance Features.instDecidableEqAttitudeValence : DecidableEq AttitudeValence

Equations

• Features.instDecidableEqAttitudeValence x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Features.instReprAttitudeValence.repr : AttitudeValence → Nat → Std.Format

Equations

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

@[implicit_reducible]

instance Features.instReprAttitudeValence : Repr AttitudeValence

Equations

• Features.instReprAttitudeValence = { reprPrec := Features.instReprAttitudeValence.repr }

inductive Features.Preferential : Type

Which Montague predicate strategy this preferential verb uses.

Links the Fragment entry to the compositional semantics in Semantics.Attitudes.Preferential. Properties like C-distributivity are DERIVED from this tag via theorems, not stipulated.

• degreeComparison: Uses mkDegreeComparisonPredicate → C-distributive
• uncertaintyBased: Uses worry constructor → NOT C-distributive
• relevanceBased: Uses qidai constructor → NOT C-distributive

• degreeComparison (valence : AttitudeValence) : Preferential

  Degree comparison semantics: ⟦x V Q⟧ = ∃p ∈ Q. μ(x,p) > θ. C-distributive.

• uncertaintyBased : Preferential

  Uncertainty-based semantics (worry): involves global uncertainty. NOT C-distributive.

• relevanceBased (valence : AttitudeValence) : Preferential

  Relevance-based semantics (qidai, care): involves resolution. NOT C-distributive.

@[implicit_reducible]

instance Features.instDecidableEqPreferential : DecidableEq Preferential

Equations

• Features.instDecidableEqPreferential = Features.instDecidableEqPreferential.decEq

def Features.instDecidableEqPreferential.decEq (x✝ x✝¹ : Preferential) : Decidable (x✝ = x✝¹)

Equations

• Features.instDecidableEqPreferential.decEq (Features.Preferential.degreeComparison a) (Features.Preferential.degreeComparison b) = if h : a = b then h ▸ isTrue ⋯ else isFalse ⋯
• Features.instDecidableEqPreferential.decEq (Features.Preferential.degreeComparison valence) Features.Preferential.uncertaintyBased = isFalse ⋯
• Features.instDecidableEqPreferential.decEq (Features.Preferential.degreeComparison valence) (Features.Preferential.relevanceBased valence_1) = isFalse ⋯
• Features.instDecidableEqPreferential.decEq Features.Preferential.uncertaintyBased (Features.Preferential.degreeComparison valence) = isFalse ⋯
• Features.instDecidableEqPreferential.decEq Features.Preferential.uncertaintyBased Features.Preferential.uncertaintyBased = isTrue ⋯
• Features.instDecidableEqPreferential.decEq Features.Preferential.uncertaintyBased (Features.Preferential.relevanceBased valence) = isFalse ⋯
• Features.instDecidableEqPreferential.decEq (Features.Preferential.relevanceBased valence) (Features.Preferential.degreeComparison valence_1) = isFalse ⋯
• Features.instDecidableEqPreferential.decEq (Features.Preferential.relevanceBased valence) Features.Preferential.uncertaintyBased = isFalse ⋯
• Features.instDecidableEqPreferential.decEq (Features.Preferential.relevanceBased a) (Features.Preferential.relevanceBased b) = if h : a = b then h ▸ isTrue ⋯ else isFalse ⋯

@[implicit_reducible]

instance Features.instReprPreferential : Repr Preferential

Equations

• Features.instReprPreferential = { reprPrec := Features.instReprPreferential.repr }

def Features.instReprPreferential.repr : Preferential → Nat → Std.Format

Equations

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

def Features.Preferential.valence : Preferential → AttitudeValence

Get the valence from the preferential classification.

Equations

• (Features.Preferential.degreeComparison a).valence = a
• Features.Preferential.uncertaintyBased.valence = Features.AttitudeValence.negative
• (Features.Preferential.relevanceBased a).valence = a

inductive Features.Attitude : Type

Unified classification for all attitude verbs, covering both doxastic (believe, know) and preferential (hope, fear) attitudes.

This is the minimal basis from which theoretical properties are derived:

1. Doxastic attitudes: Use accessibility relations (Hintikka semantics)
2. Preferential attitudes: Use degree/uncertainty semantics (Villalta)

Derived properties (in Theory layer):

• C-distributivity: from Preferential structure
• NVP class: from C-distributivity + valence
• Parasitic on belief: from being preferential
• Presupposition projection: from veridicality + attitude type

• doxastic (veridicality : Veridicality) : Attitude

  Doxastic attitude (believe, know, think) with accessibility semantics

• preferential (kind : Preferential) : Attitude

  Preferential attitude (hope, fear, worry) with degree/uncertainty semantics

def Features.instDecidableEqAttitude.decEq (x✝ x✝¹ : Attitude) : Decidable (x✝ = x✝¹)

Equations

• Features.instDecidableEqAttitude.decEq (Features.Attitude.doxastic a) (Features.Attitude.doxastic b) = if h : a = b then h ▸ isTrue ⋯ else isFalse ⋯
• Features.instDecidableEqAttitude.decEq (Features.Attitude.doxastic veridicality) (Features.Attitude.preferential kind) = isFalse ⋯
• Features.instDecidableEqAttitude.decEq (Features.Attitude.preferential kind) (Features.Attitude.doxastic veridicality) = isFalse ⋯
• Features.instDecidableEqAttitude.decEq (Features.Attitude.preferential a) (Features.Attitude.preferential b) = if h : a = b then h ▸ isTrue ⋯ else isFalse ⋯

@[implicit_reducible]

instance Features.instDecidableEqAttitude : DecidableEq Attitude

Equations

• Features.instDecidableEqAttitude = Features.instDecidableEqAttitude.decEq

@[implicit_reducible]

instance Features.instReprAttitude : Repr Attitude

Equations

• Features.instReprAttitude = { reprPrec := Features.instReprAttitude.repr }

def Features.instReprAttitude.repr : Attitude → Nat → Std.Format

Equations

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

def Features.Attitude.veridicality : Attitude → Veridicality

Get veridicality from an attitude classification.

Equations

• (Features.Attitude.doxastic a).veridicality = a
• (Features.Attitude.preferential a).veridicality = Features.Veridicality.nonVeridical

def Features.Attitude.isDoxastic : Attitude → Bool

Is this a doxastic attitude?

Equations

• (Features.Attitude.doxastic a).isDoxastic = true
• (Features.Attitude.preferential a).isDoxastic = false

def Features.Attitude.isPreferential : Attitude → Bool

Is this a preferential attitude?

Equations

• (Features.Attitude.doxastic a).isPreferential = false
• (Features.Attitude.preferential a).isPreferential = true

def Features.Attitude.getPreferential : Attitude → Option Preferential

Get the preferential classification if this is a preferential attitude.

Equations

• (Features.Attitude.doxastic a).getPreferential = none
• (Features.Attitude.preferential a).getPreferential = some a

def Features.Attitude.valence : Attitude → Option AttitudeValence

Get valence for preferential attitudes.

Equations

• (Features.Attitude.doxastic a).valence = none
• (Features.Attitude.preferential a).valence = some a.valence

def Features.Attitude.PermitsCircumstantial : Attitude → Prop

Can this attitude verb take a circumstantial modal base? @cite{klecha-2016}: doxastic attitudes (think, believe) take only DOX; preferential attitudes (hope, want, pray) can also take CIR, which permits future temporal orientation. This is the source of the Upper Limit Constraint: DOX-only verbs block future readings.

Equations

• (Features.Attitude.doxastic a).PermitsCircumstantial = False
• (Features.Attitude.preferential a).PermitsCircumstantial = True

@[implicit_reducible]

instance Features.Attitude.instDecidablePredPermitsCircumstantial : DecidablePred PermitsCircumstantial

Equations

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