Is there a formalization of syllogistic logic? Is there a book or paper that formalizes Aristotle's syllogistic logic? As in, define the well-formed formulas, define the semantics, define deduction rules, and prove that the deduction rules are both sound and complete?
 A: This has been studied by Larry Moss - see e.g. here. In particular, Moss presented a sound and complete proof system for the whole syllogistic and several of its fragments.
It's worth noting that Moss is by no means the first person to whip up a complete proof system for syllogistic logic. I believe the first was Lukasiewicz, who Moss mentions (and I think Moss's bibliography will in general be helpful). My understanding is that the novel feature of Moss's work is primarily its study of the fragments of syllogistic logic, and so it's worth mentioning for that reason. (I also think it's very well-written, whereas I find a number of papers in the area fairly difficult to read.)
A: To add another couple of references to those given by @NoahSchweber, there are two must-read classic papers by Timothy Smiley (who by the way shows that Lukasiewicz radically misunderstands what is going on in Aristotle's system). Both papers are eminently clear and straightforward [links are to Jstor, if you have access]:


*

*Timothy Smiley, Syllogism and Quantification, JSL 1962

*Timothy Smiley, What is a Syllogism, JPL 1963
