Modal anchors

This file defines the sources from which an event projects a modal domain — the content of a speech act, the content of an attitude, or the decision that caused a volitional event — the partial anchoring function a source assignment induces, and the definedness conditions a modal item may impose on its anchor.

Main definitions

• ModalSource — what an event projects from, with its background and flavor.
• anchoring — the anchoring function of a source assignment, defined on events with a source.
• AnchorConstraint — the definedness condition an item imposes, and Admits.

References

• [hacquard-2006]
• [hacquard-2010]
• [alonso-ovalle-menendez-benito-2018]
• [alonso-ovalle-royer-2024]

inductive Modality.ModalSource (W : Type u_3) : Type u_3

What an event projects a modal domain from: a speech act's content CON(e*), an attitude holder's doxastic alternatives, or the fulfilment conditions of the decision that caused a volitional event.

• speechAct {W : Type u_3} (sa : Mood.SpeechEvent W) : ModalSource W
• attitude {W : Type u_3} (dox : Kratzer.ConvBackground W) : ModalSource W
• decision {W : Type u_3} (fulfilled : Kratzer.ConvBackground W) : ModalSource W

def Modality.ModalSource.background {W : Type u_2} : ModalSource W → Kratzer.ConvBackground W

The conversational background a source projects.

Equations

• (Modality.ModalSource.speechAct sa).background = sa.content
• (Modality.ModalSource.attitude dox).background = dox
• (Modality.ModalSource.decision fulfilled).background = fulfilled

def Modality.ModalSource.flavor {W : Type u_2} : ModalSource W → ModalFlavor

The flavor a source projects: the speech act's own, epistemic for an attitude, and circumstantial — random choice — for a decision.

Equations

• (Modality.ModalSource.speechAct sa).flavor = sa.force.primaryFlavor
• (Modality.ModalSource.attitude dox).flavor = Modality.ModalFlavor.epistemic
• (Modality.ModalSource.decision fulfilled).flavor = Modality.ModalFlavor.circumstantial

def Modality.ModalSource.IsDecision {W : Type u_2} : ModalSource W → Prop

A source is a decision.

Equations

• (Modality.ModalSource.decision fulfilled).IsDecision = True
• x✝.IsDecision = False

@[instance_reducible]

instance Modality.instDecidableIsDecision {W : Type u_2} (s : ModalSource W) : Decidable s.IsDecision

Equations

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

def Modality.anchoring {Event : Type u_1} {W : Type u_2} (src : Event → Option (ModalSource W)) (e : Event) : Option (Kratzer.ConvBackground W)

The anchoring function of a source assignment, defined on the events with a source.

Equations

• Modality.anchoring src e = Option.map Modality.ModalSource.background (src e)

inductive Modality.AnchorConstraint : Type

The definedness condition a modal item imposes on its anchor: any source, or only the decision of a volitional event.

• unrestricted : AnchorConstraint
• volitionalOnly : AnchorConstraint

@[instance_reducible]

instance Modality.instDecidableEqAnchorConstraint : DecidableEq AnchorConstraint

Equations

• Modality.instDecidableEqAnchorConstraint x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[instance_reducible]

instance Modality.instReprAnchorConstraint : Repr AnchorConstraint

Equations

• Modality.instReprAnchorConstraint = { reprPrec := Modality.instReprAnchorConstraint.repr }

def Modality.instReprAnchorConstraint.repr : AnchorConstraint → ℕ → Std.Format

Equations

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

def Modality.AnchorConstraint.Admits {W : Type u_2} : AnchorConstraint → ModalSource W → Prop

The constraint admits the source.

Equations

• Modality.AnchorConstraint.unrestricted.Admits x✝ = True
• Modality.AnchorConstraint.volitionalOnly.Admits x✝ = x✝.IsDecision

@[instance_reducible]

instance Modality.instDecidableAdmits {W : Type u_2} (c : AnchorConstraint) (s : ModalSource W) : Decidable (c.Admits s)

Equations

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