AIEO Square as a Diagram instance

The four syllogistic forms (syllAll, syllSome, syllSomeNot, syllNone) applied to a fixed (X, Y) term-predicate pair form a 4-corner Aristotelian diagram (Square) over the model class W = VennState.

This file constructs the Diagram (Fin 4) instance and provides the individual conditional Aristotelian relations. Some relations require the restrictor (s ∧ X) to be non-empty (Aristotelian sortal restriction); these are stated with explicit hypothesis or restricted to the non-degenerate substate.

Mapping

Following Demey & Smessaert (and the medieval ordering):

Position	Aristotelian	Form	Lean
0	A	universal +	syllAll
1	E	universal −	syllNone
2	I	particular +	syllSome
3	O	particular −	syllSomeNot

Status

The Square is provided as a Diagram (the fragment cornerForm); its relations are derived. The contradiction diagonals (A↔O, E↔I) hold unconditionally under the modern (FOL) reading and are recorded as theorems (aieoSquare_AO_contradictory, aieoSquare_EI_contradictory). The subalternations A→I, E→O are conditional on existential import (∃R); the sortal-restricted Aristotelian variant where the full Square holds is the natural follow-up (TODO).

Corner indexing

inductive Quantification.Syllogistic.Corner : Type

Square corners in A/E/I/O order.

• A : Corner
• E : Corner
• I : Corner
• O : Corner

@[implicit_reducible]

instance Quantification.Syllogistic.instDecidableEqCorner : DecidableEq Corner

Equations

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

def Quantification.Syllogistic.instReprCorner.repr : Corner → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance Quantification.Syllogistic.instReprCorner : Repr Corner

Equations

• Quantification.Syllogistic.instReprCorner = { reprPrec := Quantification.Syllogistic.instReprCorner.repr }

@[implicit_reducible]

instance Quantification.Syllogistic.instFintypeCorner : Fintype Corner

Equations

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

The AIEO Square as a Diagram

def Quantification.Syllogistic.cornerForm (X Y : Region → Bool) : Corner → VennState → Bool

The four syllogistic forms applied to (X, Y), indexed by Corner.

Equations

• Quantification.Syllogistic.cornerForm X Y Quantification.Syllogistic.Corner.A = fun (s : Quantification.Syllogistic.VennState) => Quantification.Syllogistic.syllAll s X Y
• Quantification.Syllogistic.cornerForm X Y Quantification.Syllogistic.Corner.E = fun (s : Quantification.Syllogistic.VennState) => Quantification.Syllogistic.syllNone s X Y
• Quantification.Syllogistic.cornerForm X Y Quantification.Syllogistic.Corner.I = fun (s : Quantification.Syllogistic.VennState) => Quantification.Syllogistic.syllSome s X Y
• Quantification.Syllogistic.cornerForm X Y Quantification.Syllogistic.Corner.O = fun (s : Quantification.Syllogistic.VennState) => Quantification.Syllogistic.syllSomeNot s X Y

Contradictory diagonal lemmas (modern reading, unconditional)

theorem Quantification.Syllogistic.syllAll_contradictory_syllSomeNot (X Y : Region → Bool) : Aristotelian.IsContradictory (fun (s : VennState) => syllAll s X Y) fun (s : VennState) => syllSomeNot s X Y

syllAll and syllSomeNot are contradictories at every state: exactly one is true. The "no clash" half follows from extracting the syllSomeNot witness and applying syllAll's universal; the "exhaustion" half is classical LEM on the existence of a Y-counterexample restrictor element.

theorem Quantification.Syllogistic.syllNone_contradictory_syllSome (X Y : Region → Bool) : Aristotelian.IsContradictory (fun (s : VennState) => syllNone s X Y) fun (s : VennState) => syllSome s X Y

syllNone and syllSome are contradictories at every state. Symmetric structure to syllAll_contradictory_syllSomeNot.

The AIEO Square as a Diagram instance

noncomputable def Quantification.Syllogistic.aieoSquare (X Y : Region → Bool) : Aristotelian.Diagram Corner (VennState → Bool)

The AIEO Square as a Diagram over Corner corners — the fragment cornerForm.

Equations

• Quantification.Syllogistic.aieoSquare X Y = { φ := Quantification.Syllogistic.cornerForm X Y }

theorem Quantification.Syllogistic.aieoSquare_AO_contradictory (X Y : Region → Bool) : Aristotelian.IsContradictory ((aieoSquare X Y).φ Corner.A) ((aieoSquare X Y).φ Corner.O)

A and O are contradictories in the AIEO Square (unconditional, modern reading).

theorem Quantification.Syllogistic.aieoSquare_EI_contradictory (X Y : Region → Bool) : Aristotelian.IsContradictory ((aieoSquare X Y).φ Corner.E) ((aieoSquare X Y).φ Corner.I)

E and I are contradictories in the AIEO Square (unconditional, modern reading).