Syllogistic forms: modern (FOL) reading

The four syll* predicates correspond to the A/I/E/O corners of the Aristotelian square, evaluated over a Venn state with given term predicates X, Y : Region → Bool. This file uses the modern (first-order) reading: no existential import on the universal forms (syllAll, syllNone).

Form	A (universal +)	I (particular +)	E (universal −)	O (particular −)
Lean	syllAll	syllSome	syllNone	syllSomeNot
GQ	every_sem	some_sem	no_sem	¬every_sem
FOL	∀ X→Y	∃ X∧Y	∀ X→¬Y	∃ X∧¬Y

The grounding theorems syll*_eq_true_iff connect each syll* to the corresponding GQ denotation from Quantifier.lean, making the relationship true by construction.

Existential import lives in study files

Aristotelian readings (existential import on universal forms — e.g. "All A is B" presupposes ∃A) are paper-specific stances and live as study-file wrappers, e.g.

def tesslerAll s X Y := syllAll s X Y && decide (∃ r, s r ∧ X r)

This matches the codebase convention: substrate stays modern/FOL/mathlib-style; paper-specific commitments wrap the substrate at the point of use.

The Aristotelian Square (with full SquareRelations) lives in Square.lean as a sortal restriction to states with non-empty restrictor — see that file for the full opposition diagram in the Demey–Smessaert sense.

Syllogistic forms (modern reading, no existential import)

def Quantification.Syllogistic.syllAll (s : VennState) (X Y : Region → Bool) : Bool

"All Xs are Ys" in state s (modern reading): every populated X-region also has Y. Vacuously true when no populated X-region exists.

Equations

• Quantification.Syllogistic.syllAll s X Y = decide (∀ (r : Quantification.Syllogistic.Region), s r = true ∧ X r = true → Y r = true)

def Quantification.Syllogistic.syllSome (s : VennState) (X Y : Region → Bool) : Bool

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

Equations

• Quantification.Syllogistic.syllSome s X Y = decide (∃ (r : Quantification.Syllogistic.Region), (s r = true ∧ X r = true) ∧ Y r = true)

def Quantification.Syllogistic.syllSomeNot (s : VennState) (X Y : Region → Bool) : Bool

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

Equations

• Quantification.Syllogistic.syllSomeNot s X Y = decide (∃ (r : Quantification.Syllogistic.Region), (s r = true ∧ X r = true) ∧ ¬Y r = true)

def Quantification.Syllogistic.syllNone (s : VennState) (X Y : Region → Bool) : Bool

"No Xs are Ys" (modern reading): no populated X-region has Y. Vacuously true when no populated X-region exists.

Equations

• Quantification.Syllogistic.syllNone s X Y = decide (∀ (r : Quantification.Syllogistic.Region), s r = true ∧ X r = true → ¬Y r = true)

Grounding in every_sem / some_sem / no_sem

theorem Quantification.Syllogistic.syllAll_eq_true_iff (s : VennState) (X Y : Region → Bool) : syllAll s X Y = true ↔ every_sem (fun (r : Region) => s r = true ∧ X r = true) fun (r : Region) => Y r = true

syllAll is exactly every_sem over the state-restricted restrictor.

theorem Quantification.Syllogistic.syllSome_eq_true_iff (s : VennState) (X Y : Region → Bool) : syllSome s X Y = true ↔ some_sem (fun (r : Region) => s r = true ∧ X r = true) fun (r : Region) => Y r = true

syllSome is exactly some_sem over the state-restricted restrictor.

theorem Quantification.Syllogistic.syllNone_eq_true_iff (s : VennState) (X Y : Region → Bool) : syllNone s X Y = true ↔ no_sem (fun (r : Region) => s r = true ∧ X r = true) fun (r : Region) => Y r = true

syllNone is exactly no_sem over the state-restricted restrictor.

Quantifier and premise evaluation

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

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

Equations

• Quantification.Syllogistic.syllQuantEval Quantification.Syllogistic.AristQuant.all s X Y = Quantification.Syllogistic.syllAll s X Y
• Quantification.Syllogistic.syllQuantEval Quantification.Syllogistic.AristQuant.some s X Y = Quantification.Syllogistic.syllSome s X Y
• Quantification.Syllogistic.syllQuantEval Quantification.Syllogistic.AristQuant.someNot s X Y = Quantification.Syllogistic.syllSomeNot s X Y
• Quantification.Syllogistic.syllQuantEval Quantification.Syllogistic.AristQuant.no s X Y = Quantification.Syllogistic.syllNone s X Y

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

Truth value of premise 1 in state s.

Equations

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

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

Truth value of premise 2 in state s.

Equations

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

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

Literal meaning of each conclusion in a Venn state (modern reading). NVC ("nothing follows") is true in every state — the vacuous utterance.

Equations

• Quantification.Syllogistic.concMeaning Quantification.Syllogistic.Conclusion.allAC x✝ = Quantification.Syllogistic.syllAll x✝ Quantification.Syllogistic.hasA Quantification.Syllogistic.hasC
• Quantification.Syllogistic.concMeaning Quantification.Syllogistic.Conclusion.allCA x✝ = Quantification.Syllogistic.syllAll x✝ Quantification.Syllogistic.hasC Quantification.Syllogistic.hasA
• Quantification.Syllogistic.concMeaning Quantification.Syllogistic.Conclusion.someAC x✝ = Quantification.Syllogistic.syllSome x✝ Quantification.Syllogistic.hasA Quantification.Syllogistic.hasC
• Quantification.Syllogistic.concMeaning Quantification.Syllogistic.Conclusion.someCA x✝ = Quantification.Syllogistic.syllSome x✝ Quantification.Syllogistic.hasC Quantification.Syllogistic.hasA
• Quantification.Syllogistic.concMeaning Quantification.Syllogistic.Conclusion.someNotAC x✝ = Quantification.Syllogistic.syllSomeNot x✝ Quantification.Syllogistic.hasA Quantification.Syllogistic.hasC
• Quantification.Syllogistic.concMeaning Quantification.Syllogistic.Conclusion.someNotCA x✝ = Quantification.Syllogistic.syllSomeNot x✝ Quantification.Syllogistic.hasC Quantification.Syllogistic.hasA
• Quantification.Syllogistic.concMeaning Quantification.Syllogistic.Conclusion.noAC x✝ = Quantification.Syllogistic.syllNone x✝ Quantification.Syllogistic.hasA Quantification.Syllogistic.hasC
• Quantification.Syllogistic.concMeaning Quantification.Syllogistic.Conclusion.noCA x✝ = Quantification.Syllogistic.syllNone x✝ Quantification.Syllogistic.hasC Quantification.Syllogistic.hasA
• Quantification.Syllogistic.concMeaning Quantification.Syllogistic.Conclusion.nvc x✝ = true

@[simp]

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

"Nothing follows" is always true.

Subalternation A → I (conditional on non-empty restrictor)

theorem Quantification.Syllogistic.syllAll_imp_syllSome (s : VennState) (X Y : Region → Bool) (hExists : ∃ (r : Region), s r = true ∧ X r = true) (h : syllAll s X Y = true) : syllSome s X Y = true

Subalternation in the modern reading: "All Xs are Ys" entails "Some Xs are Ys" only when at least one X-region is populated. Derived from subalternation_a_i in Quantifier.lean.

Named syllogisms

def Quantification.Syllogistic.barbara : Syllogism

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

Equations

• Quantification.Syllogistic.barbara = { q1 := Quantification.Syllogistic.AristQuant.all, order1AB := true, q2 := Quantification.Syllogistic.AristQuant.all, order2BC := true }

def Quantification.Syllogistic.allAB_allCB : Syllogism

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

Equations

• Quantification.Syllogistic.allAB_allCB = { q1 := Quantification.Syllogistic.AristQuant.all, order1AB := true, q2 := Quantification.Syllogistic.AristQuant.all, order2BC := false }

def Quantification.Syllogistic.someSome : Syllogism

Some A-B, Some B-C. Figure 1 (also invalid).

Equations

• Quantification.Syllogistic.someSome = { q1 := Quantification.Syllogistic.AristQuant.some, order1AB := true, q2 := Quantification.Syllogistic.AristQuant.some, order2BC := true }

Validity: Barbara

theorem Quantification.Syllogistic.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). State-restricted transitivity of every_sem. Modern reading; existential import not required for the All conclusion.

theorem Quantification.Syllogistic.barbara_some_valid (s : VennState) (h1 : syllAll s hasA hasB = true) (h2 : syllAll s hasB hasC = true) (hExists : ∃ (r : Region), s r = true ∧ hasA r = true) : syllSome s hasA hasC = true

Barbara also validates "Some A are C" provided some A exists. Composes barbara_valid with syllAll_imp_syllSome. The Aristotelian reading takes existential import on the premises as built-in; the modern reading exposes it as an explicit hypothesis.

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

For Barbara, every state where both premises are literally true also satisfies "All A-C".

Witness states and invalidity

def Quantification.Syllogistic.state_AB_BC : VennState

Only AB and BC populated. Witnesses invalidity of certain syllogism patterns by falsifying A/I A-C and A/I C-A.

Equations

• Quantification.Syllogistic.state_AB_BC Quantification.Syllogistic.Region.AB = true
• Quantification.Syllogistic.state_AB_BC Quantification.Syllogistic.Region.BC = true
• Quantification.Syllogistic.state_AB_BC x✝ = false

def Quantification.Syllogistic.state_ABC : VennState

Only ABC populated. Witnesses invalidity by falsifying E/O A-C and E/O C-A.

Equations

• Quantification.Syllogistic.state_ABC Quantification.Syllogistic.Region.ABC = true
• Quantification.Syllogistic.state_ABC x✝ = false

def Quantification.Syllogistic.state_A_AC : VennState

Only A and AC populated. syllSome A-C holds; syllAll A-C fails.

Equations

• Quantification.Syllogistic.state_A_AC Quantification.Syllogistic.Region.A = true
• Quantification.Syllogistic.state_A_AC Quantification.Syllogistic.Region.AC = true
• Quantification.Syllogistic.state_A_AC x✝ = false

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

Strict informativity: "All A-C" is compatible with strictly fewer states than "Some A-C" (witnessed by state_A_AC).

theorem Quantification.Syllogistic.allAB_allCB_invalid : concMeaning Conclusion.allAC state_AB_BC = false ∧ concMeaning Conclusion.someAC state_AB_BC = false ∧ concMeaning Conclusion.allCA state_AB_BC = false ∧ concMeaning Conclusion.someCA state_AB_BC = false ∧ concMeaning Conclusion.noAC state_ABC = false ∧ concMeaning Conclusion.someNotAC state_ABC = false ∧ concMeaning Conclusion.noCA state_ABC = false ∧ concMeaning Conclusion.someNotCA state_ABC = false

"All A-B, All C-B" is logically invalid: no Aristotelian conclusion holds in all compatible states. Two counterexample states cover the eight quantified conclusions.

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

For the invalid syllogism (All A-B, All C-B), some consistent states satisfy "All A-C" while others falsify it.