def Semantics.Entailment.PresuppositionPolarity.presupProjectsAt {W : Type u_1} (_ctx : Core.NaturalLogic.ContextPolarity) (p : Core.Presupposition.PrProp W) : BProp W

The projected presupposition at a given polarity context.

In the simplest case, presupposition projection is polarity-independent: the presupposition of "not P" is the same as the presupposition of "P". This function captures that basic behavior.

More complex interactions (e.g., presupposition strengthening under negation) would require extending this.

Equations

• Semantics.Entailment.PresuppositionPolarity.presupProjectsAt _ctx p = p.presup

theorem Semantics.Entailment.PresuppositionPolarity.impFilter_presup_polarity_independent {W : Type u_1} (p q : Core.Presupposition.PrProp W) : presupProjectsAt Core.NaturalLogic.ContextPolarity.upward (p.impFilter q) = presupProjectsAt Core.NaturalLogic.ContextPolarity.downward (p.impFilter q)

Filtering is independent of assertion polarity.

When computing presupposition projection for filtering connectives, the presupposition formula (p.presup && (!p.assertion || q.presup)) doesn't depend on whether we're in a UE or DE context.

The polarity-dependence enters only in which alternatives we consider for exhaustification, not in the projection algorithm itself.

theorem Semantics.Entailment.PresuppositionPolarity.neg_presup_polarity_independent {W : Type u_1} (p : Core.Presupposition.PrProp W) : presupProjectsAt Core.NaturalLogic.ContextPolarity.upward p.neg = presupProjectsAt Core.NaturalLogic.ContextPolarity.downward p.neg

Negation preserves presupposition regardless of polarity.

structure Semantics.Entailment.PresuppositionPolarity.PresupContext (W : Type u_2) : Type u_2

A presupposition projection context tracks both:

1. The polarity (UE/DE) for implicature computation
2. The accumulated presupposition projection

• context : BProp World → BProp World

  The semantic context function (for computing entailments)

• polarity : Core.NaturalLogic.ContextPolarity

  Whether the context is UE or DE

• accumulatedPresup : BProp W

  The presupposition accumulated from outer operators

def Semantics.Entailment.PresuppositionPolarity.composePresupContext {W : Type u_1} (outer inner : PresupContext W) : PresupContext W

Compose two presupposition contexts.

When composing contexts (e.g., "not (if P then Q)"), we compose:

1. The semantic context functions
2. The polarities (using composition rules: DE ∘ DE = UE, etc.)
3. The accumulated presuppositions (conjunction)

Equations

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

def Semantics.Entailment.PresuppositionPolarity.identityPresupContext {W : Type u_1} : PresupContext W

The identity presupposition context.

Equations

• Semantics.Entailment.PresuppositionPolarity.identityPresupContext = { context := id, polarity := Core.NaturalLogic.ContextPolarity.upward, accumulatedPresup := fun (x : W) => true }

def Semantics.Entailment.PresuppositionPolarity.negationPresupContext {W : Type u_1} : PresupContext W

Negation context: flips polarity, preserves presupposition.

Equations

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

inductive Semantics.Entailment.PresuppositionPolarity.QuantifierProjection : Type

Presupposition projection behavior varies by quantifier.

Following @cite{heim-1983}:

• Universal: "Every F is G" presupposes every F satisfies G's presup
• Existential: "Some F is G" presupposes some F satisfies G's presup (or: at least one F exists)

This is a placeholder for more sophisticated treatment.

• universal : QuantifierProjection
• existential : QuantifierProjection
• none : QuantifierProjection

instance Semantics.Entailment.PresuppositionPolarity.instDecidableEqQuantifierProjection : DecidableEq QuantifierProjection

Equations

• Semantics.Entailment.PresuppositionPolarity.instDecidableEqQuantifierProjection x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

instance Semantics.Entailment.PresuppositionPolarity.instReprQuantifierProjection : Repr QuantifierProjection

Equations

• Semantics.Entailment.PresuppositionPolarity.instReprQuantifierProjection = { reprPrec := Semantics.Entailment.PresuppositionPolarity.instReprQuantifierProjection.repr }

def Semantics.Entailment.PresuppositionPolarity.instReprQuantifierProjection.repr : QuantifierProjection → ℕ → Std.Format

Equations

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