Regarding Russell's famous attitude [1] towards Aristotle's logic [2], I have come to wonder if in the course of a justified frustration about an enormous time span of intellectual stagnation, Russell maybe missed an opportunity to recognize a few excellent aspects of Aristotle's logic, which, after dismissing them, took much effort to be rediscovered by Russell himself and then eventually by other people.

Here I am thinking of the fact that Aristotle's logic, while certainly naive and inaccurate from a modern perspective, has the exceptional feature of being a primitive kind of type theory [3].

Where Aristotle says "All A are B" we should recognize what in modern systems would be a function of types A -> B (maybe a monomorphism, if you insist, making A a subtype of B).

Where Aristotle says "Some B1 are B2" this is clearly to be read as an intersection of types, what in modern categorical logic is called a fiber product.

From this perspective, two complaints that are frequently raised against Aristotle's logic seem to be easily transmuted into virtues:

Some of Aristotle's deductions really depend on some silently assumed context. While that means that these were inaccuracies back then, today we easily know how to fix this right away: all types should be regarded as dependent types [4] that exist in some context, to be specified.

Another common complaint is that as Aristotle's types move from the subject of a judgement to the predicate, they seem to turn from types to propositions. For instance on the one hand Aristotle speaks of the collection of all mortal beings, on the other hand he speaks of the proposition "X is mortal". But there is no need to complain about this, in fact this very conflation is a famous accomplishment of modern logic, famous as the Curry-Howard isomorphism or the propositions-as-types paradigm. [5]

Summing up then, we see a logic with a concept of function types and product types formed in context. That's precisely the ingredients of locally Cartesian closed categories of types, which is what modern dependent type theory is about [6]

This is a bit ironic, because it is Russell him very self who, right after rejecting Aristotle, runs into the paradoxes of the young modern logic and is then the one to introduce the modern fix to these: types. See the references [7].

I came to think of this when following Lawvere's suggestion to keep an eye open for hidden insights in Hegel that are invisible to first-order logic but that begin to make a great deal of sense in modern categorical logic and type theory. Since Hegel likes syllogisms, that made me wonder. I have collected a few further details on what I have in mind at [8].

[0]

http://philosophy.stackexchange.com/a/23060/5473[1]

http://ncatlab.org/nlab/show/Logic+as+the+Essence+of+Philosophy[2]

http://ncatlab.org/nlab/show/Aristotle's+logic[3]

http://ncatlab.org/nlab/show/type theory

[4]

http://ncatlab.org/nlab/show/dependent+type+theory[5]

http://ncatlab.org/nlab/show/propositions+as+types[6]

http://ncatlab.org/nlab/show/relation between category theory and type theory

[7]

http://ncatlab.org/nlab/show/type%20theory#References[8]

http://ncatlab.org/nlab/show/Science+of+Logic#FormalizationText