  We prove the completeness of an axiomatization for differential equation
invariants. First, we show that the differential equation axioms in
differential dynamic logic are complete for all algebraic invariants. Our proof
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.
  We then show that extending the axiomatization with existence and uniqueness
axioms makes it complete for all local progress properties, and further
extension with a real induction axiom makes it complete for all real arithmetic
invariants. This yields a parsimonious axiomatization, which serves as the
logical foundation for reasoning about invariants of differential equations.
Moreover, our results are purely axiomatic, and so the axiomatization is
suitable for sound implementation in foundational theorem provers.
