I. INTRODUCTION
As pointed out by Sundholm,Footnote 1 since the work of Frege, quantifiers are intended to range over the universe of all objects. Hence, since all quantifications concern the same domain, there seems to be no practical or theoretical need to include explicit information about the domain of quantification in the quantifier notation. In this setting, the role of the predicate is to pick out, from an all encompassing universe, the subset of objects appropriate for analysis of the sentence at hand. Such a strategy has the side-effect that it liberates the logical form from the subject-predicate structure, explicitly imposed on propositions in the Aristotelian tradition.
However, the Fregean move is utterly unfaithful to the corresponding natural language expressions. It seems natural, on one hand, to attach to every, a noun, such as every student and every philosopher, but, on the other hand, if someone asserts that
it looks like he were picking, from the restricted universe of elephants, those that are small, and not, from the universal domain of objects, those objects that are small and elephants. It may well be that the elephant in question is small (for an elephant), but even small elephants are big creatures in the animal kingdom.
Crubellier, in a new French translation of the Analytica Footnote 2 proposes, to translate Aristotle's formulation of universal expressions with a paraphrase like
Crubellier's translation strongly suggests that the subject, restricts the predicate (to be small), to the domain of elephants.
Note that every and some always are attached to a noun. In a paper on the notion of number in Plato and Aristotle, CrubellierFootnote 3 points out that, for the ancient Greeks, a number is always attached to a noun: two apples, two flowers, etc. The pure number of the mathematicians is, according to Aristotle, an abstract presentation that achieves generality – e.g. two abbreviates two whatever objects. Perhaps, similarly, we should think of every as an abstraction from every apple, every flower, etc.
A crucial point in the type-theoretic formalization of the Aristotelian forms of propositions is the distinction drawn between two forms of judgement that both formalize natural language sentences of the form

namely:

where, in the first case, B is a set, and, in the second case, a : A and B(x) is a proposition under the assumption that x is an element of the set A.
This distinction is linked to Lorenz and Mittelstrass’ beautiful analysis of Plato's Cratylus.Footnote 4 In this paper, the authors point out two different basic acts of predication, viz., naming (όνομάζειν) and stating (λέγειν). The first amounts to the act of subsuming one individual under a concept and the latter establishes a true proposition. Naming is about correctness, i.e., one individual reveals the concept it instantiates if the naming is correct. Stating is about the truth of the proposition that results from the second kind of predication act. If the predicate indeed applies to the individual, the associated proposition is true.
In the context of our own reconstruction, naming corresponds to the assertion that an individual is an element of a given set, or, which amounts to the same, that an individual falls under a given concept, that is, it involves judgements of the form a : B; and stating corresponds to asserting the truth of a proposition, i.e., to asserting B(a) : true.
The conventional type-theoretic notation for quantifiers stresses the two-term structure of the Aristotelian forms of propositions:

In the example above, S ≡ {elephant}, and P(x) ≡ “x is small”, where the variable x stands for an elephant.Footnote 5 This clearly reveals that S and P have different status.
Aristotle did not apply his logical analysis of quantification either to relations or equality, but Ibn Sīnā considered the latter, as well as propositions and syllogisms where quantification combines via equality with singular terms.
These reflections provide the basis for his theory or numbers that is based on the interplay between One and the Many.Footnote 6 Certainly, as pointed out by Hasnawi,Footnote 7 Aristotle discusses the case of relations and unity in many places of his work, such as in the books Δ and I of his Metaphysics.Footnote 8 Moreover, Ibn Sīnā’s classification of unity, which we discuss in the present paper, is Aristotelian.
However, and this is the main claim of our paper, it is Ibn Sīnā’s quantification of the predicate that allows him to introduce these distinctions into the object language and prefigure, perhaps for the first time, a logic with an equality predicate.
II. QUANTIFICATION OF THE PREDICATE
Many logicians of the middle-ages avoided relations, particularly in the context of building syllogisms. Thus, syllogisms were based on monadic predicates and the logic of monadic predicates does not naturally lead to repeated or nested quantification.
However, Ibn Sīnā devotes two chapters of al-ʿIbāra to the quantification of the predicate. Al-ʿIbāra is the third book of the logical collection of his philosophical encyclopaedia entitled al-Shifāʾ (the Cure). It is in these texts that Ibn Sīnā shows that his approach to quantification is very close to Aristotle's analysis of relations, mentioned above, though Ibn Sīnā’s own understanding of quantification allows him both to study double quantification and defend its study from detractors. This has been made apparent in the excellent paper of HasnawiFootnote 9 on Ibn Sīnā’s double quantification – a paper that, by the way, contains an English translation of these two chapters, the first in any language.
Indeed, one of the mediaeval objections against the quantification of the predicate is that, because of the possibility of a negation in the scope of the second quantifier, propositions could not anymore said to be either affirmative or negative.Footnote 10 For example, does some man is not every animal express an affirmative or a negative proposition? Hasnawi sums up Ibn Sīnā’s position very well:
Avicenna upholds here a radical point of view: according to him the predicate in double quantified propositions is constituted by the quantifier plus the initial predicate, which form together a unit. So a proposition which has the form of a normal affirmative proposition will keep this quality even though a negative quantifier has been prefixed to its predicate. The quantifier of the predicate is conceived of as a predicate-forming operator on predicates: it generates new predicates from previous ones by attaching a quantifier to them.Footnote 11
It very much looks as if Ibn Sīnā thinks of quantification of the second term as building a new predicate, and this deviates from the normal use of quantification. Let us once more quote Hasnawi, who this time quotes Ibn Sīnā himself:
The same semantic core, namely that a clause added to a proposition or to a part of it, makes the proposition deviate from its normal functioning, is present in the description Avicenna gives of propositions with a quantified predicate as munḥarifāt: “If you try then to add a quantifier, the proposition will be deviate (inḥarafat): the predicate will no longer be a predicate, but rather it will become part of the predicate. The consideration of the truth will thus be transferred to the relation which occurs between this sum and the subject. That is why these propositions were called deviating” (al-ʿIbāra: 64,17–65,1).Footnote 12
Before formalizing Ibn Sīnā’s quantified predicates, recall that the subject term S in the Aristotelian forms of propositions
can be taken in two different ways when formalized in type theory: either as a set, as above, or as a subset, of a larger domain of quantification, the universe of discourse D, i.e., as a propositional function, or a predicate, in the logical sense of the word, on the set D. For example, the proposition some white thing is round can be formalized using

Clearly, some S is P has to be formalized as (∃ x : D) S(x) & P(x) in this case. We introduce the following compact notation for the case when the subject term is taken as a subset of a larger universe of discourse:

where both S(x) and P(x) are propositions under the assumption that x is an element of the universe of discourse D. The symbol ⊃ stands for logical implication. This interpretation of quantification over a restricted domain is standard in modern predicate logic.Footnote 13
Using this notation, we can now make sense of Ibn Sīnā’s cryptic remark that “the predicate will no longer be a predicate, but rather it will become part of the predicate”. For example, consider the sentence every S is some P, or, which amounts to the same, every S is equal to some P, where P is a propositional function on S: we get the formalization

By substitution, P(x) is logically equivalent to (∃P(y))(x = y), whence “every S is some P” is logically equivalent to “every S is P”.Footnote 14
III. THE ONE AND EQUALITY
The discussions on the One and the Many are ubiquitous in the work of Ibn Sīnā, and they share the features of many Neo-Platonists who, quite often, attempt to combine the Platonic and Aristotelian Metaphysics. In fact these two notions set the basis for Ibn Sīnā’s theory of numbers. A salient sense of the notion of One is, according to our author, identity developed in the first chapter on Metaphysics in the Book of Science Footnote 15 and in the second chapter of third book of the Metaphysics of the Shifāʾ.Footnote 16 In this context, Ibn Sīnā distinguishes between
• One in nature: no aspect of multiplicity is involved, such as, God and the geometrical point.
• One in an aspect: this is said of specific things either
– according to essence, or
– per accidens.
The first sense of One, i.e., One in nature, is related to the unity of an object – even with the very concept of existence of an object. The second sense of One (by essence or per accidens) is the one that builds Ibn Sīnā’s theory of equality and that combines with his quantification of the predicate. It is crucial that the interaction between quantification of the predicate and equality can be applied to Ibn Sīnā’s own examples of syllogisms involving these notions. The investigation of this second sense of One will occupy the rest of this paper. We will interpret One in essence as dealing with equality, interpreted in type theory either as definitional equality, a ≡ b : A, or as propositional equality, (a = b) : true.
In his Autobiography our author claims that he has reconstructed all the inference steps of the Euclid's geometry. This certainly requires a profuse use of the logic of equality. On the topic of equality, Ibn Sīnā discusses transitivity of equality in Qiyās i.6: “Thus when you say C is equal to B and B is equal to D, so C is equal to D.”Footnote 17
There are quite a number of syllogisms in Ibn Sīnā’s work on logic involving equality and equivalence: they have not all been compiled yet, but let us analyze a few examples.
At Qiyās 472.15f we find:
Here Ibn Sīnā makes use of the substitution rule

where a and b are elements of a set A and P(x) is a predicate defined on the set A.
The syllogism discussed at Qiyās 488.10 could be read with equality too:
However, it is perhaps more natural to interpret the word is in these sentences as logical equivalence.
IV. ONE PER ACCIDENS
Ibn Sīnā distinguished six cases of unity per accidens:Footnote 18 unity by species, unity by genus, unity by accidental predicate, unity by relationship, unity in subject, and unity in number. In general, sentences expressing this form of unity have the form
Our analysis of this form of sentences will associate a (possibly higher order) schema S with the aspect A, and the interpretation of the sentence will be that the predicate applies equally to both a and b, i.e., the interpretation will be that S(a) and S(b) are both true.
This analysis holds good for the first four cases of unity per accidens, but, as we shall see, it breaks down for unity in subject and unity in number.
Let us first consider unity by species (al-wāḥid bi-al-nawʿ). An example due to Ibn Sīnā is given by
In this case, the schema is simply the predicate

where x ranges over some suitable domain, such as living being. That is, Zayd and Amr are one in the sense that both propositions SH(Zayd) and SH(Amr) are true. Put differently, Zayd and Amr are one by humanity is interpreted as Zayd and Amr are both human.
Next, let us consider unity by genus (al-wāḥid bi-al-jins). An example due to Ibn Sīnā is given by
Again, we pick living being as the universe of discourse L, and we interpret Human(x) and Horse(x) as predicates on L. In this case, the schema is of the second order as it takes a predicate X on L as argument:

The sentence is now interpreted in type theory as SA(Human) and SA(Horse) both being true.
Unity by accidental predicate (al-wāḥid bi-al-ʿaraḍ). An example due to Ibn Sīnā is given by
Here we take the universe of discourse to be substance, abbreviated S, and the schema is

where X is a predicate on S. If we view Snow(x) and Camphor(x) as predicates on S, it is clear that both propositions SW(Snow) and SW(Camphor) are true. Note that, in the formalization of unity by genus, the universe of discourse cannot be taken to be animal, as this would make the schema SA(X) vacuously true for any predicate X. Interestingly, the type-theoretic formalization is the same as for unity by genus. This is because the Aristotelian distinction between essential and accidental predicates pertains to semantics, or meaning, rather than to logical form. In type theory, a formal distinction is made between the universe of discourse (which always is a set) and predicates on this universe, but a distinction between essential and accidental predicates can only be done we have access to the definitions of the predicates involved: a predicate on a genus is essential if it is a mark,Footnote 19 of the definition of the genus, or a combination of such marks. In summary, the Aristotelian distinction between essential and accidental predicate holds good in type theory, but it is not visible in the logical form of the identity sentence – however it can be made visible in the so-called formation rules for the semantic elements of those sentences.
A particularly interesting kind of unity is unity by relationship (al-wāḥid bi-al-munāsaba). An example due to Ibn Sīnā is given by
We read this example as unity with respect to the relation is governed by. Let us introduce two universes of discourse, one for things governed, governees, abbreviated GE, e.g., cities and bodies, and one for governors, abbreviated GN, e.g., sovereigns and souls. We view City(x) and Body(x) as predicates on the set GE. In addition, we view Sovereign(x, y) as a dyadic predicate on a governee x and a governor y, so that Sovereign(x, y) means y is a sovereign of x. Similarly, Soul(x, y) means that y is the/a soul of x. Other formalizations are also possible, such as taking Sovereign and Soul to be functions, or restricting the first argument x to be an element of the subset of cities or bodies respectively. However, the formalization we have chosen is probably the simplest. The schema related to unity with respect to governance is given by

where X ranges over predicates on GE and Y ranges over dyadic predicates on GE and GN. The propositions SG(City, Sovereign) and SG(Body, Soul) come out as true under this interpretation.
Next we have unity in subject (al-wāḥid bi-al-mawḍuʿ). An example due to Ibn Sīnā is given by
Here we cannot fit the formalization into the general schema presented above. Instead we directly formalize this sentence as

where ⊂ ⊃ stands for bidirectional implication, the universe of discourse is substance, abbreviated S, and Sugar(x), White(x), and Soft(x) are predicates on the universe of discourse. That is, our interpretation is every substance that is sugar is white if and only if it is soft.
Finally, we have unity in number (al-wāḥid bi-al-ʿadad). It is important to recall here that Ibn Sīnā thought, as did Aristotle before him, that numbers are properties of terms – a claim that lost popularity after Frege's incisive objections in his Grundlagen der Arithmetik.Footnote 20 Be this as it may: it is natural to formalize a sentence such as
as the sets or subsets A and B admitting a bijection between them.
V. CONCLUSION
This paper suggests that Ibn Sīnā explored new paths of logic beyond the work of Aristotle, particularly so in relation to equality. As already mentioned in the introduction, Ibn Sīnā’s quantification of the predicate, rejected by Aristotle,Footnote 21 allows him to combine, perhaps for the first time, a logical analysis of quantification combined with a theory of equality.
A topic that deserves further study is Ibn Sīnā’s theory of the relation between equality and existence in the context of his overall philosophical view on mathematics, and particularly in the context of his theory of numbers.
Acknowledgements
The final form of the paper is due to discussions with Ahmad Hasnawi, who encouraged the first author to the exploration of the fascinating issues underlying the subject of the paper and who shared some wise commentaries on an early draft of the paper, the assistance of my colleague Michel Crubellier and the deep insights of Göran Sundholm during his visit at our university in Lille. We would like to record herewith our fond recollection of the learned interactions with all of them.
Dedication
The first author wishes to dedicate the paper to his colleague and friend Michel Crubellier who just started the exercise of his (administrative) retirement and with whom the first author engaged in many fascinating discussions on Aristotle, Arabic philosophy and beyond.