Graded Propositions

Infrastructure for graded/continuous-valued propositions (W → ℚ) used in probabilistic approaches to semantics.

@[reducible, inline]

abbrev Core.GradedProposition.GProp (W : Type u_1) : Type u_1

A graded proposition assigns a truth degree in ℚ to each world.

Equations

• Core.GradedProposition.GProp W = (W → ℚ)

def Core.GradedProposition.neg {W : Type u_1} (p : GProp W) : GProp W

Graded negation: P(¬A) = 1 - P(A).

Equations

• Core.GradedProposition.neg p w = 1 - p w

def Core.GradedProposition.conj {W : Type u_1} (p q : GProp W) : GProp W

Graded conjunction: P(A ∧ B) = P(A) × P(B) under independence.

Equations

• Core.GradedProposition.conj p q w = p w * q w

def Core.GradedProposition.disj {W : Type u_1} (p q : GProp W) : GProp W

Graded disjunction: P(A ∨ B) = P(A) + P(B) - P(A)P(B) under independence.

Equations

• Core.GradedProposition.disj p q w = p w + q w - p w * q w

def Core.GradedProposition.conjMin {W : Type u_1} (p q : GProp W) : GProp W

Minimum-based conjunction (alternative to product).

Equations

• Core.GradedProposition.conjMin p q w = min (p w) (q w)

def Core.GradedProposition.disjMax {W : Type u_1} (p q : GProp W) : GProp W

Maximum-based disjunction (alternative to probabilistic or).

Equations

• Core.GradedProposition.disjMax p q w = max (p w) (q w)

def Core.GradedProposition.top {W : Type u_1} : GProp W

The always-true graded proposition (degree 1 everywhere).

Equations

• Core.GradedProposition.top x✝ = 1

def Core.GradedProposition.bot {W : Type u_1} : GProp W

The always-false graded proposition (degree 0 everywhere).

Equations

• Core.GradedProposition.bot x✝ = 0

def Core.GradedProposition.entails {W : Type u_1} (p q : GProp W) : Prop

Graded entailment: p entails q iff p(w) ≤ q(w) for all worlds.

Equations

• Core.GradedProposition.entails p q = ∀ (w : W), p w ≤ q w

def Core.GradedProposition.equiv {W : Type u_1} (p q : GProp W) : Prop

Graded equivalence: p and q have the same truth degree everywhere.

Equations

• Core.GradedProposition.equiv p q = ∀ (w : W), p w = q w

instance Core.GradedProposition.instLEGProp {W : Type u_1} : LE (GProp W)

Equations

• Core.GradedProposition.instLEGProp = { le := Core.GradedProposition.entails }

instance Core.GradedProposition.instPreorderGProp {W : Type u_1} : Preorder (GProp W)

Equations

• Core.GradedProposition.instPreorderGProp = { le := Core.GradedProposition.entails, toLT := Pi.preorder.toLT, le_refl := ⋯, le_trans := ⋯, lt_iff_le_not_ge := ⋯ }

instance Core.GradedProposition.instTopGProp {W : Type u_1} : Top (GProp W)

Equations

• Core.GradedProposition.instTopGProp = { top := Core.GradedProposition.top }

instance Core.GradedProposition.instBotGProp {W : Type u_1} : Bot (GProp W)

Equations

• Core.GradedProposition.instBotGProp = { bot := Core.GradedProposition.bot }

instance Core.GradedProposition.instPartialOrderGProp {W : Type u_1} : PartialOrder (GProp W)

Partial order on graded propositions.

Equations

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

def Core.GradedProposition.ofBool {W : Type u_1} (p : W → Bool) : GProp W

Convert a Boolean proposition to a graded proposition.

Equations

• Core.GradedProposition.ofBool p w = if p w = true then 1 else 0

def Core.GradedProposition.boolToGProp {W : Type u_1} (p : W → Bool) : GProp W

Alias matching the existing RSA function name.

Equations

• Core.GradedProposition.boolToGProp p = Core.GradedProposition.ofBool p

theorem Core.GradedProposition.neg_involutive {W : Type u_1} (p : GProp W) : neg (neg p) = p

Graded negation is involutive: neg (neg p) = p.

theorem Core.GradedProposition.neg_antitone {W : Type u_1} (p q : GProp W) (h : entails p q) : entails (neg q) (neg p)

Graded negation is antitone: if p ≤ q then neg q ≤ neg p.

theorem Core.GradedProposition.neg_top {W : Type u_1} : neg top = bot

Negation swaps top and bot.

theorem Core.GradedProposition.neg_bot {W : Type u_1} : neg bot = top

theorem Core.GradedProposition.conj_comm {W : Type u_1} (p q : GProp W) : conj p q = conj q p

Product conjunction is commutative.

theorem Core.GradedProposition.conj_assoc {W : Type u_1} (p q r : GProp W) : conj (conj p q) r = conj p (conj q r)

Product conjunction is associative.

theorem Core.GradedProposition.conj_top {W : Type u_1} (p : GProp W) : conj p top = p

Top is the identity for product conjunction.

theorem Core.GradedProposition.top_conj {W : Type u_1} (p : GProp W) : conj top p = p

theorem Core.GradedProposition.conj_bot {W : Type u_1} (p : GProp W) : conj p bot = bot

Bot is absorbing for product conjunction.

theorem Core.GradedProposition.disj_comm {W : Type u_1} (p q : GProp W) : disj p q = disj q p

Probabilistic disjunction is commutative.

theorem Core.GradedProposition.disj_bot {W : Type u_1} (p : GProp W) : disj p bot = p

Bot is the identity for disjunction.

theorem Core.GradedProposition.disj_top {W : Type u_1} (p : GProp W) : disj p top = top

Top is absorbing for disjunction.

theorem Core.GradedProposition.deMorgan_conj {W : Type u_1} (p q : GProp W) : neg (conj p q) = disj (neg p) (neg q)

De Morgan's law for graded conjunction.

theorem Core.GradedProposition.deMorgan_disj {W : Type u_1} (p q : GProp W) : neg (disj p q) = conj (neg p) (neg q)

De Morgan's law for graded disjunction.

theorem Core.GradedProposition.neg_preserves_bounds {W : Type u_1} (p : GProp W) (w : W) (h0 : 0 ≤ p w) (h1 : p w ≤ 1) : 0 ≤ neg p w ∧ neg p w ≤ 1

Negation preserves [0,1] bounds.

theorem Core.GradedProposition.conj_preserves_bounds {W : Type u_1} (p q : GProp W) (w : W) (hp0 : 0 ≤ p w) (hp1 : p w ≤ 1) (hq0 : 0 ≤ q w) (hq1 : q w ≤ 1) : 0 ≤ conj p q w ∧ conj p q w ≤ 1

Conjunction preserves [0,1] bounds.

theorem Core.GradedProposition.disj_preserves_bounds {W : Type u_1} (p q : GProp W) (w : W) (hp0 : 0 ≤ p w) (hp1 : p w ≤ 1) (hq0 : 0 ≤ q w) (hq1 : q w ≤ 1) : 0 ≤ disj p q w ∧ disj p q w ≤ 1

Disjunction preserves [0,1] bounds.

theorem Core.GradedProposition.conj_monotone_left {W : Type u_1} (p q r : GProp W) (hpq : entails p q) (hr : ∀ (w : W), 0 ≤ r w) : entails (conj p r) (conj q r)

Conjunction is monotone in both arguments.

theorem Core.GradedProposition.disj_monotone_left {W : Type u_1} (p q r : GProp W) (hpq : entails p q) (_hr : ∀ (w : W), 0 ≤ r w) (hr1 : ∀ (w : W), r w ≤ 1) : entails (disj p r) (disj q r)

Disjunction is monotone in both arguments.

theorem Core.GradedProposition.neg_ofBool {W : Type u_1} (p : W → Bool) : neg (ofBool p) = ofBool fun (w : W) => !p w

When restricted to Boolean values, graded negation equals Boolean negation.

theorem Core.GradedProposition.conj_ofBool {W : Type u_1} (p q : W → Bool) : conj (ofBool p) (ofBool q) = ofBool fun (w : W) => p w && q w

When restricted to Boolean values, graded conjunction equals Boolean conjunction.

theorem Core.GradedProposition.disj_ofBool {W : Type u_1} (p q : W → Bool) : disj (ofBool p) (ofBool q) = ofBool fun (w : W) => p w || q w

When restricted to Boolean values, graded disjunction equals Boolean disjunction.

def Core.GradedProposition.«term∼_» : Lean.ParserDescr

Equations

• Core.GradedProposition.«term∼_» = Lean.ParserDescr.node `Core.GradedProposition.«term∼_» 75 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol "∼") (Lean.ParserDescr.cat `term 75))

def Core.GradedProposition.«term_⊗_» : Lean.TrailingParserDescr

Equations

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

def Core.GradedProposition.«term_⊕_» : Lean.TrailingParserDescr

Equations

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

def Core.GradedProposition.«term_⊓ᵍ_» : Lean.TrailingParserDescr

Equations

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

def Core.GradedProposition.«term_⊔ᵍ_» : Lean.TrailingParserDescr

Equations

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

@[reducible, inline]

abbrev Core.GradedProposition.GPred (E : Type u_2) : Type u_2

A graded predicate is a function from entities to truth degrees.

Equations

• Core.GradedProposition.GPred E = (E → ℚ)

def Core.GradedProposition.GPred.ofBool {E : Type u_2} (p : E → Bool) : GPred E

Lift a Boolean predicate to a graded predicate.

Equations

• Core.GradedProposition.GPred.ofBool p e = if p e = true then 1 else 0

structure Core.GradedProposition.FeatureReliability : Type

Semantic reliability parameters for a feature dimension.

• onMatch : ℚ

  Truth degree when feature matches

• onMismatch : ℚ

  Truth degree when feature doesn't match

• match_gt_mismatch : self.onMismatch ≤ self.onMatch

  Match value should be higher than mismatch

def Core.GradedProposition.instReprFeatureReliability.repr : FeatureReliability → ℕ → Std.Format

Equations

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

instance Core.GradedProposition.instReprFeatureReliability : Repr FeatureReliability

Equations

• Core.GradedProposition.instReprFeatureReliability = { reprPrec := Core.GradedProposition.instReprFeatureReliability.repr }

def Core.GradedProposition.FeatureReliability.crisp : FeatureReliability

Boolean (crisp) feature reliability.

Equations

• Core.GradedProposition.FeatureReliability.crisp = { match_gt_mismatch := Core.GradedProposition.FeatureReliability.crisp._proof_1 }

def Core.GradedProposition.FeatureReliability.high : FeatureReliability

High reliability feature (like color).

Equations

• Core.GradedProposition.FeatureReliability.high = { onMatch := 99 / 100, onMismatch := 1 / 100, match_gt_mismatch := Core.GradedProposition.FeatureReliability.high._proof_1 }

def Core.GradedProposition.FeatureReliability.medium : FeatureReliability

Medium reliability feature (like size).

Equations

• Core.GradedProposition.FeatureReliability.medium = { onMatch := 8 / 10, onMismatch := 2 / 10, match_gt_mismatch := Core.GradedProposition.FeatureReliability.medium._proof_1 }

def Core.GradedProposition.FeatureReliability.apply (rel : FeatureReliability) (isMatch : Bool) : ℚ

Apply a feature reliability to a Boolean match result.

Equations

• rel.apply isMatch = if isMatch = true then rel.onMatch else rel.onMismatch

theorem Core.GradedProposition.entails_ofBool_of_implies {W : Type u_2} (p q : W → Bool) (h : ∀ (w : W), p w = true → q w = true) : entails (ofBool p) (ofBool q)

Entailment is preserved by ofBool.

theorem Core.GradedProposition.entails_iff_bool {W : Type u_2} (p q : W → Bool) : entails (ofBool p) (ofBool q) ↔ ∀ (w : W), p w = true → q w = true

Graded entailment reduces to Boolean entailment for {0,1} propositions.

theorem Core.GradedProposition.bot_entails {W : Type u_1} (p : GProp W) (hp : ∀ (w : W), 0 ≤ p w) : entails bot p

Bot is the smallest graded proposition (for non-negative propositions).