Sorry, I'm still not clear on what you mean by the tail sigma algebra. Do you mean the sets that are closed under all finite modifications?

Descriptive set theory provides many ways to measure the complexity of such sets, with its various hierarchies, and these gives substance to various notions of what it means to "exhibit" the basis. For example, perhaps there can be no Borel basis, but there can be a projective basis.

Well, that is true, for definitions of sufficintly complexity. But this is the nature of set theory, no? Even the set of real numbers can vary from one model of set theory to another. My point was that if you define your object in ZF+DC, then for all you knew, you could have been in L(R) to begin with. And then the things about it that are expressible in L(R) will be provable in ZF+DC if and only if there are provable in ZFC, since L(R) has an expansion not adding reals to a model of ZFC.

In particular, any von Neumann algebra or any other mathematical object that you can prove exists in ZF+DC, will exist in L(R), and so they are covered by the argument.

Of course you are right, and perhaps my post is a bit of a rant! I apologize. (But surely it is implicit in the question that all the equivalent formulations of a definition might find a suitable usage.) My point is that in an undergraduate linear algebra class, a computational approach to the determinant obscures its fundamental geometric meaning as a measure of volume inflation. The permutation sum definition is especially curious in an undergraduate course, because the method is not feasible (exponential time), whereas other methods, such as the LU decomposition, are polynomial time.

Yes, that's right. I added a link to the Wikepedia article on the double negation translation.

+1. I'm happy to push you up to 10, evidently for your first silver badge.