Documentation

Linglib.Theories.Semantics.Quantification.Syllogistic.Square

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

PositionAristotelianFormLean
0Auniversal +syllAll
1Euniversal −syllNone
2Iparticular +syllSome
3Oparticular −syllSomeNot

Status #

The Square is provided as Diagram data with the relation matrix labeled. The full relation_correct discharge is partial — modern (FOL) reading makes some relations conditional on ∃R, so we mark those as unconnected in the labeled matrix and provide them as separate conditional theorems. The Aristotelian (sortal-restricted) variant where the full Square holds is the natural follow-up in Aristotelian.lean (TODO).

source
inductive Semantics.Quantification.Syllogistic.Corner :
Type

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

Instances For
    source
    @[implicit_reducible]
    instance Semantics.Quantification.Syllogistic.instDecidableEqCorner :
    DecidableEq Corner
    Equations
    source
    def Semantics.Quantification.Syllogistic.instReprCorner.repr :
    Corner → ℕ → Std.Format
    Equations
    • One or more equations did not get rendered due to their size.
    Instances For
      source
      @[implicit_reducible]
      instance Semantics.Quantification.Syllogistic.instReprCorner :
      Repr Corner
      Equations
      source
      @[implicit_reducible]
      instance Semantics.Quantification.Syllogistic.instFintypeCorner :
      Fintype Corner
      Equations
      • One or more equations did not get rendered due to their size.
      source
      def Semantics.Quantification.Syllogistic.cornerForm (X Y : Region → Bool) :
      Corner → VennState → Bool

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

      Equations
      • One or more equations did not get rendered due to their size.
      Instances For
        source
        def Semantics.Quantification.Syllogistic.cornerRel :
        Corner → Corner → Core.Opposition.AristotelianRel

        The labeled relation between corners. Modern reading: subalternations A→I and E→O depend on existential import, so they appear as unconnected in the unconditional matrix; the contradiction diagonals A↔O and E↔I are unconditional under modern reading.

        Equations
        Instances For
          source
          theorem Semantics.Quantification.Syllogistic.syllAll_contradictory_syllSomeNot (X Y : Region → Bool) :
          Core.Opposition.Contradictory (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.

          source
          theorem Semantics.Quantification.Syllogistic.syllNone_contradictory_syllSome (X Y : Region → Bool) :
          Core.Opposition.Contradictory (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.

          source
          noncomputable def Semantics.Quantification.Syllogistic.aieoSquare (X Y : Region → Bool) :
          Core.Opposition.Diagram Corner VennState

          The AIEO Square as a Diagram instance over Corner corners. Discharges the contradictory cases via the lemmas above. The contrary/subcontrary/subaltern cases are vacuous because cornerRel labels all non-A↔O / non-E↔I pairs as unconnected.

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