# LTL globally implies

I have got confused in undressing the informal definition of LTL below: $$G(\phi \Longrightarrow\psi)\Longrightarrow(G\phi \Longrightarrow G\psi)$$

1. in many literatures I have seen implies is said as replies like for LHS we can say Always/Globally $\psi$ replies to $\phi$. is it correct?
2. Does the LHS implies the RHS if so what is the informal interpretation of the formula? (Alway $\psi$ replies to Always $\phi$) replies to (Always $\psi$ replies to $\phi$)

You seem to be pretty confused, so let's sort some things out. First, it's "implies", not "replies". That is, the formula $\phi\implies \psi$ means that if $\phi$ holds, then $\psi$ holds.

To be more precise, the formula $\phi\implies \psi$ is true in one of two cases: either $\phi$ is false, in which case we say that the implication is vacuously true, or if both $\phi$ and $\psi$ are true.

Now, in LTL, the operator $G$ means that something holds in every position in the computation. Let's examine the two "sides" of your formula with respect to that.

The formula $G(\phi\implies \psi)$ means that in every point of the computation, the formula $\phi\implies \psi$ is true, in the form mentioned above.

The formula $G\phi\implies G\psi$ means, as above, that either $G\phi$ is false, or both $G\phi$ and $G\psi$ is true.

Now it is fairly easy to see why the formula you have is true: if $G(\phi\implies \psi)$ is true, then, if $G\phi$ is true, then $\phi$ is true in every position, but then according to the LHS we have that $\psi$ is also true in every position, so $G\phi\implies G\psi$ is true.

For your second question, an informal way to think about this (there are many others, probably) is this: if you require that whenever $\phi$ holds, then $\psi$ must also hold, then in particular, if $\phi$ is always true, then $\psi$ is also always true.