Rival trivalent connective families

The rival trivalent connective families on PartialProp, beyond the classical (Weak Kleene) and filtering (middle Kleene) canon of Semantics.Presupposition.Basic: Strong Kleene ([Kle52]), Belnap conditional assertion / flexible accommodation ([Bel70], [Geu05]), the symmetric K&P disjunction ([KP79]), and the positive-antecedent rival ([Sha25]).

Main declarations

• orStrong, andStrong — Strong Kleene: the Trivalent lattice join/meet (eval_orStrong/eval_andStrong).
• orBelnap, andBelnap — Belnap conditional assertion; the flexible-accommodation orFlex/andFlex are definitionally the same operators.
• belnapLift — unifier showing Belnap = flexible accommodation for any binary Prop operator with an identity.
• orKPSymmetric — symmetric two-dimensional K&P disjunction.
• orPositive — positive-antecedent symmetric disjunction, a documented rival ([Sha25], [Yag25]).
• liveness, genuineness — [Yag25] disjunction-update conditions.
• all_or_agree_when_both_defined / all_and_agree_when_both_defined — the families diverge only when presuppositions conflict.

Todo

• evalLift : (Trivalent → Trivalent → Trivalent) → (PartialProp W → PartialProp W → PartialProp W) would collapse xor, andBelnap, orBelnap into one definition each, with one bridge theorem instead of eight.

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 }

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

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 Trivalent 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 Trivalent lattice meet — see eval_andStrong.

Equations

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

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 Trivalent 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 Trivalent lattice meet pointwise, unconditionally.

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.

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: Belnap

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

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.

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.