I want to express the following in a computationally less-loaded way:

$\forall i < A [F(i) = B \implies H(i) = C]$

Taking some shortcuts, this says:

For all $i$, if $F(i) = B$, then $H(i)$ should equal $C$.

Considering the following fact, this is making us check too much: $\forall i, j < A [F(i) = F(j) \implies H(i) = H(j)]$. Hence, a computationally more concise way to say the same is:

For the first $i$ satisfying $F(i) = B$, $H(i)$ should equal $C$.

However, the best I can think of for this is very heavy in notation:

$\left|\{i<A:F(i)=B\}\right| >0 \implies H(\min{\{i<A:F(i)=B\}})=C$

Is there a best-of-both-worlds solution to this?

  • $\begingroup$ Does $i$ range over a finite or infinite set? $\endgroup$
    – R. Burton
    Commented Aug 30, 2019 at 22:59
  • $\begingroup$ @R.Burton Finite set. Precisely, $i$ is from $\mathbb{N}_0$. It is finite for being limited by $A$ from above. $\endgroup$ Commented Aug 30, 2019 at 23:58

1 Answer 1


The formula $\forall i<A.F(i)=B\implies H(i)=C$ states that for every instance of $i<A$, if $F(i)=B$ then $H(i)=C$. It is not sufficient to check only the least $i$ such that $F(i)=B$.

Unless $F$ is stated to be a bijection, it may be the case that for the least $i<A$ such that $F(i)=B$, $H(i)=C$, and yet for some $i<j<A$, $F(j)=B$ and $H(j)\ne C$.

For example, say that $A=3$, $B=1$ and $C=4$. If $F(0)=0$, $F(1)=1$, and $F(2)=1$, and $H(0)=0$, $H(1)=4$, and $H(2)=1$, then your formula...

$$\left\vert\{i<A\mid F(i)=B\}\right\vert>0\implies H\left(\min\{i<A\mid F(i)=B\}\right)=C$$

...holds, since both the consequent and antecedent are true (1 is th minimum, and $F(1)=1$ and $H(1)=4$). However, the orignal formula...

$$\forall i<A.F(i)=B\implies H(i)=C$$

...does not, since $F(2)=1$ and $H(2)=1\ne4$.

As far as notation goes, the original formula is about as concise as it can possibly be.

As for making the evaluation of the original formula more computation friendly, this is what I would do:

Let $G(i)=\begin{cases}1&F(i)=B\\0&\text{otherwise}\end{cases}$ and $K(i)=\begin{cases}1&F(i)=B\land H(i)=C\\0&\text{otherwise}\end{cases}$


$$\forall i<A.F(i)=B\implies H(i)=C\iff i<A\implies G(i)-K(i)=0$$

This works best if you treat $G$ and $K$ as 'vectors' - then $G-K$ is the zero vector. In the above example where $B=1$ and $C=4$, you get $G=(0,1,1)$ and $K=(0,1,0)$.

$$(0,1,1)-(0,1,0)=(0,0,1)\ne(0,0,0),\qquad\therefore \neg(\forall i<A.F(i)=B\implies H(i)=C)$$

By this method, the formula reduces to...

$$\forall i<A.F(i)=B\implies H(i)=C\iff G-K=\mathbf{0}$$

I can't guarantee that there isn't a more computationally efficinet method of checking your formula (there almost certainly is), but this works well enough. If your doing this by hand, you can simplify the process to:

1) write out $F$ in one row

2) write $H$ in a row below it

3) every time you see $B$ in the top row, draw a box around it and the entry below it.

4) continue until you hit a box whose lower entry is not $C$ or you reach the end of the list.


OP has clarified that the function $F$ satisfies $\forall i,j<A.F(i)=F(j)\implies H(i)=H(j)$

That being the case, we need only check that if there is at least one $i$ such that $F(i)=B$, then $H(i)=C$. As a first order formula, this is written...

$$\exists i<A.F(i)=B\implies\exists i<A.F(i)=B\land H(i)=C$$

As for an algorithm to evaluate the formula, I'm not sure whether it is more or less efficient to parse $F$ and $H$ through to the first $i$ satisfying the formula, or to treat them as vectors, as above. It may depend on the value of $A$. In either case, the original method can be modified to work with the new formula.

Let $G(i)=\begin{cases}1&F(i)=B\\0&\text{otherwise}\end{cases}$ and $K(i)=\begin{cases}1&F(i)=B\land H(i)=C\\0&\text{otherwise}\end{cases}$.


$$\exists i<A.F(i)=B\land H(i)=C\iff G=\mathbf{0}\lor K(i)\ne\mathbf{0}$$

By hand...

1) write out $F$ in one row

2) write $H$ in a row below it

3) find the first instance of $B$ in the top row - your formula holds iff the entry below it is $C$ or there are no $B$

  • $\begingroup$ I see that a lot of effort has been put here, but unfortunately, I have to say that there must have been a misunderstanding. The statement $\forall i < A [F(i) = B \implies H(i) = C]$ combined with the fact $\forall i, j < A [F(i) = F(j) \implies H(i) = H(j)]$ is to be simplified. Maybe I should have used something stronger than "Considering the fact"; I thought it'd fit the bill. Your example is not compliant with the fact I'm asserting, since $F(1) = F(2)$ but $H(1) \ne H(2)$. Hence, it is not a contradictory counterexample. I am sorry. $\endgroup$ Commented Sep 3, 2019 at 13:01
  • $\begingroup$ @ThoAppelsin It's alright. I've edited the answer, hopefully this helps. $\endgroup$
    – R. Burton
    Commented Sep 3, 2019 at 15:03
  • $\begingroup$ Thank you for your continual effort to help. If I am understanding this correctly, your solution requires at least one $i$ to exist satisfying $F(i) = B \wedge H(i) = C$ to be true. There are further cases in which the original formula is true, namely, $\forall i < A. F(i) \ne B$ (adopting your notation). This is why I used an implication on the latest formula in my question, and not just the consequent of it. This does suggest that I could change update that last formula in my question as $\exists i<A. F(i)=B \implies \exists i<A. F(i) = B \wedge H(i) = C$, which is at least easier to read. $\endgroup$ Commented Sep 3, 2019 at 15:41
  • $\begingroup$ @ThoAppelsin You're right. I didn't think about the case where $\forall i<A. F(i)\ne B$. Now that you mention, your second formula guarantees that either there is at least one $i$ such that $F(i)=B\land H(i)=C$, or $\forall i<A.F(i)\ne B$. $\endgroup$
    – R. Burton
    Commented Sep 3, 2019 at 16:56

You must log in to answer this question.

Not the answer you're looking for? Browse other questions tagged .