The meaning of quantifiers

Quantifiers very likely are equivocal. These differences in meaning are revealed when they occur within an intensional context. There are universal quantifiers which express the sum total of the instantiations (which must pertain to a finite or constructible domain) and those that do not (for instance mass nouns). There are quantifiers that are subordinate to relations of intension. Also in our previous post we argued that quantifiers express the ability to understand and follow rules, to do computation. All rules can be expressed via universal monadic second and first-order quantification (which is Aristotle's implicit metalogic in the Topics). There are also quantifiers that express generic properties.

It seems very plausible that all quantifiers are implicitly limited to some domain (even for 'everything'), that unbounded quantifiers are meaningless.  We should focus specifically on nested quantifiers $\forall (x:A) \exists (y : B). P(x,y)$ and $\exists (x: A)\forall (y :B). P(x,y)$. The first has meaning: every A has a P, and plausibly that P can be found through a computatable function.The second has meaning: there is an A which is the P of every B, which plausibly can be checked.

Perhaps Aristotle took pairs (combinations) of natural deduction rules for quantifiers as primitive rules.  Notice how $\exists E$ and $\exists I$ can combine, the latter being 'in the middle' of the former.

It is plausible that the Mitchell-Peirce system of quantifier logic (1885) is not only technically and philosophically superior to Frege's Begriffsschrift (1879) but was developed earlier (by Peirce's student O. Mitchell).  Modern dependent type theory uses Peirce's symbols $\Pi$ and $\Sigma$. Or even the Boole-De Morgan relation calculus approach can make this claim. For instance $\forall x \exists y R(x,y)$ can be formulated as $RU \cap \Delta = \Delta$ where $U$ is the universal relation and $\Delta$ is the diagonal relation. $\exists x\forall yR(x,y)$ can be expressed as $UR = \Delta$. $R(a,b)$ is expressed as $(a,b) \in R$. So we have an open theory expressing first-order logic for monadic and binary predicates. $R$ being transitive is simply expressed as $RR \subset R$. But what about when we leave relations as in $S(x,y,z) = R(x,y) \& R(y,z)$ ? Although obviously we cannot define such relations in our calculus it would appear (check this) that every first-order sentence or monadic or binary relation over binary predicates can be defined in the calculus (sentences via equations). Also how would we write $\forall x(G(x,x) \rightarrow \exists yH(y,x))$ which is equivalent to $\forall x\exists y(\neg G(x,x)\vee H(y,x))$ ? Maybe $((G\cap\Delta)^c \cup H^{-1})U \cap \Delta = \Delta$ ?

In Leibniz's Non inelegans specimen there are certainly definitions which employ $\exists$. The containment relation (let us write it $A\leq B$) is defined (Def. 3) as 

\[ A \leq B \equiv \exists N(B = A\oplus N)\]

But consider a general situation in which we have a defined predicate $P(x_1,...,x_n) \equiv \exists y_1...y_n\phi(x_1,...,x_n,y_1,...,y_n)$. Then there are situations in which  a $\psi$ involving occurrences of $P$ can be transformed into an equivalent (or rather stronger) sentence of the form

\[\forall z_1.....z_m\psi'(z_1,...,z_m)\]

in which $P$ does not occur, being replaced by $\phi(x_1,....x_n,y_1,....y_n)$ where the $y_i$ occur among the $z_i$.  For instance using Skolemization or constructivist techniques. Perhaps this fragment of Leibniz could be expressed in open logic. Transitivity of inclusions might be expressed as

\[\forall N,M((B = A \oplus N) \& (C = B \oplus M) \rightarrow C = A \oplus N \oplus M) \] Maybe Aristotle's ekthesis had to do with producing universal constructive sentences which are stronger than the sentence to be proven. Open formulas (unsaturated lekta) are problematic (and they not just universally quantified in disguise ?). An important task is to reformulate the axioms and rules of modern logic to deal only in closed formulas (sentences).

As for metalogic or metamathematics we must never forget that all results are themselves necessarily formalizable within certain recursive-axiomatic systems (including the very same system as the object system). Thus metalogic and metamathematics is just the study of formal reflections of systems into each other as well as self-reflection.  However knowledge and computation in recursive-axiomatic systems presupposes always a logical system at least as strong as monadic second-order logic. 

Hume's Treatise contains the following logical observations (when discussing causality): from the fact that every husband has a wife it does not follow that every man has a wife. Let $M(x,y)$ be the marriage (husband-wife) relation between a man $x$ and woman $y$. Then $Husband(a) \equiv \exists x M(a,x)$ and $Wife(a) \equiv \exists y M(y,a)$. Certainly $\forall x Husband(x) \rightarrow \exists y M(x,y)$ and $\forall x Wife(x) \rightarrow \exists y M(y,x)$. But it does not follow that $\forall x \exists y M(x,y)$.

Addendum on Aristotle:

We should examine the logic in Book V of Euclid which is supposed to be a presentation of Eudoxus' general theory of analogy. There are quaternary predicates involved $A(a,b,c,d)$  (expressing that $a$ is to $b$ as $c$ is to $d$) which have purely universal definitions. How much of Book V could be derived without $\exists$-rules ? 

What about monadic second-order logic ? Is this Aristotle's metalogic in the Analytics ? For instance what is the enunciation of Barbara (ignoring the existence condition) but

\[  \forall P,Q,R (\forall x(Px \rightarrow Qx) \& \forall x(Qx \rightarrow Rx) \rightarrow \forall x(Px \rightarrow Rx))  \]

How can this logic represent the logic of relations and multiple generality (we already know Prawitz's answer for full-second order logic representing first-order existential quantification) ?  That is, could we argue that ancient logic dealt with multiple generality through some kind of second-order monadic logic (perhaps with some basic binary relations) ? 

Or else Aristotle could have worked with the classical equivalence between $\exists$ and $\sim\forall\sim$.  

That is with natural deduction for classical predicate logic but without the rules for $\exists$. Instead use is made of the derivable Hilbertian axiom-schemes together with modus ponens (that is the simplest way to transform a proof using $\exists$-rules into one without them: $\phi(a) \rightarrow \exists x\phi(x)$ and \[\forall x(\phi(x) \rightarrow A) \rightarrow (\exists x\phi(x) \rightarrow A)\] where $x$ is not free in $A$. To prove this one can use the contrapositive of \[(\forall x\phi(x) \vee A) \rightarrow \forall x(\phi(x) \vee A)\]

For instance from the definition $Gxy \equiv \exists z(Rxz \& Rzy)$ and axiom $\forall x\exists y Rxy$ to derive $\forall x\exists y Gxy$, that is, show that \[ \forall x \sim \forall y \sim Gxy \] With Galen's hypothetical syllogism and the logic of the Topics and the proper theory of negation and conversion Aristotle had the full power of classical first-order logic - but we must deal with the problem of nested quantifiers vs.  prenex normal form.