Definition of liveness property in model checking
I'm not sure where the particular liveness definition you wrote comes from, but the definition given in Defining Liveness (Schneider, Alpern, 1985) is as follows.
A property $P$ is a liveness property if and only if:
$$
\forall \alpha \in S^* : (\exists \beta \in S^\omega : \alpha\beta \vDash P)
$$
where $S^*$ is the set of all partial executions and $S^\omega$ is the set of all infinite executions.
This definition captures the intuition that the &quot;good thing&quot; (the &quot;something good&quot; that you mentioned) specified by a liveness property can always occur in the future. That is, no matter the finite prefix $\alpha$ you choose, you can always find an infinite suffix $\beta$ to extend it with that will satisfy a liveness property $P$. I am assuming that the $\leq$ symbol in the definition you gave is used to express a prefix relationship between traces, which makes it analogous to the definition from the paper.
You might make an argument for defining liveness in some alternative way. Indeed, two slightly different characterizations of liveness are given in that same paper (see uniform liveness and absolute liveness). The definition given above, though, provides a basis for the topological characterization of safety and liveness properties which they use to prove the decomposition theorem i.e. that any property can be expressed as a conjunction of a safety and liveness property. So, it would seem that the definition is relatively &quot;natural&quot;.
As they remark in the final paragraph of that paper:

It seems naive to hope for a proof that a formal definition for liveness (or safety) is correct, because &quot;good things&quot; and &quot;bad things&quot; are not well-defined concepts. However, the simple topological characterization of the definitions suggests that they do indeed capture fundamental distinctions.