Not quite, Nat.
Its kind of the set theoretic equivalent of the
fundamental theorem of interval arithmetic.
While it is true that assertions on the empty set are
vacuously true, we are not gathering assertions.
We are mapping the function P(f,x) onto the elements
of the set {true, false} FOR ALL x in xx. Thus, the
definition:
decorationP(f,xx) = { P(f,x) for all x in xx }
must have the result {} (the empty set) if there are
no elements in xx because it must be true that:
decorationP(f,xx) \contained decorationP(f,yy)
for all xx \contained yy.
In particular, we must have that:
decorationP(f,[empty]) \contained
decorationP(f,xx) \contained
decorationP(f,[entire])
for all f & for all xx.
Since the empty interval is trivially contained in all
intervals we must haved that decoration(f,[empty]) = {}
(the empty set).
Don't you agree?