Docs / Logic / Trivalent / Supervaluation
import Linglib.Logic.Trivalent.Supervaluation
A trivalent value is the supervaluation of its two bivalent readings, true where it is 1 and
true where it is not -1, its designation at K3 and at LP. Reading each occurrence of an atom at
a standard of its own, independently of its other occurrences, gives the bivalent variants of a
formula, and the Strong Kleene value of the formula is the supervaluation of its bivalent
variants. The same holds of the Strong Kleene quantifiers, each instance read at its own
standard. Spector states the propositional case and uses it to read an occurrence of
presuppositional exhaustification as underspecified between a parse with an exhaustivity operator
and one without.
Uniform supervaluation, which reads every occurrence of an atom at the same standard, is not
Strong Kleene: p ∨ ¬p is supertrue where p is 0, and Strong Kleene leaves it undefined.
Trivalent.Formula.bivalentVariants: the formulas over atoms paired with standards that read
each occurrence of an atom at a standard.SignType.supervaluationOn: the supervaluation of a predicate over a set.SignType.supervaluation_product_and, SignType.supervaluation_product_or: over a product of
families, supervaluation takes independent conjunctions and disjunctions to ⊓ and ⊔.Trivalent.Formula.eval_strongKleene_eq_supervaluation: the Strong Kleene value of a formula
is the supervaluation of its bivalent variants.Trivalent.forallStrong_eq_supervaluation, Trivalent.existsStrong_eq_supervaluation: the
Strong Kleene quantifiers are supervaluations over the readings of their instances.Trivalent.supervaluationOn_pi_eq_const_of_monotone: for a monotone Q, reading each index at
a standard of its own gives the supervaluation of reading every index at one.Over a product of nonempty families, the supervaluation of independent conditions on the two coordinates, conjoined, is the Strong Kleene conjunction of their supervaluations.
Over a product of nonempty families, the supervaluation of independent conditions on the two coordinates, disjoined, is the Strong Kleene disjunction of their supervaluations.
Over the choice functions of nonempty families, the supervaluation of independent conditions on the choices, all holding, is the Strong Kleene universal over their supervaluations.
Over the choice functions of nonempty families, the supervaluation of independent conditions on the choices, one holding, is the Strong Kleene existential over their supervaluations.
supervaluation decides its cases over a finite family. Over a set they are decided classically,
and over a finite set the two agree. Where the predicate at every member of a set follows from its
value at one member lo and implies its value at another hi, it holds throughout the set
exactly when it holds at lo and fails throughout exactly when it fails at hi, so the set has
the supervaluation of the two.
The supervaluation of P over a set is 1 when P holds throughout it, -1 when P fails
throughout it and it is nonempty, and 0 otherwise.
Used by SignType.supervaluationOn_eq_one_iff, SignType.supervaluationOn_eq_neg_one_iff, SignType.supervaluationOn_eq_zero_iff, SignType.supervaluationOn_congr, SignType.supervaluationOn_coe_finset, SignType.supervaluationOn_image, SignType.supervaluationOn_eq_of_between, Trivalent.supervaluationOn_pi_eq_const_of_monotone, Trivalent.supervaluationOn_pi_eq_const_of_antitone
Used in Spector2025
Built from
Built from
Built from
Built from
Over a finite set, supervaluation over the set is the supervaluation of the family.
Built from
Built from
Over a set where P at each member follows from P lo and implies P hi, for members lo
and hi, the supervaluation of P is its supervaluation over lo and hi.
Built from
Over a finite family where P at each member follows from P lo and implies P hi, for
members lo and hi, the supervaluation of P is its supervaluation over lo and hi.
For a monotone Q, reading each index at a standard of its own gives the supervaluation of
reading every index at one standard.
Built from
For an antitone Q, reading each index at a standard of its own gives the supervaluation of
reading every index at one standard.
Built from
The Strong Kleene universal is the supervaluation over the readings of its instances, each at a standard of its own.
The Strong Kleene existential is the supervaluation over the readings of its instances, each at a standard of its own.
The bivalent variants of a formula (Spector 2025) read each occurrence of an atom at a standard, independently of its other occurrences.
Used by Trivalent.Formula.bivalentVariants_nonempty, Trivalent.Formula.eval_strongKleene_eq_supervaluation
Used in Spector2025
Built from
The Strong Kleene value of a formula is the supervaluation of its bivalent variants, each occurrence of an atom designated at its standard (Spector 2025, §5).
Built from