“It’s all Greek to me”– on the pre-history ofcoherence in categorical logic
Peter M. Hines
This talk details a somewhat whimsical quest to give algebraic / categoricalmodels of ancient Greek logic : precisely, the Stoic treatment of connectives
expounded by Chrysippus, as understood – possibly misunderstood – by Hipparchus.
Our starting point is a well-documented disagreement between followers ofHipparchus, and those of Chrysippus, described in Plutarch’s Quaestiones Conviviales and other sources. This was on the oddly specific question of how manydistinct ‘non-simple assertibles’ [compound propositions] may be formed byconjunctions (or simply ‘combinations’) of ten ‘elementary assertibles’ [atomicpropositions]. Chrysippus claimed to give an order of magnitude figure ‘exceeding one million’ (i.e. tens of myriads). In contrast, Plutarch reports —seemingly as a well-established fact — that Hipparchus and ‘all the arithmeticians’ had refuted Chrysippus, and established the precise number to be 103049.
The significance of this number remained unknown until 1994, when it wasidentified by Daniel Hough as the 10th little Schröder number, and hence thenumber of rooted planar trees with ten leaves [10]. Taking the very natural stepof interpreting each tree leaf as an atomic proposition, and each branching as aconnective, we arrive at the ‘obvious interpretation’ of such trees as compound
propositions – giving a solution to a very long-standing unresolved question.
The little Schröder numbers are now known as the Schröder-Hipparchus
numbers; more generally, it has recently become clear that the combinatorics
of ancient Greece was significantly more advanced than previously understood.
This, of course, provoked intense interest among historians of science and mathematics, and several convincing attempts (e.g. [1]) have been made to reconstruct
how Hipparchus’ calculations could be computed with the framework of ancient
Greek mathematics.
Even more recently, the logical system in question has been re-investigated,
and found to be similarly ahead of its time. The Stanford Encyclopedia ofPhilosophy https://plato.stanford.edu/ describes Chrysipus’ contribution
to Greek logic as, “a substructural backwards-working Gentzen-style natural
deduction system” – features that are more usually associated with late 20th1

century logical systems such as [9]. In [3], we find further startlingly modern features such as, recursively formulated syntax, Cut rules, Gentzen-style negation
introduction, and avoidance of paradoxes by deliberate rejection of [structuralrules].
This leaves us with a puzzle : both Chrysippus and Hipparchus were spectacularly ahead of their time, in logic and combinatorics respectively. How,
then, did they arrive at such different figures, and what was the root cause of
their disagreement?
This question is analysed by Suzanne Bobzien in [2], who makes the case that,“Hipparchus, as one might expect, got his mathematics right. What I suggest
is that he got his Stoic logic wrong”. The core of this is that propositions thatshould have been identified were instead counted separately. Precisely, propositions arising via different (partial or total) bracketings of the same elementary
propositions were incorrectly considered as entirely distinct.
This is of course familiar from modern categorical logic; we are often forced touse ‘identical up to unique natural isomorphism’ instead of some strict notion ofequality, and impose coherence conditions that ensure the natural isomorphisms
relating distinct bracketings are indeed unique.
A fun question (albeit with no historical justification whatsoever) is to consider how this dispute could be resolved by working within a system where thepropositions that Bobzien claims as incorrectly counted separately were indeed
related in this way? We give a system that does precisely this. We extend
logical models that reflect the known sub-structural properties of Stoic logic1 toinclude the assumptions apparently made by Hipparchus.
The result is ‘freely generated’ in the operadic sense; distinct partial or total bracketings are not identified, & we may therefore label arbitrary facets ofStasheff’s associahedra with functors corresponding to partial or total bracketings of conjunctions. We also exhibit natural transformations between themthat live in a posetal groupoid, and are therefore unique – thus accounting forcoherence & uniqueness in the natural isomorphisms that replace equality.
This gives a range of diagrams, based on associahedra, guaranteed to commute (including, of course, MacLane’s pentagon as a very special case). As arather neat surprise, the components of these natural transformations between‘conjunctions’ are the operations used in John Conway’s proof2 of undecidability in elementary arithmetic [4]. Further, they include his motivating example(his claimed ‘simplest undecidable arithmetic statement’ [5]) as a special case.
Finally, we briefly consider some work of John Conway linking this motivating
example to some additional classical Greek mathematics.
1 Precisely, it is believed that the Weakening rule was not accepted; some sources also
indicate that caution is needed concerning the Contraction rule. We therefore borrow andextend a model of conjunction (introduced in [7, 8]) from Multiplicative Linear Logic.
2 Significantly prefigured by Sergei Maslov [6].

2References[1] F. Acerbi. On the shoulders of hipparchus: A reappraisal of ancient greek
combinatorics. Archive for History of Exact Sciences, 57(6):465–502, 2003.
[2] Susanne Bobzien. The combinatorics of stoic conjunction. Oxford Studies
in Ancient Philosophy, 40:157–188, 2011.
[3] Susanne Bobzien. Stoic sequent logic and proof theory. History and Philosophy of Logic, 40, 03 2019.
[4] John Conway. Unpredictable iterations. Proc. 1972 Number Theory, pages
49–52, 1972.
[5] John Conway. On unsettleable arithmetical problems. The American Mathematical Monthly, 120 (3):192–198, 2013.
[6] E. M. Fels. Review of: On e.l. post’sa tag problem, by sergei maslov. The
Journal of Symbolic Logic, 32(4):524–526, 1967.
[7] J.-Y. Girard. Geometry of interaction 1. In Proceedings Logic Colloquium’88, pages 221–260. North-Holland, 1988.
[8] J.-Y. Girard. Geometry of interaction 2: deadlock-free algorithms. In
Conference on Computer Logic, volume 417 of Lecture Notes in Computer
Science, pages 76–93. Springer, 1988.
[9] Jean-Yves Girard. Linear logic: Its syntax and semantics. In Proceedings of the Workshop on Advances in Linear Logic, page 1–42, USA, 1995.
Cambridge University Press.
[10] Richard P. Stanley. Hipparchus, plutarch, schröder, and hough. The American Mathematical Monthly, 104(4):344–350, 1997.

3