> If you say "at least in the sense that F is almost everywhere differentiable", you're already redefining "anti-derivative" to some extent, I feel. But this is just arguing over semantics.
It is, but let's! Before we re-define the anti-derivative, we'd have to define it. A sensible definition is: a function F is an anti-derivative of a function f if F is everywhere differentiable, and if F' = f everywhere. By this definition, not every integrable function has an anti-derivative.
On the other hand, we could also just choose to define—not re-define!—an anti-derivative of f to be a function F that is almost everywhere differentiable, and such that F' = f almost everywhere. This definition is more complicated, but also more inclusive; and it handles everything the old definition could.
In this respect it is, and it's no accident, exactly like the Lebesgue integral vis a vis the Riemann integral. Lebesgue's integral has a more complicated definition than Riemann's, and we could call it a re-definition; but, since it handles everything that Riemann's does (with the same answer), we could say in retrospect that Lebesgue's was the correct definition, and Riemann's was just the special case we happened to discover first.
> I think the more important insight here is that integration fundamentally isn't defined through the anti-derivative, and that the two notions are actually related is a deep theorem, rather than just a definition.
Certainly I agree with this!
> And the fact that non-elementary antiderivatives exist is interesting in theory, but in practice you can't use them directly for anything. In particular, in practical situations you will often use numerical methods to integrate a function which will not be based on any notion of anti-derivative at all.
Here again I'd argue over semantics, though I'd concede it's much more a matter of personal preference than my argument above, which I think has mathematical weight behind it. Namely, I'd argue that the numerical integration is doing something directly with the non-elementary anti-derivative, namely, evaluating it at a point—just like we call reading off the value of, say, the sine of an angle from our calculator doing something directly with the sine, even though what we're really doing is summing sufficiently many terms in a Taylor-series approximation.
> [^1] Edit: I think I was wrong here. If you take the function identically zero, then its derivative is identically zero and as such equal to the Dirichlet function almost everywhere. So this is not a counterexample. I still think it's weird to call than an "antiderivative" though.
I agree that it's not a counterexample for the reason you say, and there's no arguing with perceptions of something being weird; it certainly is counter to intuition built out of Riemann integrals. And yet, if we didn't steel ourselves to handle this weirdness, we'd have to say that it didn't have an anti-derivative at all; and why artificially restrict our theorems to match our intuition, rather than expanding our intuition to meet our theorems?