def Semantics.Conditionals.Assertability.conditionalProbability (ws : Core.CausalBayesNet.WorldState) : ℚ

Conditional probability P(C|A) = P(A ∧ C) / P(A).

Returns 0 if P(A) = 0 (undefined case).

Equations

• Semantics.Conditionals.Assertability.conditionalProbability ws = ws.pCGivenA

def Semantics.Conditionals.Assertability.reversedConditionalProbability (ws : Core.CausalBayesNet.WorldState) : ℚ

Conditional probability P(A|C) = P(A ∧ C) / P(C).

Returns 0 if P(C) = 0 (undefined case).

Equations

• Semantics.Conditionals.Assertability.reversedConditionalProbability ws = ws.pAGivenC

def Semantics.Conditionals.Assertability.defaultThreshold : ℚ

The default assertability threshold θ.

A conditional "if A then C" is assertable when P(C|A) > θ. The paper uses θ = 0.9 as a reasonable default.

Equations

• Semantics.Conditionals.Assertability.defaultThreshold = 9 / 10

def Semantics.Conditionals.Assertability.assertable (ws : Core.CausalBayesNet.WorldState) (θ : ℚ := defaultThreshold) : Bool

Check if a conditional "if A then C" is assertable given a world state.

A conditional is assertable when:

1. P(A) > 0 (the antecedent is possible)
2. P(C|A) > θ (the conditional probability is high enough)

Equations

• Semantics.Conditionals.Assertability.assertable ws θ = (decide (ws.pA > 0) && decide (Semantics.Conditionals.Assertability.conditionalProbability ws > θ))

def Semantics.Conditionals.Assertability.assertabilityScore (ws : Core.CausalBayesNet.WorldState) : ℚ

Assertability as a rational value for soft semantics.

Returns P(C|A) if P(A) > 0, otherwise 0. This is useful for RSA models that use soft (graded) semantics.

Equations

• Semantics.Conditionals.Assertability.assertabilityScore ws = if ws.pA > 0 then Semantics.Conditionals.Assertability.conditionalProbability ws else 0

def Semantics.Conditionals.Assertability.assertabilityBool (ws : Core.CausalBayesNet.WorldState) (θ : ℚ := defaultThreshold) : ℚ

Threshold-based assertability as a rational value.

Returns 1 if assertable, 0 otherwise.

Equations

• Semantics.Conditionals.Assertability.assertabilityBool ws θ = if Semantics.Conditionals.Assertability.assertable ws θ = true then 1 else 0

def Semantics.Conditionals.Assertability.contrapositiveProbability (ws : Core.CausalBayesNet.WorldState) : ℚ

Assertability of the contrapositive: "if ¬C then ¬A".

P(¬A|¬C) = P(¬A ∧ ¬C) / P(¬C)

Equations

• Semantics.Conditionals.Assertability.contrapositiveProbability ws = if 1 - ws.pC > 0 then ws.pNotANotC / (1 - ws.pC) else 0

def Semantics.Conditionals.Assertability.contrapositiveAssertable (ws : Core.CausalBayesNet.WorldState) (θ : ℚ := defaultThreshold) : Bool

Check if the contrapositive "if ¬C then ¬A" is assertable.

Equations

• Semantics.Conditionals.Assertability.contrapositiveAssertable ws θ = (decide (ws.pC < 1) && decide (Semantics.Conditionals.Assertability.contrapositiveProbability ws > θ))

def Semantics.Conditionals.Assertability.reverseAssertable (ws : Core.CausalBayesNet.WorldState) (θ : ℚ := defaultThreshold) : Bool

Assertability of the reverse conditional: "if C then A".

P(A|C) = P(A ∧ C) / P(C)

This is relevant for inferring causal direction:

• If "if A then C" is assertable but "if C then A" is not, this suggests A→C
• If both are assertable, this suggests correlation or common cause

Equations

• Semantics.Conditionals.Assertability.reverseAssertable ws θ = (decide (ws.pC > 0) && decide (Semantics.Conditionals.Assertability.reversedConditionalProbability ws > θ))

def Semantics.Conditionals.Assertability.biconditionalAssertable (ws : Core.CausalBayesNet.WorldState) (θ : ℚ := defaultThreshold) : Bool

A biconditional "A iff C" is assertable when both directions are.

This corresponds to strong correlation or deterministic causation.

Equations

• Semantics.Conditionals.Assertability.biconditionalAssertable ws θ = (Semantics.Conditionals.Assertability.assertable ws θ && Semantics.Conditionals.Assertability.reverseAssertable ws θ)

def Semantics.Conditionals.Assertability.hasMissingLink (ws : Core.CausalBayesNet.WorldState) (ε : ℚ := 1 / 20) : Bool

Detect "missing-link" cases where the conditional seems odd.

A conditional "if A then C" has a "missing link" when:

1. A and C are (approximately) independent: P(C|A) ≈ P(C)
2. There's no clear causal or correlational connection

This is formalized as: |P(C|A) - P(C)| < ε for some small ε.

Equations

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

def Semantics.Conditionals.Assertability.correlationStrength (ws : Core.CausalBayesNet.WorldState) : ℚ

Correlation strength: how much P(C|A) differs from P(C).

Positive values indicate positive correlation. Negative values indicate negative correlation. Values near 0 indicate independence (missing link).

Equations

• Semantics.Conditionals.Assertability.correlationStrength ws = if ws.pA > 0 then Semantics.Conditionals.Assertability.conditionalProbability ws - ws.pC else 0

def Semantics.Conditionals.Assertability.asymmetryScore (ws : Core.CausalBayesNet.WorldState) : ℚ

Asymmetry score: how much more assertable is "if A then C" than "if C then A"?

Large positive values suggest A→C causal direction. Large negative values suggest C→A causal direction. Values near 0 suggest independence or bidirectional causation.

Equations

• Semantics.Conditionals.Assertability.asymmetryScore ws = Semantics.Conditionals.Assertability.assertabilityScore ws - Semantics.Conditionals.Assertability.reversedConditionalProbability ws

def Semantics.Conditionals.Assertability.inferCausalRelation (ws : Core.CausalBayesNet.WorldState) (θ : ℚ := defaultThreshold) : Core.CausalBayesNet.CausalRelation

Infer the most likely causal relation based on conditional assertability patterns.

Heuristic:

• If "if A then C" is assertable but "if C then A" is not: likely A→C
• If "if C then A" is assertable but "if A then C" is not: likely C→A
• If both or neither are assertable: likely independent or common cause

Equations

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

def Semantics.Conditionals.Assertability.conditionalSemantics (ws : Core.CausalBayesNet.WorldState) (θ : ℚ := defaultThreshold) : ℚ

The key connection to RSA: the literal listener L0 interprets a conditional by sampling world states where the conditional is assertable.

This function provides the "agreement" score φ for RSA:

• Returns 1 if the conditional is assertable in the world state
• Returns 0 otherwise

For soft semantics, use assertabilityScore instead.

Equations

• Semantics.Conditionals.Assertability.conditionalSemantics ws θ = Semantics.Conditionals.Assertability.assertabilityBool ws θ

def Semantics.Conditionals.Assertability.softConditionalSemantics (ws : Core.CausalBayesNet.WorldState) : ℚ

Soft semantics: the agreement is the conditional probability itself.

This allows the RSA model to reason about degrees of assertability.

Equations

• Semantics.Conditionals.Assertability.softConditionalSemantics ws = Semantics.Conditionals.Assertability.assertabilityScore ws

theorem Semantics.Conditionals.Assertability.not_assertable_if_antecedent_impossible (ws : Core.CausalBayesNet.WorldState) (θ : ℚ) (h : ws.pA = 0) : assertable ws θ = false

If P(A) = 0, the conditional is not assertable (antecedent impossible).

theorem Semantics.Conditionals.Assertability.assertable_implies_antecedent_possible (ws : Core.CausalBayesNet.WorldState) (θ : ℚ) (h : assertable ws θ = true) : ws.pA > 0

Assertability implies the antecedent is possible.

theorem Semantics.Conditionals.Assertability.assertability_monotone (ws : Core.CausalBayesNet.WorldState) (θ₁ θ₂ : ℚ) : θ₁ ≤ θ₂ → assertable ws θ₂ = true → assertable ws θ₁ = true

Assertability is monotone in threshold (lower threshold → more assertable).

If a conditional is assertable at threshold θ₂, it is also assertable at any lower threshold θ₁ ≤ θ₂.

theorem Semantics.Conditionals.Assertability.assertability_score_bounded (ws : Core.CausalBayesNet.WorldState) (h : ws.IsValid) : 0 ≤ assertabilityScore ws ∧ assertabilityScore ws ≤ 1

Assertability score is bounded in [0, 1].

The assertability score (conditional probability when defined) is always between 0 and 1.

theorem Semantics.Conditionals.Assertability.conditional_probability_bounded (ws : Core.CausalBayesNet.WorldState) (h : ws.IsValid) (hA : 0 < ws.pA) : 0 ≤ conditionalProbability ws ∧ conditionalProbability ws ≤ 1

Conditional probability is bounded when the antecedent is possible.

theorem Semantics.Conditionals.Assertability.missing_link_iff_weak_correlation (ws : Core.CausalBayesNet.WorldState) (ε : ℚ) (hA : 0 < ws.pA) : hasMissingLink ws ε = true ↔ -ε < correlationStrength ws ∧ correlationStrength ws < ε

Missing-link iff weak correlation.

A conditional has a missing link iff the correlation strength is within ε of 0. This is a bidirectional characterization when P(A) > 0.

theorem Semantics.Conditionals.Assertability.independent_implies_missing_link (ws : Core.CausalBayesNet.WorldState) (ε : ℚ) (hε : 0 < ε) (hA : 0 < ws.pA) (h_indep : ws.pAC = ws.pA * ws.pC) : hasMissingLink ws ε = true

Independence implies missing link.

If A and C are probabilistically independent (P(A∧C) = P(A)·P(C)), then the conditional has a missing link (for any positive ε).

theorem Semantics.Conditionals.Assertability.missing_link_no_boost (ws : Core.CausalBayesNet.WorldState) (ε : ℚ) (hA : 0 < ws.pA) : hasMissingLink ws ε = true → conditionalProbability ws - ε < ws.pC ∧ ws.pC < conditionalProbability ws + ε

Missing link means no correlation boost.

If there's a missing link, then P(C|A) ≈ P(C), meaning knowing A doesn't significantly change the probability of C.

theorem Semantics.Conditionals.Assertability.correlation_strength_zero_iff_independent (ws : Core.CausalBayesNet.WorldState) (hA : 0 < ws.pA) : correlationStrength ws = 0 ↔ ws.pAC = ws.pA * ws.pC

Correlation strength is zero iff independence.

When P(A) > 0, correlation strength is exactly 0 iff A and C are independent.