What is the relation between the formal definition of strictness and its intuitive notion
The intuition: if executing f(x) causes x to be evaluated, and evaluating x doesn't terminate, then this will cause f(x) to fail to terminate (because evaluating x doesn't terminate, so the execution of f(x) never completes).

So, if executing f(x) always causes x to be executed, then f will be strict by the formal definition above.  That's why "f(x) completely evaluates x" implies "f(x) evaluates to bottom for all x that evaluate to bottom".

In contrast, with a lazy function, evaluating f(x) doesn't necessarily trigger evaluation of x, so it doesn't necessarily terminate (even if evaluating x wouldn't terminate).  Thus, for a function that is intuitively lazy, it won't meet the formal definition of strict.