Predicate Logic to Natural Language

Question

Is my translation correct?

$P(x)$ - "$x$ is a program"
$F(x) $- "$x$ is a function"
$I(x,y)$ - "$x$ invokes y"

$ \forall x (P(x) \rightarrow \forall y (F(y) \rightarrow \neg I (x, y)))$

"For every $x$, if $x$ is a program then
For every $y$, if $y$ is a function then
$x$ does not invoke $y$"

$ \therefore $ "Every program does not invoke a function"

Answer 1

Yes... but to make it a little more clear, I would say:

"Every program does not invoke any function"

Another option is:

"No program invokes a function"

or:

"Programs never invoke functions"