On effectively closed sets of effective strong measure zero

The strong measure zero sets of reals have been widely studied in the context of set theory of the real line. The notion of strong measure zero is straightforwardly effectivized. A set of reals is said to be of effective strong measure zero if for any computable sequence {εn}n∈N of positive rationals, a sequence of intervals In of diameter εn covers the set. We observe that a set is of effective strong measure zero if and only if it is of measure zero with respect to any outer measure constructed by Monroe's Method from a computable atomless outer premeasure defined on all open balls. This measure-theoretic restatement permits many characterizations of strong measure zero in terms of semimeasures as well as martingales. We show that for closed subsets of Cantor space, effective strong nullness is equivalent to another well-studied notion called diminutiveness, the property of not having a computably perfect subset. Further, we prove that if P is a nonempty effective strong measure zero Π10 set consisting only of noncomputable elements, then some Martin-Löf random reals compute no element in P, and P has an element that computes no autocomplex real. Finally, we construct two different special Π10 sets, one of which is not of effective strong measure zero, but consists only of infinitely-often K-trivial reals, and the other is perfect and of effective strong measure zero, but contains no anti-complex reals.