Addenda on Ancient Natural Deduction

 The following notes can serve as a complement to our paper Ancient Natural Deduction.  First we have a formalisation of Euclid I.1 and Euclid  VII.1 in linearised natural deduction to illustrate the constructivist use of the existential quantifier.  The following note on Physics 231b18-232a18 contains an additional example of how Aristotle is lead to reason with multiple and embedded quantifiers.

 A striking revolution in the history of logic has been the rediscovery of the richness and sophistication of ancient logic, specially Stoic logic and Indian Logic (cf. papers of G. Priest and John N. Martin as well as [jaya, gan] ) and its often close anticipation of modern formal and philosophical logic and philosophy of language. A substructural sequent calculus and many key concepts of Frege's philosophy of logic and language have been shown to have been  in possession by the Stoics.   This has rendered the traditional narrative surrounding Frege untenable (we also need to investigate connections to Lotze and Bolzano.  We need to accumulate evidence that the ancients had a logic embodying axioms and rules capable of dealing with multiple generality and nested quantifiers (see the article by Bobzien and Shogry on multiple generality in the Stoics and T. Parsons' book Articulating Medieval Logic) , and that many concepts of modern logic and category theory were anticipated in ancient logic. We must study the Stoic categories and theory of definition and their affinity to Leibniz's approach as well as the methodology  employed in modern mathematics and science.