@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:

1. Listener: interprets premises via Bayesian update over Venn diagram states
2. 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 within each syllogism (the additive entropy term H(L₀(·|premises)) is conclusion-independent and cancels in the per-syllogism softmax; between syllogisms, this entropy varies, which is why the paper's MCMC fits report different optimal α values for SC vs BA — same functional form, different scale). This per-syllogism cancellation is proved as stateCom_eq_beliefAlignment.

Substrate (Semantics.Quantification.Syllogistic)

This file consumes the syllogistic substrate at Theories/Semantics/Quantification/:

• Region, VennState, AristQuant, Syllogism, Conclusion types
• hasA/hasB/hasC region predicates
• syllAll/syllSome/syllSomeNot/syllNone (modern FOL reading)
• barbara/allAB_allCB/someSome named syllogisms
• state_A_AC/state_AB_BC/state_ABC witness states
• Validity (barbara_valid) + invalidity (allAB_allCB_invalid) theorems

Per footnote 2 of @cite{tessler-tenenbaum-goodman-2022}, this paper takes the Aristotelian stance on the All form: "All As are Bs is false if there are no As." The substrate is modern (FOL); existential import is added here as a paper-local wrapper tesslerAll. Other Aristotelian forms (E, I, O) take the modern reading in this paper, so the asymmetric stance is encoded honestly.

RSA pipeline

• Noisy semantics via RSA.Noise.noiseChannel
• Belief Alignment utility via the inline discrete sum ∑ p · log(p/q) (the canonical PMF form is (P.klDiv Q).toReal, bridged by PMF.toReal_klDiv_eq_sum_log_div; the (VennState → ℝ) form is natural here)
• SC ≡ BA equivalence via Real.log_div + sum manipulation (Cover-Thomas identity KL = -H(P) - ∑ P log Q)
• "Nothing follows" as vacuous utterance (true in every state)

See also

• Core.Opposition.Probabilistic — the Bayesian listener's posterior probabilities P_μ[c] jointly satisfy the probabilistic Aristotelian inequalities (subalternation P[A] ≤ P[I], contradiction P[A]+P[O]=1, etc.). Tessler's speaker models are functionals of these probabilities; this is the natural framework for unifying RSA-syllogistic models with the broader Demey–Smessaert opposition-diagram tradition.

The paper engages the mental-models tradition (Khemlani & Johnson-Laird) and the Probability Heuristics Model @cite{chater-oaksford-1999}, fits parameters on the Ragni et al. 2019 dataset; bib entries for the latter two are deferred pending verified DOI/page metadata.

def TesslerTenenbaumGoodman2022.tesslerAll (s : Semantics.Quantification.Syllogistic.VennState) (X Y : Semantics.Quantification.Syllogistic.Region → Bool) : Bool

The paper's Aristotelian "All": existential import on the restrictor. "All Xs are Ys" presupposes that some X exists, per footnote 2: "All As are Bs is false if there are no As."

Equations

• TesslerTenenbaumGoodman2022.tesslerAll s X Y = (Semantics.Quantification.Syllogistic.syllAll s X Y && decide (∃ (r : Semantics.Quantification.Syllogistic.Region), s r = true ∧ X r = true))

def TesslerTenenbaumGoodman2022.tesslerSyllQuantEval (q : Semantics.Quantification.Syllogistic.AristQuant) (s : Semantics.Quantification.Syllogistic.VennState) (X Y : Semantics.Quantification.Syllogistic.Region → Bool) : Bool

Paper-specific quantifier eval: Aristotelian on All, modern on the others.

Equations

• TesslerTenenbaumGoodman2022.tesslerSyllQuantEval Semantics.Quantification.Syllogistic.AristQuant.all s X Y = TesslerTenenbaumGoodman2022.tesslerAll s X Y
• TesslerTenenbaumGoodman2022.tesslerSyllQuantEval Semantics.Quantification.Syllogistic.AristQuant.some s X Y = Semantics.Quantification.Syllogistic.syllSome s X Y
• TesslerTenenbaumGoodman2022.tesslerSyllQuantEval Semantics.Quantification.Syllogistic.AristQuant.someNot s X Y = Semantics.Quantification.Syllogistic.syllSomeNot s X Y
• TesslerTenenbaumGoodman2022.tesslerSyllQuantEval Semantics.Quantification.Syllogistic.AristQuant.no s X Y = Semantics.Quantification.Syllogistic.syllNone s X Y

def TesslerTenenbaumGoodman2022.premise1Truth (syl : Semantics.Quantification.Syllogistic.Syllogism) (s : Semantics.Quantification.Syllogistic.VennState) : Bool

Truth value of premise 1 in state s (Tessler-Aristotelian).

Equations

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

def TesslerTenenbaumGoodman2022.premise2Truth (syl : Semantics.Quantification.Syllogistic.Syllogism) (s : Semantics.Quantification.Syllogistic.VennState) : Bool

Truth value of premise 2 in state s (Tessler-Aristotelian).

Equations

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

def TesslerTenenbaumGoodman2022.concMeaning : Semantics.Quantification.Syllogistic.Conclusion → Semantics.Quantification.Syllogistic.VennState → Bool

Literal meaning of each conclusion in a Venn state, using Tessler-Aristotelian All. NVC ("nothing follows") is the vacuous utterance, true everywhere.

Equations

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

@[simp]

theorem TesslerTenenbaumGoodman2022.nvc_always_true (s : Semantics.Quantification.Syllogistic.VennState) : concMeaning Semantics.Quantification.Syllogistic.Conclusion.nvc s = true

"Nothing follows" is always true.

def TesslerTenenbaumGoodman2022.noisyConcMeaning (φ : ℚ) (c : Semantics.Quantification.Syllogistic.Conclusion) (s : Semantics.Quantification.Syllogistic.VennState) : ℚ

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

Equations

• TesslerTenenbaumGoodman2022.noisyConcMeaning φ c s = RSA.Noise.noiseChannel (1 - φ) φ (if TesslerTenenbaumGoodman2022.concMeaning c s = true then 1 else 0)

theorem TesslerTenenbaumGoodman2022.noisyConcMeaning_zero (c : Semantics.Quantification.Syllogistic.Conclusion) (s : Semantics.Quantification.Syllogistic.VennState) : noisyConcMeaning 0 c s = if concMeaning c s = true then 1 else 0

Noise zero ⇒ noisy meaning is literal meaning.

theorem TesslerTenenbaumGoodman2022.noisyConcMeaning_nvc (φ : ℚ) (s : Semantics.Quantification.Syllogistic.VennState) : noisyConcMeaning φ Semantics.Quantification.Syllogistic.Conclusion.nvc s = 1 - φ

NVC's noisy meaning is 1 − φ everywhere — hearing "nothing follows" does not update the listener's beliefs.

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

L₀ joint likelihood of two premises in state s (unnormalized). The uniform prior θ = 0.5 cancels in normalization (eq. 2).

Equations

• TesslerTenenbaumGoodman2022.l0PremiseLikelihood φ p1 p2 s = RSA.Noise.noiseChannel (1 - φ) φ (if p1 s = true then 1 else 0) * RSA.Noise.noiseChannel (1 - φ) φ (if p2 s = true then 1 else 0)

noncomputable def TesslerTenenbaumGoodman2022.literalSpeakerScore (premPost : Semantics.Quantification.Syllogistic.VennState → ℝ) (α : ℝ) (c : Semantics.Quantification.Syllogistic.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₂)]

Equations

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

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

State Communication (S₁, eq. 4): standard RSA informativity.

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

Equations

• TesslerTenenbaumGoodman2022.stateComScore premPost naivePost α c = Real.exp (α * ∑ s : Semantics.Quantification.Syllogistic.VennState, premPost s * Real.log (naivePost c s))

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

Belief Alignment (S₁, eq. 6) — the paper's winning model.

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

Inlined discrete KL ∑ p · log(p/q) (mathlib-canonical form; the 0 · log 0 = 0 guard collapses for Real.log). The PMF-canonical form is (P.klDiv Q).toReal via PMF.toReal_klDiv_eq_sum_log_div.

Equations

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

theorem TesslerTenenbaumGoodman2022.stateCom_eq_beliefAlignment (premPost : Semantics.Quantification.Syllogistic.VennState → ℝ) (naivePost : Semantics.Quantification.Syllogistic.Conclusion → Semantics.Quantification.Syllogistic.VennState → ℝ) (α : ℝ) (c : Semantics.Quantification.Syllogistic.Conclusion) (hQ : ∀ (s : Semantics.Quantification.Syllogistic.VennState), 0 < naivePost c s) : beliefAlignmentScore premPost naivePost α c = Real.exp (α * -∑ s : Semantics.Quantification.Syllogistic.VennState, premPost s * Real.log (premPost s)) * stateComScore premPost naivePost α c

State Communication and Belief Alignment differ by a multiplicative factor exp(α · H(premPost)) that depends only on the reasoner's premise posterior, not on the conclusion. Within a single syllogism's softmax over conclusions, this factor cancels — the two models predict identical conclusion distributions. Between syllogisms, H(premPost) varies, so the same conclusion-distribution data is fit by different α values under SC vs BA — explaining the paper's distinct fit statistics (r = .67 vs .82) without any difference in functional form.

Derivation via Real.log_div: KL(P ∥ Q) = Σ P · log(P/Q) = Σ P·log P − Σ P·log Q −KL(P ∥ Q) = Σ P·log Q − Σ P·log P = [SC utility] + H(P)

theorem TesslerTenenbaumGoodman2022.beliefAlignment_nvc_uninformative (post prior : Semantics.Quantification.Syllogistic.VennState → ℝ) (α : ℝ) : beliefAlignmentScore post (fun (c : Semantics.Quantification.Syllogistic.Conclusion) => if c = Semantics.Quantification.Syllogistic.Conclusion.nvc then prior else fun (x : Semantics.Quantification.Syllogistic.VennState) => 0) α Semantics.Quantification.Syllogistic.Conclusion.nvc = Real.exp (α * -∑ s : Semantics.Quantification.Syllogistic.VennState, post s * Real.log (post s / prior s))

The Belief Alignment score for NVC, when the naive listener for NVC receives the prior, is exp(α · −KL(post ‖ prior)). When premises are uninformative (posterior ≈ prior), KL ≈ 0, so the NVC score approaches exp(0) = 1, the maximum — explaining the model's preference for NVC on uninformative premise combinations.

theorem TesslerTenenbaumGoodman2022.all_entails_some_AC (s : Semantics.Quantification.Syllogistic.VennState) (h : concMeaning Semantics.Quantification.Syllogistic.Conclusion.allAC s = true) : concMeaning Semantics.Quantification.Syllogistic.Conclusion.someAC s = true

"All A-C" entails "Some A-C" under Tessler-Aristotelian All (existential import is built into tesslerAll so the witness is free). With the substrate's modern syllAll this would require an explicit ∃A hypothesis.

theorem TesslerTenenbaumGoodman2022.all_strictly_stronger_than_some : concMeaning Semantics.Quantification.Syllogistic.Conclusion.someAC Semantics.Quantification.Syllogistic.state_A_AC = true ∧ concMeaning Semantics.Quantification.Syllogistic.Conclusion.allAC Semantics.Quantification.Syllogistic.state_A_AC = false

Strict informativity: "All A-C" is compatible with strictly fewer states than "Some A-C". Witness: state_A_AC.

def TesslerTenenbaumGoodman2022.l0Unnorm (φ : ℚ) (syl : Semantics.Quantification.Syllogistic.Syllogism) (s : Semantics.Quantification.Syllogistic.VennState) : ℚ

Unnormalized L₀ likelihood for a syllogism in state s.

Equations

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

def TesslerTenenbaumGoodman2022.l0Z (φ : ℚ) (syl : Semantics.Quantification.Syllogistic.Syllogism) : ℚ

Normalization constant: Σ_s L₀_unnorm(s) over all 128 Venn states. Uses Finset.univ over VennState = Region → Bool via Pi.fintype.

Equations

• TesslerTenenbaumGoodman2022.l0Z φ syl = ∑ s : Semantics.Quantification.Syllogistic.VennState, TesslerTenenbaumGoodman2022.l0Unnorm φ syl s

def TesslerTenenbaumGoodman2022.l0Post (φ : ℚ) (syl : Semantics.Quantification.Syllogistic.Syllogism) (s : Semantics.Quantification.Syllogistic.VennState) : ℚ

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

Equations

• TesslerTenenbaumGoodman2022.l0Post φ syl s = TesslerTenenbaumGoodman2022.l0Unnorm φ syl s / TesslerTenenbaumGoodman2022.l0Z φ syl

def TesslerTenenbaumGoodman2022.naiveL0Z (φ : ℚ) (c : Semantics.Quantification.Syllogistic.Conclusion) : ℚ

Normalization constant for naive L₀ on a single conclusion.

Equations

• TesslerTenenbaumGoodman2022.naiveL0Z φ c = ∑ s : Semantics.Quantification.Syllogistic.VennState, TesslerTenenbaumGoodman2022.noisyConcMeaning φ c s

def TesslerTenenbaumGoodman2022.naiveL0Post (φ : ℚ) (c : Semantics.Quantification.Syllogistic.Conclusion) (s : Semantics.Quantification.Syllogistic.VennState) : ℚ

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

Equations

• TesslerTenenbaumGoodman2022.naiveL0Post φ c s = TesslerTenenbaumGoodman2022.noisyConcMeaning φ c s / TesslerTenenbaumGoodman2022.naiveL0Z φ c

def TesslerTenenbaumGoodman2022.figuralWeight (β : ℚ) (syl : Semantics.Quantification.Syllogistic.Syllogism) (c : Semantics.Quantification.Syllogistic.Conclusion) : ℚ

Figural bias prior weight, determined by which of A, C appears in subject position of one of the premises (per the paper's figural-effects discussion).

• Both premises in A-B/B-C order (Figure 1): only A appears in subject position (of P1) → A-C conclusions get weight β.
• Both in B-A/C-B order (Figure 4): only C in subject (of P2) → C-A conclusions get weight β.
• Mixed (Figures 2 & 3): both or neither of A, C appear in subject position → no figural bias (weight 1 for all conclusions).

NVC always gets weight 1. The paper fits β ≈ 2.01 (MAP).

Equations

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

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

Belief Alignment score for conclusion c given syllogism syl. Parameters: α (rationality), φ (noise), β (figural bias).

Equations

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

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

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

Equations

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

noncomputable def TesslerTenenbaumGoodman2022.α_fit : ℝ

MAP estimates from the Bayesian data analysis. α ≈ 6.88, φ ≈ 0.06, β ≈ 2.01. Numerical evaluation of conclusionProb at these parameters is not performed in-Lean (would require Float, banned project-wide); the paper's reported predictions can be reproduced via the model code at https://github.com/mhtessler/syllogism-paper.

Equations

• TesslerTenenbaumGoodman2022.α_fit = 688 / 100

def TesslerTenenbaumGoodman2022.φ_fit : ℚ

Equations

• TesslerTenenbaumGoodman2022.φ_fit = 6 / 100

def TesslerTenenbaumGoodman2022.β_fit : ℚ

Equations

• TesslerTenenbaumGoodman2022.β_fit = 201 / 100

theorem TesslerTenenbaumGoodman2022.barbara_l0_concentrates_on_allAC (s : Semantics.Quantification.Syllogistic.VennState) : premise1Truth Semantics.Quantification.Syllogistic.barbara s = true → premise2Truth Semantics.Quantification.Syllogistic.barbara s = true → concMeaning Semantics.Quantification.Syllogistic.Conclusion.allAC s = true

For Barbara, every state where both premises are literally true also satisfies "All A-C" — the L₀ posterior concentrates on All-A-C states. Reduces to barbara_premises_imply_allAC from the substrate plus the Tessler-Aristotelian concMeaning wrapping.

theorem TesslerTenenbaumGoodman2022.allAB_allCB_l0_does_not_concentrate : (premise1Truth Semantics.Quantification.Syllogistic.allAB_allCB Semantics.Quantification.Syllogistic.state_ABC = true ∧ premise2Truth Semantics.Quantification.Syllogistic.allAB_allCB Semantics.Quantification.Syllogistic.state_ABC = true ∧ concMeaning Semantics.Quantification.Syllogistic.Conclusion.allAC Semantics.Quantification.Syllogistic.state_ABC = true) ∧ premise1Truth Semantics.Quantification.Syllogistic.allAB_allCB Semantics.Quantification.Syllogistic.state_AB_BC = true ∧ premise2Truth Semantics.Quantification.Syllogistic.allAB_allCB Semantics.Quantification.Syllogistic.state_AB_BC = true ∧ concMeaning Semantics.Quantification.Syllogistic.Conclusion.allAC Semantics.Quantification.Syllogistic.state_AB_BC = false

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.

theorem TesslerTenenbaumGoodman2022.allAC_subaltern_someAC : Core.Opposition.Subaltern (concMeaning Semantics.Quantification.Syllogistic.Conclusion.allAC) (concMeaning Semantics.Quantification.Syllogistic.Conclusion.someAC)

"All A-C" properly subalternates "Some A-C" in the Tessler-Aristotelian reading: All entails Some (via existential import in tesslerAll), and state_A_AC witnesses that the converse fails (Some without All).

theorem TesslerTenenbaumGoodman2022.prob_subaltern_allAC_someAC (μ : PMF Semantics.Quantification.Syllogistic.VennState) : Core.Opposition.ProbSubaltern μ (concMeaning Semantics.Quantification.Syllogistic.Conclusion.allAC) (concMeaning Semantics.Quantification.Syllogistic.Conclusion.someAC)

Probabilistic subalternation on the L₀ posterior. Tessler's Bayesian listener model assigns to every conclusion c an L₀ posterior probability μ({s | concMeaning c s = true}). Aristotelian subalternation lifts to this probabilistic level: under any μ, P_μ[allAC] ≤ P_μ[someAC].

The lift is automatic via Core.Opposition.Subaltern.toProb once allAC_subaltern_someAC is established. The probabilistic Aristotelian diagram (Demey-Smessaert 2018-style, with the convex generalization in Probabilistic.lean) is implicitly the framework Tessler's Bayesian listener computes within.