We enable the theory of differential dynamic logic (dL) for hybrid systems to play catchup with its practice in the theorem prover KeYmaera X by augmenting dL with terms for definite descriptions that describe definable partial functions. At least in the form of divisions, nth roots, or absolute values do such extended terms arise frequently in applications. Besides the woes of partiality do they come with subtleties in differential equations, because definable functions may ruin local Lipschitz continuity and, thereby, uniqueness and longevity of solutions.

Our extension of dL to definite descriptions (dLi) is a free logic; we investigate the interaction of free logic and the differential equations (ODEs) of dL, showing that this combination is sound. We show how dLi can be used not only to recover practical features used today in KeYmaera X, but also many desirable features not yet available in implementation, proving it to be a useful foundation. We give examples showing how new systems can be defined and verified using these extensions.