structure Semantics.Presupposition.TonhauserDerivation.SCF_Requires (W : Type u_3) : Type u_3

SCF (Strong Contextual Felicity) in local context terms.

A trigger has SCF=yes iff its projective content MUST be entailed by the global context for felicitous use. Accommodation is blocked.

In Schlenker's terms: the local context at matrix level IS the global context, and the presupposition must be entailed (not just "could be accommodated").

This is a marker structure. The constraint that accommodation is blocked is a property of the trigger class, not derivable from the content alone. Full derivation requires connecting to Accommodation.AccommodationOK and trigger-specific constraints (anaphoric binding, salience, etc.).

• content : BProp W

  The projective content that must be established

structure Semantics.Presupposition.TonhauserDerivation.SCF_Allows (W : Type u_3) : Type u_3

SCF=no means accommodation is ALLOWED.

The projective content can be informative — it can update the context rather than being required to already hold.

Witness: there exist non-empty contexts where the content is NOT entailed yet the trigger's use is still felicitous (via accommodation).

• content : BProp W

  The projective content

• accommodable : ∃ (c : Core.CommonGround.ContextSet W), c.nonEmpty ∧ ¬c ⊧ self.content

  Accommodation is possible: there exist contexts where content is informative (not entailed) yet use is felicitous

def Semantics.Presupposition.TonhauserDerivation.OLE_Obligatory {W : Type u_1} {Agent : Type u_2} (Dox : BeliefEmbedding.DoxasticAccessibility W Agent) (content : BProp W) : Prop

OLE (Obligatory Local Effect) in local context terms.

OLE=yes means: under belief embedding, the local context is the attitude holder's belief state. The projective content is attributed to the holder.

Equations

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

def Semantics.Presupposition.TonhauserDerivation.OLE_NotObligatory {W : Type u_1} {Agent : Type u_2} (Dox : BeliefEmbedding.DoxasticAccessibility W Agent) (content : BProp W) : Prop

OLE=no means: under belief embedding, the projective content is still evaluated relative to the speaker's (global) context, not the holder's beliefs.

Formally: there exist doxastic contexts where the content holds globally but NOT in the attitude holder's beliefs. The content is "speaker-anchored" — it does not shift under belief embedding.

Class B triggers (expressives) and Class D triggers exhibit this behavior.

Equations

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

theorem Semantics.Presupposition.TonhauserDerivation.matrix_local_context_is_global {W : Type u_1} (c : Core.CommonGround.ContextSet W) : (LocalContext.initialLocalCtx c).worlds = c

Main Theorem 1: Local context at matrix position = global context.

This is the foundation for SCF: in unembedded sentences, the local context is just the global context C.

theorem Semantics.Presupposition.TonhauserDerivation.belief_local_context_is_holder_beliefs {W : Type u_1} {Agent : Type u_2} (blc : BeliefEmbedding.BeliefLocalCtx W Agent) (w_star : W) (h : blc.globalCtx w_star) : (BeliefEmbedding.beliefToLocalCtx blc w_star h).worlds = blc.atWorld w_star

Main Theorem 2: Local context under belief = attitude holder's beliefs.

This is the foundation for OLE=yes: under belief embedding, the local context is determined by the attitude holder's doxastic state.

theorem Semantics.Presupposition.TonhauserDerivation.negation_projects {W : Type u_1} (c : Core.CommonGround.ContextSet W) (p : Core.Presupposition.PrProp W) : LocalContext.presupProjects (LocalContext.localCtxNegation (LocalContext.initialLocalCtx c)) p ↔ LocalContext.presupProjects (LocalContext.initialLocalCtx c) p

Projection Theorem 1: Presuppositions project from negation.

"not pp'" has local context = global context at pp'. Therefore pp' projects (unless globally entailed).

theorem Semantics.Presupposition.TonhauserDerivation.conditional_filters {W : Type u_1} (c : LocalContext.LocalCtx W) (p q : Core.Presupposition.PrProp W) (h : ∀ (w : W), c.worlds w → p.assertion w = true → q.presup w = true) : LocalContext.presupFiltered (LocalContext.localCtxConsequent c p) q

Projection Theorem 2: Conditionals filter consequent presuppositions.

"if p then qq'" — if p.assertion entails q.presup, it's filtered.

theorem Semantics.Presupposition.TonhauserDerivation.belief_derives_ole {W : Type u_1} {Agent : Type u_2} (blc : BeliefEmbedding.BeliefLocalCtx W Agent) (p : Core.Presupposition.PrProp W) (h : BeliefEmbedding.presupAttributedToHolder blc p) (w_star : W) (hw : blc.globalCtx w_star) : LocalContext.presupFiltered (BeliefEmbedding.beliefToLocalCtx blc w_star hw) p

Projection Theorem 3: Belief embedding creates attitude-holder context.

Under "x believes φ", the local context at φ is x's belief state. This derives OLE=yes behavior.