Tessler, Tenenbaum and Goodman (2022): Logic, Probability, and Pragmatics in Syllogistic Reasoning

Tessler, Tenenbaum and Goodman model syllogistic reasoning as language use, in the Rational Speech Act framework of Frank and Goodman. A state records which object types exist, the regions of a three-circle Venn diagram. The reasoner first acts as a listener, updating a prior over states on the two premises, then as a speaker choosing among nine conclusions for a naive listener who hears the conclusion alone: the eight quantified sentences relating the end terms, and nothing follows, which says nothing. Three speakers are compared. The literal speaker scores a conclusion by its probability of being true; the state-communication speaker by the expected log-probability the naive listener gives the reasoner's state; the belief-alignment speaker by the negative Kullback–Leibler divergence of the naive listener's beliefs from the reasoner's. A figural preference favors conclusions whose subject is the only end term in subject position in the premises. The Bayesian data analysis and the comparison with the Probability Heuristics Model of Chater and Oaksford are not formalized.

Main statements

• stateCommunication_eq_beliefAlignment: as printed, the state-communication and belief-alignment speakers are one speaker, since their utilities differ by the entropy of the reasoner's beliefs, which no conclusion changes.
• nothing_follows_of_invalid: without semantic noise, and at any prior giving every state positive mass, the belief-alignment speaker answers nothing follows to every syllogism that entails no quantified conclusion.
• barbara_prefers_all: to All A are B, All B are C that speaker prefers All A are C to the weaker Some A are C and to nothing follows.
• literalSpeaker_le_nothing_follows: the literal speaker never prefers a quantified conclusion to nothing follows.

Implementation notes

• Only all carries existential import (section 2.1). Table 1 prints the particular forms with an arrow under the existential quantifier, read here as a conjunction.
• Noise follows section 3.1.1: the listener disregards each sentence with probability φ, so a state pays a factor φ for every sentence false at it. The weights 1 - φ and φ of section 2.2 give the same listeners at noise φ / (1 - φ).
• The speakers are the printed equations without the figural preference, which withFigure adds by reweighting their conclusion probabilities. The paper's fitted state-communication model differs from belief alignment, so it is not the printed one.

References

• [TTG22]
• [FG12]
• [GS13]
• [CO99]
• [DHG+20]

Sentences and states

inductive TesslerTenenbaumGoodman2022.Term : Type

The terms of a syllogism are the end terms A and C and the middle term B.

• A : Term
• B : Term
• C : Term

@[instance_reducible]

instance TesslerTenenbaumGoodman2022.instDecidableEqTerm : DecidableEq Term

Equations

• TesslerTenenbaumGoodman2022.instDecidableEqTerm x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[instance_reducible]

instance TesslerTenenbaumGoodman2022.instFintypeTerm : Fintype Term

Equations

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

@[reducible, inline]

abbrev TesslerTenenbaumGoodman2022.Region : Type

A region of the Venn diagram is an object type, the nonempty set of terms true of its objects.

Equations

• TesslerTenenbaumGoodman2022.Region = { r : Finset TesslerTenenbaumGoodman2022.Term // r.Nonempty }

@[reducible, inline]

abbrev TesslerTenenbaumGoodman2022.region (ts : Finset Term) (h : ts.Nonempty := by decide) : Region

region ts is the region of the objects of which exactly the terms ts are true.

Equations

• TesslerTenenbaumGoodman2022.region ts h = ⟨ts, h⟩

@[reducible, inline]

abbrev TesslerTenenbaumGoodman2022.State : Type

A state is the set of object types that exist.

Equations

• TesslerTenenbaumGoodman2022.State = Finset TesslerTenenbaumGoodman2022.Region

inductive TesslerTenenbaumGoodman2022.Quant : Type

The Aristotelian quantifiers are all, some, some … not and no.

• all : Quant
• some : Quant
• someNot : Quant
• no : Quant

@[instance_reducible]

instance TesslerTenenbaumGoodman2022.instDecidableEqQuant : DecidableEq Quant

Equations

• TesslerTenenbaumGoodman2022.instDecidableEqQuant x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[instance_reducible]

instance TesslerTenenbaumGoodman2022.instFintypeQuant : Fintype Quant

Equations

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

structure TesslerTenenbaumGoodman2022.Sentence : Type

A categorical sentence relates a subject term to a predicate term by a quantifier.

• quant : Quant
• subj : Term
• pred : Term

@[instance_reducible]

instance TesslerTenenbaumGoodman2022.instDecidableEqSentence : DecidableEq Sentence

Equations

• TesslerTenenbaumGoodman2022.instDecidableEqSentence = TesslerTenenbaumGoodman2022.instDecidableEqSentence.decEq

def TesslerTenenbaumGoodman2022.instDecidableEqSentence.decEq (x✝ x✝¹ : Sentence) : Decidable (x✝ = x✝¹)

Equations

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

@[instance_reducible]

instance TesslerTenenbaumGoodman2022.instFintypeSentence : Fintype Sentence

Equations

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

@[instance_reducible]

instance TesslerTenenbaumGoodman2022.instMeasurableSpaceSentence : MeasurableSpace Sentence

Equations

• TesslerTenenbaumGoodman2022.instMeasurableSpaceSentence = ⊤

def TesslerTenenbaumGoodman2022.Quant.denote : Quant → Quantifier.GQ Region

The quantifiers' meanings (Table 1) are every with a nonempty restrictor, some, its inner negation, and no.

Equations

• TesslerTenenbaumGoodman2022.Quant.all.denote = fun (R S : TesslerTenenbaumGoodman2022.Region → Prop) => Quantifier.GQ.every R S ∧ ∃ (r : TesslerTenenbaumGoodman2022.Region), R r
• TesslerTenenbaumGoodman2022.Quant.some.denote = Quantifier.GQ.some
• TesslerTenenbaumGoodman2022.Quant.someNot.denote = Quantifier.GQ.some.innerNeg
• TesslerTenenbaumGoodman2022.Quant.no.denote = Quantifier.GQ.no

def TesslerTenenbaumGoodman2022.Sentence.Holds (p : Sentence) (s : State) : Prop

A sentence holds at a state when its quantifier relates the existing object types of the subject term to the object types of the predicate term.

Equations

• p.Holds s = p.quant.denote (fun (r : TesslerTenenbaumGoodman2022.Region) => r ∈ s ∧ p.subj ∈ ↑r) fun (r : TesslerTenenbaumGoodman2022.Region) => p.pred ∈ ↑r

theorem TesslerTenenbaumGoodman2022.holds_all {x y : Term} {s : State} : { quant := Quant.all, subj := x, pred := y }.Holds s ↔ (∀ r ∈ s, x ∈ ↑r → y ∈ ↑r) ∧ ∃ r ∈ s, x ∈ ↑r

theorem TesslerTenenbaumGoodman2022.holds_some {x y : Term} {s : State} : { quant := Quant.some, subj := x, pred := y }.Holds s ↔ ∃ r ∈ s, x ∈ ↑r ∧ y ∈ ↑r

theorem TesslerTenenbaumGoodman2022.holds_someNot {x y : Term} {s : State} : { quant := Quant.someNot, subj := x, pred := y }.Holds s ↔ ∃ r ∈ s, x ∈ ↑r ∧ y ∉ ↑r

theorem TesslerTenenbaumGoodman2022.holds_no {x y : Term} {s : State} : { quant := Quant.no, subj := x, pred := y }.Holds s ↔ ∀ r ∈ s, x ∈ ↑r → y ∉ ↑r

theorem TesslerTenenbaumGoodman2022.holds_some_of_holds_all {x y : Term} {s : State} (h : { quant := Quant.all, subj := x, pred := y }.Holds s) : { quant := Quant.some, subj := x, pred := y }.Holds s

With existential import all entails some.

@[instance_reducible]

instance TesslerTenenbaumGoodman2022.instDecidableHolds (p : Sentence) (s : State) : Decidable (p.Holds s)

Equations

• One or more equations did not get rendered due to their size.
• TesslerTenenbaumGoodman2022.instDecidableHolds { quant := TesslerTenenbaumGoodman2022.Quant.some, subj := subj, pred := pred } s = decidable_of_iff (∃ r ∈ s, subj ∈ ↑r ∧ pred ∈ ↑r) ⋯
• TesslerTenenbaumGoodman2022.instDecidableHolds { quant := TesslerTenenbaumGoodman2022.Quant.someNot, subj := subj, pred := pred } s = decidable_of_iff (∃ r ∈ s, subj ∈ ↑r ∧ pred ∉ ↑r) ⋯
• TesslerTenenbaumGoodman2022.instDecidableHolds { quant := TesslerTenenbaumGoodman2022.Quant.no, subj := subj, pred := pred } s = decidable_of_iff (∀ r ∈ s, subj ∈ ↑r → pred ∉ ↑r) ⋯

theorem TesslerTenenbaumGoodman2022.holds_table_one : { quant := Quant.all, subj := Term.A, pred := Term.B }.Holds {region {Term.A, Term.B} holds_table_one._proof_1, region {Term.A, Term.B, Term.C} holds_table_one._proof_2} ∧ ¬{ quant := Quant.all, subj := Term.A, pred := Term.B }.Holds {region {Term.A} holds_table_one._proof_3, region {Term.A, Term.B, Term.C} holds_table_one._proof_2} ∧ { quant := Quant.some, subj := Term.A, pred := Term.B }.Holds {region {Term.A} holds_table_one._proof_3, region {Term.A, Term.B} holds_table_one._proof_1} ∧ ¬{ quant := Quant.some, subj := Term.A, pred := Term.B }.Holds {region {Term.A} holds_table_one._proof_3, region {Term.A, Term.C} holds_table_one._proof_4} ∧ { quant := Quant.someNot, subj := Term.A, pred := Term.B }.Holds {region {Term.A} holds_table_one._proof_3, region {Term.A, Term.B} holds_table_one._proof_1} ∧ ¬{ quant := Quant.someNot, subj := Term.A, pred := Term.B }.Holds {region {Term.A, Term.B} holds_table_one._proof_1, region {Term.A, Term.B, Term.C} holds_table_one._proof_2} ∧ { quant := Quant.no, subj := Term.A, pred := Term.B }.Holds {region {Term.A} holds_table_one._proof_3, region {Term.A, Term.C} holds_table_one._proof_4} ∧ ¬{ quant := Quant.no, subj := Term.A, pred := Term.B }.Holds {region {Term.A} holds_table_one._proof_3, region {Term.A, Term.B} holds_table_one._proof_1}

The four sentences of Table 1 hold at its consistent states and fail at its inconsistent ones.

def TesslerTenenbaumGoodman2022.extension (us : List Sentence) : Set State

The extension of a list of sentences is the set of states at which all of them hold.

Equations

• TesslerTenenbaumGoodman2022.extension us = {s : TesslerTenenbaumGoodman2022.State | ∀ p ∈ us, p.Holds s}

theorem TesslerTenenbaumGoodman2022.mem_extension {us : List Sentence} {s : State} : s ∈ extension us ↔ ∀ p ∈ us, p.Holds s

@[simp]

theorem TesslerTenenbaumGoodman2022.extension_nil : extension [] = Set.univ

theorem TesslerTenenbaumGoodman2022.mem_extension_singleton {p : Sentence} {s : State} : s ∈ extension [p] ↔ p.Holds s

theorem TesslerTenenbaumGoodman2022.mem_extension_pair {p q : Sentence} {s : State} : s ∈ extension [p, q] ↔ p.Holds s ∧ q.Holds s

@[instance_reducible]

instance TesslerTenenbaumGoodman2022.instDecidableMemStateSetExtension (us : List Sentence) (s : State) : Decidable (s ∈ extension us)

Equations

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

The listener (section 2.2)

noncomputable def TesslerTenenbaumGoodman2022.noisy (φ : ENNReal) (us : List Sentence) (s : State) : ENNReal

The noisy meaning of a list of sentences charges a state a factor φ for every sentence false at it, since the listener disregards each sentence with probability φ.

Equations

• TesslerTenenbaumGoodman2022.noisy φ us s = φ ^ List.countP (fun (p : TesslerTenenbaumGoodman2022.Sentence) => decide ¬p.Holds s) us

theorem TesslerTenenbaumGoodman2022.noisy_zero (us : List Sentence) : noisy 0 us = (extension us).indicator 1

noncomputable def TesslerTenenbaumGoodman2022.listener (φ : ENNReal) (μ : MeasureTheory.Measure State) : ProbabilityTheory.Kernel (List Sentence) State

The literal listener reweights the prior by the noisy meaning of the sentences heard.

Equations

• TesslerTenenbaumGoodman2022.listener φ μ = ProbabilityTheory.Kernel.ofDensity μ (TesslerTenenbaumGoodman2022.noisy φ)

instance TesslerTenenbaumGoodman2022.instIsFiniteKernelListSentenceStateListener {φ : ENNReal} {μ : MeasureTheory.Measure State} : ProbabilityTheory.IsFiniteKernel (listener φ μ)

theorem TesslerTenenbaumGoodman2022.listener_zero (μ : MeasureTheory.Measure State) : listener 0 μ = RSA.listener μ (RSA.truthful extension)

Without noise the listener conditions the prior on the sentences heard.

theorem TesslerTenenbaumGoodman2022.lintegral_noisy_ne_top {φ : ENNReal} {μ : MeasureTheory.Measure State} [MeasureTheory.IsFiniteMeasure μ] (hφ : φ ≠ ⊤) (us : List Sentence) : ∫⁻ (s : State), noisy φ us s ∂μ ≠ ⊤

theorem TesslerTenenbaumGoodman2022.isProbabilityMeasure_listener {φ : ENNReal} {μ : MeasureTheory.Measure State} [MeasureTheory.IsProbabilityMeasure μ] (hφ : φ ≠ 0) (hφ' : φ ≠ ⊤) (us : List Sentence) : MeasureTheory.IsProbabilityMeasure ((listener φ μ) us)

theorem TesslerTenenbaumGoodman2022.listener_absolutelyContinuous {φ : ENNReal} {μ : MeasureTheory.Measure State} [MeasureTheory.IsFiniteMeasure μ] (hφ : φ ≠ 0) (hφ' : φ ≠ ⊤) (us us' : List Sentence) : ((listener φ μ) us).AbsolutelyContinuous ((listener φ μ) us')

With noise any two posteriors of the listener have the same null sets.

Syllogisms and conclusions (section 2.3.1)

structure TesslerTenenbaumGoodman2022.Syllogism : Type

A syllogism is two premises; in the classical ones the first relates A and B and the second B and C.

• first : Sentence
• second : Sentence

def TesslerTenenbaumGoodman2022.instDecidableEqSyllogism.decEq (x✝ x✝¹ : Syllogism) : Decidable (x✝ = x✝¹)

Equations

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

@[instance_reducible]

instance TesslerTenenbaumGoodman2022.instDecidableEqSyllogism : DecidableEq Syllogism

Equations

• TesslerTenenbaumGoodman2022.instDecidableEqSyllogism = TesslerTenenbaumGoodman2022.instDecidableEqSyllogism.decEq

@[instance_reducible]

instance TesslerTenenbaumGoodman2022.instFintypeSyllogism : Fintype Syllogism

Equations

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

@[instance_reducible]

instance TesslerTenenbaumGoodman2022.instMeasurableSpaceSyllogism : MeasurableSpace Syllogism

Equations

• TesslerTenenbaumGoodman2022.instMeasurableSpaceSyllogism = ⊤

def TesslerTenenbaumGoodman2022.Syllogism.premises (syl : Syllogism) : List Sentence

The reasoner hears the two premises of a syllogism in order.

Equations

• syl.premises = [syl.first, syl.second]

def TesslerTenenbaumGoodman2022.Syllogism.subjects (syl : Syllogism) : Finset Term

The subjects of a syllogism are the terms in subject position in its premises.

Equations

• syl.subjects = {syl.first.subj, syl.second.subj}

def TesslerTenenbaumGoodman2022.Sentence.IsConclusion (p : Sentence) : Prop

A sentence is a candidate conclusion when it relates the two end terms.

Equations

• p.IsConclusion = (p.subj ≠ TesslerTenenbaumGoodman2022.Term.B ∧ p.pred ≠ TesslerTenenbaumGoodman2022.Term.B ∧ p.subj ≠ p.pred)

@[instance_reducible]

instance TesslerTenenbaumGoodman2022.instDecidablePredSentenceIsConclusion : DecidablePred Sentence.IsConclusion

Equations

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

@[reducible, inline]

abbrev TesslerTenenbaumGoodman2022.Conclusion : Type

A conclusion is a sentence relating the end terms or, as none, nothing follows.

Equations

• TesslerTenenbaumGoodman2022.Conclusion = Option { p : TesslerTenenbaumGoodman2022.Sentence // p.IsConclusion }

def TesslerTenenbaumGoodman2022.Conclusion.said : Conclusion → List Sentence

A conclusion says its sentence, or nothing at all.

Equations

• TesslerTenenbaumGoodman2022.Conclusion.said none = []
• TesslerTenenbaumGoodman2022.Conclusion.said (some p) = [↑p]

@[reducible, inline]

abbrev TesslerTenenbaumGoodman2022.ac (q : Quant) : Conclusion

ac q is the conclusion relating A to C by the quantifier q.

Equations

• TesslerTenenbaumGoodman2022.ac q = some ⟨{ quant := q, subj := TesslerTenenbaumGoodman2022.Term.A, pred := TesslerTenenbaumGoodman2022.Term.C }, ⋯⟩

theorem TesslerTenenbaumGoodman2022.extension_said_none : extension (Conclusion.said none) = Set.univ

The speakers (section 2.3)

@[reducible, inline]

noncomputable abbrev TesslerTenenbaumGoodman2022.reasoner (φ : ENNReal) (μ : MeasureTheory.Measure State) (syl : Syllogism) : MeasureTheory.Measure State

The reasoner's beliefs are the listener's posterior after the premises.

Equations

• TesslerTenenbaumGoodman2022.reasoner φ μ syl = (TesslerTenenbaumGoodman2022.listener φ μ) syl.premises

@[reducible, inline]

noncomputable abbrev TesslerTenenbaumGoodman2022.naive (φ : ENNReal) (μ : MeasureTheory.Measure State) (c : Conclusion) : MeasureTheory.Measure State

The naive listener's beliefs are the listener's posterior after a conclusion.

Equations

• TesslerTenenbaumGoodman2022.naive φ μ c = (TesslerTenenbaumGoodman2022.listener φ μ) c.said

noncomputable def TesslerTenenbaumGoodman2022.literalSpeaker (φ : ENNReal) (μ : MeasureTheory.Measure State) (α : ℝ) : ProbabilityTheory.Kernel Syllogism Conclusion

The literal speaker scores a conclusion by the reasoner's probability that it is true.

Equations

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

noncomputable def TesslerTenenbaumGoodman2022.stateCommunication (φ : ENNReal) (μ : MeasureTheory.Measure State) (α : ℝ) : ProbabilityTheory.Kernel Syllogism Conclusion

The state-communication speaker scores a conclusion by the expected log-probability the naive listener gives the reasoner's state.

Equations

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

noncomputable def TesslerTenenbaumGoodman2022.beliefAlignment (φ : ENNReal) (μ : MeasureTheory.Measure State) (α : ℝ) : ProbabilityTheory.Kernel Syllogism Conclusion

The belief-alignment speaker believes what the reasoner believes and addresses the naive listener.

Equations

• TesslerTenenbaumGoodman2022.beliefAlignment φ μ α = RSA.speaker α 0 (TesslerTenenbaumGoodman2022.naive φ μ) (TesslerTenenbaumGoodman2022.reasoner φ μ)

instance TesslerTenenbaumGoodman2022.instIsFiniteKernelSyllogismConclusionBeliefAlignment (φ : ENNReal) (μ : MeasureTheory.Measure State) (α : ℝ) : ProbabilityTheory.IsFiniteKernel (beliefAlignment φ μ α)

theorem TesslerTenenbaumGoodman2022.beliefAlignment_eq_softmax_klDiv {φ : ENNReal} {μ : MeasureTheory.Measure State} {α : ℝ} [MeasureTheory.IsProbabilityMeasure μ] (hα : 0 < α) (hφ : φ ≠ 0) (hφ' : φ ≠ ⊤) : beliefAlignment φ μ α = ProbabilityTheory.Kernel.softmax fun (syl : Syllogism) (c : Conclusion) => -↑(ENNReal.ofReal α * InformationTheory.klDiv (reasoner φ μ syl) (naive φ μ c))

The belief-alignment speaker scores a conclusion by the negative divergence of the naive listener's beliefs from the reasoner's.

theorem TesslerTenenbaumGoodman2022.stateCommunication_eq_beliefAlignment {φ : ENNReal} {μ : MeasureTheory.Measure State} {α : ℝ} [MeasureTheory.IsFiniteMeasure μ] (hφ : φ ≠ 0) (hφ' : φ ≠ ⊤) : stateCommunication φ μ α = beliefAlignment φ μ α

As printed, the state-communication and belief-alignment speakers are one speaker.

theorem TesslerTenenbaumGoodman2022.literalSpeaker_le_nothing_follows {φ : ENNReal} {μ : MeasureTheory.Measure State} {α : ℝ} (hα : 0 ≤ α) (syl : Syllogism) (c : Conclusion) : ((literalSpeaker φ μ α) syl).real {c} ≤ ((literalSpeaker φ μ α) syl).real {none}

The literal speaker never prefers a quantified conclusion to nothing follows, which is true at every state.

The figural preference (section 3.1.1)

def TesslerTenenbaumGoodman2022.figuralWeight (β : NNReal) (syl : Syllogism) : Conclusion → NNReal

The figural preference gives weight β to a conclusion whose subject, but not its predicate, is the subject of a premise, and weight 1 to every other conclusion.

Equations

• TesslerTenenbaumGoodman2022.figuralWeight β syl none = 1
• TesslerTenenbaumGoodman2022.figuralWeight β syl (some p) = if (↑p).subj ∈ syl.subjects ∧ (↑p).pred ∉ syl.subjects then β else 1

noncomputable def TesslerTenenbaumGoodman2022.withFigure (β : NNReal) (S : ProbabilityTheory.Kernel Syllogism Conclusion) : ProbabilityTheory.Kernel Syllogism Conclusion

The figural preference reweights a speaker's conclusion probabilities and renormalizes them.

Equations

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

theorem TesslerTenenbaumGoodman2022.withFigure_apply_none_eq_one {β : NNReal} {S : ProbabilityTheory.Kernel Syllogism Conclusion} [ProbabilityTheory.IsFiniteKernel S] {syl : Syllogism} (h0 : (S syl) {none} ≠ 0) (h : ∀ (c : Option { p : Sentence // p.IsConclusion }), c ≠ none → (S syl) {c} = 0) : ((withFigure β S) syl) {none} = 1

A speaker certain of nothing follows stays certain under the figural preference.

theorem TesslerTenenbaumGoodman2022.withFigure_real_singleton_lt_iff {β : NNReal} {S : ProbabilityTheory.Kernel Syllogism Conclusion} [ProbabilityTheory.IsFiniteKernel S] {syl : Syllogism} {c c' : Conclusion} (h0 : (S syl) {none} ≠ 0) : ((withFigure β S) syl).real {c} < ((withFigure β S) syl).real {c'} ↔ ↑(figuralWeight β syl c) * (S syl).real {c} < ↑(figuralWeight β syl c') * (S syl).real {c'}

Without noise (section 2.3.4)

theorem TesslerTenenbaumGoodman2022.beliefAlignment_zero (μ : MeasureTheory.Measure State) (α : ℝ) : beliefAlignment 0 μ α = RSA.speaker α 0 ⇑(RSA.listener μ (RSA.truthful fun (c : Conclusion) => extension c.said)) fun (syl : Syllogism) => μ[|extension syl.premises]

Without noise the belief-alignment speaker believes the prior conditioned on the premises and addresses a literal listener.

theorem TesslerTenenbaumGoodman2022.beliefAlignment_zero_apply_singleton_eq_zero_iff {μ : MeasureTheory.Measure State} {α : ℝ} {syl : Syllogism} {c : Conclusion} [MeasureTheory.IsFiniteMeasure μ] (hμ : ∀ (s : State), μ {s} ≠ 0) (hα : 0 < α) : ((beliefAlignment 0 μ α) syl) {c} = 0 ↔ ¬extension syl.premises ⊆ extension c.said

The speaker produces exactly the conclusions the premises entail.

theorem TesslerTenenbaumGoodman2022.beliefAlignment_zero_real_singleton_lt_iff {μ : MeasureTheory.Measure State} {α : ℝ} {syl : Syllogism} {c c' : Conclusion} [MeasureTheory.IsFiniteMeasure μ] (hμ : ∀ (s : State), μ {s} ≠ 0) (hα : 0 < α) (hne : (extension syl.premises).Nonempty) (hc : extension syl.premises ⊆ extension c.said) (hc' : extension syl.premises ⊆ extension c'.said) : ((beliefAlignment 0 μ α) syl).real {c} < ((beliefAlignment 0 μ α) syl).real {c'} ↔ μ (extension c'.said) < μ (extension c.said)

Among the conclusions the premises entail, the speaker prefers the one of smaller prior mass.

theorem TesslerTenenbaumGoodman2022.nothing_follows_of_invalid {μ : MeasureTheory.Measure State} {α : ℝ} {β : NNReal} {syl : Syllogism} [MeasureTheory.IsFiniteMeasure μ] (hμ : ∀ (s : State), μ {s} ≠ 0) (hα : 0 < α) (h : ∀ (c : Option { p : Sentence // p.IsConclusion }), c ≠ none → ¬extension syl.premises ⊆ extension (Conclusion.said c)) : ((withFigure β (beliefAlignment 0 μ α)) syl) {none} = 1

Without noise the belief-alignment speaker answers nothing follows to every syllogism that entails no quantified conclusion (section 2.3.4).

All A are B, All B are C and All A are B, All C are B (Figures 3, 4 and 8)

def TesslerTenenbaumGoodman2022.barbara : Syllogism

Barbara is the syllogism All A are B, All B are C.

Equations

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

def TesslerTenenbaumGoodman2022.allAB_allCB : Syllogism

The syllogism All A are B, All C are B has both end terms in subject position.

Equations

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

theorem TesslerTenenbaumGoodman2022.figuralWeight_barbara {β : NNReal} (q : Quant) : figuralWeight β barbara (ac q) = β

theorem TesslerTenenbaumGoodman2022.figuralWeight_allAB_allCB {β : NNReal} (c : Conclusion) : figuralWeight β allAB_allCB c = 1

With both end terms in subject position there is no figural preference.

theorem TesslerTenenbaumGoodman2022.barbara_entails_all : extension barbara.premises ⊆ extension (ac Quant.all).said

theorem TesslerTenenbaumGoodman2022.barbara_prefers_all {μ : MeasureTheory.Measure State} {α : ℝ} {β : NNReal} [MeasureTheory.IsFiniteMeasure μ] (hμ : ∀ (s : State), μ {s} ≠ 0) (hα : 0 < α) (hβ : 1 ≤ β) : ((withFigure β (beliefAlignment 0 μ α)) barbara).real {ac Quant.some} < ((withFigure β (beliefAlignment 0 μ α)) barbara).real {ac Quant.all} ∧ ((withFigure β (beliefAlignment 0 μ α)) barbara).real {none} < ((withFigure β (beliefAlignment 0 μ α)) barbara).real {ac Quant.all}

To All A are B, All B are C the noiseless belief-alignment speaker prefers All A are C to the weaker Some A are C and to nothing follows (Figure 8).

theorem TesslerTenenbaumGoodman2022.allAB_allCB_nothing_follows {μ : MeasureTheory.Measure State} {α : ℝ} {β : NNReal} [MeasureTheory.IsFiniteMeasure μ] (hμ : ∀ (s : State), μ {s} ≠ 0) (hα : 0 < α) : ((withFigure β (beliefAlignment 0 μ α)) allAB_allCB) {none} = 1

All A are B, All C are B entails no quantified conclusion, so the noiseless speaker answers nothing follows.