Partial Propositions

Partial propositions — propositions that may be undefined at some evaluation points. References: [Hei83], [Bel70], [BS22].

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.
• eval — evaluation into Prop3 W, with the simp-normal interface eval_eq_true_iff/eval_eq_false_iff/eval_eq_indet_iff; eval_surjective/eval_eq_eval_iff make precise that PartialProp is the total-representative presentation of Prop3 (values outside the presupposition are inert).

The connective families on PartialProp live in Semantics.Presupposition.Basic (classical, filtering, entailment) and Semantics.Presupposition.Trivalent (rival trivalent families).

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

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.

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

def Semantics.Presupposition.PartialValue.toPart {W : Type u_1} {α : Type u_2} (pv : PartialValue W α) : W → Part α

The mathlib rendering: pointwise, a presupposed value is a Part-valued function, the presupposition as domain. PartialValue is the total-representative presentation — the record carries a value everywhere (no proof-carrying Part.get); toPart forgets the values outside the presupposition.

Equations

• pv.toPart w = { Dom := pv.presup w, get := fun (x : pv.presup w) => pv.value w }

theorem Semantics.Presupposition.PartialValue.toPart_surjective {W : Type u_1} {α : Type u_2} [Inhabited α] : Function.Surjective toPart

Every Part-valued function has a total representative: toPart is surjective, so the two presentations differ only by the (linguistically inert) values outside the presupposition.

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_iff {W : Type u_1} {x y : PartialProp W} : x = y ↔ x.presup = y.presup ∧ x.assertion = y.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

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 : Trivalent.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 ≠ Trivalent.indet, assertion := fun (w : W) => p w = Trivalent.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) : Trivalent.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 Trivalent.true else Trivalent.false else Trivalent.indet

The simp-normal interface to eval: consumers reason through the three value characterizations rather than the classical if-nest.

@[simp]

theorem Semantics.Presupposition.PartialProp.eval_eq_true_iff {W : Type u_1} (p : PartialProp W) (w : W) : p.eval w = Trivalent.true ↔ p.presup w ∧ p.assertion w

@[simp]

theorem Semantics.Presupposition.PartialProp.eval_eq_false_iff {W : Type u_1} (p : PartialProp W) (w : W) : p.eval w = Trivalent.false ↔ p.presup w ∧ ¬p.assertion w

@[simp]

theorem Semantics.Presupposition.PartialProp.eval_eq_indet_iff {W : Type u_1} (p : PartialProp W) (w : W) : p.eval w = Trivalent.indet ↔ ¬p.presup w

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

Round-trip: Prop3 ↔ PartialProp

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

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

theorem Semantics.Presupposition.PartialProp.eval_surjective {W : Type u_1} : Function.Surjective eval

eval is surjective — every three-valued proposition has a total representative, ofProp3 being a section.

theorem Semantics.Presupposition.PartialProp.eval_eq_eval_iff {W : Type u_1} (p q : PartialProp W) : p.eval = q.eval ↔ ∀ (w : W), (p.presup w ↔ q.presup w) ∧ (p.presup w → (p.assertion w ↔ q.assertion w))

eval identifies exactly agreement on definedness and, where defined, on assertion: PartialProp is the total-representative presentation of Prop3 W, carrying (linguistically inert) assertion values outside the presupposition that eval forgets — so ofProp3 ∘ eval is not the identity, only eval ∘ ofProp3 is (eval_ofProp3).