Outlook-indexed two-dimensional meaning

[Cop18] [Pot05] [HP09]

[Cop18]'s outlook-relative enrichment of the two-dimensional meaning of [Pot05]. A TwoDimProp fixes a single perspective; an Outlook is a family of two-dimensional meanings indexed by an outlook O (a circumstance of evaluation that settles matters of opinion, not just fact), together with a presupposed counterstance.

The point of the index is perspective shift ([HP09]): the use-conditional tier is evaluated at the speaker's outlook by default, but an attitude verb may supply the holder's outlook instead. A pure expressive is the constant family (ofTwoDimProp), so it cannot shift; IsRigid is exactly that constancy, and the perspective-shift diagnostic is then a theorem about the structure rather than a stipulated flag.

Main definitions

• Outlook — prejacent + counterstance + outlook-relative evaluation.
• Outlook.toPartialProp, Outlook.toTwoDimProp — the presuppositional and (perspective-fixed) two-dimensional projections.
• Outlook.IsRigid — the evaluation ignores the outlook (the pure-expressive corner).
• Outlook.ofTwoDimProp — a TwoDimProp as the constant (speaker-rigid) outlook family.

Main results

• rigid_noShift — a rigid outlook's CI is invariant under a change of outlook.
• ofTwoDimProp_isRigid — every embedded TwoDimProp is rigid.
• not_isRigid_of_evaluation_ne — distinct evaluations witness perspective shift.

References

[Cop18] [Pot05] [HP09]

structure Pragmatics.Expressives.Outlook (W : Type u_3) (O : Type u_4) : Type (max u_3 u_4)

An outlook-indexed two-dimensional meaning ([Cop18]). At-issue content is shared across outlooks (only the use-conditional tier shifts), so the prejacent is stored once and the CI tier is a function of the outlook.

• prejacent : W → Prop

  At-issue content, outlook-independent.

• counterstance : W → Prop

  Presupposed salient counterstance.

• evaluation : O → W → Prop

  Use-conditional tier, relative to an outlook.

def Pragmatics.Expressives.Outlook.toPartialProp {W : Type u_1} {O : Type u_2} (m : Outlook W O) : Semantics.Presupposition.PartialProp W

Presuppositional projection: the counterstance is the presupposition, the prejacent the assertion. Outlook-independent.

Equations

• m.toPartialProp = { presup := m.counterstance, assertion := m.prejacent }

def Pragmatics.Expressives.Outlook.toTwoDimProp {W : Type u_1} {O : Type u_2} (m : Outlook W O) (o : O) : TwoDimProp W

Two-dimensional projection at an outlook o: an ordinary TwoDimProp recovered by fixing the perspective.

Equations

• m.toTwoDimProp o = { atIssue := m.prejacent, ci := m.evaluation o }

def Pragmatics.Expressives.Outlook.ciFrom {W : Type u_1} {O : Type u_2} (m : Outlook W O) (o : O) : W → Prop

The CI content attributed when the judge has outlook o.

Equations

• m.ciFrom o = m.evaluation o

@[simp]

theorem Pragmatics.Expressives.Outlook.toPartialProp_presup {W : Type u_1} {O : Type u_2} (m : Outlook W O) : m.toPartialProp.presup = m.counterstance

@[simp]

theorem Pragmatics.Expressives.Outlook.toPartialProp_assertion {W : Type u_1} {O : Type u_2} (m : Outlook W O) : m.toPartialProp.assertion = m.prejacent

@[simp]

theorem Pragmatics.Expressives.Outlook.toTwoDimProp_atIssue {W : Type u_1} {O : Type u_2} (m : Outlook W O) (o : O) : (m.toTwoDimProp o).atIssue = m.prejacent

@[simp]

theorem Pragmatics.Expressives.Outlook.toTwoDimProp_ci {W : Type u_1} {O : Type u_2} (m : Outlook W O) (o : O) : (m.toTwoDimProp o).ci = m.evaluation o

@[simp]

theorem Pragmatics.Expressives.Outlook.ciFrom_eq {W : Type u_1} {O : Type u_2} (m : Outlook W O) (o : O) : m.ciFrom o = m.evaluation o

theorem Pragmatics.Expressives.Outlook.counterstance_projects_through_neg {W : Type u_1} {O : Type u_2} (m : Outlook W O) : m.toPartialProp.neg.presup = m.counterstance

The counterstance (presupposition) projects through negation — via PartialProp.neg.

theorem Pragmatics.Expressives.Outlook.ci_projects_through_neg {W : Type u_1} {O : Type u_2} (m : Outlook W O) (o : O) : (m.toTwoDimProp o).neg.ci = m.evaluation o

The CI tier projects through negation at a fixed outlook — via TwoDimProp.neg.

Rigidity: the pure-expressive corner

def Pragmatics.Expressives.Outlook.IsRigid {W : Type u_1} {O : Type u_2} (m : Outlook W O) : Prop

An outlook is rigid when its CI ignores the outlook — the perspective-insensitive (pure-expressive) case. Perspective shift is exactly the failure of this. This is the canonical rigidity predicate of Semantics.Intensional.Rigidity (Intension.IsRigid) applied to evaluation: constancy of the CI tier across the outlook index.

Equations

• m.IsRigid = ∀ (o₁ o₂ : O), m.evaluation o₁ = m.evaluation o₂

theorem Pragmatics.Expressives.Outlook.rigid_noShift {W : Type u_1} {O : Type u_2} {m : Outlook W O} (h : m.IsRigid) (o₁ o₂ : O) : m.ciFrom o₁ = m.ciFrom o₂

A rigid outlook's CI is invariant under a change of outlook: no perspective shift.

theorem Pragmatics.Expressives.Outlook.not_isRigid_of_evaluation_ne {W : Type u_1} {O : Type u_2} {m : Outlook W O} {o₁ o₂ : O} (h : m.evaluation o₁ ≠ m.evaluation o₂) : ¬m.IsRigid

Distinct evaluations witness perspective shift: the outlook is not rigid.

def Pragmatics.Expressives.Outlook.ofTwoDimProp {W : Type u_1} {O : Type u_2} (t : TwoDimProp W) : Outlook W O

A TwoDimProp (a pure expressive — a single, speaker-rigid CI) as the constant outlook family: its evaluation ignores the outlook, and it carries the trivial counterstance.

Equations

• Pragmatics.Expressives.Outlook.ofTwoDimProp t = { prejacent := t.atIssue, counterstance := fun (x : W) => True, evaluation := fun (x : O) => t.ci }

@[simp]

theorem Pragmatics.Expressives.Outlook.ofTwoDimProp_toTwoDimProp {W : Type u_1} {O : Type u_2} (t : TwoDimProp W) (o : O) : (ofTwoDimProp t).toTwoDimProp o = t

theorem Pragmatics.Expressives.Outlook.ofTwoDimProp_isRigid {W : Type u_1} {O : Type u_2} (t : TwoDimProp W) : (ofTwoDimProp t).IsRigid

Every embedded TwoDimProp is rigid — pure expressives do not perspective-shift, by construction.