Partial Propositions

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

Partial propositions — propositions that may be undefined at some evaluation points.

PrProp W: presup : W → Prop, assertion : W → Prop. The canonical type for partial propositions. Following the Mathlib convention, fields are Prop-valued; use open Classical + by_cases for case splits. For finite worlds with DecidableEq, the predicates are auto-decidable and PrProp.eval reduces via if_pos/if_neg.

PrValue W α (Bool-based presupposition, polymorphic value): a separate type for presupposed non-boolean values (degrees, entities, etc.).

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

Satisfaction relations

• PrProp.defined w p — presupposition holds at w
• PrProp.holds w p — both presupposition and assertion hold

Connective systems

The choice of connective system (how gaps behave under ∧/∨) is orthogonal to the representation type — see Truth3.GapPolicy. The full set is provided: classical, filtering (Karttunen), Belnap, flexible, Weak Kleene, K&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 presuppositional propositions: 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.

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 Core.Presupposition.PrProp.ext_iff {W : Type u_1} {x y : PrProp W} : x = y ↔ x.presup = y.presup ∧ x.assertion = y.assertion

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

def Core.Presupposition.PrProp.ofProp' {W : Type u_1} (p : W → Prop) : PrProp W

Create a presuppositionless proposition from a W → Prop.

Equations

• Core.Presupposition.PrProp.ofProp' p = { presup := fun (x : W) => True, assertion := p }

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 iff value ≠ indet, assertion iff value = true.

Equations

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

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 := fun (w : W) => pv.presup w = true, assertion := fun (w : W) => pv.value w = true }

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

Convert a PrProp to a PrValue W Bool (noncomputable — requires deciding Props to produce Bool values).

Equations

• p.toPrValue = { presup := fun (w : W) => decide (p.presup w), value := fun (w : W) => decide (p.assertion w) }

def Core.Presupposition.PrProp.condAssert {W : Type u_1} (A B : W → Prop) : 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.holds {W : Type u_1} (w : W) (p : PrProp W) : Prop

Full satisfaction relation: both presupposition and assertion hold.

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

Equations

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

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) supports updateFromSat: updateFromSat PrProp.defined p gives the presupposition test CCP.

Equations

• Core.Presupposition.PrProp.defined w p = p.presup w

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 }

noncomputable def Core.Presupposition.PrProp.eval {W : Type u_1} (p : PrProp W) : 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

def Core.Presupposition.PrProp.neg {W : Type u_1} (p : PrProp W) : PrProp 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 Core.Presupposition.PrProp.truthOp {W : Type u_1} (p : PrProp W) : PrProp W

Bochvar's truth operator t: a plug-as-affirmation. Always defined; maps presupposition failure to False. @cite{karttunen-1973} §10 footnote 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 Core.Presupposition.PrProp.negExt {W : Type u_1} (p : PrProp W) : PrProp 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 @cite{karttunen-1973} §10 fn 18: ⌜¬A⌝ ≡ ⌜~t(A)⌝.

Equations

• p.negExt = p.truthOp.neg

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.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 ∨ ¬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

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

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.

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

K&P two-dimensional disjunction (@cite{karttunen-peters-1979}).

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

Uses the symmetric version from @cite{yagi-2025} Definition 2 (cf. @cite{kalomoiros-schwarz-2021} for experimental support of symmetry).

Equations

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

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

Weak Kleene disjunction: undefined iff either operand undefined. Both disjuncts must be defined for the disjunction to be defined.

@cite{kleene-1952}: indet is absorbing for both ∧ and ∨.

Equations

• p.orWeak 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.andWeak {W : Type u_1} (p q : PrProp W) : PrProp W

Weak Kleene conjunction.

Equations

• p.andWeak 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.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 @cite{yagi-2025}'s dynamic update.

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 }

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

Flexible accommodation conjunction.

Each conjunct is evaluated only against worlds where its own presupposition holds. Undefined conjuncts are vacuously true (the identity element for ∧), so they don't constrain the result. Dual of orFlex.

Equations

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

@[reducible, inline]

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

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.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

• 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 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

• 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 }

noncomputable def Core.Presupposition.PrProp.belnapLift {W : Type u_1} (f : Prop → Prop → Prop) (id : Prop) (p q : PrProp W) : PrProp W

Belnap lift: uniform construction for conditional assertion connectives.

Given a binary Prop function f and its identity element id, constructs a PrProp connective where:

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

@cite{belnap-1970}: 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.

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 → q.presup w → p.assertion w → q.assertion w

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 → p.assertion w → q.presup w ∧ (q.presup w → q.assertion w)

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.liveness {W : Type u_1} (p q : PrProp 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 @cite{yagi-2025} 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, Core.Presupposition.PrProp.holds w p) ∧ ∃ w ∈ s, Core.Presupposition.PrProp.holds w q)

def Core.Presupposition.PrProp.genuineness {W : Type u_1} (p q : PrProp W) (s : Finset W) (disj : PrProp W) : Prop

Genuineness for disjunction (@cite{yagi-2025} Definition 8, after @cite{zimmermann-2000}). 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 @cite{yagi-2025} §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 / orBelnap / classical or / Geurts modal split).

Equations

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

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

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.

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

Presupposition projection: get the presupposition as a W → Prop.

Equations

• p.projectPresup = p.presup

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

Assertion extraction: get the assertion as a W → Prop.

Equations

• p.projectAssertion = p.assertion

theorem Core.Presupposition.PrProp.ext_pointwise {W : Type u_1} {p q : PrProp W} (h₁ : ∀ (w : W), p.presup w ↔ q.presup w) (h₂ : ∀ (w : W), p.assertion w ↔ q.assertion w) : p = q

Extensionality for PrProp via pointwise ↔.

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_presup_eq {W : Type u_1} (p : PrProp W) (w : W) : p.neg.presup w ↔ p.presup w

Presupposition projects through negation (by construction).

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 restores assertion (classical).

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

Double negation identity.

@[simp]

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

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

@[simp]

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

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

theorem Core.Presupposition.PrProp.neg_assertion_iff_negExt_assertion_when_defined {W : Type u_1} (p : PrProp 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. @cite{karttunen-1973} §10 fn 18.

theorem Core.Presupposition.PrProp.negExt_assertion {W : Type u_1} (p : PrProp 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 Core.Presupposition.PrProp.negExt_assertion_of_presup_failure {W : Type u_1} (p : PrProp 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).

theorem Core.Presupposition.PrProp.impFilter_eliminates_presup {W : Type u_1} (p q : PrProp 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 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.

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

The filtering presupposition of impFilter and andFilter are identical. This is the formal content of @cite{karttunen-1973} §8: the filtering rules for if A then B and A and B coincide because both reduce to p.presup ∧ (p.assertion → q.presup).

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.

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) (hq : q.presup w) : (p.and q).eval w = min (p.eval w) (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) (ha : ¬p.assertion w) : (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) (ha : p.assertion w) (hq : q.presup w) : (p.impFilter q).eval w = if q.assertion w then Duality.Truth3.true else Duality.Truth3.false

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) (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 Core.Presupposition.PrProp.eval_xor_no_filter {W : Type u_1} (p q : PrProp W) (w : W) (hq : ¬q.presup w) : (p.xor q).eval w = Duality.Truth3.indet

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

theorem Core.Presupposition.PrProp.orKP_presup_entails_when_conflicting {W : Type u_1} (p q : PrProp W) (w : W) (h_conflict : ¬(p.presup w ∧ q.presup w)) (h_presup : (p.orKP q).presup w) : (p.orKP q).assertion w

When presuppositions conflict at w, K&P's presupposition entails the assertion: defined → true, so the disjunction can never be both defined and false. @cite{yagi-2025} §2.2

theorem Core.Presupposition.PrProp.orFlex_eq_orBelnap {W : Type u_1} (p q : PrProp W) : p.orFlex q = p.orBelnap q

Flexible accommodation disjunction IS Belnap disjunction. The two concepts, developed independently (@cite{belnap-1970} vs @cite{geurts-2005}/@cite{aloni-2022}), produce identical truth conditions.

theorem Core.Presupposition.PrProp.andFlex_eq_andBelnap {W : Type u_1} (p q : PrProp W) : p.andFlex q = p.andBelnap q

Flexible accommodation conjunction IS Belnap conjunction. Extends orFlex_eq_orBelnap: the flex = Belnap identity holds for all binary connectives, not just disjunction.

theorem Core.Presupposition.PrProp.orWeak_eq_or {W : Type u_1} (p q : PrProp W) : p.orWeak q = p.or q

orWeak agrees with or — they have the same definition for inclusive disjunction, since both require both presuppositions.

theorem Core.Presupposition.PrProp.andWeak_eq_and {W : Type u_1} (p q : PrProp W) : p.andWeak q = p.and q

andWeak agrees with and — they have the same definition for conjunction, since both require both presuppositions.

theorem Core.Presupposition.PrProp.orFlex_eq_or_when_both_defined {W : Type u_1} (p q : PrProp 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 Core.Presupposition.PrProp.orFlex_presup_weaker {W : Type u_1} (p q : PrProp 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 Core.Presupposition.PrProp.andFlex_eq_and_when_both_defined {W : Type u_1} (p q : PrProp 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 Core.Presupposition.PrProp.andFlex_presup_weaker {W : Type u_1} (p q : PrProp 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).

theorem Core.Presupposition.PrProp.eval_orWeak {W : Type u_1} (p q : PrProp W) (w : W) : (p.orWeak q).eval w = (p.eval w).joinWeak (q.eval w)

orWeak evaluates to Truth3.joinWeak pointwise.

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.

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

orFlex evaluates to Truth3.joinBelnap pointwise. Corollary of orFlex_eq_orBelnap + eval_orBelnap.

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

andFlex evaluates to Truth3.meetBelnap pointwise.

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

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

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

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

theorem Core.Presupposition.PrProp.orFlex_eq_belnapLift {W : Type u_1} (p q : PrProp W) : p.orFlex q = belnapLift (fun (x1 x2 : Prop) => x1 ∨ x2) False p q

orFlex is the Belnap lift of (· ∨ ·) with identity False. Corollary: flexible accommodation = conditional assertion = Belnap lift, all three for any binary connective.

theorem Core.Presupposition.PrProp.andFlex_eq_belnapLift {W : Type u_1} (p q : PrProp W) : p.andFlex q = belnapLift (fun (x1 x2 : Prop) => x1 ∧ x2) True p q

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

theorem Core.Presupposition.PrProp.belnapLift_eq_classical {W : Type u_1} (f : Prop → Prop → Prop) (id : Prop) (p q : PrProp W) (w : W) (hp : p.presup w) (hq : q.presup w) : (belnapLift f id 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 Core.Presupposition.PrProp.belnapLift_right_undefined {W : Type u_1} (f : Prop → Prop → Prop) (id : Prop) (hid : ∀ (b : Prop), f b id = b) (p q : PrProp W) (w : W) (hp : p.presup w) (hq : ¬q.presup w) : (belnapLift f id p q).assertion w = p.assertion w

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

theorem Core.Presupposition.PrProp.belnapLift_left_undefined {W : Type u_1} (f : Prop → Prop → Prop) (id : Prop) (hid : ∀ (b : Prop), f id b = b) (p q : PrProp W) (w : W) (hp : ¬p.presup w) (hq : q.presup w) : (belnapLift f id p q).assertion w = q.assertion w

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

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

belnapLift is commutative when f is commutative.

theorem Core.Presupposition.PrProp.all_or_agree_when_both_defined {W : Type u_1} (p q : PrProp 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.orKP q).assertion w) ∧ ((p.or q).assertion w ↔ (p.orFlex q).assertion w) ∧ ((p.or q).assertion w ↔ (p.orBelnap q).assertion w) ∧ ((p.or q).assertion w ↔ (p.orWeak 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 Core.Presupposition.PrProp.all_and_agree_when_both_defined {W : Type u_1} (p q : PrProp 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) ∧ ((p.and q).assertion w ↔ (p.andBelnap q).assertion w) ∧ ((p.and q).assertion w ↔ (p.andWeak 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.

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.

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

Liveness is symmetric.

theorem Core.Presupposition.PrProp.genuineness_comm {W : Type u_1} (p q : PrProp W) (s : Finset W) (disj : PrProp W) : p.genuineness q s disj ↔ q.genuineness p s disj

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

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

Asymmetric filtering disjunction: plain proposition ∨ PrProp.

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. @cite{karttunen-1973}, @cite{heim-1983}

Equations

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

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

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

"x is unaware that p" presupposes p and asserts ¬Bel_x(p). When the complement is a PrProp, the factive presupposes both the assertion and presupposition of its complement (i.e., full satisfaction), and asserts that the subject doesn't believe the assertive component.

@cite{heim-1992}: factives presuppose their complement. @cite{delpinal-bassi-sauerland-2024} §3: this is what makes pex solve the presupposed FC puzzle — the homogeneity presupposition projects through the factive independently of the belief content.

Equations

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

theorem Core.Presupposition.PrProp.disjFilterLeft_recovers {W : Type u_1} (firstDisjunct : W → Prop) (sp : PrProp 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 Core.Presupposition.PrProp.disjFilterLeft_eliminates_presup_when_neg_entails {W : Type u_1} (A : W → Prop) (q : PrProp 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 @cite{karttunen-1973}'s asymmetric disjunction filtering rule (24b), p. 181: "A or B" carries no residual presupposition from B when ¬A entails it.

theorem Core.Presupposition.PrProp.negFactive_presup_eq {W : Type u_1} (complement : PrProp 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 Core.Presupposition.PrProp.forallPr {W : Type u_1} {α : Type u_2} (S : α → Prop) (φ : α → PrProp W) : PrProp W

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

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

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

@cite{chemla-2009a}, @cite{fox-2013}, @cite{mayr-sauerland-2015}: presuppositions triggered in the scope of a universal quantifier tend to project universally.

Equations

• Core.Presupposition.PrProp.forallPr S φ = { presup := fun (w : W) => ∀ (x : α), S x → (φ x).presup w, assertion := fun (w : W) => ∀ (x : α), S x → (φ x).assertion w }

def Core.Presupposition.PrProp.existsPrUniv {W : Type u_1} {α : Type u_2} (S : α → Prop) (φ : α → PrProp W) : PrProp W

Existential presupposition projection (universal presup, existential assert).

For ∃x ∈ S, φ(x): presuppositions still project universally, but the assertion is existential.

This models the pattern where ∃x ∈ S(φ(x)) presupposes ∀x ∈ S(presup(φ(x))) — the "universal projection from existential quantifier" pattern supported by @cite{chemla-2009a}.

Equations

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

def Core.Presupposition.PrProp.negExistsPr {W : Type u_1} {α : Type u_2} (S : α → Prop) (φ : α → PrProp W) : PrProp W

Negated existential with universal presupposition projection.

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

Equations

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

theorem Core.Presupposition.PrProp.forallPr_holds {W : Type u_1} {α : Type u_2} (S : α → Prop) (φ : α → PrProp W) (w : W) : holds w (forallPr S φ) ↔ (∀ (x : α), S x → (φ x).presup w) ∧ ∀ (x : α), S x → (φ x).assertion w

forallPr holds iff every member satisfies both presupposition and assertion.

def Core.Presupposition.PrProp.presupOfReferent {W : Type u_1} {E : Type u_2} (referent : W → Option E) (scope : E → W → Bool) : PrProp 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 → Bool — what is asserted of the chosen referent,

build the PrProp 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 Core.Presupposition.PrProp.presupOfReferent_presup {W : Type u_1} {E : Type u_2} (referent : W → Option E) (scope : E → W → Bool) (w : W) : (presupOfReferent referent scope).presup w = ((referent w).isSome = true)

presupOfReferent is defined iff a referent is selected at w.

theorem Core.Presupposition.PrProp.presupOfReferent_assertion_some {W : Type u_1} {E : Type u_2} (referent : W → Option E) (scope : E → W → Bool) (w : W) (e : E) (h : referent w = some e) : (presupOfReferent referent scope).assertion w = (scope e w = true)

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

theorem Core.Presupposition.PrProp.presupOfReferent_assertion_none {W : Type u_1} {E : Type u_2} (referent : W → Option E) (scope : E → W → Bool) (w : W) (h : referent w = none) : (presupOfReferent referent scope).assertion w = (false = true)

Without a referent, the assertion is false.