Documentation

Linglib.Studies.GrusdtLassiterFranke2022

[GLF22] #

"Probabilistic modeling of rational communication with conditionals" PLoS ONE 17(7): e0269937.

Overview #

This paper extends RSA to model conditionals by:

Treating "worlds" as probability distributions (WorldState)
Using assertability (P(C|A) ≥ θ) as the literal meaning of conditionals
Having L1 infer both the world state AND the causal structure

The key insight is that the literal meaning of "if A then C" is an assertability condition — P(C|A) ≥ θ — rather than material implication. This grounds RSA's meaning function in conditional probability.

Toy Example (§2.3, Table 2) #

The paper's illustrative example uses 3 states and 4 utterances with θ = 0.9:

	P(A)	P(C)	P(A,C)	P(C\|A)	likely C	if A, C	C	A and C
s1	0.9	0.9	0.81	0.9	✓	✓	✓	—
s2	0.65	0.65	0.6	12/13	✓	✓	—	—
s3	0.6	0.6	0.36	0.6	✓	—	—	—

Key predictions:

S1 in s1 prefers "C" (most informative true utterance)
S1 in s2 prefers "if A then C" (only true non-trivial utterance)
S1 in s3 prefers "likely C" (only true utterance)
L1 hearing "if A then C" infers s2 > s1 (dependency inference)
L1 hearing "C" identifies s1 (high marginal probability)

Full Model (§3) #

The full model uses 10,000 sampled world states and three causal relations (A→C, C→A, A⊥C) as latent variables. We formalize only the toy example here, which captures all qualitative predictions with finite types amenable to exact PMF evaluation.

Grounding #

The assertability truth values are grounded in the probabilistic assertability condition from Semantics.Probabilistic.ConditionalAssertability: a conditional "if A then C" is assertable when P(A) > 0 and P(C|A) ≥ θ.

Experiments #

Experiment 1: Dependency Inference — Participants hear "if A then C" and judge causal structure. 72% infer A→C, 15% C→A, 10% A⊥C.
Experiment 2: Conditional Perfection — 85% endorse "if ¬A then ¬C" in A→C contexts vs 45% in independent contexts.
Experiment 3: Assertability Thresholds — θ ≈ 0.88 from model fitting.

inductive GrusdtLassiterFranke2022.Utt :

Utterances from the toy example (Table 2, §2.3).

The paper uses a richer utterance space in the full model, but the toy example uses four utterances ordered by informativity:

"likely C": assertable when P(C) ≥ 0.5 (weakest, true in all toy states)
"if A then C": assertable when P(C|A) ≥ 0.9
"C": assertable when P(C) ≥ 0.9
"A and C": assertable when P(A∧C) ≥ 0.9

"A and C" is false in all three toy states, making it a vacuous alternative that nonetheless affects the pragmatic competition.

likelyC : Utt
conditional : Utt
C : Utt
conjAC : Utt

Instances For

@[implicit_reducible]

instance GrusdtLassiterFranke2022.instDecidableEqUtt :

DecidableEq Utt

Equations

GrusdtLassiterFranke2022.instDecidableEqUtt x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[implicit_reducible]

instance GrusdtLassiterFranke2022.instReprUtt :

Repr Utt

Equations

GrusdtLassiterFranke2022.instReprUtt = { reprPrec := GrusdtLassiterFranke2022.instReprUtt.repr }

def GrusdtLassiterFranke2022.instReprUtt.repr :

Utt → ℕ → Std.Format

Equations

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

Instances For

@[implicit_reducible]

instance GrusdtLassiterFranke2022.instInhabitedUtt :

Inhabited Utt

Equations

GrusdtLassiterFranke2022.instInhabitedUtt = { default := GrusdtLassiterFranke2022.instInhabitedUtt.default }

@[implicit_reducible]

instance GrusdtLassiterFranke2022.instFintypeUtt :

Fintype Utt

Equations

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

instance GrusdtLassiterFranke2022.instNonemptyUtt :

Nonempty Utt

inductive GrusdtLassiterFranke2022.State :

World states from the toy example (Table 2, §2.3).

Each state is a probability distribution (pA, pC, pAC) representing a different degree of dependence between A and C:

s1: High marginals, P(C|A) = 0.9 = θ (borderline assertable)
s2: Moderate marginals, P(C|A) = 12/13 ≈ 0.923 > θ (clearly assertable)
s3: Moderate marginals, P(C|A) = 0.6 < θ (not assertable)

s1 : State
s2 : State
s3 : State

Instances For

@[implicit_reducible]

instance GrusdtLassiterFranke2022.instDecidableEqState :

DecidableEq State

Equations

GrusdtLassiterFranke2022.instDecidableEqState x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def GrusdtLassiterFranke2022.instReprState.repr :

State → ℕ → Std.Format

Equations

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

Instances For

@[implicit_reducible]

instance GrusdtLassiterFranke2022.instReprState :

Repr State

Equations

GrusdtLassiterFranke2022.instReprState = { reprPrec := GrusdtLassiterFranke2022.instReprState.repr }

@[implicit_reducible]

instance GrusdtLassiterFranke2022.instInhabitedState :

Inhabited State

Equations

GrusdtLassiterFranke2022.instInhabitedState = { default := GrusdtLassiterFranke2022.instInhabitedState.default }

@[implicit_reducible]

instance GrusdtLassiterFranke2022.instFintypeState :

Fintype State

Equations

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

instance GrusdtLassiterFranke2022.instNonemptyState :

Nonempty State

def GrusdtLassiterFranke2022.ws1 :

Causation.BayesNet.WorldState

WorldState for s1: P(A)=0.9, P(C)=0.9, P(A∧C)=0.81. P(C|A) = 0.81/0.9 = 0.9 = θ.

Equations

GrusdtLassiterFranke2022.ws1 = { pA := 9 / 10, pC := 9 / 10, pAC := 81 / 100 }

Instances For

def GrusdtLassiterFranke2022.ws2 :

Causation.BayesNet.WorldState

WorldState for s2: P(A)=0.65, P(C)=0.65, P(A∧C)=0.6. P(C|A) = 0.6/0.65 = 12/13 ≈ 0.923 > θ.

Equations

GrusdtLassiterFranke2022.ws2 = { pA := 13 / 20, pC := 13 / 20, pAC := 3 / 5 }

Instances For

def GrusdtLassiterFranke2022.ws3 :

Causation.BayesNet.WorldState

WorldState for s3: P(A)=0.6, P(C)=0.6, P(A∧C)=0.36. P(C|A) = 0.36/0.6 = 0.6 < θ.

Equations

GrusdtLassiterFranke2022.ws3 = { pA := 3 / 5, pC := 3 / 5, pAC := 9 / 25 }

Instances For

def GrusdtLassiterFranke2022.stateToWorldState :

State → Causation.BayesNet.WorldState

Map states to their WorldState representations.

Equations

Instances For

def GrusdtLassiterFranke2022.θ :

ℚ

Assertability threshold θ = 0.9 from the paper.

Equations

GrusdtLassiterFranke2022.θ = 9 / 10

Instances For

def GrusdtLassiterFranke2022.assertable' :

Utt → State → Bool

Assertability truth table for the toy example (Table 2).

Defines when each utterance is assertable in each state. The paper uses P(C|A) ≥ θ (non-strict), while Assertability.assertable uses > θ. For the toy example, s1 has P(C|A) = 0.9 = θ exactly, so assertability under ≥ is true but under > is false. We define the truth table directly to match the paper's non-strict threshold.

Truth values from Table 2:

likely C (P(C) ≥ 0.5): s1 ✓, s2 ✓, s3 ✓ (all states have P(C) ≥ 0.6 > 0.5)
if A then C (P(C|A) ≥ 0.9): s1 ✓, s2 ✓, s3 ✗
C (P(C) ≥ 0.9): s1 ✓, s2 ✗, s3 ✗
A and C (P(A∧C) ≥ 0.9): s1 ✗, s2 ✗, s3 ✗

Equations

Instances For

Verify that the assertability truth values are grounded in the actual conditional/marginal probabilities of the WorldStates. These connect the directly-defined truth table to the assertability theory.

theorem GrusdtLassiterFranke2022.ws1_conditional_prob :

ws1.pCGivenA = 9 / 10

s1 has P(C|A) = 9/10 ≥ θ.

theorem GrusdtLassiterFranke2022.ws2_conditional_prob :

ws2.pCGivenA = 12 / 13

s2 has P(C|A) = 12/13 > θ.

theorem GrusdtLassiterFranke2022.ws3_conditional_prob :

ws3.pCGivenA = 3 / 5

s3 has P(C|A) = 3/5 < θ.

theorem GrusdtLassiterFranke2022.ws1_marginal_C :

ws1.pC = 9 / 10

s1 has P(C) = 9/10 ≥ 0.9 (so "C" is assertable).

theorem GrusdtLassiterFranke2022.ws2_marginal_C :

ws2.pC = 13 / 20

s2 has P(C) = 13/20 ≥ 0.5 (so "likely C" is assertable).

theorem GrusdtLassiterFranke2022.ws3_marginal_C :

ws3.pC = 3 / 5

s3 has P(C) = 3/5 ≥ 0.5 (so "likely C" is assertable).

theorem GrusdtLassiterFranke2022.ws1_joint :

ws1.pAC = 81 / 100

s1 has P(A∧C) = 81/100 < 0.9 (so "A and C" is not assertable).

theorem GrusdtLassiterFranke2022.strict_assertability_s1_false :

Semantics.Probabilistic.ConditionalAssertability.assertable ws1 θ = false

The forward conditional is assertable (using strict >) only for s2, not s1, because Assertability.assertable uses strict >. This demonstrates the ≥ vs > mismatch that motivates the direct truth table.

theorem GrusdtLassiterFranke2022.strict_assertability_s2_true :

Semantics.Probabilistic.ConditionalAssertability.assertable ws2 θ = true

theorem GrusdtLassiterFranke2022.strict_assertability_s3_false :

Semantics.Probabilistic.ConditionalAssertability.assertable ws3 θ = false

The toy example as a mathlib-PMF Frank-Goodman model [FG12]: the literal listener is uniform on each utterance's assertability extension, the pragmatic speaker S1 normalises the literal weights over utterances (α = 1, no cost), and the pragmatic listener L1 is the Bayesian posterior against the uniform world prior. conjAC, assertable in no state, has an empty extension: it carries weight 0 and drops out of the competition rather than receiving an (undefined) literal-listener PMF.

@[reducible, inline]

abbrev GrusdtLassiterFranke2022.ext (u : Utt) :

Finset State

Assertability extension of an utterance: the states where it holds.

Equations

GrusdtLassiterFranke2022.ext u = RSA.extensionOf GrusdtLassiterFranke2022.assertable' u

Instances For

noncomputable def GrusdtLassiterFranke2022.litWeight (s : State) (u : Utt) :

ENNReal

Literal-listener weight L0(s | u) at α = 1: uniform on the extension, 1/|ext u| where u is assertable at s, else 0. For the three assertable utterances this coincides with RSA.L0OfBoolMeaning (litWeight_eq_L0OfBoolMeaning); the never-assertable conjAC is weightless.

Equations

GrusdtLassiterFranke2022.litWeight s u = if GrusdtLassiterFranke2022.assertable' u s = true then (↑(GrusdtLassiterFranke2022.ext u).card)⁻¹ else 0

Instances For

theorem GrusdtLassiterFranke2022.litWeight_of_true {s : State} {u : Utt} {k : ℕ} (h : assertable' u s = true) (hk : (ext u).card = k) :

litWeight s u = (↑k)⁻¹

theorem GrusdtLassiterFranke2022.litWeight_of_false {s : State} {u : Utt} (h : assertable' u s = false) :

litWeight s u = 0

theorem GrusdtLassiterFranke2022.litWeight_eq_L0OfBoolMeaning (s : State) {u : Utt} (h : (ext u).Nonempty) :

litWeight s u = (RSA.L0OfBoolMeaning assertable' u h) s

Where an utterance is assertable somewhere, litWeight is exactly the canonical literal listener uniform on the extension; conjAC gets 0.

theorem GrusdtLassiterFranke2022.litWeight_ne_top (s : State) (u : Utt) :

litWeight s u ≠ ⊤

Toy-example weights (Table 2): likelyC is assertable in all 3 states, conditional in {s1, s2}, C in {s1}, conjAC in none.

theorem GrusdtLassiterFranke2022.lw_likelyC (s : State) :

litWeight s Utt.likelyC = 3⁻¹

theorem GrusdtLassiterFranke2022.lw_s1_conditional :

litWeight State.s1 Utt.conditional = 2⁻¹

theorem GrusdtLassiterFranke2022.lw_s2_conditional :

litWeight State.s2 Utt.conditional = 2⁻¹

theorem GrusdtLassiterFranke2022.lw_s3_conditional :

litWeight State.s3 Utt.conditional = 0

theorem GrusdtLassiterFranke2022.lw_s1_C :

litWeight State.s1 Utt.C = 1

theorem GrusdtLassiterFranke2022.lw_s2_C :

litWeight State.s2 Utt.C = 0

theorem GrusdtLassiterFranke2022.lw_s3_C :

litWeight State.s3 Utt.C = 0

theorem GrusdtLassiterFranke2022.lw_conjAC (s : State) :

litWeight s Utt.conjAC = 0

noncomputable def GrusdtLassiterFranke2022.S1 (s : State) :

PMF Utt

Pragmatic speaker S1(· | s) ∝ L0(s | ·) (α = 1, no cost), normalising the literal weights over utterances.

Equations

GrusdtLassiterFranke2022.S1 s = PMF.normalize (GrusdtLassiterFranke2022.litWeight s) ⋯ ⋯

Instances For

theorem GrusdtLassiterFranke2022.S1_lt_iff (s : State) (u₁ u₂ : Utt) :

(S1 s) u₁ < (S1 s) u₂ ↔ litWeight s u₁ < litWeight s u₂

Same-state utterance preference reduces to comparing literal weights — the speaker's partition function cancels.

theorem GrusdtLassiterFranke2022.S1_ne_zero {s : State} {u : Utt} (h : litWeight s u ≠ 0) :

(S1 s) u ≠ 0

noncomputable def GrusdtLassiterFranke2022.worldPrior :

Uniform world prior over the three states.

Equations

GrusdtLassiterFranke2022.worldPrior = PMF.uniformOfFintype GrusdtLassiterFranke2022.State

Instances For

theorem GrusdtLassiterFranke2022.worldPrior_ne_zero (s : State) :

worldPrior s ≠ 0

theorem GrusdtLassiterFranke2022.marginal_conditional_ne_zero :

PMF.marginal S1 worldPrior Utt.conditional ≠ 0

theorem GrusdtLassiterFranke2022.marginal_C_ne_zero :

PMF.marginal S1 worldPrior Utt.C ≠ 0

theorem GrusdtLassiterFranke2022.marginal_likelyC_ne_zero :

PMF.marginal S1 worldPrior Utt.likelyC ≠ 0

noncomputable def GrusdtLassiterFranke2022.L1 (u : Utt) (h : PMF.marginal S1 worldPrior u ≠ 0) :

Pragmatic listener L1(· | u): the Bayesian posterior of S1 against the uniform world prior.

Equations

GrusdtLassiterFranke2022.L1 u h = PMF.posterior GrusdtLassiterFranke2022.S1 GrusdtLassiterFranke2022.worldPrior u h

Instances For

Partition functions Z(s) = ∑_u L0(s | u) per state (s1: 11/6, s2: 5/6, s3: 1/3). A smaller partition means a sharper speaker, so L1 prefers the world with the smaller partition when the numerators agree.

S1 predictions from the toy example (Table 2) #

The pragmatic speaker in each state prefers the most informative true utterance. Informativity is measured by L0's posterior concentration: utterances that are true in fewer states are more informative.

s1: "C" > "conditional" > "likely C" (C is true in 1 state, conditional in 2, likely C in 3)
s2: "conditional" > "likely C" (conditional in 2 states, likely C in 3; C and conjAC are false)
s3: "likely C" dominates (only true utterance; conditional, C, and conjAC are all false)

The ordering follows informativity: utterances true in fewer states give L0 a sharper posterior, yielding higher S1 scores.

theorem GrusdtLassiterFranke2022.s1_C_gt_conditional :

(S1 State.s1) Utt.C > (S1 State.s1) Utt.conditional

s1: S1 prefers "C" over "if A then C."

In s1, both "C" and "conditional" are true, but "C" is true only in s1 while "conditional" is true in both s1 and s2. So "C" is more informative. S1(C|s1) = 6/11, S1(conditional|s1) = 3/11.

theorem GrusdtLassiterFranke2022.s1_conditional_gt_likelyC :

(S1 State.s1) Utt.conditional > (S1 State.s1) Utt.likelyC

s1: S1 prefers "if A then C" over "likely C."

"conditional" is true in 2 states vs "likely C" in all 3. S1(conditional|s1) = 3/11, S1(likelyC|s1) = 2/11.

theorem GrusdtLassiterFranke2022.s2_conditional_gt_likelyC :

(S1 State.s2) Utt.conditional > (S1 State.s2) Utt.likelyC

s2: S1 prefers "if A then C" over "likely C."

In s2, "conditional" is true in 2 states while "likely C" is true in all 3. S1(conditional|s2) = 3/5, S1(likelyC|s2) = 2/5.

theorem GrusdtLassiterFranke2022.s2_conditional_gt_C :

(S1 State.s2) Utt.conditional > (S1 State.s2) Utt.C

s2: S1 prefers "if A then C" over "C."

"C" is false in s2 (P(C) = 0.65 < 0.9), so S1 assigns it zero.

theorem GrusdtLassiterFranke2022.s3_likelyC_dominates :

(S1 State.s3) Utt.likelyC > (S1 State.s3) Utt.conditional

s3: "likely C" dominates — no other utterance beats it.

"likely C" is the only true utterance in s3. The conditional, C, and conjAC are all false, so they get zero S1 score.

L1 predictions: the core dependency inference result #

The central prediction: hearing "if A then C" makes the pragmatic listener infer s2 (moderate dependence) over s1 (high marginals). This is because S1 in s1 would have used the more informative "C" instead of the conditional.

This is the key mechanism behind dependency inference: conditionals signal that the speaker could not have used a stronger utterance, implicating a state where only the conditional is assertable.

Each L1 comparison cancels the shared marginal and uniform prior (PMF.posterior_lt_iff_kernel_lt_of_uniform), reducing to an S1 comparison across states: a vacuous-zero at the world where the utterance is false, or a partition-dominance where the numerators agree.

theorem GrusdtLassiterFranke2022.l1_conditional_prefers_s2 :

(L1 Utt.conditional marginal_conditional_ne_zero) State.s2 > (L1 Utt.conditional marginal_conditional_ne_zero) State.s1

L1 hearing "if A then C": prefers s2 over s1.

The core dependency inference result. S1 in s1 would prefer "C" over "conditional" (by s1_C_gt_conditional), so hearing "conditional" makes L1 shift probability toward s2 where "conditional" is the best available utterance.

theorem GrusdtLassiterFranke2022.l1_conditional_s2_gt_s3 :

(L1 Utt.conditional marginal_conditional_ne_zero) State.s2 > (L1 Utt.conditional marginal_conditional_ne_zero) State.s3

L1 hearing "if A then C": prefers s2 over s3.

s3 makes the conditional literally false, so it gets zero L1 weight.

theorem GrusdtLassiterFranke2022.l1_C_identifies_s1 :

(L1 Utt.C marginal_C_ne_zero) State.s1 > (L1 Utt.C marginal_C_ne_zero) State.s2

L1 hearing "C": identifies s1.

"C" is true only in s1, so L1 assigns it probability 1.

theorem GrusdtLassiterFranke2022.l1_likelyC_prefers_s3 :

(L1 Utt.likelyC marginal_likelyC_ne_zero) State.s3 > (L1 Utt.likelyC marginal_likelyC_ne_zero) State.s1

L1 hearing "likely C": prefers s3 over s1.

"likely C" is true in all states, but S1 in s1 prefers "C" and S1 in s2 prefers "conditional," so hearing "likely C" implicates that stronger utterances were unavailable — i.e., the state is s3 where "likely C" is the only option. L1(s3|likelyC) = 55/87 > L1(s1|likelyC) = 10/87.

theorem GrusdtLassiterFranke2022.conditional_assertable_iff_high_pCGivenA :

(assertable' Utt.conditional State.s1 = true ∧ ws1.pCGivenA ≥ θ) ∧ (assertable' Utt.conditional State.s2 = true ∧ ws2.pCGivenA ≥ θ) ∧ assertable' Utt.conditional State.s3 = false ∧ ws3.pCGivenA < θ

The conditional's meaning in the RSA model equals the assertability condition: assertable iff P(C|A) ≥ θ. Since we use the direct truth table, we verify consistency with the WorldState probabilities.

theorem GrusdtLassiterFranke2022.C_assertable_iff_high_pC :

(assertable' Utt.C State.s1 = true ∧ ws1.pC ≥ 9 / 10) ∧ (assertable' Utt.C State.s2 = false ∧ ws2.pC < 9 / 10) ∧ assertable' Utt.C State.s3 = false ∧ ws3.pC < 9 / 10

"C" is assertable iff P(C) ≥ 0.9.

theorem GrusdtLassiterFranke2022.likelyC_always_assertable :

(assertable' Utt.likelyC State.s1 = true ∧ ws1.pC ≥ 1 / 2) ∧ (assertable' Utt.likelyC State.s2 = true ∧ ws2.pC ≥ 1 / 2) ∧ assertable' Utt.likelyC State.s3 = true ∧ ws3.pC ≥ 1 / 2

"likely C" is assertable in all states (P(C) ≥ 0.5 everywhere).

theorem GrusdtLassiterFranke2022.conjAC_never_assertable :

assertable' Utt.conjAC State.s1 = false ∧ assertable' Utt.conjAC State.s2 = false ∧ assertable' Utt.conjAC State.s3 = false

"A and C" is never assertable (P(A∧C) < 0.9 in all states).

Connection to causal inference #

The toy example does not include causal relations as a latent variable (the full model in §3 does). However, the key qualitative prediction — that conditionals signal dependency between A and C — is captured by the L1 inference: hearing "if A then C" makes the listener prefer s2 (where A and C are strongly correlated: P(C|A) = 12/13 ≈ 0.923) over s1 (where A and C have high marginals but weaker per-unit correlation).

The full model adds CausalRelation (A→C, C→A, A⊥C) as a latent variable, but the dependency inference result already emerges from the simpler model via scalar implicature.

theorem GrusdtLassiterFranke2022.causal_asymmetry_detection (ws : Causation.BayesNet.WorldState) (thr : ℚ) (h_fwd : Semantics.Probabilistic.ConditionalAssertability.assertable ws thr = true) (h_bwd : Semantics.Probabilistic.ConditionalAssertability.reverseAssertable ws thr = false) :

Semantics.Probabilistic.ConditionalAssertability.inferCausalRelation ws thr = Causation.BayesNet.CausalRelation.ACausesC

Causal asymmetry detection from assertability patterns.

If the forward conditional "if A then C" is assertable but the reverse "if C then A" is not, inferCausalRelation returns .ACausesC.

theorem GrusdtLassiterFranke2022.perfection_not_semantic :

∃ (ws : Causation.BayesNet.WorldState), Semantics.Probabilistic.ConditionalAssertability.assertable ws (9 / 10) = true ∧ Semantics.Probabilistic.ConditionalAssertability.contrapositiveAssertable ws (9 / 10) = false

Conditional perfection is NOT a semantic entailment.

There exist world states where "if A then C" is assertable but the converse "if ¬A then ¬C" need not be. This supports the paper's claim that conditional perfection is a pragmatic implicature, not entailment.

structure GrusdtLassiterFranke2022.Experiment1Result :

Experiment 1 result: causal structure inference from conditionals.

Participants (N≈150) hear "if A then C" and judge causal structure. The asymmetry between forward and reverse conditionals is the key finding.

utterance : String
pACausesC : ℚ
pCCausesA : ℚ
pIndependent : ℚ

Instances For

@[implicit_reducible]

instance GrusdtLassiterFranke2022.instReprExperiment1Result :

Repr Experiment1Result

Equations

GrusdtLassiterFranke2022.instReprExperiment1Result = { reprPrec := GrusdtLassiterFranke2022.instReprExperiment1Result.repr }

def GrusdtLassiterFranke2022.instReprExperiment1Result.repr :

Experiment1Result → ℕ → Std.Format

Equations

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

Instances For

def GrusdtLassiterFranke2022.conditionalResult :

Experiment1Result

Equations

GrusdtLassiterFranke2022.conditionalResult = { utterance := "if A then C", pACausesC := 72 / 100, pCCausesA := 18 / 100, pIndependent := 10 / 100 }

Instances For

def GrusdtLassiterFranke2022.reverseConditionalResult :

Experiment1Result

Equations

GrusdtLassiterFranke2022.reverseConditionalResult = { utterance := "if C then A", pACausesC := 15 / 100, pCCausesA := 75 / 100, pIndependent := 10 / 100 }

Instances For

def GrusdtLassiterFranke2022.fittedThreshold :

ℚ

Fitted assertability threshold from Experiment 3.

Equations

GrusdtLassiterFranke2022.fittedThreshold = 88 / 100

Instances For

structure GrusdtLassiterFranke2022.PerfectionResult :

Experiment 2 perfection rates by causal context.

causalContext : Causation.BayesNet.CausalRelation
perfectionRate : ℚ

Instances For

def GrusdtLassiterFranke2022.instReprPerfectionResult.repr :

PerfectionResult → ℕ → Std.Format

Equations

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

Instances For

@[implicit_reducible]

instance GrusdtLassiterFranke2022.instReprPerfectionResult :

Repr PerfectionResult

Equations

GrusdtLassiterFranke2022.instReprPerfectionResult = { reprPrec := GrusdtLassiterFranke2022.instReprPerfectionResult.repr }

def GrusdtLassiterFranke2022.perfectionInCausal :

PerfectionResult

Equations

GrusdtLassiterFranke2022.perfectionInCausal = { causalContext := Causation.BayesNet.CausalRelation.ACausesC, perfectionRate := 85 / 100 }

Instances For

def GrusdtLassiterFranke2022.perfectionInIndependent :

PerfectionResult

Equations

GrusdtLassiterFranke2022.perfectionInIndependent = { causalContext := Causation.BayesNet.CausalRelation.Independent, perfectionRate := 45 / 100 }

Instances For

theorem GrusdtLassiterFranke2022.perfection_modulated_by_context :

perfectionInCausal.perfectionRate > perfectionInIndependent.perfectionRate

Conditional perfection is modulated by causal context: much higher in A→C contexts than in independent contexts.

Key claims supported by the model #

Conditionals communicate dependency: L1 hearing "if A then C" infers a state with high P(C|A) relative to P(C) — i.e., a state where A and C are dependent. This is l1_conditional_prefers_s2.
Conditional perfection is pragmatic: The semantic meaning of conditionals (assertability) does NOT entail perfection (perfection_not_semantic). Perfection arises via scalar implicature in the full model.
Speaker informativity drives inference: S1 in s1 prefers "C" over "conditional" (s1_C_gt_conditional), so hearing "conditional" implicates that "C" was unavailable (i.e., the state is s2, not s1).
Weak states produce weak utterances: In s3, the speaker can only use "likely C" (s3_likelyC_dominates). Hearing "likely C" makes L1 infer s3 (l1_likelyC_prefers_s3), the state with weakest dependence.

The earlier Structural ↔ Probabilistic Bridge section (≈150 LOC) parameterised on the legacy CausalDynamics / Situation / causallySufficient / causallyNecessary substrate was dropped along with that substrate. The qualitative claim — structural sufficiency ∧ necessity ⇒ probabilistic ACausesC — is now witnessed at the V2 SEM level by [NL20]'s Fire/Bus/Lighthouse scenarios (NadathurLauer2020.{Fire,Bus,Lighthouse}): the make/cause divergence cases concretely demonstrate sufficiency without necessity (Bus) and necessity without sufficiency (Fire); the GLF2022 RSA model above uses WorldState directly without going through a structural-causal extractor.