Motivation for Dependent Type By the Curry-Howard Isomorphism we view propositions (or theorems if true/inhabited) as types.

But take the type $\mathbb{N} \implies \mathbb{N} \implies \mathbb{N} $.

We have as witnesses to this type (i.e., proofs of this theorem) both

f x y = x + y
f x y = x * y


Yet they "attest to the validity" of two very different programs. Is this the motivation for increasing the expressivity of a type system, as we see with dependent types? How would the type signature above be spoken in English - "for all naturals, x and y, it is true for all naturals"...?
Actually, the motivation for introducing dependent types goes in the opposite direction! Curry had noticed that there was a direct correspondence between typed terms in the $SK$ calculus and proofs in (minimal implicational) propositional logic, but there was no programing language known to correspond in such a way to predicate logic.

Indeed, introducing $\Pi$ types are necessary to model propositions of the form $\forall x.P$, which clearly do not admit representation as a simple type $A\rightarrow B$. (Actually, one can imagine a "forgetful" translation, where $A$ is the domain of $x$, and $B$ is the domain of "proofs of $P$", and in this way one can construct something very similar to certain forms of realizability, but this is clearly not an isomorphism.)

In summary, there is an isomorphism between functions $\mathbb{N}\rightarrow\mathbb{N}\rightarrow\mathbb{N}$ in the simply typed $\lambda$-calculus and proofs of $N\Rightarrow N\Rightarrow N$ in minimal logic, in the context $N,N\Rightarrow N$.

It is clear, however, that most programing languages have more than the STLC to define functions, and that there is more reason to care about the operational behavior of programs than that of (most) proofs.

It makes sense to use dependent types to explore these distinctions, as well as more subtle notions of types to distinguish between "computationally relevant" things and "computationally irrelevant" ones (e.g. in Coq, the $\mathrm{Prop}$ vs $\mathrm{Set}$ distinction).

But these were not the original motivation for dependent types.



As a direct answer to your question, the "statement" $\mathbb{N}\Rightarrow\mathbb{N}\Rightarrow\mathbb{N}$ should be read in English as something like


  For every pair of natural numbers, there is a natural number.


And that's it! The fact that $\lambda x y. x+y$ and $\lambda x y. x\cdot y$ are two very computationally meaningful proofs of that statement does not factor at all into the statement as it stands.