After recognising explicit and implicit quantifiers, we now apply them to programming statements. Arrays and loops naturally create finite universes of discourse, such as index sets $\{1,2,\ldots,20\}$. A universal quantifier describes a property of every array entry, while an existential quantifier describes at least one entry with a property. In this lesson, quantifiers in programming statements will translate array properties into precise logical form. :::definition[Quantified Programming Statement] A quantified programming statement is a logical statement involving arrays, loops, or indexed data that can be written using quantifiers. A universal quantifier is used when a property holds for all entries. An existential quantifier is used when a property holds for at least one entry. ::: :::example[One-Dimensional Pascal Array] Let $n$ be an integer variable and let $A$ be an array $$\begin{equation*} A[1],A[2],\ldots,A[20]. \end{equation*}$$ Suppose the Pascal segment is $$\begin{equation*} \text{For }n:=1\text{ to }20\text{ do }A[n]:=n*n-n. \end{equation*}$$ Then $$\begin{equation*} A[n]=n^2-n. \end{equation*}$$ The universe of discourse for $n$ is $\{1,2,\ldots,20\}$. ::: :::definition[Nonnegative Array Entries] For the array $A[n]=n^2-n$ with $n\in\{1,2,\ldots,20\}$, the statement “all entries of $A$ are nonnegative” is written as $$\begin{equation*} \forall n(A[n]\geq 0). \end{equation*}$$ Since $A[n]=n(n-1)$ and $n\geq 1$, every entry is nonnegative. ::: :::definition[Largest Array Entry] For the same array, the statement “$A[20]$ is larger than every preceding entry” is written as $$\begin{equation*} \forall n[(1\leq n\leq 19)\to(A[n]<A[20])]. \end{equation*}$$ The restriction $1\leq n\leq 19$ is necessary because “preceding entry” excludes the index $20$. ::: :::definition[Consecutive Entries with a Doubling Relation] The statement “there exist two consecutive entries such that the latter is twice the former” is written as $$\begin{equation*} \exists n(A[n+1]=2A[n]). \end{equation*}$$ Here the universe for $n$ must be restricted to $\{1,2,\ldots,19\}$ so that $n+1$ is a valid array index. ::: :::definition[Strictly Ascending Array Entries] The statement “the entries of $A$ are in strictly ascending order” is written as $$\begin{equation*} \forall n[(1\leq n\leq 19)\to(A[n]<A[n+1])]. \end{equation*}$$ This compares each entry only with its next valid neighbour. ::: An array gives a finite universe, so each quantified statement becomes a definite collection of index checks. Choose a property and inspect the entries or neighboring entries that must be tested. A universal statement passes only when every required index check succeeds, while an existential statement passes as soon as one valid index works. This is especially important when a formula contains $n+1$, because the last valid index for $n$ may change. :::scientific-preview[Array Quantifier Table] ::: :::definition[Distinct Array Entries] The statement “all entries of $A$ are distinct” is written as $$\begin{equation*} \forall m\forall n[(m\neq n)\to(A[m]\neq A[n])]. \end{equation*}$$ Equivalently, it may be written as $$\begin{equation*} \forall m\forall n[(m<n)\to(A[m]\neq A[n])]. \end{equation*}$$ The second form avoids checking each unordered pair twice. ::: :::solved-problem Let $A$ be the two-dimensional array with $A[m,n]=m+3n$, where $1\leq m\leq 10$ and $1\leq n\leq 20$. Write and verify the statement that all entries are positive. ::: :::solution Given that $A[m,n]=m+3n$, where $1\leq m\leq 10$ and $1\leq n\leq 20$. The statement that all entries are positive is $$\begin{equation*} \forall m\forall n(A[m,n]>0). \end{equation*}$$ Since $m\geq 1$ and $n\geq 1$, we have $$\begin{equation*} m+3n\geq 1+3=4. \end{equation*}$$ Therefore $A[m,n]>0$ for every valid pair $(m,n)$. Hence the statement is true. ::: :::solved-problem For $A[m,n]=m+3n$, where $1\leq m\leq 10$ and $1\leq n\leq 20$, write and verify that the entries in every row are strictly ascending. ::: :::solution Given that $A[m,n]=m+3n$. The entries in every row are in strictly ascending order when $$\begin{equation*} \forall m\forall n[(1\leq n\leq 19)\to(A[m,n]<A[m,n+1])]. \end{equation*}$$ Now $$\begin{align*} A[m,n+1]&=m+3(n+1)\\ &=m+3n+3. \end{align*}$$ Since $m+3n<m+3n+3$, we get $A[m,n]<A[m,n+1]$. Hence the entries in each row are strictly ascending. ::: In programming translations, the universe is not only mathematical; it is also determined by valid indices. A statement involving $A[n+1]$ must not allow $n=20$ if the array ends at $20$. Similarly, a two-dimensional array requires separate index restrictions for rows and columns. Many incorrect translations come from using a correct quantifier with an invalid index range. :::exercise For the array $A[m,n]=m+3n$, where $1\leq m\leq 10$ and $1\leq n\leq 20$, write each statement symbolically: all entries are positive; all entries are positive and at most $70$; some entries exceed $60$; rows are strictly ascending; columns are strictly ascending. ::: :::answer The symbolic forms are $\forall m\forall n(A[m,n]>0)$, $\forall m\forall n[(A[m,n]>0)\land(A[m,n]\leq 70)]$, $\exists m\exists n(A[m,n]>60)$, $\forall m\forall n[(1\leq n\leq 19)\to(A[m,n]<A[m,n+1])]$, and $\forall m\forall n[(1\leq m\leq 9)\to(A[m,n]<A[m+1,n])]$. ::: :::faq[Frequently Asked Questions] Q: Why are programming quantifiers often finite? A: Array indices and loop ranges usually form finite universes. Q: Why must $n+1$ be checked? A: The expression $A[n+1]$ is valid only when $n+1$ is within the array bounds. Q: What is the difference between all entries and some entries? A: “All” uses $\forall$, while “some” uses $\exists$. ::: :::call-to-action[Translate Program Properties] subtitle: Practise writing quantified array statements before studying formal truth conditions for quantifiers. button: Next Lesson | /discrete-mathematics/mathematical-logic/predicates-and-quantifiers/truth-conditions-for-quantified-statements button-ghost: Previous Lesson | /discrete-mathematics/mathematical-logic/predicates-and-quantifiers/implicit-quantification-and-universe-dependence :::