Stoic Logic and Natural Term Logic

 We intend to use Natural Term Logic to formalize Stoic logic (in particular the use of indefinite pronouns in the conditional rendering of universal quantification) and following Bobzien argue that much of 19th and early 20th century philosophy of logic plagiarized the Stoics.  

We are thinking about writing a paper in which we apply my Natural Term Logic to Stoic logic. We are considering the hypothesis that modern propositional logic is not adequate to represent Stoic logic, in particular, to represent the schemes of arguments (DL. 7.76), indemonstrables,  modes. The Stoic "conditional" cannot be abstracted into a propositional conditional (truth-functional or not).  Rather a new type of variable-free formal system is called for (closer to the syntax of natural language).  I consider the example: Aug. Dial.3.84-6, i. Fat. 11-15.  In NTL this would be expressed in NTL as: $\Lambda_{\forall}\Upsilon^{\{1,2\}}\Lambda_{\rightarrow}W^{(1)}M^{(1)}, \Pi^{(0)} W\tau \vdash \Pi^{(0)} M\tau$. Here the $\Upsilon$ expresses the intertwining (in the graph calculus for NTL this becomes more than a metaphor!) of the indefinite pronouns, the anaphora. Stoic logic (and all human rational systems) must accept and implicitly contain the universal instantiation rule ($\forall E$):  $\Lambda^1_\forall T^{(1)} \vdash \Pi^{(0)}TS$ alongside $\Lambda_\rightarrow A^{(0)}B^{(0)}, A \vdash B$. We use the NTL reduction rules to obtain the above syllogism.  

If a something is A then it is B.   Surely the above interpretation is not quite right, or at least there should be another way of expressing this - perhaps using a variant of NTL and based on a modification of $\exists x A(x) \rightarrow B(x)$. Somehow we got to let the bound variable escape its initial scope. We need to formalize anaphora (maybe like control structures, continuation style passing, in computer science) and this is a most profound and interesting question in logic and linguistics! For example $\exists x A(x) \rightarrow B(\tau x. x)$ would mean that the $x$ in the scope of $\tau$ is still in the scope of $\exists x$ but not existentially quantified only exemplifcationally quantified - proof theoretically if we took by ekthesis such an a such that $A(a)$ then we would be able to conclude that $B(a)$. Now we should transpose these ideas into a variant of NTL. Eliminate $\Lambda_\forall$ and instead use pseudo-variables $\tau$ (or $\tau_i$) with the rule that they can be substituted for any NTL term.  Thus our sentence is $\Lambda_{\rightarrow} \Pi W^{(1)}\tau \Pi M^{(1)}\tau$ or $\Pi\Upsilon^{\{1,2\}}\Lambda_{\rightarrow}W^{(1)}M^{(1)}\tau$.  We can read $\tau$ as "anything". Find a similar way to deal with existential quantifiers. This is through another constructor $\alpha T$ read "a T" which need not denote.  We can introduce a existence constructor or term $\chi^{(1)}$. Thus "every man has a father" becomes

$\Lambda_\rightarrow M\tau  \chi\alpha F\tau$ 

Bobzien: "formulation of universals as quantified conditionals".