Note on the Stoic Categories (older post)

We plan to study the formalization of Stoic logic and the Stoic categories.  I had made a close study of Bealer's  first-order intensional  logic such as presented in his book Quality and Concept. Unlike most approaches  Bealer takes propositions, unary predicates, relations, etc. to be primitive entities, units of meaning which are woven together by complex logico-combinatoric relations including the attribution of truth-value depending on states-of-affairs.  Afterwards I read Susanne Bobzien's papers on Stoic logic and specially  Did Frege plagiarize the Stoics which offered insights into both the Stoics and Frege. I then realized that the Stoic theory of lekta was an intensional version of Frege's logic and that not only did it agree with Bealer but my experience working with  dependent type theory in the Coq proof assistant suggested to me an alternative intensional type-theoretic  version of the semantics of Bealer's logic which is closely aligned to Stoic logic. There is a primitive type of 'saturared' lekta $\Lambda$  corresponding to Bealer's set of propositions $\mathcal{D}_0$,   a primitive type of truth-values $\Omega$ and a primitive type $W$ which can be thought of as indexing possible states-of-affairs or 'possible worlds'.  Our logic is essentially a logic of meaning and all operations are defined primitively on $\Lambda$ or types involving $\Lambda$ rather than on $\Omega$ (like in topos theory). The logic of truth and extensions is mediated by what I call the alethic term $\alpha : W \times \Lambda \rightarrow \Omega$ which specifies which assertibles hold in a given situation or state-of-affairs. As Bobzien writes in the Cambridge Companion (2006): The most far-reaching one is that truth and falsehood are temporal properties of assertibles. They can belong to an assertible at one time but not at another.  Note that in the Calculus of Constructions upon which Coq is based we could consider taking the type Prop as $\Lambda$. I found that  section II  of Logic and General Theory of Science (lectures from 1917/1918)  Husserl carries out an analysis of natural language which corresponds closely to the type-theoretic intensional logic I had in mind. I noted that in paragraph of section II Husserl writes: A grammatical distinction passed down from Scholasticism, and otherwise going back to the Stoics, can serve as our point of departure. This is the distinction between independent and dependent expressions.

There is also the enigma of the Stoic categories. An old paper by Margaret Reesor (1957) presents some interesting information about the category of 'relation'  pros ti  and specially pros ti pôs ekhôn translated as 'relative disposition'.   It seems that the older Stoics considered such  terms as 'intelligence' and 'virtue' both in themselves simply and qualified and related to something else.  For instance for Zeno courage is wisdom in things to be endured and justice is wisdom in things to be distributed.  It does not seem straightforward to present this in terms of the modern predicate calculus, for instance a binary relation $\exists y.R(x,y)$ instantiated differently as $ R_1(x):=R(x,a),  R_2(x) := R(x,b)$, etc. Rather this situation recalls polymorphism in modern type theory or its more general form involving dependent type theory with universes.  This can be understood by an example from programming languages where there is a general class for 'list'  taking a type as a parameter which then becomes a concrete object according to the specified type (we get lists of integers, lists of boolean values, lists of strings, etc.).  Thus dependent types such as $\Pi_{T: Type} Type$ would seem to capture the Stoic category of relation which includes 'virtue' and 'intelligence'. These are both  types in themselves and  types which can be further determined through specification of an external type $S$ which we obtain through application $(\Pi_{T: Type} Type) S : Type$.  Thus we can speak of 'list' simply or 'list of $X$s', 'list of $Y$s', etc. Likewise we have both 'wisdom' and 'wisdom in $X$', 'wisdom in $Y$' for types X and Y.

What of the concepts of  dependent and independent meaning ?  The type $\Lambda$ is certainly independent. The corresponding dependent types are those that can be written equivalently (i.e. via currying) in the form $X \rightarrow \Lambda$. Thus for example 'or' would have type $\Lambda\rightarrow(\Lambda \rightarrow \Lambda)$ which is equivalent to $\Lambda\times\Lambda \rightarrow \Lambda$.  But there are other types of independent and dependent meanings.  A preliminary proposal might be that independent meanings are atomic types and dependent meanings non-atomic types.

A dependent meaning can be transformed into a independent one, for instance when we talk about 'the connective or'.  This can be handled by a term $ n_X : (X\rightarrow \Lambda) \rightarrow N$ which transforms a dependent meaning type into for instance a noun term of the atomic type $N$. This is of course also Bealer's  intensional abstraction /nominalization operator.