  This article proves the completeness of an axiomatization for differential
equation invariants described by Noetherian functions. First, the differential
equation axioms of differential dynamic logic are shown to be complete for
reasoning about analytic invariants. Completeness crucially exploits
differential ghosts, which introduce additional variables that can be chosen to
evolve freely along new differential equations. Cleverly chosen differential
ghosts are the proof-theoretical counterpart of dark matter. They create new
hypothetical state, whose relationship to the original state variables
satisfies invariants that did not exist before. The reflection of these new
invariants in the original system then enables its analysis.
  An extended axiomatization with existence and uniqueness axioms is complete
for all local progress properties, and, with a real induction axiom, is
complete for all semianalytic invariants. This parsimonious axiomatization
serves as the logical foundation for reasoning about invariants of differential
equations. Indeed, it is precisely this logical treatment that enables the
generalization of completeness to the Noetherian case.
