 Formulas in the language of the typed theory with \(\in\) and \(\sim\) have a monotonicity property: if \(\phi\) is a generalized positive formula and one of its typed versions is false, then any version of the same formula obtained by raising types and refining the values of free variables in the formula will continue to be false. It is not hard to see why this will fail to work if negation is allowed.