Docs / Logic / Trivalent / Part

Partial propositions and three-valued truth

import Linglib.Logic.Trivalent.Part

A presuppositional meaning is carried either by a partial proposition Part Prop, as in Heim and Kratzer's composition engine, or by a three-valued one, SignType. SignType.ofPart maps the first carrier onto the second, sending an undefined value to 0 and a defined one to its classical value, so theorems proved over either carrier transfer to the other.

Main definitions

SignType.ofPart: the three-valued value of a partial proposition.

Main results

SignType.ofPart_eq_zero_iff, SignType.ofPart_eq_one_iff, SignType.ofPart_eq_neg_one_iff: the three values of ofPart.
SignType.ofPart_map_not, SignType.ofPart_ite_some_false: negation and enrichment by a two-valued condition transport along ofPart.
Trivalent.gapExt_ofPart: pointwise, the gap is the set of undefined points.

References

Heim & Kratzer 1998, Semantics in Generative Grammar formalized
Beaver & Krahmer 2001, A Partial Account of Presupposition Projection formalized

Declarations

The three-valued value of a partial proposition is 0 where it is undefined and its classical value elsewhere.

SignType.ofPart L42–45

noncomputable def SignType.ofPart (p : Part Prop) :

SignType

SignType.ofPart p = if h : p.Dom then SignType.ofProp (p.get h) else 0

Used by SignType.ofPart_eq_zero_iff, SignType.ofPart_eq_one_iff, SignType.ofPart_eq_neg_one_iff, SignType.ofPart_some, SignType.ofPart_none, SignType.ofPart_map_not, SignType.ofPart_ite_some_false, Trivalent.gapExt_ofPart

Used in Semantics/Composition/Partial, ChatainSchlenker2026

@[simp] theorem SignType.ofPart_eq_zero_iff L49–50

{p : Part Prop} :

ofPart p = 0 ↔ ¬p.Dom

Built from

@[simp] theorem SignType.ofPart_eq_one_iff L52–57

{p : Part Prop} :

ofPart p = 1 ↔ ∃ a ∈ p, a

Built from

@[simp] theorem SignType.ofPart_eq_neg_one_iff L59–64

{p : Part Prop} :

ofPart p = -1 ↔ ∃ a ∈ p, ¬a

Built from

Negation transports along ofPart.

theorem SignType.ofPart_map_not L74–85

{p : Part Prop} :

ofPart (Part.map Not p) = -ofPart p

Built from

Enrichment by a two-valued condition transports along ofPart.

theorem SignType.ofPart_ite_some_false L87–90

(R : Prop) [Decidable R] (p : Part Prop) :

ofPart (if R then p else Part.some False) = min (ofProp R) (ofPart p)

Built from

Pointwise, the gap of a partial proposition's three-valued value is where it is undefined.

theorem Trivalent.gapExt_ofPart L98–101

{W : Type u_1} (p : W → Part Prop) :

(gapExt fun (w : W) => SignType.ofPart (p w)) = {w : W | ¬(p w).Dom}

Built from