Syllogistic forms as composition-engine trees

The A/I/E/O forms as QR'd Heim-Kratzer trees over the default logical vocabulary, with the first-figure syllogisms (Barbara, Celarent, Darii, Ferio) as cross-model tree entailments: each is a one-line instance of holdsAt_of_models — the first-order consequence is stated once, and the engine-level entailment over every composition model, world, and assignment follows through the agreement theorem. Complements Forms.lean's Venn-state semantics (grounded in the same every_sem/some_sem/no_sem denotations via Model.lexiconFO).

The four forms as trees

def Quantification.Syllogistic.aTree (x y : String) : Syntax.Tree Unit String

A-form: "every x y" after QR.

Equations

• Quantification.Syllogistic.aTree x y = ((Syntax.Tree.leaf "every").bin (Syntax.Tree.leaf x)).bin (Syntax.Tree.binder 1 ((Syntax.Tree.tr 1).bin (Syntax.Tree.leaf y)))

def Quantification.Syllogistic.iTree (x y : String) : Syntax.Tree Unit String

I-form: "some x y" after QR.

Equations

• Quantification.Syllogistic.iTree x y = ((Syntax.Tree.leaf "some").bin (Syntax.Tree.leaf x)).bin (Syntax.Tree.binder 1 ((Syntax.Tree.tr 1).bin (Syntax.Tree.leaf y)))

def Quantification.Syllogistic.eTree (x y : String) : Syntax.Tree Unit String

E-form: "no x y" after QR.

Equations

• Quantification.Syllogistic.eTree x y = ((Syntax.Tree.leaf "no").bin (Syntax.Tree.leaf x)).bin (Syntax.Tree.binder 1 ((Syntax.Tree.tr 1).bin (Syntax.Tree.leaf y)))

def Quantification.Syllogistic.oTree (x y : String) : Syntax.Tree Unit String

O-form: "not every x y" (the modern reading's ¬A).

Equations

• Quantification.Syllogistic.oTree x y = (Syntax.Tree.leaf "not").bin (Quantification.Syllogistic.aTree x y)

def Quantification.Syllogistic.andTree (p₁ p₂ : Syntax.Tree Unit String) : Syntax.Tree Unit String

Premise pair: "p₁ and p₂".

Equations

• Quantification.Syllogistic.andTree p₁ p₂ = p₁.bin ((Syntax.Tree.leaf "and").bin p₂)

First-figure syllogisms as cross-model tree entailments

Each is holdsAt_of_models applied to the compiled premises and a three-line first-order argument: state the consequence once over Realize, and the entailment between the trees holds in every composition model, world, and assignment.

theorem Quantification.Syllogistic.barbara {L : FirstOrder.Language} {nm : Semantics.Composition.LexNaming L} (hfr : { }.FreshFor nm) (hdj : nm.Disjoint) {x y z : String} {X Y Z : L.Relations 1} (hx : nm.preds₁ x = some X) (hy : nm.preds₁ y = some Y) (hz : nm.preds₁ z = some Z) (m : Semantics.Composition.Model L) (w : m.W) (g : Core.Assignment m.E) : Semantics.Composition.HoldsAt m (m.lexiconFO { } nm w) g (andTree (aTree y z) (aTree x y)) → Semantics.Composition.HoldsAt m (m.lexiconFO { } nm w) g (aTree x z)

Barbara (AAA-1): "every y z and every x y" entails "every x z".

theorem Quantification.Syllogistic.celarent {L : FirstOrder.Language} {nm : Semantics.Composition.LexNaming L} (hfr : { }.FreshFor nm) (hdj : nm.Disjoint) {x y z : String} {X Y Z : L.Relations 1} (hx : nm.preds₁ x = some X) (hy : nm.preds₁ y = some Y) (hz : nm.preds₁ z = some Z) (m : Semantics.Composition.Model L) (w : m.W) (g : Core.Assignment m.E) : Semantics.Composition.HoldsAt m (m.lexiconFO { } nm w) g (andTree (eTree y z) (aTree x y)) → Semantics.Composition.HoldsAt m (m.lexiconFO { } nm w) g (eTree x z)

Celarent (EAE-1): "no y z and every x y" entails "no x z".

theorem Quantification.Syllogistic.darii {L : FirstOrder.Language} {nm : Semantics.Composition.LexNaming L} (hfr : { }.FreshFor nm) (hdj : nm.Disjoint) {x y z : String} {X Y Z : L.Relations 1} (hx : nm.preds₁ x = some X) (hy : nm.preds₁ y = some Y) (hz : nm.preds₁ z = some Z) (m : Semantics.Composition.Model L) (w : m.W) (g : Core.Assignment m.E) : Semantics.Composition.HoldsAt m (m.lexiconFO { } nm w) g (andTree (aTree y z) (iTree x y)) → Semantics.Composition.HoldsAt m (m.lexiconFO { } nm w) g (iTree x z)

Darii (AII-1): "every y z and some x y" entails "some x z".

theorem Quantification.Syllogistic.ferio {L : FirstOrder.Language} {nm : Semantics.Composition.LexNaming L} (hfr : { }.FreshFor nm) (hdj : nm.Disjoint) {x y z : String} {X Y Z : L.Relations 1} (hx : nm.preds₁ x = some X) (hy : nm.preds₁ y = some Y) (hz : nm.preds₁ z = some Z) (m : Semantics.Composition.Model L) (w : m.W) (g : Core.Assignment m.E) : Semantics.Composition.HoldsAt m (m.lexiconFO { } nm w) g (andTree (eTree y z) (iTree x y)) → Semantics.Composition.HoldsAt m (m.lexiconFO { } nm w) g (oTree x z)

Ferio (EIO-1): "no y z and some x y" entails "not every x z".