Syllogistic substrate: types

Theory-neutral types for the Aristotelian syllogistic fragment.

The four Aristotelian quantifiers (AristQuant: A/I/O/E = all/some/someNot/no) applied to three terms (A, B, C) generate the classical syllogism: two quantified premises sharing a middle term B, plus a conclusion relating A and C. The state space is the 7 non-empty regions of a three-circle Venn diagram — the empty region {¬A, ¬B, ¬C} is excluded since it does not affect quantifier truth conditions.

Used by:

• Theories.Semantics.Quantification.Syllogistic.Basic for the semantics
• Phenomena.Quantification.Studies.TesslerTenenbaumGoodman2022 and any future Bayesian/RSA/mental-models paper formalisation

inductive Semantics.Quantification.Syllogistic.AristQuant : Type

The four Aristotelian quantifiers. Names follow the medieval mnemonic: A = all (universal affirmative), I = some (particular affirmative), O = someNot (particular negative), E = no (universal negative).

• all : AristQuant
• some : AristQuant
• someNot : AristQuant
• no : AristQuant

@[implicit_reducible]

instance Semantics.Quantification.Syllogistic.instDecidableEqAristQuant : DecidableEq AristQuant

Equations

• Semantics.Quantification.Syllogistic.instDecidableEqAristQuant x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[implicit_reducible]

instance Semantics.Quantification.Syllogistic.instReprAristQuant : Repr AristQuant

Equations

• Semantics.Quantification.Syllogistic.instReprAristQuant = { reprPrec := Semantics.Quantification.Syllogistic.instReprAristQuant.repr }

def Semantics.Quantification.Syllogistic.instReprAristQuant.repr : AristQuant → ℕ → Std.Format

Equations

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

def Semantics.Quantification.Syllogistic.instInhabitedAristQuant.default : AristQuant

Equations

• Semantics.Quantification.Syllogistic.instInhabitedAristQuant.default = Semantics.Quantification.Syllogistic.AristQuant.all

@[implicit_reducible]

instance Semantics.Quantification.Syllogistic.instInhabitedAristQuant : Inhabited AristQuant

Equations

• Semantics.Quantification.Syllogistic.instInhabitedAristQuant = { default := Semantics.Quantification.Syllogistic.instInhabitedAristQuant.default }

@[implicit_reducible]

instance Semantics.Quantification.Syllogistic.instFintypeAristQuant : Fintype AristQuant

Equations

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

inductive Semantics.Quantification.Syllogistic.Region : Type

The 7 non-empty regions of a three-circle (A, B, C) Venn diagram. The empty region {¬A, ¬B, ¬C} is excluded because it does not affect quantifier truth conditions for any A/I/O/E form.

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

@[implicit_reducible]

instance Semantics.Quantification.Syllogistic.instDecidableEqRegion : DecidableEq Region

Equations

• Semantics.Quantification.Syllogistic.instDecidableEqRegion x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Semantics.Quantification.Syllogistic.instReprRegion.repr : Region → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance Semantics.Quantification.Syllogistic.instReprRegion : Repr Region

Equations

• Semantics.Quantification.Syllogistic.instReprRegion = { reprPrec := Semantics.Quantification.Syllogistic.instReprRegion.repr }

@[implicit_reducible]

instance Semantics.Quantification.Syllogistic.instInhabitedRegion : Inhabited Region

Equations

• Semantics.Quantification.Syllogistic.instInhabitedRegion = { default := Semantics.Quantification.Syllogistic.instInhabitedRegion.default }

def Semantics.Quantification.Syllogistic.instInhabitedRegion.default : Region

Equations

• Semantics.Quantification.Syllogistic.instInhabitedRegion.default = Semantics.Quantification.Syllogistic.Region.A

@[implicit_reducible]

instance Semantics.Quantification.Syllogistic.instFintypeRegion : Fintype Region

Equations

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

@[reducible, inline]

abbrev Semantics.Quantification.Syllogistic.VennState : Type

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

Equations

• Semantics.Quantification.Syllogistic.VennState = (Semantics.Quantification.Syllogistic.Region → Bool)

def Semantics.Quantification.Syllogistic.hasA : Region → Bool

Region predicate: does region r have property A?

Equations

• Semantics.Quantification.Syllogistic.hasA Semantics.Quantification.Syllogistic.Region.A = true
• Semantics.Quantification.Syllogistic.hasA Semantics.Quantification.Syllogistic.Region.AB = true
• Semantics.Quantification.Syllogistic.hasA Semantics.Quantification.Syllogistic.Region.AC = true
• Semantics.Quantification.Syllogistic.hasA Semantics.Quantification.Syllogistic.Region.ABC = true
• Semantics.Quantification.Syllogistic.hasA x✝ = false

def Semantics.Quantification.Syllogistic.hasB : Region → Bool

Region predicate: does region r have property B?

Equations

• Semantics.Quantification.Syllogistic.hasB Semantics.Quantification.Syllogistic.Region.B = true
• Semantics.Quantification.Syllogistic.hasB Semantics.Quantification.Syllogistic.Region.AB = true
• Semantics.Quantification.Syllogistic.hasB Semantics.Quantification.Syllogistic.Region.BC = true
• Semantics.Quantification.Syllogistic.hasB Semantics.Quantification.Syllogistic.Region.ABC = true
• Semantics.Quantification.Syllogistic.hasB x✝ = false

def Semantics.Quantification.Syllogistic.hasC : Region → Bool

Region predicate: does region r have property C?

Equations

• Semantics.Quantification.Syllogistic.hasC Semantics.Quantification.Syllogistic.Region.C = true
• Semantics.Quantification.Syllogistic.hasC Semantics.Quantification.Syllogistic.Region.AC = true
• Semantics.Quantification.Syllogistic.hasC Semantics.Quantification.Syllogistic.Region.BC = true
• Semantics.Quantification.Syllogistic.hasC Semantics.Quantification.Syllogistic.Region.ABC = true
• Semantics.Quantification.Syllogistic.hasC x✝ = false

structure Semantics.Quantification.Syllogistic.Syllogism : Type

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".

The four combinations of orderings give the four classical figures:

• Figure 1: A-B, B-C (order1AB = true, order2BC = true)
• Figure 2: B-A, B-C (order1AB = false, order2BC = true)
• Figure 3: A-B, C-B (order1AB = true, order2BC = false)
• Figure 4: B-A, C-B (order1AB = false, order2BC = false)

With 4 quantifier choices per premise, this gives 4 × 2 × 4 × 2 = 64 syllogisms.

• q1 : AristQuant
• order1AB : Bool
• q2 : AristQuant
• order2BC : Bool

def Semantics.Quantification.Syllogistic.instDecidableEqSyllogism.decEq (x✝ x✝¹ : Syllogism) : Decidable (x✝ = x✝¹)

Equations

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

@[implicit_reducible]

instance Semantics.Quantification.Syllogistic.instDecidableEqSyllogism : DecidableEq Syllogism

Equations

• Semantics.Quantification.Syllogistic.instDecidableEqSyllogism = Semantics.Quantification.Syllogistic.instDecidableEqSyllogism.decEq

@[implicit_reducible]

instance Semantics.Quantification.Syllogistic.instReprSyllogism : Repr Syllogism

Equations

• Semantics.Quantification.Syllogistic.instReprSyllogism = { reprPrec := Semantics.Quantification.Syllogistic.instReprSyllogism.repr }

def Semantics.Quantification.Syllogistic.instReprSyllogism.repr : Syllogism → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance Semantics.Quantification.Syllogistic.instInhabitedSyllogism : Inhabited Syllogism

Equations

• Semantics.Quantification.Syllogistic.instInhabitedSyllogism = { default := Semantics.Quantification.Syllogistic.instInhabitedSyllogism.default }

def Semantics.Quantification.Syllogistic.instInhabitedSyllogism.default : Syllogism

Equations

• Semantics.Quantification.Syllogistic.instInhabitedSyllogism.default = { q1 := default, order1AB := default, q2 := default, order2BC := default }

@[implicit_reducible]

instance Semantics.Quantification.Syllogistic.instFintypeSyllogism : Fintype Syllogism

Equations

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

inductive Semantics.Quantification.Syllogistic.Conclusion : Type

The 9 possible conclusions: 4 quantifiers × 2 term orders + NVC ("nothing follows"). NVC is the explicit response that no Aristotelian conclusion is warranted — modeled semantically as the vacuous utterance.

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

@[implicit_reducible]

instance Semantics.Quantification.Syllogistic.instDecidableEqConclusion : DecidableEq Conclusion

Equations

• Semantics.Quantification.Syllogistic.instDecidableEqConclusion x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[implicit_reducible]

instance Semantics.Quantification.Syllogistic.instReprConclusion : Repr Conclusion

Equations

• Semantics.Quantification.Syllogistic.instReprConclusion = { reprPrec := Semantics.Quantification.Syllogistic.instReprConclusion.repr }

def Semantics.Quantification.Syllogistic.instReprConclusion.repr : Conclusion → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance Semantics.Quantification.Syllogistic.instInhabitedConclusion : Inhabited Conclusion

Equations

• Semantics.Quantification.Syllogistic.instInhabitedConclusion = { default := Semantics.Quantification.Syllogistic.instInhabitedConclusion.default }

def Semantics.Quantification.Syllogistic.instInhabitedConclusion.default : Conclusion

Equations

• Semantics.Quantification.Syllogistic.instInhabitedConclusion.default = Semantics.Quantification.Syllogistic.Conclusion.allAC

@[implicit_reducible]

instance Semantics.Quantification.Syllogistic.instFintypeConclusion : Fintype Conclusion

Equations

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

def Semantics.Quantification.Syllogistic.Conclusion.isAC : Conclusion → Bool

Does the conclusion use A→C term order (vs C→A)? Used by figural-bias parameterisations that prefer one term order based on the syllogism's figure.

Equations

• Semantics.Quantification.Syllogistic.Conclusion.allAC.isAC = true
• Semantics.Quantification.Syllogistic.Conclusion.someAC.isAC = true
• Semantics.Quantification.Syllogistic.Conclusion.someNotAC.isAC = true
• Semantics.Quantification.Syllogistic.Conclusion.noAC.isAC = true
• x✝.isAC = false

def Semantics.Quantification.Syllogistic.Conclusion.short : Conclusion → String

Short label for display (Aristotelian medieval letter codes: A = universal affirmative, I = particular affirmative, E = universal negative, O = particular negative).

Equations

• Semantics.Quantification.Syllogistic.Conclusion.allAC.short = "Aac"
• Semantics.Quantification.Syllogistic.Conclusion.allCA.short = "Aca"
• Semantics.Quantification.Syllogistic.Conclusion.someAC.short = "Iac"
• Semantics.Quantification.Syllogistic.Conclusion.someCA.short = "Ica"
• Semantics.Quantification.Syllogistic.Conclusion.someNotAC.short = "Oac"
• Semantics.Quantification.Syllogistic.Conclusion.someNotCA.short = "Oca"
• Semantics.Quantification.Syllogistic.Conclusion.noAC.short = "Eac"
• Semantics.Quantification.Syllogistic.Conclusion.noCA.short = "Eca"
• Semantics.Quantification.Syllogistic.Conclusion.nvc.short = "NVC"