Another argument for keeping it is that it works nicely with the
assumptions system. In the assumptions system, ~Q.positive means "not
positive", whereas Q.nonpositive means "real and not positive". The
former item means *anything* that is not a positive real number. It
could be a negative number, a complex number, a matrix, a set, etc. In
other words, negation in the assumptions implicitly means universal
complement. Therefore if we want there to be a one-to-one mapping
between assumptions and sets (and I think we do), we need to allow the
universal set, because that is the corresponding set to Q.is_true (or
more simply, S.true).
Aaron Meurer