Documentation

Linglib.Phenomena.Quantification.Studies.TesslerTenenbaumGoodman2022

@cite{tessler-tenenbaum-goodman-2022} — Logic, Probability, and Pragmatics in Syllogistic Reasoning #

Topics in Cognitive Science 14: 574–601.

Core Idea #

Syllogistic reasoning decomposes into two pragmatic subproblems:

Listener: interprets premises via Bayesian update over Venn diagram states
Speaker: selects the conclusion that best communicates beliefs to a naive listener

Three speaker models are formalized:

S₀ (Literal Speaker, eq. 3): scores conclusions by expected literal truth
State Communication (eq. 4): scores by expected log-likelihood (standard RSA)
Belief Alignment (eq. 6): scores by −KL divergence (the paper's winning model, r = .82 with 3 parameters: α, φ, β)

State Communication and Belief Alignment produce identical conclusion distributions after softmax normalization (they differ by an additive constant H(post) that cancels); their distinct fitted parameters reflect the fitting procedure, not the functional form. This equivalence is proved as stateCom_eq_beliefAlignment.

Grounding in Linglib #

Syllogistic quantifiers are every_sem/some_sem/no_sem from Quantifier.lean applied to Venn diagram regions as entities
Subalternation (All→Some) proved via subalternation_a_i from Quantifier.lean
Noisy semantics via RSA.Noise.noiseChannel
Belief Alignment utility via Core.Divergence.klDivergence
SC ≡ BA equivalence via Core.Divergence.kl_eq_neg_crossEntropy_plus_negEntropy
"Nothing follows" as vacuous utterance (true in every state)

inductive Phenomena.Quantification.Studies.TesslerTenenbaumGoodman2022.Region :

The 7 non-empty regions of a three-circle (A, B, C) Venn diagram. The empty region {¬A, ¬B, ¬C} does not affect quantifier truth conditions for all, some, some...not, none, and is excluded.

A : Region
B : Region
C : Region
AB : Region
AC : Region
BC : Region
ABC : Region

Instances For

instance Phenomena.Quantification.Studies.TesslerTenenbaumGoodman2022.instDecidableEqRegion :

DecidableEq Region

Equations

Phenomena.Quantification.Studies.TesslerTenenbaumGoodman2022.instDecidableEqRegion x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

instance Phenomena.Quantification.Studies.TesslerTenenbaumGoodman2022.instBEqRegion :

Equations

Phenomena.Quantification.Studies.TesslerTenenbaumGoodman2022.instBEqRegion = { beq := Phenomena.Quantification.Studies.TesslerTenenbaumGoodman2022.instBEqRegion.beq }

def Phenomena.Quantification.Studies.TesslerTenenbaumGoodman2022.instBEqRegion.beq :

Region → Region → Bool

Equations

Phenomena.Quantification.Studies.TesslerTenenbaumGoodman2022.instBEqRegion.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

Instances For

def Phenomena.Quantification.Studies.TesslerTenenbaumGoodman2022.instReprRegion.repr :

Region → ℕ → Std.Format

Equations

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

Instances For

instance Phenomena.Quantification.Studies.TesslerTenenbaumGoodman2022.instReprRegion :

Equations

Phenomena.Quantification.Studies.TesslerTenenbaumGoodman2022.instReprRegion = { reprPrec := Phenomena.Quantification.Studies.TesslerTenenbaumGoodman2022.instReprRegion.repr }

instance Phenomena.Quantification.Studies.TesslerTenenbaumGoodman2022.instInhabitedRegion :

Inhabited Region

Equations

Phenomena.Quantification.Studies.TesslerTenenbaumGoodman2022.instInhabitedRegion = { default := Phenomena.Quantification.Studies.TesslerTenenbaumGoodman2022.instInhabitedRegion.default }

def Phenomena.Quantification.Studies.TesslerTenenbaumGoodman2022.instInhabitedRegion.default :

Equations

Phenomena.Quantification.Studies.TesslerTenenbaumGoodman2022.instInhabitedRegion.default = Phenomena.Quantification.Studies.TesslerTenenbaumGoodman2022.Region.A

Instances For

instance Phenomena.Quantification.Studies.TesslerTenenbaumGoodman2022.instFintypeRegion :

Equations

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

@[reducible, inline]

abbrev Phenomena.Quantification.Studies.TesslerTenenbaumGoodman2022.VennState :

A Venn state: which regions are populated. 2⁷ = 128 possible states.

Equations

Phenomena.Quantification.Studies.TesslerTenenbaumGoodman2022.VennState = (Phenomena.Quantification.Studies.TesslerTenenbaumGoodman2022.Region → Bool)

Instances For

def Phenomena.Quantification.Studies.TesslerTenenbaumGoodman2022.regionModel :

Semantics.Montague.Model

Regions as a Montague model, enabling reuse of every_sem/some_sem/no_sem.

Equations

Phenomena.Quantification.Studies.TesslerTenenbaumGoodman2022.regionModel = { Entity := Phenomena.Quantification.Studies.TesslerTenenbaumGoodman2022.Region, decEq := inferInstance }

Instances For

instance Phenomena.Quantification.Studies.TesslerTenenbaumGoodman2022.regionFM :

Fintype regionModel.Entity

Equations

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

def Phenomena.Quantification.Studies.TesslerTenenbaumGoodman2022.syllAll (s : VennState) (X Y : Region → Bool) :

"All Xs are Ys" in state s: every populated X-region also has Y, AND there is at least one populated X-region (existential import).

Per @cite{tessler-tenenbaum-goodman-2022} footnote 4: "All As are Bs is false if there are no As." This ensures All entails Some. Grounded in every_sem and some_sem from Quantifier.lean.

Equations

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

Instances For

def Phenomena.Quantification.Studies.TesslerTenenbaumGoodman2022.syllSome (s : VennState) (X Y : Region → Bool) :

"Some Xs are Ys": some populated X-region also has Y.

Equations

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

Instances For

def Phenomena.Quantification.Studies.TesslerTenenbaumGoodman2022.syllSomeNot (s : VennState) (X Y : Region → Bool) :

"Some Xs are not Ys": some populated X-region lacks Y.

Equations

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

Instances For

def Phenomena.Quantification.Studies.TesslerTenenbaumGoodman2022.syllNone (s : VennState) (X Y : Region → Bool) :

"No Xs are Ys": no populated X-region has Y.

Equations

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

Instances For

inductive Phenomena.Quantification.Studies.TesslerTenenbaumGoodman2022.SyllQuant :

Syllogistic quantifier: the four Aristotelian quantifiers.

all : SyllQuant
some : SyllQuant
someNot : SyllQuant
no : SyllQuant

Instances For

instance Phenomena.Quantification.Studies.TesslerTenenbaumGoodman2022.instDecidableEqSyllQuant :

DecidableEq SyllQuant

Equations

Phenomena.Quantification.Studies.TesslerTenenbaumGoodman2022.instDecidableEqSyllQuant x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

instance Phenomena.Quantification.Studies.TesslerTenenbaumGoodman2022.instBEqSyllQuant :

Equations

Phenomena.Quantification.Studies.TesslerTenenbaumGoodman2022.instBEqSyllQuant = { beq := Phenomena.Quantification.Studies.TesslerTenenbaumGoodman2022.instBEqSyllQuant.beq }

def Phenomena.Quantification.Studies.TesslerTenenbaumGoodman2022.instBEqSyllQuant.beq :

SyllQuant → SyllQuant → Bool

Equations

Phenomena.Quantification.Studies.TesslerTenenbaumGoodman2022.instBEqSyllQuant.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

Instances For

instance Phenomena.Quantification.Studies.TesslerTenenbaumGoodman2022.instReprSyllQuant :

Equations

Phenomena.Quantification.Studies.TesslerTenenbaumGoodman2022.instReprSyllQuant = { reprPrec := Phenomena.Quantification.Studies.TesslerTenenbaumGoodman2022.instReprSyllQuant.repr }

def Phenomena.Quantification.Studies.TesslerTenenbaumGoodman2022.instReprSyllQuant.repr :

SyllQuant → ℕ → Std.Format

Equations

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

Instances For

def Phenomena.Quantification.Studies.TesslerTenenbaumGoodman2022.instInhabitedSyllQuant.default :

Equations

Phenomena.Quantification.Studies.TesslerTenenbaumGoodman2022.instInhabitedSyllQuant.default = Phenomena.Quantification.Studies.TesslerTenenbaumGoodman2022.SyllQuant.all

Instances For

instance Phenomena.Quantification.Studies.TesslerTenenbaumGoodman2022.instInhabitedSyllQuant :

Inhabited SyllQuant

Equations

Phenomena.Quantification.Studies.TesslerTenenbaumGoodman2022.instInhabitedSyllQuant = { default := Phenomena.Quantification.Studies.TesslerTenenbaumGoodman2022.instInhabitedSyllQuant.default }

instance Phenomena.Quantification.Studies.TesslerTenenbaumGoodman2022.instFintypeSyllQuant :

Fintype SyllQuant

Equations

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

structure Phenomena.Quantification.Studies.TesslerTenenbaumGoodman2022.Syllogism :

A syllogism is a pair of quantified premises sharing middle term B. order1AB = true means premise 1 is "Q₁ A-B"; false means "Q₁ B-A". order2BC = true means premise 2 is "Q₂ B-C"; false means "Q₂ C-B". This gives 4 × 2 × 4 × 2 = 64 syllogisms.

q1 : SyllQuant
order1AB : Bool
q2 : SyllQuant
order2BC : Bool

Instances For

instance Phenomena.Quantification.Studies.TesslerTenenbaumGoodman2022.instDecidableEqSyllogism :

DecidableEq Syllogism

Equations

Phenomena.Quantification.Studies.TesslerTenenbaumGoodman2022.instDecidableEqSyllogism = Phenomena.Quantification.Studies.TesslerTenenbaumGoodman2022.instDecidableEqSyllogism.decEq

def Phenomena.Quantification.Studies.TesslerTenenbaumGoodman2022.instDecidableEqSyllogism.decEq (x✝ x✝¹ : Syllogism) :

Decidable (x✝ = x✝¹)

Equations

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

Instances For

instance Phenomena.Quantification.Studies.TesslerTenenbaumGoodman2022.instBEqSyllogism :

Equations

Phenomena.Quantification.Studies.TesslerTenenbaumGoodman2022.instBEqSyllogism = { beq := Phenomena.Quantification.Studies.TesslerTenenbaumGoodman2022.instBEqSyllogism.beq }

def Phenomena.Quantification.Studies.TesslerTenenbaumGoodman2022.instBEqSyllogism.beq :

Syllogism → Syllogism → Bool

Equations

One or more equations did not get rendered due to their size.
Phenomena.Quantification.Studies.TesslerTenenbaumGoodman2022.instBEqSyllogism.beq x✝¹ x✝ = false

Instances For

def Phenomena.Quantification.Studies.TesslerTenenbaumGoodman2022.instReprSyllogism.repr :

Syllogism → ℕ → Std.Format

Equations

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

Instances For

instance Phenomena.Quantification.Studies.TesslerTenenbaumGoodman2022.instReprSyllogism :

Equations

Phenomena.Quantification.Studies.TesslerTenenbaumGoodman2022.instReprSyllogism = { reprPrec := Phenomena.Quantification.Studies.TesslerTenenbaumGoodman2022.instReprSyllogism.repr }

instance Phenomena.Quantification.Studies.TesslerTenenbaumGoodman2022.instInhabitedSyllogism :

Inhabited Syllogism

Equations

Phenomena.Quantification.Studies.TesslerTenenbaumGoodman2022.instInhabitedSyllogism = { default := Phenomena.Quantification.Studies.TesslerTenenbaumGoodman2022.instInhabitedSyllogism.default }

def Phenomena.Quantification.Studies.TesslerTenenbaumGoodman2022.instInhabitedSyllogism.default :

Equations

Phenomena.Quantification.Studies.TesslerTenenbaumGoodman2022.instInhabitedSyllogism.default = { q1 := default, order1AB := default, q2 := default, order2BC := default }

Instances For

inductive Phenomena.Quantification.Studies.TesslerTenenbaumGoodman2022.Conclusion :

The 9 possible conclusions: 4 quantifiers × 2 term orders + NVC.

allAC : Conclusion
allCA : Conclusion
someAC : Conclusion
someCA : Conclusion
someNotAC : Conclusion
someNotCA : Conclusion
noAC : Conclusion
noCA : Conclusion
nvc : Conclusion

Instances For

instance Phenomena.Quantification.Studies.TesslerTenenbaumGoodman2022.instDecidableEqConclusion :

DecidableEq Conclusion

Equations

Phenomena.Quantification.Studies.TesslerTenenbaumGoodman2022.instDecidableEqConclusion x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Phenomena.Quantification.Studies.TesslerTenenbaumGoodman2022.instBEqConclusion.beq :

Conclusion → Conclusion → Bool

Equations

Phenomena.Quantification.Studies.TesslerTenenbaumGoodman2022.instBEqConclusion.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

Instances For

instance Phenomena.Quantification.Studies.TesslerTenenbaumGoodman2022.instBEqConclusion :

Equations

Phenomena.Quantification.Studies.TesslerTenenbaumGoodman2022.instBEqConclusion = { beq := Phenomena.Quantification.Studies.TesslerTenenbaumGoodman2022.instBEqConclusion.beq }

instance Phenomena.Quantification.Studies.TesslerTenenbaumGoodman2022.instReprConclusion :

Repr Conclusion

Equations

Phenomena.Quantification.Studies.TesslerTenenbaumGoodman2022.instReprConclusion = { reprPrec := Phenomena.Quantification.Studies.TesslerTenenbaumGoodman2022.instReprConclusion.repr }

def Phenomena.Quantification.Studies.TesslerTenenbaumGoodman2022.instReprConclusion.repr :

Conclusion → ℕ → Std.Format

Equations

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

Instances For

instance Phenomena.Quantification.Studies.TesslerTenenbaumGoodman2022.instInhabitedConclusion :

Inhabited Conclusion

Equations

Phenomena.Quantification.Studies.TesslerTenenbaumGoodman2022.instInhabitedConclusion = { default := Phenomena.Quantification.Studies.TesslerTenenbaumGoodman2022.instInhabitedConclusion.default }

def Phenomena.Quantification.Studies.TesslerTenenbaumGoodman2022.instInhabitedConclusion.default :

Equations

Phenomena.Quantification.Studies.TesslerTenenbaumGoodman2022.instInhabitedConclusion.default = Phenomena.Quantification.Studies.TesslerTenenbaumGoodman2022.Conclusion.allAC

Instances For

instance Phenomena.Quantification.Studies.TesslerTenenbaumGoodman2022.instFintypeConclusion :

Fintype Conclusion

Equations

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

def Phenomena.Quantification.Studies.TesslerTenenbaumGoodman2022.Conclusion.isAC :

Conclusion → Bool

Does the conclusion use A→C term order (vs C→A)? Used for the figural bias parameter β.

Equations

Instances For

def Phenomena.Quantification.Studies.TesslerTenenbaumGoodman2022.figuralWeight (β : ℚ) (syl : Syllogism) (c : Conclusion) :

Figural bias prior weight, determined by the Aristotelian figure.

The "figural effect" biases toward conclusions whose end-term order matches the chain direction through the middle term B:

Figure 1 (A-B, B-C): B is predicate of P1, subject of P2 → chain reads A→B→C → A-C conclusions get weight β
Figure 4 (B-A, C-B): B is subject of P1, predicate of P2 → chain reads C→B→A → C-A conclusions get weight β
Figures 2 & 3: B occupies the same position in both premises → no directional chain → all conclusions get weight 1

NVC always gets weight 1 (no directional bias for "nothing follows"). The paper fits β ≈ 2.01 (MAP).

Equations

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

Instances For

def Phenomena.Quantification.Studies.TesslerTenenbaumGoodman2022.concMeaning :

Conclusion → VennState → Bool

Literal meaning of each conclusion in a Venn state. "Nothing follows" is true in every state — the vacuous utterance.

Equations

One or more equations did not get rendered due to their size.
Phenomena.Quantification.Studies.TesslerTenenbaumGoodman2022.concMeaning Phenomena.Quantification.Studies.TesslerTenenbaumGoodman2022.Conclusion.nvc x✝ = true

Instances For

theorem Phenomena.Quantification.Studies.TesslerTenenbaumGoodman2022.nvc_always_true (s : VennState) :

concMeaning Conclusion.nvc s = true

"Nothing follows" is always true: the key insight enabling the Belief Alignment model to rationally produce NVC when premises are uninformative.

theorem Phenomena.Quantification.Studies.TesslerTenenbaumGoodman2022.barbara_valid (s : VennState) (h1 : syllAll s hasA hasB = true) (h2 : syllAll s hasB hasC = true) :

syllAll s hasA hasC = true

Barbara (All A-B, All B-C ⊢ All A-C) is logically valid.

The proof chains through populated regions: if r is a populated A-region, premise 1 gives it B, making it a populated B-region, and premise 2 gives it C. This is a state-restricted form of transitivity — stricter than every_transitive from Quantifier.lean, which applies to unrestricted universal quantification. Here the restrictors shift between premises (s ∧ hasA vs s ∧ hasB), and the middle term B bridges them via the population predicate s.

theorem Phenomena.Quantification.Studies.TesslerTenenbaumGoodman2022.barbara_some_valid (s : VennState) (h1 : syllAll s hasA hasB = true) (h2 : syllAll s hasB hasC = true) :

syllSome s hasA hasC = true

Barbara also validates "Some A are C" (by subalternation: All → Some). Uses barbara_valid for the All A-C premise, then extracts the existential import — with existential import in syllAll, the non-emptiness hypothesis is built in, so no separate witness needed.

theorem Phenomena.Quantification.Studies.TesslerTenenbaumGoodman2022.allAB_allCB_invalid :

concMeaning Conclusion.allAC Phenomena.Quantification.Studies.TesslerTenenbaumGoodman2022.state_AB_BC✝ = false ∧ concMeaning Conclusion.someAC Phenomena.Quantification.Studies.TesslerTenenbaumGoodman2022.state_AB_BC✝¹ = false ∧ concMeaning Conclusion.allCA Phenomena.Quantification.Studies.TesslerTenenbaumGoodman2022.state_AB_BC✝² = false ∧ concMeaning Conclusion.someCA Phenomena.Quantification.Studies.TesslerTenenbaumGoodman2022.state_AB_BC✝³ = false ∧ concMeaning Conclusion.noAC Phenomena.Quantification.Studies.TesslerTenenbaumGoodman2022.state_ABC✝ = false ∧ concMeaning Conclusion.someNotAC Phenomena.Quantification.Studies.TesslerTenenbaumGoodman2022.state_ABC✝¹ = false ∧ concMeaning Conclusion.noCA Phenomena.Quantification.Studies.TesslerTenenbaumGoodman2022.state_ABC✝² = false ∧ concMeaning Conclusion.someNotCA Phenomena.Quantification.Studies.TesslerTenenbaumGoodman2022.state_ABC✝³ = false

"All A-B, All C-B" is logically invalid: no Aristotelian conclusion holds in all compatible states. Proof by two counterexamples.

def Phenomena.Quantification.Studies.TesslerTenenbaumGoodman2022.noisyConcMeaning (φ : ℚ) (c : Conclusion) (s : VennState) :

Noisy semantics ℒ(u, s): a small probability φ of misjudging truth value. Directly instantiates RSA.Noise.noiseChannel(1−φ, φ, ⟦u⟧): ℒ(u,s) = 1−φ when ⟦u⟧(s) = true, φ when false.

Equations

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

Instances For

theorem Phenomena.Quantification.Studies.TesslerTenenbaumGoodman2022.noisyConcMeaning_zero (c : Conclusion) (s : VennState) :

noisyConcMeaning 0 c s = if concMeaning c s = true then 1 else 0

When noise is zero, noisy meaning reduces to literal meaning.

theorem Phenomena.Quantification.Studies.TesslerTenenbaumGoodman2022.noisyConcMeaning_nvc (φ : ℚ) (s : VennState) :

noisyConcMeaning φ Conclusion.nvc s = 1 - φ

Noisy semantics assigns the NVC utterance a constant value in every state, since concMeaning .nvc s = true for all s. This means L₀(s|NVC) = P(s): hearing "nothing follows" does not update the listener's beliefs.

def Phenomena.Quantification.Studies.TesslerTenenbaumGoodman2022.l0PremiseLikelihood (φ : ℚ) (p1 p2 : VennState → Bool) (s : VennState) :

L₀ joint likelihood of two premises in state s (unnormalized).

Computes ℒ(u₁,s) · ℒ(u₂,s) — the likelihood term only. The full L₀ posterior (eq. 2) also includes the state prior P(s). The paper fixes θ = 0.5 per region, making P(s) = 0.5⁷ = 1/128 for all states — a uniform prior that cancels in normalization. For this reason, the likelihood alone determines the relative posterior weights.

Equations

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

Instances For

noncomputable def Phenomena.Quantification.Studies.TesslerTenenbaumGoodman2022.literalSpeakerScore (premPost : VennState → ℝ) (α : ℝ) (c : Conclusion) :

S₀ (Literal Speaker, eq. 3): scores conclusions by expected literal truth under the reasoner's posterior.

S₀(u₃ | u₁,u₂) ∝ exp[α · Σ_s ℒ(u₃,s) · L₀(s|u₁,u₂)]

Here ℒ(u₃,s) is the deterministic semantic function (not the noisy version inside L₀). This speaker samples states from the posterior and randomly selects conclusions that are literally true.

Equations

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

Instances For

noncomputable def Phenomena.Quantification.Studies.TesslerTenenbaumGoodman2022.stateComScore (premPost : VennState → ℝ) (naivePost : Conclusion → VennState → ℝ) (α : ℝ) (c : Conclusion) :

State Communication (S₁, eq. 4): scores conclusions by expected log-likelihood — standard RSA informativity applied to syllogisms.

S₁(u₃ | u₁,u₂) ∝ exp[α · Σ_s L₀(s|u₁,u₂) · ln L₀(s|u₃)]

The two L₀ agents are distinct: L₀(s|u₁,u₂) is the reasoner who interpreted the premises; L₀(s|u₃) is a hypothetical naive listener who interprets just the conclusion. Both use noisy semantics (same φ).

Equations

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

Instances For

noncomputable def Phenomena.Quantification.Studies.TesslerTenenbaumGoodman2022.beliefAlignmentScore (premPost : VennState → ℝ) (naivePost : Conclusion → VennState → ℝ) (α : ℝ) (c : Conclusion) :

Belief Alignment (S₁, eq. 6): the paper's winning model. Scores conclusions by negative KL divergence between the reasoner's full posterior and the naive listener's posterior given the conclusion.

S₁(u₃ | u₁,u₂) ∝ exp[α · −KL(L₀(·|u₁,u₂) ‖ L₀(·|u₃))]

Uses Core.Divergence.klDivergence directly.

Equations

Phenomena.Quantification.Studies.TesslerTenenbaumGoodman2022.beliefAlignmentScore premPost naivePost α c = Real.exp (α * -Core.Divergence.klDivergence premPost (naivePost c))

Instances For

theorem Phenomena.Quantification.Studies.TesslerTenenbaumGoodman2022.stateCom_eq_beliefAlignment (premPost : VennState → ℝ) (naivePost : Conclusion → VennState → ℝ) (α : ℝ) (c : Conclusion) (hQ : ∀ (s : VennState), 0 < naivePost c s) :

beliefAlignmentScore premPost naivePost α c = Real.exp (α * -∑ s : VennState, premPost s * Real.log (premPost s)) * stateComScore premPost naivePost α c

State Communication and Belief Alignment differ by an additive constant (the entropy H(post)) that does not depend on the conclusion.

By kl_eq_neg_crossEntropy_plus_negEntropy from Divergence.lean: KL(P ∥ Q) = Σ P·log P − Σ P·log Q

So: −KL(P ∥ Q) = Σ P·log Q − Σ P·log P = [State Com utility] + H(P).

Since H(P) is constant in the conclusion c, it cancels in softmax normalization: both models produce identical conclusion distributions. The paper's different fit statistics (r = .67 vs .82) reflect different optimal α values found by MCMC, not different functional forms.

theorem Phenomena.Quantification.Studies.TesslerTenenbaumGoodman2022.beliefAlignment_nvc_uninformative (post prior : VennState → ℝ) (α : ℝ) :

beliefAlignmentScore post (fun (c : Conclusion) => if c = Conclusion.nvc then prior else fun (x : VennState) => 0) α Conclusion.nvc = Real.exp (α * -Core.Divergence.klDivergence post prior)

The Belief Alignment score for NVC depends on how much the premises shifted beliefs from the prior. When premises are uninformative (posterior ≈ prior), KL(post ‖ prior) ≈ 0, so −KL ≈ 0, and exp(α · 0) = 1 — the maximum score. This is why the model naturally produces NVC for uninformative premise combinations.

theorem Phenomena.Quantification.Studies.TesslerTenenbaumGoodman2022.all_entails_some_AC (s : VennState) (h : concMeaning Conclusion.allAC s = true) :

concMeaning Conclusion.someAC s = true

Subalternation in the region model: "All A are C" entails "Some A are C". With existential import built into syllAll, no separate non-emptiness hypothesis is needed — syllAll guarantees at least one A exists.

For the Belief Alignment model, this means "All A-C" produces a more peaked L₀ posterior than "Some A-C", yielding lower KL divergence and hence higher speaker utility — explaining why Barbara participants prefer "All" over the also-valid "Some".

theorem Phenomena.Quantification.Studies.TesslerTenenbaumGoodman2022.all_strictly_stronger_than_some :

concMeaning Conclusion.someAC Phenomena.Quantification.Studies.TesslerTenenbaumGoodman2022.state_A_AC✝ = true ∧ concMeaning Conclusion.allAC Phenomena.Quantification.Studies.TesslerTenenbaumGoodman2022.state_A_AC✝¹ = false

def Phenomena.Quantification.Studies.TesslerTenenbaumGoodman2022.syllQuantEval (q : SyllQuant) (s : VennState) (X Y : Region → Bool) :

Evaluate a syllogistic quantifier on given terms in a Venn state.

Equations

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

Instances For

def Phenomena.Quantification.Studies.TesslerTenenbaumGoodman2022.premise1Truth (syl : Syllogism) (s : VennState) :

Truth value of premise 1 in state s.

Equations

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

Instances For

def Phenomena.Quantification.Studies.TesslerTenenbaumGoodman2022.premise2Truth (syl : Syllogism) (s : VennState) :

Truth value of premise 2 in state s.

Equations

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

Instances For

def Phenomena.Quantification.Studies.TesslerTenenbaumGoodman2022.barbara :

Barbara: All A-B, All B-C. Figure 1 (paradigmatic valid syllogism).

Equations

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

Instances For

def Phenomena.Quantification.Studies.TesslerTenenbaumGoodman2022.allAB_allCB :

All A-B, All C-B. Figure 3 (paradigmatic invalid syllogism).

Equations

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

Instances For

def Phenomena.Quantification.Studies.TesslerTenenbaumGoodman2022.someSome :

Some A-B, Some B-C. Figure 1.

Equations

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

Instances For

def Phenomena.Quantification.Studies.TesslerTenenbaumGoodman2022.allStates :

All 128 Venn diagram states, enumerated for computable summation. Each state is a function Region → Bool indicating which regions are populated. Generated by the List monad over all 7 regions.

Equations

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

Instances For

def Phenomena.Quantification.Studies.TesslerTenenbaumGoodman2022.l0Unnorm (φ : ℚ) (syl : Syllogism) (s : VennState) :

Unnormalized L₀ likelihood for a syllogism in state s. Computes ℒ(p₁,s) · ℒ(p₂,s) where ℒ is noisy semantics. The uniform prior (θ = 0.5) cancels in normalization.

Equations

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

Instances For

def Phenomena.Quantification.Studies.TesslerTenenbaumGoodman2022.l0Z (φ : ℚ) (syl : Syllogism) :

Normalization constant: Σ_s L₀_unnorm(s). Computable via allStates.

Equations

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

Instances For

def Phenomena.Quantification.Studies.TesslerTenenbaumGoodman2022.l0Post (φ : ℚ) (syl : Syllogism) (s : VennState) :

Normalized L₀ posterior: L₀(s|premises) = L₀_unnorm(s) / Z.

Equations

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

Instances For

def Phenomena.Quantification.Studies.TesslerTenenbaumGoodman2022.naiveL0Z (φ : ℚ) (c : Conclusion) :

Normalization constant for naive L₀ on a single conclusion.

Equations

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

Instances For

def Phenomena.Quantification.Studies.TesslerTenenbaumGoodman2022.naiveL0Post (φ : ℚ) (c : Conclusion) (s : VennState) :

Naive L₀ posterior for a conclusion: L₀(s|c) ∝ ℒ(c,s). The naive listener has heard only the conclusion, not the premises.

Equations

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

Instances For

noncomputable def Phenomena.Quantification.Studies.TesslerTenenbaumGoodman2022.baScore (α : ℝ) (φ β : ℚ) (syl : Syllogism) (c : Conclusion) :

Belief Alignment score for conclusion c given syllogism syl. Uses the full pipeline: premises → L₀ posterior → KL → exp. Parameters: α (rationality), φ (noise), β (figural bias).

Equations

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

Instances For

noncomputable def Phenomena.Quantification.Studies.TesslerTenenbaumGoodman2022.conclusionProb (α : ℝ) (φ β : ℚ) (syl : Syllogism) (c : Conclusion) :

Conclusion probability: P(c|syl) = baScore(c) / Σ_c' baScore(c').

Equations

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

Instances For

noncomputable def Phenomena.Quantification.Studies.TesslerTenenbaumGoodman2022.α_fit :

MAP estimates from the Bayesian data analysis on Ragni et al. 2019 data. α ≈ 6.88, φ ≈ 0.06, β ≈ 2.01.

Equations

Phenomena.Quantification.Studies.TesslerTenenbaumGoodman2022.α_fit = 688 / 100

Instances For

def Phenomena.Quantification.Studies.TesslerTenenbaumGoodman2022.φ_fit :

Equations

Phenomena.Quantification.Studies.TesslerTenenbaumGoodman2022.φ_fit = 6 / 100

Instances For

def Phenomena.Quantification.Studies.TesslerTenenbaumGoodman2022.β_fit :

Equations

Phenomena.Quantification.Studies.TesslerTenenbaumGoodman2022.β_fit = 201 / 100

Instances For

def Phenomena.Quantification.Studies.TesslerTenenbaumGoodman2022.klFloat (P Q : VennState → Float) :

KL divergence over allStates in Float arithmetic. Skips states with P(s) = 0 (contributes 0 to KL by convention).

Equations

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

Instances For

def Phenomena.Quantification.Studies.TesslerTenenbaumGoodman2022.allConclusions :

List Conclusion

All 9 conclusions as a list.

Equations

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

Instances For

def Phenomena.Quantification.Studies.TesslerTenenbaumGoodman2022.predictFloat (α : Float) (φ β : ℚ) (syl : Syllogism) :

List (Conclusion × Float)

Compute conclusion distribution for a syllogism using Float arithmetic. L₀ posteriors are computed exactly in ℚ (via l0Post, naiveL0Post), then converted to Float for the KL divergence and softmax steps. Parameters: α (rationality, Float), φ and β (exact in ℚ).

Equations

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

Instances For

def Phenomena.Quantification.Studies.TesslerTenenbaumGoodman2022.Conclusion.short :

Conclusion → String

Short name for display.

Equations

Instances For

def Phenomena.Quantification.Studies.TesslerTenenbaumGoodman2022.showPrediction (α : Float) (φ β : ℚ) (syl : Syllogism) :

Compact string output for a syllogism's predicted distribution, showing conclusions sorted by predicted probability.

Equations

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

Instances For

theorem Phenomena.Quantification.Studies.TesslerTenenbaumGoodman2022.barbara_l0_concentrates_on_allAC (s : VennState) :

premise1Truth barbara s = true → premise2Truth barbara s = true → concMeaning Conclusion.allAC s = true

For Barbara (All A-B, All B-C), every L₀-probable state satisfies All A-C. Proof: states where both premises are literally true form a subset of states where All A-C holds (by barbara_valid).

With noise φ, the L₀ posterior concentrates on these states: the likelihood ℒ(p₁,s)·ℒ(p₂,s) is (1−φ)² for consistent states but only (1−φ)·φ, φ·(1−φ), or φ² for inconsistent ones.

This theorem verifies computably that every state where BOTH premises are literally true also satisfies All A-C — the semantic backbone of the Belief Alignment model's "All A-C" preference for Barbara.

For the invalid syllogism (All A-B, All C-B), the L₀ posterior does NOT concentrate on any single conclusion — some consistent states satisfy All A-C while others falsify it.