On the set of natural number, we can consider the finitely-additive measure defined as: $$\mu(A) = \lim_{n\to\infty}\frac{\#(A\cap [1,n])}{n}.$$
However, there is a definable (by PA, or some first-order arithmetic) subset of natural numbers that is not $\mu$-measurable (e.g. set of all natural numbers whose first digit of decimal expression is 1.) This problem can be resolved if we take an ultralimit rather than the ordinary limit.
However, ultralimit requires free ultrafilter and it makes calculation of ultralimit impossible. I want a (finitely-additive) measure, which gives a hope to calculate the measure for "explicitly-given" sets of natural numbers.
So my question is: Can we find a (possibly partially defined) explicitly defined finite-additive measure over $\Bbb{N}$ extended from $\mu$ mentioned above, that is defined for every arithmetic (or hyperarithmetic) sets?
("explicitly defined" means that, we can find that without full axiom of choice or ultrafilter lemma. I admit the countable choice and dependent choice. I already know that the existence of full finitely-additive measure over $\Bbb{N}$ implies the existence of a set of reals without Baire property.)
Thanks for any help!
If $\mathcal{A}$ is any countable family of sets, you can simply list $\mathcal{A}$ and iteratively extend $\mu$ to all of $\mathcal{A}$. So we do not really quote Hahn-Banach but simply run its proof for $\omega$ steps.