Partial Propositions

Partial propositions — propositions that may be undefined at some evaluation points. References: [Hei83], [Sch09a], [vF99a], [Geu05], [Bel70], [Kar73], [KP79], [Boc37].

Main declarations

• PartialProp W — partial proposition with presup, assertion : W → Prop. The canonical type for partial propositions. Fields are Prop-valued following the mathlib convention.
• PartialValue W α — presupposed value polymorphic in the at-issue content type (α = ℚ for degrees, α = E for entities). Presupposition is also W → Prop.
• Connective families on PartialProp W: classical (and, or, imp, xor), filtering / Karttunen (andFilter, impFilter, orFilter), K&P symmetric disjunction (orKPSymmetric), positive-antecedent disjunction (orPositive, a documented rival), Strong Kleene (andStrong, orStrong — the Truth3 lattice meet/join), and Belnap conditional assertion (andBelnap, orBelnap; the flexible-accommodation andFlex/orFlex are definitionally the same operators). Classical and/or are simultaneously Weak Kleene; the filtering connectives are Peters' middle Kleene ([Pet79], eval_andFilter/eval_orFilter).
• belnapLift — unifier showing Belnap = flexible accommodation for any binary Prop operator with an identity.
• strawsonEntails, strongEntails — entailment relations: the canonical [vF99a] form (presup-as-premise) and the stronger variant that additionally requires q's presupposition to project from p's satisfaction.
• liveness, genuineness — [Yag25] disjunction-update conditions.
• presupOfReferent — definite-description combinator (single source of truth for singular definite denotations).

Implementation notes

PartialProp W is parametric over the evaluation point. Common instantiations: PartialProp World (classical possible worlds), PartialProp (Possibility W E) (dynamic world-assignment pairs).

The choice of connective system (how gaps behave under ∧/∨) is orthogonal to the representation type — see Truth3.GapPolicy. Connectives are paired with eval_* bridge theorems mapping each to the corresponding Truth3 operator on the evaluation.

open Classical is in scope at the namespace level because most theorems case-split on Prop-valued fields. Mathlib uses the same idiom in logic-heavy files such as Mathlib/Order/Filter/Basic.lean.

Todo

• PartialProp W = PartialValue W Prop unification: PartialValue already generalizes PartialProp at the type level; unifying would let the connective zoo lift to arbitrary at-issue carriers.
• evalLift : (Truth3 → Truth3 → Truth3) → (PartialProp W → PartialProp W → PartialProp W) would collapse xor, andBelnap, orBelnap into one definition each, with one bridge theorem instead of eight.

structure Semantics.Presupposition.PartialValue (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.

PartialValue W α generalizes presuppositional propositions: the presupposition is W → Prop, and the at-issue content is any type — a truth value (Bool), a degree (ℚ), a measure, etc.

Linguistic motivation: many presupposition triggers return non-boolean values. The revised per entry ([BS22], eq. 43) returns a presupposed pure number (ℚ). Definite descriptions return presupposed entities. PartialValue handles all of these uniformly.

• presup : W → Prop

  The presupposition (must hold for definedness).

• value : W → α

  The at-issue content (value).

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

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

Equations

• Semantics.Presupposition.PartialValue.defined w pv = pv.presup w

PartialProp: Prop-based partial propositions

structure Semantics.Presupposition.PartialProp (W : Type u_1) : Type u_1

A presuppositional proposition: assertion + presupposition.

Fields are Prop-valued following the Mathlib convention. Construct directly with { presup := ..., assertion := ... }; for finite worlds with DecidableEq, the predicates are auto-decidable.

• presup : W → Prop

  The presupposition (must hold for definedness).

• assertion : W → Prop

  The at-issue content (assertion).

theorem Semantics.Presupposition.PartialProp.ext {W : Type u_1} {x y : PartialProp W} (presup : x.presup = y.presup) (assertion : x.assertion = y.assertion) : x = y

theorem Semantics.Presupposition.PartialProp.ext_iff {W : Type u_1} {x y : PartialProp W} : x = y ↔ x.presup = y.presup ∧ x.assertion = y.assertion

Constructors

def Semantics.Presupposition.PartialProp.ofProp {W : Type u_1} (p : W → Prop) : PartialProp W

Create a presuppositionless proposition from a W → Prop.

Equations

• Semantics.Presupposition.PartialProp.ofProp p = { presup := fun (x : W) => True, assertion := p }

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

Convert a three-valued proposition to a PartialProp. Inverse of PartialProp.eval: defined iff value ≠ indet, assertion iff value = true.

Equations

• Semantics.Presupposition.PartialProp.ofProp3 p = { presup := fun (w : W) => p w ≠ Core.Duality.Truth3.indet, assertion := fun (w : W) => p w = Core.Duality.Truth3.true }

def Semantics.Presupposition.PartialProp.condAssert {W : Type u_1} (A B : W → Prop) : PartialProp W

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

Assertive_w iff A is true at w; what is asserted = B. [Bel70], (3): "(A/B) is assertive_w just in case A is true_w. (A/B)_w = B_w."

Equations

• Semantics.Presupposition.PartialProp.condAssert A B = { presup := A, assertion := B }

Satisfaction relations

def Semantics.Presupposition.PartialProp.holds {W : Type u_1} (w : W) (p : PartialProp W) : Prop

Full satisfaction relation: both presupposition and assertion hold.

Argument order (w : W) (p : PartialProp W) supports updateFromSat: updateFromSat PartialProp.holds p gives the full CCP (presupposition test + assertion filter).

Equations

• Semantics.Presupposition.PartialProp.holds w p = (p.presup w ∧ p.assertion w)

def Semantics.Presupposition.PartialProp.defined {W : Type u_1} (w : W) (p : PartialProp W) : Prop

Definedness relation: presupposition holds at the evaluation point.

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

Equations

• Semantics.Presupposition.PartialProp.defined w p = p.presup w

Constants

def Semantics.Presupposition.PartialProp.top {W : Type u_1} : PartialProp W

Create a tautological presupposition.

Equations

• Semantics.Presupposition.PartialProp.top = { presup := fun (x : W) => True, assertion := fun (x : W) => True }

def Semantics.Presupposition.PartialProp.bot {W : Type u_1} : PartialProp W

Create a contradictory presupposition.

Equations

• Semantics.Presupposition.PartialProp.bot = { presup := fun (x : W) => True, assertion := fun (x : W) => False }

def Semantics.Presupposition.PartialProp.undefined {W : Type u_1} : PartialProp W

Create a presupposition failure (never defined).

Equations

• Semantics.Presupposition.PartialProp.undefined = { presup := fun (x : W) => False, assertion := fun (x : W) => False }

Evaluation

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

Evaluate a presuppositional proposition to three-valued truth. Noncomputable because it decides Prop-valued presupposition and assertion via classical logic.

Equations

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

Classical connectives

def Semantics.Presupposition.PartialProp.neg {W : Type u_1} (p : PartialProp W) : PartialProp W

Classical (internal / choice) negation: a hole. Lets the presupposition through unchanged.

Equations

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

def Semantics.Presupposition.PartialProp.truthOp {W : Type u_1} (p : PartialProp W) : PartialProp W

Bochvar's truth operator t: a plug-as-affirmation ([Boc37]). Always defined; maps presupposition failure to False. [Kar73] §10 fn 18: t(A) has truth-table T → T, F → F, # → F. Composing classical negation with t yields external negation: negExt p = neg (truthOp p).

Equations

• p.truthOp = { presup := fun (x : W) => True, assertion := fun (w : W) => p.presup w ∧ p.assertion w }

def Semantics.Presupposition.PartialProp.negExt {W : Type u_1} (p : PartialProp W) : PartialProp W

Bochvar external (exclusion) negation: a plug. Always defined; true when p is false or undefined, false only when p is true. Equals neg (truthOp p) per [Kar73] §10 fn 18: ⌜¬A⌝ ≡ ⌜~t(A)⌝.

Equations

• p.negExt = p.truthOp.neg

def Semantics.Presupposition.PartialProp.and {W : Type u_1} (p q : PartialProp W) : PartialProp W

Classical conjunction: both presuppositions must hold. This is also Weak Kleene conjunction ([Kle52]: indet is absorbing).

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 Semantics.Presupposition.PartialProp.or {W : Type u_1} (p q : PartialProp W) : PartialProp W

Classical disjunction: both presuppositions must hold. This is also Weak Kleene disjunction ([Kle52]: indet is absorbing) — see eval_or.

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 Semantics.Presupposition.PartialProp.imp {W : Type u_1} (p q : PartialProp W) : PartialProp 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 Semantics.Presupposition.PartialProp.xor {W : Type u_1} (p q : PartialProp W) : PartialProp 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. [WD26]

Equations

• p.xor q = { presup := fun (w : W) => p.presup w ∧ q.presup w, assertion := fun (w : W) => p.assertion w ∧ ¬q.assertion w ∨ ¬p.assertion w ∧ q.assertion w }

Filtering connectives (Karttunen)

def Semantics.Presupposition.PartialProp.andFilter {W : Type u_1} (p q : PartialProp W) : PartialProp W

Filtering conjunction ([Kar73], [Pet79]): the first conjunct can satisfy the second'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 Semantics.Presupposition.PartialProp.impFilter {W : Type u_1} (p q : PartialProp W) : PartialProp W

Filtering implication ([Kar73], [Pet79]): the antecedent can satisfy the 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 Semantics.Presupposition.PartialProp.orFilter {W : Type u_1} (p q : PartialProp W) : PartialProp W

Filtering disjunction (asymmetric, [Kar73]): the negation of the first disjunct can satisfy the second's presupposition — Either there is no bathroom or the bathroom is upstairs is defined because the second disjunct's bathroom presupposition is required only at worlds where the first disjunct is false.

Generalizes disjFilterLeft to a presuppositional first disjunct (orFilter_ofProp). The symmetric K&P variant is orKPSymmetric; the positive-antecedent variant is orPositive.

Equations

• p.orFilter 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 Semantics.Presupposition.PartialProp.«term_/\'_» : Lean.TrailingParserDescr

Equations

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

def Semantics.Presupposition.PartialProp.«term_->'_» : Lean.TrailingParserDescr

Equations

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

def Semantics.Presupposition.PartialProp.«term_\/'_» : Lean.TrailingParserDescr

Equations

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

Positive-antecedent symmetric disjunction

def Semantics.Presupposition.PartialProp.orPositive {W : Type u_1} (p q : PartialProp W) : PartialProp W

Positive-antecedent symmetric disjunction: each disjunct's presupposition is required where the other disjunct's assertion holds, plus at least one disjunct defined. This is NOT Karttunen filtering (orFilter): it demands the second disjunct's presupposition exactly where the first is true, un-filtering bathroom-sentence data. Retained as a documented rival: [Sha25] identifies it as the root cause of K/P-style failure (Studies/Sharvit2025.lean), and [Yag25] §2.2 discusses the Π(φ) ∨ Π(ψ) conjunct as a candidate fix (Studies/Yagi2025.lean).

Equations

• p.orPositive q = { presup := fun (w : W) => (p.assertion w → q.presup w) ∧ (q.assertion w → p.presup w) ∧ (p.presup w ∨ q.presup w), assertion := fun (w : W) => p.assertion w ∨ q.assertion w }

K&P two-dimensional disjunction

def Semantics.Presupposition.PartialProp.orKPSymmetric {W : Type u_1} (p q : PartialProp W) : PartialProp W

Symmetric two-dimensional disjunction in the K&P ([KP79]) tradition:

Π(φ ∨ ψ) = (A(ψ) ∨ Π(φ)) ∧ (A(φ) ∨ Π(ψ)) A(φ ∨ ψ) = A(φ) ∨ A(ψ)

The name carries the Symmetric suffix because the literal K&P 1979 formulation was asymmetric (it would project the first disjunct's presupposition unconditionally; [Yag25] fn 2). This is the symmetrized variant standard in post-2021 literature, matching [Yag25] Definition 2 (cf. [KS21a] for experimental support of symmetry).

Equations

• p.orKPSymmetric q = { presup := fun (w : W) => (q.assertion w ∨ p.presup w) ∧ (p.assertion w ∨ q.presup w), assertion := fun (w : W) => p.assertion w ∨ q.assertion w }

Strong Kleene

def Semantics.Presupposition.PartialProp.orStrong {W : Type u_1} (p q : PartialProp W) : PartialProp W

Strong Kleene disjunction ([Kle52]): defined iff both disjuncts are defined or either is defined-and-true (T ∨ # = T, F ∨ # = #). This is the Truth3 lattice join — see eval_orStrong.

Equations

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

def Semantics.Presupposition.PartialProp.andStrong {W : Type u_1} (p q : PartialProp W) : PartialProp W

Strong Kleene conjunction: defined iff both conjuncts are defined or either is defined-and-false (F ∧ # = F, T ∧ # = #). This is the Truth3 lattice meet — see eval_andStrong.

Equations

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

Belnap conditional assertion ([Bel70])

Under the Belnap reading, presup is the assertive field — whether the proposition asserts something at w (vs being nonassertive / silent).

def Semantics.Presupposition.PartialProp.andBelnap {W : Type u_1} (p q : PartialProp W) : PartialProp W

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

[Bel70], (8). Contrast with classical PartialProp.and (both must be defined) and filtering PartialProp.andFilter (left-to-right).

Equations

• p.andBelnap 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) }

def Semantics.Presupposition.PartialProp.orBelnap {W : Type u_1} (p q : PartialProp W) : PartialProp W

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

[Bel70], (9).

Equations

• p.orBelnap 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 }

Flexible accommodation

The flexible-accommodation connectives of the pragmatic tradition ([Geu05], [Alo22], the static counterpart of [Yag25]'s dynamic update) are definitionally the Belnap connectives: each operand is evaluated only against worlds where its own presupposition holds, which handles conflicting presuppositions (where classical and filtering disjunction both fail). The two traditions differ in the accommodation theory surrounding the operator (default ⊤ vs unconditional assertive), not in the operator itself — see [Yag25] §3.2 for the distinction.

@[reducible, inline]

abbrev Semantics.Presupposition.PartialProp.orFlex {W : Type u_1} : PartialProp W → PartialProp W → PartialProp W

Flexible accommodation disjunction = orBelnap.

Equations

• Semantics.Presupposition.PartialProp.orFlex = Semantics.Presupposition.PartialProp.orBelnap

@[reducible, inline]

abbrev Semantics.Presupposition.PartialProp.andFlex {W : Type u_1} : PartialProp W → PartialProp W → PartialProp W

Flexible accommodation conjunction = andBelnap.

Equations

• Semantics.Presupposition.PartialProp.andFlex = Semantics.Presupposition.PartialProp.andBelnap

noncomputable def Semantics.Presupposition.PartialProp.belnapLift {W : Type u_1} (f : Prop → Prop → Prop) (unit : Prop) (p q : PartialProp W) : PartialProp W

Belnap lift: uniform construction for conditional assertion connectives.

Given a binary Prop function f and its identity element unit, constructs a PartialProp connective where:

• Defined (assertive) iff at least one operand is defined
• Assertion applies f to each operand's content, substituting unit for undefined operands (making them "silent")

[Bel70]: undefined operands contribute the identity element. Noncomputable because it uses classical if on Props.

Defined instances:

• belnapLift (· ∨ ·) False = orBelnap = orFlex (False is identity for ∨)
• belnapLift (· ∧ ·) True = andBelnap = andFlex (True is identity for ∧)

Equations

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

Entailment relations

def Semantics.Presupposition.PartialProp.strawsonEntails {W : Type u_1} (p q : PartialProp W) : Prop

Strawson entailment ([vF99a]): p entails q at every world where both presuppositions hold. The conclusion q's presupposition is a premise added to the entailment, not something the entailment delivers. Matches Semantics.Dynamic.Bilateral.BUS's strawsonEntails (canonical Strawson).

Equations

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

def Semantics.Presupposition.PartialProp.strongEntails {W : Type u_1} (p q : PartialProp W) : Prop

Strong (Strawson-projecting) entailment: at every world where p is defined and true, q is both defined and true. Stronger than strawsonEntails: this variant also requires that q's presupposition projects from p's satisfaction (so it embeds a presupposition-projection burden the canonical von Fintel form exempts).

Equations

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

def Semantics.Presupposition.PartialProp.strawsonEquiv {W : Type u_1} (p q : PartialProp W) : Prop

Strawson equivalence: mutual Strawson entailment.

Equations

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

Genuineness / liveness ([Zim00], [Geu05], [KS12])

def Semantics.Presupposition.PartialProp.liveness {W : Type u_1} (p q : PartialProp W) (s : Finset W) : Prop

Liveness for disjunction: each disjunct is satisfied (presupposition AND assertion hold) at some world of the state.

This is the singleton-survival side of [Yag25] Definition 8: {w}[φ] = {w} for some w ∈ s. The disjunction-update side (w ∈ s[φ ∨ ψ]) is the additional constraint expressed by genuineness below.

Equations

• p.liveness q s = ((∃ w ∈ s, Semantics.Presupposition.PartialProp.holds w p) ∧ ∃ w ∈ s, Semantics.Presupposition.PartialProp.holds w q)

def Semantics.Presupposition.PartialProp.genuineness {W : Type u_1} (disj : PartialProp W → PartialProp W → PartialProp W) (p q : PartialProp W) (s : Finset W) : Prop

Genuineness for disjunction ([Yag25] Definition 8, after [Zim00]). A disjunction p ∨ q, with disjunction-update realised by the connective disj, follows genuineness in a state s iff there are worlds w, w' ∈ s such that:

• {w}[p] = {w} AND w ∈ s[p ∨ q] — the left disjunct's witness survives both its own update (= p.holds w) and the disjunction's update (= disj.holds w).
• {w'}[q] = {w'} AND w' ∈ s[p ∨ q] — analogously for the right disjunct.

The disjunction-update side rules out witnesses that survive the local presupposition+assertion update but are eliminated by the joint update — a vacuous addition under orFlex/orBelnap (liveness_implies_genuineness_orFlex), but the substantive constraint [Yag25] §3.2 invokes for dynamic negation: genuineness must hold even within the scope of negation, where "we end up negating both disjuncts".

The disj argument is parametric so the substrate stays framework-neutral; consumers supply the disjunction connective whose update they wish to test against (orFlex / classical or / Geurts modal split).

Equations

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

theorem Semantics.Presupposition.PartialProp.liveness_implies_genuineness_orFlex {W : Type u_1} (p q : PartialProp W) (s : Finset W) (h : p.liveness q s) : genuineness orFlex p q s

Under orFlex, liveness implies genuineness: each witness for p.holds/q.holds automatically survives the disjunction's update, because (orFlex p q).holds w reduces to p.holds w ∨ q.holds w.

Negation theorems

@[simp]

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

Negation preserves presupposition.

theorem Semantics.Presupposition.PartialProp.neg_neg_assertion {W : Type u_1} (p : PartialProp W) (w : W) : p.neg.neg.assertion w ↔ p.assertion w

Double negation restores assertion (classical).

@[simp]

theorem Semantics.Presupposition.PartialProp.neg_neg {W : Type u_1} (p : PartialProp W) : p.neg.neg = p

Double negation identity.

@[simp]

theorem Semantics.Presupposition.PartialProp.truthOp_presup {W : Type u_1} (p : PartialProp W) (w : W) : p.truthOp.presup w

The truth operator is always defined (it's a plug).

@[simp]

theorem Semantics.Presupposition.PartialProp.negExt_presup {W : Type u_1} (p : PartialProp W) (w : W) : p.negExt.presup w

External negation is always defined (it's a plug).

theorem Semantics.Presupposition.PartialProp.neg_assertion_iff_negExt_assertion_when_defined {W : Type u_1} (p : PartialProp W) (w : W) (h : p.presup w) : p.neg.assertion w ↔ p.negExt.assertion w

Internal and external negation agree on assertion when the presupposition holds. They diverge only at presupposition failure: neg p is undefined, negExt p is true. [Kar73] §10 fn 18.

theorem Semantics.Presupposition.PartialProp.negExt_assertion {W : Type u_1} (p : PartialProp W) (w : W) : p.negExt.assertion w ↔ ¬p.truthOp.assertion w

External negation has the dual assertion to the truth operator at every world: negExt = ¬truthOp extensionally, by definition (negExt = neg ∘ truthOp and neg is ¬ on assertion).

theorem Semantics.Presupposition.PartialProp.negExt_assertion_of_presup_failure {W : Type u_1} (p : PartialProp W) (w : W) (h : ¬p.presup w) : p.negExt.assertion w

Karttunen §10 fn 18 truth table for external negation, presup-failure case: when p's presupposition fails, negExt p is true (the plug behavior).

Filtering theorems

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

Filtering implication eliminates presupposition when antecedent entails it.

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

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

theorem Semantics.Presupposition.PartialProp.impFilter_presup_eq_andFilter_presup {W : Type u_1} (p q : PartialProp W) : (p.impFilter q).presup = (p.andFilter q).presup

The filtering presupposition of impFilter and andFilter are identical. This is the formal content of [Kar73] §8: the filtering rules for if A then B and A and B coincide because both reduce to p.presup ∧ (p.assertion → q.presup).

Evaluation theorems

@[simp]

theorem Semantics.Presupposition.PartialProp.eval_isDefined {W : Type u_1} (p : PartialProp W) (w : W) : (p.eval w).isDefined ↔ p.presup w

Evaluation is defined iff presupposition holds.

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

Negation evaluation.

theorem Semantics.Presupposition.PartialProp.eval_and {W : Type u_1} (p q : PartialProp W) (w : W) (hp : p.presup w) (hq : q.presup w) : (p.and q).eval w = min (p.eval w) (q.eval w)

Classical conjunction evaluation (both defined).

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

Filtering implication when antecedent false: result is true.

theorem Semantics.Presupposition.PartialProp.eval_impFilter_antecedent_true {W : Type u_1} (p q : PartialProp W) (w : W) (hp : p.presup w) (ha : p.assertion w) (hq : q.presup w) : (p.impFilter q).eval w = if q.assertion w then Core.Duality.Truth3.true else Core.Duality.Truth3.false

Filtering implication when antecedent true: depends on consequent.

theorem Semantics.Presupposition.PartialProp.eval_orStrong {W : Type u_1} (p q : PartialProp W) (w : W) : (p.orStrong q).eval w = max (p.eval w) (q.eval w)

orStrong evaluates to the Truth3 lattice join pointwise: Strong Kleene disjunction is ⊔ in the false < indet < true order, unconditionally.

theorem Semantics.Presupposition.PartialProp.eval_andStrong {W : Type u_1} (p q : PartialProp W) (w : W) : (p.andStrong q).eval w = min (p.eval w) (q.eval w)

andStrong evaluates to the Truth3 lattice meet pointwise, unconditionally.

theorem Semantics.Presupposition.PartialProp.eval_andFilter {W : Type u_1} (p q : PartialProp W) (w : W) : (p.andFilter q).eval w = (p.eval w).meetMiddle (q.eval w)

Karttunen filtering conjunction is Peters' middle Kleene ([Pet79]): andFilter evaluates to the asymmetric Truth3.meetMiddle on both dimensions, unconditionally.

theorem Semantics.Presupposition.PartialProp.eval_orFilter {W : Type u_1} (p q : PartialProp W) (w : W) : (p.orFilter q).eval w = (p.eval w).joinMiddle (q.eval w)

Karttunen filtering disjunction is Peters' middle Kleene ([Pet79]): orFilter evaluates to the asymmetric Truth3.joinMiddle on both dimensions, unconditionally.

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

Exclusive disjunction evaluation matches Truth3.xor when both defined.

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

Exclusive disjunction never filters: when either presupposition fails, the result is undefined. [WD26]

orKPSymmetric theorem

theorem Semantics.Presupposition.PartialProp.orKPSymmetric_presup_entails_when_conflicting {W : Type u_1} (p q : PartialProp W) (w : W) (h_conflict : ¬(p.presup w ∧ q.presup w)) (h_presup : (p.orKPSymmetric q).presup w) : (p.orKPSymmetric q).assertion w

When presuppositions conflict at w, the symmetric K&P presupposition entails the assertion: defined → true, so the disjunction can never be both defined and false. [Yag25] §2.2

Flex collapse theorems

theorem Semantics.Presupposition.PartialProp.orFlex_eq_or_when_both_defined {W : Type u_1} (p q : PartialProp W) (w : W) (hp : p.presup w) (hq : q.presup w) : (p.orFlex q).assertion w ↔ (p.or q).assertion w

orFlex reduces to standard disjunction when both presuppositions hold.

theorem Semantics.Presupposition.PartialProp.orFlex_presup_weaker {W : Type u_1} (p q : PartialProp W) (w : W) (h : (p.or q).presup w) : (p.orFlex q).presup w

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

theorem Semantics.Presupposition.PartialProp.andFlex_eq_and_when_both_defined {W : Type u_1} (p q : PartialProp W) (w : W) (hp : p.presup w) (hq : q.presup w) : (p.andFlex q).assertion w ↔ (p.and q).assertion w

andFlex reduces to standard conjunction when both presuppositions hold.

theorem Semantics.Presupposition.PartialProp.andFlex_presup_weaker {W : Type u_1} (p q : PartialProp W) (w : W) (h : (p.and q).presup w) : (p.andFlex q).presup w

andFlex presupposition is weaker than and's (p ∨ q vs p ∧ q).

Eval: Weak Kleene / Belnap

theorem Semantics.Presupposition.PartialProp.eval_or {W : Type u_1} (p q : PartialProp W) (w : W) : (p.or q).eval w = (p.eval w).joinWeak (q.eval w)

or evaluates to Truth3.joinWeak pointwise (classical disjunction is Weak Kleene).

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

Belnap conjunction evaluates to Truth3.meetBelnap pointwise.

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

Belnap disjunction evaluates to Truth3.joinBelnap pointwise.

Belnap lift: unification

theorem Semantics.Presupposition.PartialProp.orBelnap_eq_belnapLift {W : Type u_1} (p q : PartialProp W) : p.orBelnap q = belnapLift (fun (x1 x2 : Prop) => x1 ∨ x2) False p q

orBelnap is the Belnap lift of (· ∨ ·) with identity False.

theorem Semantics.Presupposition.PartialProp.andBelnap_eq_belnapLift {W : Type u_1} (p q : PartialProp W) : p.andBelnap q = belnapLift (fun (x1 x2 : Prop) => x1 ∧ x2) True p q

andBelnap is the Belnap lift of (· ∧ ·) with identity True.

theorem Semantics.Presupposition.PartialProp.belnapLift_eq_classical {W : Type u_1} (f : Prop → Prop → Prop) (unit : Prop) (p q : PartialProp W) (w : W) (hp : p.presup w) (hq : q.presup w) : (belnapLift f unit p q).assertion w = f (p.assertion w) (q.assertion w)

Belnap lift reduces to the classical operation when both presuppositions hold. The identity element is never used — both operands contribute directly.

theorem Semantics.Presupposition.PartialProp.belnapLift_right_undefined {W : Type u_1} (f : Prop → Prop → Prop) (unit : Prop) (hunit : ∀ (b : Prop), f b unit = b) (p q : PartialProp W) (w : W) (hp : p.presup w) (hq : ¬q.presup w) : (belnapLift f unit p q).assertion w = p.assertion w

When only the left operand is defined and unit is a right identity, belnapLift returns the left operand's value: the right operand is invisible.

theorem Semantics.Presupposition.PartialProp.belnapLift_left_undefined {W : Type u_1} (f : Prop → Prop → Prop) (unit : Prop) (hunit : ∀ (b : Prop), f unit b = b) (p q : PartialProp W) (w : W) (hp : ¬p.presup w) (hq : q.presup w) : (belnapLift f unit p q).assertion w = q.assertion w

When only the right operand is defined and unit is a left identity, belnapLift returns the right operand's value.

theorem Semantics.Presupposition.PartialProp.belnapLift_comm {W : Type u_1} (f : Prop → Prop → Prop) (hcomm : ∀ (a b : Prop), f a b = f b a) (unit : Prop) (p q : PartialProp W) : belnapLift f unit p q = belnapLift f unit q p

belnapLift is commutative when f is commutative.

Collapse: all connective families agree when both defined

theorem Semantics.Presupposition.PartialProp.all_or_agree_when_both_defined {W : Type u_1} (p q : PartialProp W) (w : W) (hp : p.presup w) (hq : q.presup w) : ((p.or q).assertion w ↔ (p.orFilter q).assertion w) ∧ ((p.or q).assertion w ↔ (p.orPositive q).assertion w) ∧ ((p.or q).assertion w ↔ (p.orKPSymmetric q).assertion w) ∧ ((p.or q).assertion w ↔ (p.orFlex q).assertion w)

When both presuppositions hold at w, ALL disjunction connectives agree on assertion: classical = filtering = K&P = flex = Belnap. The theories diverge only when presuppositions conflict.

theorem Semantics.Presupposition.PartialProp.all_and_agree_when_both_defined {W : Type u_1} (p q : PartialProp W) (w : W) (hp : p.presup w) (hq : q.presup w) : ((p.and q).assertion w ↔ (p.andFilter q).assertion w) ∧ ((p.and q).assertion w ↔ (p.andFlex q).assertion w)

When both presuppositions hold at w, ALL conjunction connectives agree on assertion: classical = filtering = flex = Belnap. The theories diverge only when presuppositions conflict.

Round-trip: Prop3 ↔ PartialProp

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

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

Genuineness theorems

theorem Semantics.Presupposition.PartialProp.liveness_comm {W : Type u_1} (p q : PartialProp W) (s : Finset W) : p.liveness q s ↔ q.liveness p s

Liveness is symmetric.

theorem Semantics.Presupposition.PartialProp.genuineness_comm {W : Type u_1} (disj : PartialProp W → PartialProp W → PartialProp W) (p q : PartialProp W) (s : Finset W) (hcomm : disj p q = disj q p) : genuineness disj p q s ↔ genuineness disj q p s

Genuineness is symmetric whenever the supplied disjunction connective is symmetric in its operands.

Embedding combinators ([Hei92], [Kar73], [DPBS24])

def Semantics.Presupposition.PartialProp.disjFilterLeft {W : Type u_1} (firstDisjunct : W → Prop) (second : PartialProp W) : PartialProp W

Asymmetric filtering disjunction: plain proposition ∨ PartialProp.

For "A ∨ B_ψ" where only B carries a presupposition ψ, the overall presupposition is ¬A → ψ (Karttunen's generalization for disjunction). The assertion is A ∨ B.

This is the standard projection rule for presuppositions in the second disjunct of a disjunction. [Kar73], [Hei83]

Equations

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

theorem Semantics.Presupposition.PartialProp.orFilter_ofProp {W : Type u_1} (A : W → Prop) (q : PartialProp W) : (ofProp A).orFilter q = disjFilterLeft A q

orFilter with a presuppositionless first disjunct is disjFilterLeft.

def Semantics.Presupposition.PartialProp.negFactive {W : Type u_1} (complement : PartialProp W) (believes : (W → Prop) → W → Prop) : PartialProp W

Embedding under a negative factive (e.g., "is unaware that").

"x is unaware that p" presupposes p and asserts ¬Bel_x(p).

The choice of complement.holds (presupposition AND assertion) for the factive's presupposition is the [DPBS24] treatment, where projection-through-factive requires both the trigger's presupposition and the at-issue complement to be carried. The [Hei92] standard for atomic complements is complement.assertion alone; the two coincide when complement itself carries no presupposition but diverge when the complement contains its own embedded presupposition trigger (the case Del Pinal-Bassi-Sauerland use to handle presupposed free choice).

Equations

• complement.negFactive believes = { presup := fun (w : W) => Semantics.Presupposition.PartialProp.holds w complement, assertion := fun (w : W) => ¬believes complement.assertion w }

theorem Semantics.Presupposition.PartialProp.disjFilterLeft_recovers {W : Type u_1} (firstDisjunct : W → Prop) (sp : PartialProp W) (w : W) (hFirst : ¬firstDisjunct w) (hFiltered : holds w (disjFilterLeft firstDisjunct sp)) : holds w sp

When the first disjunct is false, disjFilterLeft recovers full satisfaction of the second disjunct.

theorem Semantics.Presupposition.PartialProp.disjFilterLeft_eliminates_presup_when_neg_entails {W : Type u_1} (A : W → Prop) (q : PartialProp W) (h : ∀ (w : W), ¬A w → q.presup w) : (disjFilterLeft A q).presup = fun (x : W) => True

When ¬A entails q's presupposition pointwise, disjFilterLeft A q is presuppositionless (the filtering condition is satisfied at every world). The substrate-side fact behind [Kar73]'s asymmetric disjunction filtering rule (24b), p. 181: "A or B" carries no residual presupposition from B when ¬A entails it.

theorem Semantics.Presupposition.PartialProp.negFactive_presup_eq {W : Type u_1} (complement : PartialProp W) (believes : (W → Prop) → W → Prop) : (complement.negFactive believes).presup = fun (w : W) => holds w complement

Presupposition of negFactive is full satisfaction of the complement.

def Semantics.Presupposition.PartialProp.forallPartial {W : Type u_1} {α : Type u_2} (S : α → Prop) (φ : α → PartialProp W) : PartialProp W

Universal presupposition projection: presuppositions project universally from the scope of a universal quantifier.

For ∀x ∈ S, φ(x) where φ(x) is a PartialProp:

• asserts: ∀x ∈ S, assertion(φ(x))
• presupposes: ∀x ∈ S, presup(φ(x))

[Che09a], [Fox13]: presuppositions triggered in the scope of a universal quantifier tend to project universally. ([MS15b] dissent: semantic projection is existential, pragmatically strengthened — cf. [SS17].)

Equations

• Semantics.Presupposition.PartialProp.forallPartial S φ = { presup := fun (w : W) => ∀ (x : α), S x → (φ x).presup w, assertion := fun (w : W) => ∀ (x : α), S x → (φ x).assertion w }

def Semantics.Presupposition.PartialProp.existsPartialUniv {W : Type u_1} {α : Type u_2} (S : α → Prop) (φ : α → PartialProp W) : PartialProp W

Existential presupposition projection — universal presup, existential assert.

For ∃x ∈ S, φ(x): presuppositions project universally, but the assertion is existential. This is the projection choice supported experimentally by [Che09a]; whether it is the right default is empirically contested — see [SS17] for conditions under which a non-universal (existential) reading is preferred. Consumers committing to a projection theory should pick existsPartialUniv or existsPartialExist explicitly.

Equations

• Semantics.Presupposition.PartialProp.existsPartialUniv S φ = { presup := fun (w : W) => ∀ (x : α), S x → (φ x).presup w, assertion := fun (w : W) => ∃ (x : α), S x ∧ (φ x).assertion w }

def Semantics.Presupposition.PartialProp.existsPartialExist {W : Type u_1} {α : Type u_2} (S : α → Prop) (φ : α → PartialProp W) : PartialProp W

Existential presupposition projection — existential presup, existential assert. The non-universal alternative to existsPartialUniv; see [SS17] for the empirical debate.

Equations

• Semantics.Presupposition.PartialProp.existsPartialExist S φ = { presup := fun (w : W) => ∃ (x : α), S x ∧ (φ x).presup w, assertion := fun (w : W) => ∃ (x : α), S x ∧ (φ x).assertion w }

def Semantics.Presupposition.PartialProp.negExistsPartial {W : Type u_1} {α : Type u_2} (S : α → Prop) (φ : α → PartialProp W) : PartialProp W

Negated existential with universal presupposition projection.

For ¬∃x ∈ S, φ(x): equivalent to ∀x ∈ S, ¬φ(x). Presuppositions project universally.

Equations

• Semantics.Presupposition.PartialProp.negExistsPartial S φ = { presup := fun (w : W) => ∀ (x : α), S x → (φ x).presup w, assertion := fun (w : W) => ¬∃ (x : α), S x ∧ (φ x).assertion w }

theorem Semantics.Presupposition.PartialProp.forallPartial_holds {W : Type u_1} {α : Type u_2} (S : α → Prop) (φ : α → PartialProp W) (w : W) : holds w (forallPartial S φ) ↔ (∀ (x : α), S x → (φ x).presup w) ∧ ∀ (x : α), S x → (φ x).assertion w

forallPartial holds iff every member satisfies both presupposition and assertion.

Definite-description combinator

def Semantics.Presupposition.PartialProp.presupOfReferent {W : Type u_1} {E : Type u_2} (referent : W → Option E) (scope : E → W → Prop) : PartialProp W

The canonical definite-description combinator. Given:

• referent : W → Option E — a partial selector returning the referent at each world (or none when no unique referent is determined),
• scope : E → W → Prop — what is asserted of the chosen referent,

build the PartialProp that presupposes referent definedness and asserts the scope of the referent. This is the single source of truth for all definite denotations in the library: uniqueness-based (russellIotaList domain R), familiarity-based (russellIotaList dc.salient R), anaphoric (russellIotaList domain (R ∧ Q)), and Donnellan's attributive (attributiveContent domain R) all instantiate the selector slot.

Equations

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

@[simp]

theorem Semantics.Presupposition.PartialProp.presupOfReferent_presup {W : Type u_1} {E : Type u_2} (referent : W → Option E) (scope : E → W → Prop) (w : W) : (presupOfReferent referent scope).presup w = ((referent w).isSome = true)

presupOfReferent is defined iff a referent is selected at w.

theorem Semantics.Presupposition.PartialProp.presupOfReferent_assertion_some {W : Type u_1} {E : Type u_2} (referent : W → Option E) (scope : E → W → Prop) (w : W) (e : E) (h : referent w = some e) : (presupOfReferent referent scope).assertion w = scope e w

When a referent is selected, the assertion is the scope applied to it.

theorem Semantics.Presupposition.PartialProp.presupOfReferent_assertion_none {W : Type u_1} {E : Type u_2} (referent : W → Option E) (scope : E → W → Prop) (w : W) (h : referent w = none) : (presupOfReferent referent scope).assertion w = False

Without a referent, the assertion is False.