I am going through some lecture slides and have come to something that I do not understand. I get the general idea of what he is trying to do but I am not sure how the propositions show this.
What do these propositions show and if they were to be translated into English, what would they say exactly?
The precondition states that the element $e$ is greater than or equal to the first element in the list and less than or equal to the last element. Presumably, the intention is to state that $e$ is contained in the array, even though this is not the strict meaning of the precondition. A more precise formulation of this would be "$\exists i\in\{1,\ldots,N\}$, such that $a[i]=e$".
The postcondition states that $i$ is some index in $1,\ldots,N$, such that $a[i]=e$; in other words, that the $i$'th element of the array is $e$.
The purpose of such pre- and postconditions is to prove correctness of the code in between. That is, we assume that the precondition is true and show that execution of the lines of code imply that the postconditions must be true after terminating. In this specific example, the conditions translate into something along the lines of: "If $e$ is contained in the array $a[1,\ldots,N]$, then the given code finds its index $i$".