Partial Propositions (PrProp)

@cite{heim-1983} @cite{schlenker-2009} @cite{von-fintel-1999} @cite{geurts-2005} @cite{belnap-1970}

PrProp W is linglib's canonical representation of partial propositions — propositions that may be undefined at some evaluation points. The type parameter W is the evaluation domain: worlds, possibilities, events, world-assignment pairs, or any other type. The two fields are:

• presup (= definedness): whether the proposition says anything at this point
• assertion (= content): what it says when defined

Domain generality

PrProp W is parametric over W. Common instantiations:

• PrProp World — classical presupposition over possible worlds
• PrProp (Possibility W E) — dynamic presupposition over world-assignment pairs
• PrProp (W × Event) — event presuppositions (preconditions on events)
• PrProp (W × Time) — temporal presuppositions

All operations (filtering connectives, eval, accommodation) work uniformly across domains because they are pointwise over W.

Satisfaction relations

Two satisfaction relations connect PrProp to CCP's updateFromSat:

• PrProp.defined w p — presupposition holds at w (definedness test)
• PrProp.holds w p — both presupposition and assertion hold (full satisfaction)

These enable structural integration with the dynamic semantics layer: updateFromSat PrProp.holds p produces a CCP W that is eliminative, distributive, and supports the Galois connection — all by construction.

Linguistic interpretations

• Presupposition: presup = presupposition holds; failure = undefined (@cite{heim-1983}, @cite{schlenker-2009})
• Conditional assertion: presup = assertive; failure = nonassertive (@cite{belnap-1970}: "(A/B) is assertive_w just in case A is true_w")
• Homogeneity: presup = all atoms agree; failure = truth-value gap (@cite{kriz-2016})

Connective systems

The choice of connective system (how gaps behave under ∧/∨) is orthogonal to PrProp itself — see Truth3.GapPolicy:

• Classical (PrProp.and): both must be defined
• Filtering (PrProp.andFilter): one can satisfy the other's presupposition
• Belnap (PrProp.andBelnap): gaps are skipped, defined operands contribute

Structural joints

Everything in the presupposition system derives from .presup and .assertion:

• Heritage function for p → q = (impFilter p q).presup (by construction)
• CCP update = updateFromSat PrProp.holds p (from CCP infrastructure)
• Presupposition test = updateFromSat PrProp.defined p
• Accommodation = intersect context with {w | PrProp.defined w p}
• Local context satisfaction = supportOf PrProp.defined s p

structure Core.Presupposition.PrValue (W : Type u_1) (α : Type u_2) : Type (max u_1 u_2)

A presupposed value: a value that is only defined when its presupposition holds.

PrValue W α generalizes PrProp W (= PrValue W Bool): the presupposition is always W → Bool, but the at-issue content can be any type — a truth value (Bool), a degree (ℚ), a measure, etc.

Linguistic motivation: many presupposition triggers return non-boolean values. The revised per entry (@cite{bale-schwarz-2022}, eq. 43) returns a presupposed pure number (ℚ). Definite descriptions return presupposed entities. PrValue handles all of these uniformly.

• presup : W → Bool

  The presupposition (must hold for definedness).

• value : W → α

  The at-issue content (value).

def Core.Presupposition.PrValue.defined {W : Type u_1} {α : Type u_2} (w : W) (pv : PrValue W α) : Prop

A presupposed value is defined at w iff its presupposition holds.

Equations

• Core.Presupposition.PrValue.defined w pv = (pv.presup w = true)

def Core.Presupposition.PrValue.pure {W : Type u_1} {α : Type u_2} (a : W → α) : PrValue W α

Create a presuppositionless value (always defined).

Equations

• Core.Presupposition.PrValue.pure a = { presup := fun (x : W) => true, value := a }

structure Core.Presupposition.PrProp (W : Type u_1) : Type u_1

A presuppositional proposition: assertion + presupposition.

• presup : W → Bool

  The presupposition (must hold for definedness).

• assertion : W → Bool

  The at-issue content (assertion).

def Core.Presupposition.PrProp.ofPrValue {W : Type u_1} (pv : PrValue W Bool) : PrProp W

Convert a presupposed Bool value (PrValue W Bool) to PrProp W.

Equations

• Core.Presupposition.PrProp.ofPrValue pv = { presup := pv.presup, assertion := pv.value }

def Core.Presupposition.PrProp.toPrValue {W : Type u_1} (p : PrProp W) : PrValue W Bool

Convert a PrProp to a PrValue W Bool.

Equations

• p.toPrValue = { presup := p.presup, value := p.assertion }

def Core.Presupposition.PrProp.eval {W : Type u_1} (p : PrProp W) : Duality.Prop3 W

Evaluate a presuppositional proposition to three-valued truth.

Equations

• p.eval w = if p.presup w = true then Core.Duality.Truth3.ofBool (p.assertion w) else Core.Duality.Truth3.indet

def Core.Presupposition.PrProp.defined {W : Type u_1} (w : W) (p : PrProp W) : Prop

Definedness relation: presupposition holds at the evaluation point.

Argument order (w : W) (p : PrProp W) matches updateFromSat: updateFromSat PrProp.defined p gives the presupposition test CCP.

Equations

• Core.Presupposition.PrProp.defined w p = (p.presup w = true)

def Core.Presupposition.PrProp.holds {W : Type u_1} (w : W) (p : PrProp W) : Prop

Full satisfaction relation: both presupposition and assertion hold.

updateFromSat PrProp.holds p gives the full CCP (presupposition test + assertion filter). This CCP is automatically eliminative and distributive via CCP's updateFromSat infrastructure.

Equations

• Core.Presupposition.PrProp.holds w p = (p.presup w = true ∧ p.assertion w = true)

theorem Core.Presupposition.PrProp.eval_isDefined {W : Type u_1} (p : PrProp W) (w : W) : (p.eval w).isDefined = p.presup w

Evaluation is defined iff presupposition holds.

def Core.Presupposition.PrProp.neg {W : Type u_1} (p : PrProp W) : PrProp W

Classical negation of a presuppositional proposition.

Equations

• p.neg = { presup := p.presup, assertion := fun (w : W) => !p.assertion w }

def Core.Presupposition.PrProp.and {W : Type u_1} (p q : PrProp W) : PrProp W

Classical conjunction: both presuppositions must hold.

Equations

• p.and q = { presup := fun (w : W) => p.presup w && q.presup w, assertion := fun (w : W) => p.assertion w && q.assertion w }

def Core.Presupposition.PrProp.or {W : Type u_1} (p q : PrProp W) : PrProp W

Classical disjunction: both presuppositions must hold.

Equations

• p.or q = { presup := fun (w : W) => p.presup w && q.presup w, assertion := fun (w : W) => p.assertion w || q.assertion w }

def Core.Presupposition.PrProp.imp {W : Type u_1} (p q : PrProp W) : PrProp W

Classical implication: both presuppositions must hold.

Equations

• p.imp q = { presup := fun (w : W) => p.presup w && q.presup w, assertion := fun (w : W) => !p.assertion w || q.assertion w }

def Core.Presupposition.PrProp.andFilter {W : Type u_1} (p q : PrProp W) : PrProp W

Filtering conjunction: antecedent can satisfy consequent's presupposition.

Equations

• p.andFilter q = { presup := fun (w : W) => p.presup w && (!p.assertion w || q.presup w), assertion := fun (w : W) => p.assertion w && q.assertion w }

def Core.Presupposition.PrProp.impFilter {W : Type u_1} (p q : PrProp W) : PrProp W

Filtering implication: antecedent can satisfy consequent's presupposition.

Equations

• p.impFilter q = { presup := fun (w : W) => p.presup w && (!p.assertion w || q.presup w), assertion := fun (w : W) => !p.assertion w || q.assertion w }

def Core.Presupposition.PrProp.orFilter {W : Type u_1} (p q : PrProp W) : PrProp W

Filtering disjunction: disjuncts can satisfy each other's presuppositions.

Equations

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

def Core.Presupposition.PrProp.xor {W : Type u_1} (p q : PrProp W) : PrProp W

Exclusive disjunction: both presuppositions must hold (no filtering).

Under Strong Kleene, Truth3.xor propagates undefinedness unconditionally (xor_indet_iff), so exclusive disjunction never filters presupposition failure from either disjunct. @cite{wang-davidson-2026}

Equations

• p.xor q = { presup := fun (w : W) => p.presup w && q.presup w, assertion := fun (w : W) => p.assertion w ^^ q.assertion w }

def Core.Presupposition.PrProp.«term_/\'_» : Lean.TrailingParserDescr

Equations

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

def Core.Presupposition.PrProp.«term_->'_» : Lean.TrailingParserDescr

Equations

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

def Core.Presupposition.PrProp.«term_\/'_» : Lean.TrailingParserDescr

Equations

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

theorem Core.Presupposition.PrProp.neg_presup {W : Type u_1} (p : PrProp W) : p.neg.presup = p.presup

Negation preserves presupposition.

theorem Core.Presupposition.PrProp.neg_neg_assertion {W : Type u_1} (p : PrProp W) (w : W) : p.neg.neg.assertion w = p.assertion w

Double negation preserves assertion.

theorem Core.Presupposition.PrProp.impFilter_eliminates_presup {W : Type u_1} (p q : PrProp W) (h : ∀ (w : W), p.assertion w = true → q.presup w = true) : (p.impFilter q).presup = p.presup

Filtering implication eliminates presupposition when antecedent entails it.

theorem Core.Presupposition.PrProp.impFilter_trivializes_presup {W : Type u_1} (p q : PrProp W) (h : p.assertion = q.presup) : (p.impFilter q).presup = p.presup

When A(p) = P(q), filtering implication has trivial presupposition.

def Core.Presupposition.PrProp.ofBProp {W : Type u_1} (p : BProp W) : PrProp W

Create a presuppositionless proposition from a BProp.

Equations

• Core.Presupposition.PrProp.ofBProp p = { presup := fun (x : W) => true, assertion := p }

def Core.Presupposition.PrProp.top {W : Type u_1} : PrProp W

Create a tautological presupposition.

Equations

• Core.Presupposition.PrProp.top = { presup := fun (x : W) => true, assertion := fun (x : W) => true }

def Core.Presupposition.PrProp.bot {W : Type u_1} : PrProp W

Create a contradictory presupposition.

Equations

• Core.Presupposition.PrProp.bot = { presup := fun (x : W) => true, assertion := fun (x : W) => false }

def Core.Presupposition.PrProp.undefined {W : Type u_1} : PrProp W

Create a presupposition failure (never defined).

Equations

• Core.Presupposition.PrProp.undefined = { presup := fun (x : W) => false, assertion := fun (x : W) => false }

theorem Core.Presupposition.PrProp.ofBProp_no_presup {W : Type u_1} (p : BProp W) (w : W) : (ofBProp p).presup w = true

ofBProp creates presuppositionless propositions.

theorem Core.Presupposition.PrProp.ofBProp_assertion {W : Type u_1} (p : BProp W) (w : W) : (ofBProp p).assertion w = p w

ofBProp preserves assertion.

theorem Core.Presupposition.PrProp.eval_neg {W : Type u_1} (p : PrProp W) (w : W) : p.neg.eval w = (p.eval w).neg

Negation evaluation.

theorem Core.Presupposition.PrProp.eval_and {W : Type u_1} (p q : PrProp W) (w : W) (hp : p.presup w = true) (hq : q.presup w = true) : (p.and q).eval w = (p.eval w).meet (q.eval w)

Classical conjunction evaluation (both defined).

theorem Core.Presupposition.PrProp.eval_impFilter_antecedent_false {W : Type u_1} (p q : PrProp W) (w : W) (hp : p.presup w = true) (ha : p.assertion w = false) : (p.impFilter q).eval w = Duality.Truth3.true

Filtering implication when antecedent false: result is true.

theorem Core.Presupposition.PrProp.eval_impFilter_antecedent_true {W : Type u_1} (p q : PrProp W) (w : W) (hp : p.presup w = true) (ha : p.assertion w = true) (hq : q.presup w = true) : (p.impFilter q).eval w = Duality.Truth3.ofBool (q.assertion w)

Filtering implication when antecedent true: depends on consequent.

theorem Core.Presupposition.PrProp.eval_xor {W : Type u_1} (p q : PrProp W) (w : W) (hp : p.presup w = true) (hq : q.presup w = true) : (p.xor q).eval w = (p.eval w).xor (q.eval w)

Exclusive disjunction evaluation matches Truth3.xor when both defined.

theorem Core.Presupposition.PrProp.eval_xor_no_filter {W : Type u_1} (p q : PrProp W) (w : W) (hq : q.presup w = false) : (p.xor q).eval w = Duality.Truth3.indet

Exclusive disjunction never filters: when either presupposition fails, the result is undefined. @cite{wang-davidson-2026}

def Core.Presupposition.PrProp.strongEntails {W : Type u_1} (p q : PrProp W) : Prop

Strong entailment: p entails q at all worlds where both are defined.

Equations

• p.strongEntails q = ∀ (w : W), p.presup w = true → q.presup w = true → p.assertion w = true → q.assertion w = true

def Core.Presupposition.PrProp.strawsonEntails {W : Type u_1} (p q : PrProp W) : Prop

Strawson entailment: p entails q at worlds where p is defined and true.

Equations

• p.strawsonEntails q = ∀ (w : W), p.presup w = true → p.assertion w = true → q.presup w = true ∧ (q.presup w = true → q.assertion w = true)

def Core.Presupposition.PrProp.strawsonEquiv {W : Type u_1} (p q : PrProp W) : Prop

Strawson equivalence: mutual Strawson entailment.

Equations

• p.strawsonEquiv q = (p.strawsonEntails q ∧ q.strawsonEntails p)

def Core.Presupposition.PrProp.orFlex {W : Type u_1} (p q : PrProp W) : PrProp W

Flexible accommodation disjunction.

Each disjunct is evaluated only against worlds where its own presupposition holds. The overall presupposition is the disjunction of the individual presuppositions. This handles conflicting presuppositions (p ∧ q = ⊥): standard disjunction and filtering disjunction both fail for this case, but flexible accommodation correctly predicts presupposition p ∨ q and allows the disjunction to be false.

Formally, this is the static counterpart of Yagi's dynamic update: s[φ ∨ ψ] = s[χ][φ] ∪ s[ω][ψ], where s[χ] ∪ s[ω] = s When presuppositions conflict, χ = ¬q and ω = ¬p, giving pointwise: (p(w) ∧ φ(w)) ∨ (q(w) ∧ ψ(w))

Equations

• p.orFlex q = { presup := fun (w : W) => p.presup w || q.presup w, assertion := fun (w : W) => p.presup w && p.assertion w || q.presup w && q.assertion w }

theorem Core.Presupposition.PrProp.orFlex_eq_or_when_both_defined {W : Type u_1} (p q : PrProp W) (w : W) (hp : p.presup w = true) (hq : q.presup w = true) : (p.orFlex q).assertion w = (p.or q).assertion w

orFlex reduces to standard disjunction when both presuppositions hold.

theorem Core.Presupposition.PrProp.orFlex_presup_weaker {W : Type u_1} (p q : PrProp W) (w : W) (h : (p.or q).presup w = true) : (p.orFlex q).presup w = true

orFlex presupposition is weaker than or's (p ∨ q vs p ∧ q).

def Core.Presupposition.PrProp.projectPresup {W : Type u_1} (p : PrProp W) : BProp W

Presupposition projection: get the presupposition as a classical proposition.

Equations

• p.projectPresup = p.presup

def Core.Presupposition.PrProp.projectAssertion {W : Type u_1} (p : PrProp W) : BProp W

Assertion extraction: get the assertion as a classical proposition.

Equations

• p.projectAssertion = p.assertion

@[reducible, inline]

abbrev Core.Presupposition.PrProp.assertive {W : Type u_1} (p : PrProp W) : BProp W

Alias for presup under the Belnap reading: whether the proposition is assertive at w (asserts something, vs nonassertive/silent).

Equations

• p.assertive = p.presup

def Core.Presupposition.PrProp.condAssert {W : Type u_1} (A B : BProp W) : PrProp W

Belnap's conditional assertion (A/B): assert B on condition A.

Assertive_w iff A is true at w; what is asserted = B. @cite{belnap-1970}, (3): "(A/B) is assertive_w just in case A is true_w. (A/B)_w = B_w."

Equations

• Core.Presupposition.PrProp.condAssert A B = { presup := A, assertion := B }

def Core.Presupposition.PrProp.andBelnap {W : Type u_1} (p q : PrProp W) : PrProp W

Belnap conjunction: assertive iff at least one conjunct is assertive. What it asserts = conjunction of assertive conjuncts' content.

@cite{belnap-1970}, (8). Contrast with classical PrProp.and (both must be defined) and filtering PrProp.andFilter (left-to-right).

Equations

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

def Core.Presupposition.PrProp.orBelnap {W : Type u_1} (p q : PrProp W) : PrProp W

Belnap disjunction: assertive iff at least one disjunct is assertive. What it asserts = disjunction of assertive disjuncts' content.

@cite{belnap-1970}, (9).

Equations

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

theorem Core.Presupposition.PrProp.eval_andBelnap {W : Type u_1} (p q : PrProp W) (w : W) : (p.andBelnap q).eval w = (p.eval w).meetBelnap (q.eval w)

Belnap conjunction evaluates to Truth3.meetBelnap pointwise.

theorem Core.Presupposition.PrProp.eval_orBelnap {W : Type u_1} (p q : PrProp W) (w : W) : (p.orBelnap q).eval w = (p.eval w).joinBelnap (q.eval w)

Belnap disjunction evaluates to Truth3.joinBelnap pointwise.

def Core.Presupposition.PrProp.ofProp3 {W : Type u_1} (p : Duality.Prop3 W) : PrProp W

Convert a three-valued proposition to a PrProp.

Inverse of PrProp.eval: defined ↔ value ≠ indet, assertion ↔ value = true.

Equations

• Core.Presupposition.PrProp.ofProp3 p = { presup := fun (w : W) => (p w).isDefined, assertion := fun (w : W) => (p w).toBoolOrFalse }

theorem Core.Presupposition.PrProp.eval_ofProp3 {W : Type u_1} (p : Duality.Prop3 W) : (ofProp3 p).eval = p

Prop3 → PrProp → Prop3 round-trip is the identity.