Is a loop a quantifier? Somewhere I read that the universal quantifier, i.e. $\forall p$, could be interpreted as a sequence of conjunctions of propositions, elements or variables: $p_1\land p_2 \land... \land p_n... $
The same could be said of the existential quantifier, it could be interpreted a sequence of disjunctions.
But, a loop, used in computer language, (i.e. for, while) is a sequence of conditions. 
So, can I interpret a loop, used in computer language, as a kind of quantifier? For example, could ''while (i!=10)...''  be translated as ''$\forall i(i\in \Bbb N,(i \neq 10) \to P(i))$''? If not, why?
 A: In the following sense it can be formalized using second order quantification.
In the Situation Calculus (a theory of action), while is defined as a complex action as follows:
$ while\ \phi\ do\ \delta\ endWhile \stackrel{def}{=} [\phi?; \delta]^*;\neg \phi?$
where $\delta^*$ means doing $\delta$ zero or more times and is defined as follows:
\begin{align*}
 Do(\delta&^*,s,s')\stackrel{def}{=}\\
 &(\forall P).\{(\forall s_1)P(s_1,s_1)\land(\forall s_1,s_2,s_3)[Do(\delta,s_1,s_2)\land P(s_2,s_3)\supset P(s_1,s_3)]\}\supset P(s,s'). 
\end{align*}
Which involves second order quantification. 
For all definitions and more details you can see chapter 6 of the book Knowledge in Action (2001). Here I give some of the definitions.
A situation is a finite sequence of actions. $do(a,s)$ is the situation obtained from executing action $a$ in situation $s$. $Do(\delta,s,s')$ means "it is possible to reach situation $s'$ from situation $s$ by executing a sequence of actions specified by $\delta$". 


*

*Primitive actions:
$Do(a,s,s')\stackrel{def}{=}Poss(a[s],s)\land s'=do(a[s],s)$.

*Test actions:
$Do(\phi?,s,s')\stackrel{def}{=}\phi[s]\land s'=s$.

*Sequence:
$Do(\delta_1;\delta_2,s,s')\stackrel{def}{=}(\exists s'').Do(\delta_1,s,s'')\land Do(\delta_2,s'',s')$.


$-------------$
More on Situation Calculus:
The language of the Situation Calculus is a many-sorted first order language (with some second-order elements). There are three sorts: action for actions, situation for situations, and object for everything else. A distinguished constant $S_0$ represents the initial situation, and a distinguished function symbol $do:action\times situation\rightarrow situation$ represents the execution of an action. A situation is a finite sequence of actions starting from the initial situation. A binary predicate symbol $\sqsubset$ defines an ordering relation on situations.
A fluent is a fact whose truth value may vary from situation to situation; it is a predicate that takes a situation as the final argument (e.x. $holding(x,s)$, meaning "the agent is holding object $x$ in situation $s$"). A distinguished predicate $Poss:action\times situation$ denotes it is possible to execute an action in a situation. 
The expression $Do(\delta,s,s')$ (defined above) is a shorthand for a formula of SitCalc. It is used to define complex actions.
A: Some versions of $\forall$ can be translated into loops and some cannot.  Specifically, when the domain of the quantifier is constructively isomorphic to natural numbers, and when argument to the quantifier is translatable into a decision procedure, then a general translation is possible.  Examples:
$$\forall x \in \mathbb N ~:~ 2|x \lor 2|(x + 1)$$
The domain of the loop is natural numbers, and divisibility can be written as a decision procedure, so this is just:
for i = 0; true; i++
  if (i % 2) == 0 return true
  if ((i + 1) % 2 == 0 return true

On the other hand:
$$\forall x \in \mathbb R ~:~ f(x) \ne x$$
Can't be expressed as a loop since real numbers are not isomorphic to natural numbers.  You can't loop through real numbers.  Also
$$\forall x \in \mathbb N ~:~ P \text{ is a program that converges on input } x$$
Arguably might not be completely translatable into a loop since you can't actually write a decision procedure that asserts divergence.  Also, some logics just have different rules for quantification that don't make any assumptions about the domain at all, such as
$$\forall x ~:~ (Px \to \exists y ~:~ Py)$$
is a provable in natural deduction because of its $\forall$ rules, despite not have any obvious translation as a decision procedure.
