In his discussions of the various readings of modal propositions, Ibn Sīnā’s focus is mostly on a distinction which was later labelled the distinction between descriptional (waṣfī) and substantial (ḏātī) readings of a modal proposition. Given that for Ibn Sīnā all categorical propositions are either implicitly or explicitly modal, the substantial–descriptional distinction is in some sense applicable to the readings of all categorical propositions. This distinction is based on how (i.e., under which conditions) the predicate of a categorical proposition is true of its subject. According to the substantial reading, the predicate is true of the subject (perhaps with a certain alethic or temporal modality) as long as the substance of the subject exists. On the other hand, according to the descriptional reading, the predicate is true of the subject (again, perhaps with a certain modality) as long as the substance of the subject is truly described by the subject. To be clearer, consider the following proposition: (1) Every S is P. The difference between the substantial and descriptional readings of (1) can be articulated as follows: Substantial Reading of (1): Every S, as long as it exists, is P. Descriptional Reading of (1): Every S, as long as it is S, is P. It is in principle possible that a proposition is true on one of these readings and false on the other. It is only the context which determines how a proposition must be read to be true. To give an example, consider the following proposition: (2) Every bachelor is unmarried. The substantial and descriptional readings of (2) are respectively as follows: (3) Every bachelor, as long as he exists, is unmarried. (4) Every bachelor, as long as he is bachelor, is unmarried. These two propositions have different truth values. Contrary to (3)—which is false—(4) is true. This is because a bachelor is unmarried only insofar as he is described as a bachelor. So (4) is true. By contrast, it is in principle possible for a person who is a bachelor in some period(s) of time to be married in some other period(s) of time; this is so at least if we assume that ‘as long as’ has a temporal meaning. In other words, it is not necessary for such a person to be always unmarried. The mere existence of the substance of this person does not guarantee his being unmarried. Thus (3) is false. There are, however, other propositions that are true on the substantial reading. For example, consider the following proposition: (5) Every human is animal. The predicate Animal is true of every human as long as s/he exists. Put otherwise, what makes it true to say that every human is animal is the mere existence of human substances. This means that not only the descriptional but also the substantial reading of (5) is true. Indeed, since every human exists if and only if s/he is human, the substantial and descriptional readings of (5) express one and the same fact. As Ibn Sīnā himself insists, he is the first logician to have focused on the above distinction and pondered on its fruitfulness for removing some difficulties with Aristotle’s syllogistic. Since the distinction plays a crucial role in Ibn Sīnā’s syllogistic, it is discussed in several places in his logical oeuvre. Moreover, the distinction was subject to continually heated discussions in Arabic logic after Ibn Sīnā. For instance, the distinction was accepted by Rāzī and Khūnaǧī, on the one hand, and was seen as redundant by Ibn Rushd. The substantial sense of propositions corresponds to what is called the ‘divided’ sense of propositions in the Latin tradition. However, although the descriptional sense of propositions is plays an important role in Arabic syllogistic, it has no widely discussed counterpart in the Latin tradition. These observations strongly suggest that a comprehensive picture of Arabic syllogistic from Ibn Sīnā onwards cannot be achieved unless we have a clear logical analysis of the aforementioned distinction. An effective and popular strategy for providing such an analysis is to look at the different readings of a proposition through the lens of modern formal logic. Therefore, it is important to find out which formal language has the best capacity to capture various aspects of this distinction and the insights behind it. In the literature, several attempts have been made to formalize the different readings of propositions in the languages of classical predicate or temporal logics. In this chapter, we put forward an alternative based on Martin-Löf’s constructive type theory (CTT). Compared to its rivals, our analysis is more faithful to the grammatical subject-predicate structure of propositions and can better reflect the morphological features of the verbs (and descriptions) that extend time to intervals (or spans of times). It is worth noting that our focus will mostly be on the analysis of the descriptional reading of propositions (which can also be called ‘the descriptional propositions’ for the sake of brevity).