Canonical operations on partial propositions

The canonical connectives, entailment relations, and combinators on PartialProp. References: [Hei83], [Sch09a], [vF99a], [Kar73], [Pet79], [Boc37].

Main declarations

• Negations: internal neg (a hole), Bochvar's truth operator truthOp and external negation negExt = neg ∘ truthOp (plugs).
• Classical connectives and, or, imp, xor (simultaneously Weak Kleene: indet is absorbing).
• Filtering / Karttunen connectives andFilter, impFilter, orFilter — Peters' middle Kleene ([Pet79], eval_andFilter/eval_orFilter) — with the scoped notation /\', ->', \/'.
• strawsonEntails, strongEntails — entailment relations: the canonical [vF99a] form (presup-as-premise; not transitive, strawsonEntails_not_trans) and the stronger variant that additionally requires q's presupposition to project from p's satisfaction.
• Embedding combinators disjFilterLeft, negFactive.
• presupOfReferent — definite-description combinator (single source of truth for singular definite denotations).

The rival trivalent connective families (Strong Kleene, Belnap / flexible accommodation, symmetric K&P, positive-antecedent) live in Semantics.Presupposition.Trivalent; quantified projection lives in Semantics.Presupposition.Quantified.

Implementation notes

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

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, Trivalent.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 PartialProp.orKPSymmetric; the positive-antecedent variant is PartialProp.orPositive (Semantics.Presupposition.Trivalent).

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.

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. The same notion on bilateral-update denotations is ElliottSudo2025.strawsonEntails.

Equations

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

theorem Semantics.Presupposition.PartialProp.strawsonEntails_not_trans : ¬∀ (p q r : PartialProp Unit), p.strawsonEntails q → q.strawsonEntails r → p.strawsonEntails r

Strawson entailment is not transitive — an undefined middle term discharges both premises vacuously, the well-known failure of [vF99a]'s notion — so strawsonEntails supports no Preorder instance.

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 (AntisymmRel of strawsonEntails).

Equations

• p.strawsonEquiv q = AntisymmRel Semantics.Presupposition.PartialProp.strawsonEntails p q

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

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_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 Trivalent.joinWeak pointwise (classical disjunction is Weak Kleene).

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 = Trivalent.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 Trivalent.true else Trivalent.false

Filtering implication when antecedent true: depends on consequent.

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 Trivalent.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 Trivalent.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 Trivalent.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 = Trivalent.indet

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

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.

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.