  From this little theory we want to derive HoldsAt(Dead, \(T_4)\). Unfortunately, this sequent is not valid in the classical sense of being true in all models which satisfy the theory. Think for example of a situation in which the gun obscurely becomes unloaded while Vincent is smoking. In such a model, the precondition of the shooting action is clearly not met and thus the action will lack any effects. Note that nothing rules out such a model since it is entirely consistent with our theory. We thus have to further constrain the models under consideration. Crucially, we have to find a way to deal with the non-effects of actions; this is the famous frame problem. 