A Uniform Substitution Calculus for Differential Dynamic Logic

Abstract

This paper introduces a new proof calculus for differential dynamic logic ($\mathsf {d}\mathcal {L}$) that is entirely based on uniform substitution, a proof rule that substitutes a formula for a predicate symbol everywhere. Uniform substitutions make it possible to rely on axioms rather than axiom schemata, substantially simplifying implementations. Instead of subtle schema variables and soundness-critical side conditions on the occurrence patterns of variables, the resulting calculus adopts only a finite number of ordinary $\mathsf {d}\mathcal {L}$ formulas as axioms. The static semantics of differential dynamic logic is captured exclusively in uniform substitutions and bound variable renamings as opposed to being spread in delicate ways across the prover implementation. In addition to sound uniform substitutions, this paper introduces differential forms for differential dynamic logic that make it possible to internalize differential invariants, differential substitutions, and derivations as first-class axioms in $\mathsf {d}\mathcal {L}$.

All proofs are in a companion report [9]. This material is based upon work supported by the National Science Foundation by NSF CAREER Award CNS-1054246.

These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.

1 Introduction

Differential dynamic logic ($\mathsf {d}\mathcal {L}$) [4, 6] is a logic for proving correctness properties of hybrid systems. It has a sound and complete proof calculus relative to differential equations [4, 6] and a sound and complete proof calculus relative to discrete systems [6]. Both sequent calculi [4] and Hilbert-type axiomatizations [6] have been presented for $\mathsf {d}\mathcal {L}$ but only the former has been implemented. The implementation of ${\mathsf {d}\mathcal {L}}$’s sequent calculus in KeYmaera makes it straightforward for users to prove properties of hybrid systems, because it provides rules performing natural decompositions for each operator. The downside is that the implementation of the rule schemata and their side conditions on occurrence constraints and relations of reading and writing of variables as well as rule applications in context is nontrivial and inflexible in KeYmaera.

The goal of this paper is to identify how to make it straightforward to implement the axioms and proof rules of differential dynamic logic by writing down a finite list of axioms (concrete formulas, not axiom schemata that represent an infinite list of axioms subject to sophisticated soundness-critical schema variable matching implementations). They require multiple axioms to be combined with one another to obtain the effect that a user would want for proving a hybrid system conjecture. This paper argues that this is still a net win for hybrid systems, because a substantially simpler prover core is easier to implement correctly, and the need to combine multiple axioms to obtain user-level proof steps can be achieved equally well by appropriate tactics, which are not soundness-critical.

To achieve this goal, this paper follows observations for differential game logic [8] that highlight the significance and elegance of uniform substitutions, a classical proof rule for first-order logic [2, §35,40]. Uniform substitutions uniformly instantiate predicate and function symbols with formulas and terms, respectively, as functions of their arguments. In the presence of the nontrivial binding structure that nondeterminism and differential equations of hybrid programs induce for the dynamic modalities of differential dynamic logic, flexible but sound uniform substitutions become more complex for $\mathsf {d}\mathcal {L}$, but can still be read off elegantly from its static semantics. In fact, ${\mathsf {d}\mathcal {L}}$’s static semantics is solely captured¹ in the implementation of uniform substitution (and bound variable renaming), thereby leading to a completely modular proof calculus.

This paper introduces a static and dynamic semantics for differential-form $\mathsf {d}\mathcal {L}$, proves coincidence lemmas and uniform substitution lemmas, culminating in a soundness proof for uniform substitutions (Sect. 3). It exploits the new differential forms that this paper adds to $\mathsf {d}\mathcal {L}$ for internalizing differential invariants [5], differential cuts [5, 7], differential ghosts [7], differential substitutions, total differentials and Lie-derivations [5, 7] as first-class citizens in $\mathsf {d}\mathcal {L}$, culminating in entirely modular axioms for differential equations and a superbly modular soundness proof (Sect. 4). This approach is to be contrasted with earlier approaches for differential invariants that were based on complex built-in rules [5, 7]. The relationship to related work from previous presentations of differential dynamic logic [4, 6] continues to apply except that $\mathsf {d}\mathcal {L}$ now internalizes differential equation reasoning axiomatically via differential forms.

2 Differential-Form Differential Dynamic Logic

2.1 Syntax

Formulas and hybrid programs (HPs) of $\mathsf {d}\mathcal {L}$ are defined by simultaneous induction based on the following definition of terms. Similar simultaneous inductions are used throughout the proofs for $\mathsf {d}\mathcal {L}$. The set of all variables is $\mathcal {V}$. For any $V\subseteq \mathcal {V}$ is ${V}^{\prime }\mathop {=}\limits ^{\mathrm{def}}\{{x}^{\prime } : x\in V\}$ the set of differential symbols ${x}^{\prime }$ for the variables in V. Function symbols are written f, g, h, predicate symbols p, q, r, and variables $x,y,z\in \mathcal {V}$ with differential symbols ${x}^{\prime },{y}^{\prime },{z}^{\prime }\in {\mathcal {V}}^{\prime }$. Program constants are a, b, c.

Definition 1

(Terms). Terms are defined by this grammar (with $\theta ,\eta ,\theta _1,\dots ,\theta _k$ as terms, $x\in \mathcal {V}$ as variable, ${x}^{\prime }\in {\mathcal {V}}^{\prime }$ differential symbol, and f function symbol):

$$\begin{aligned} \theta ,\eta ~~{:}{:}\!\!=~ x ~|~{x}^{\prime } ~|~f(\theta _1,\dots ,\theta _k) ~|~\theta +\eta ~|~\theta \cdot \eta ~|~(\theta )' \end{aligned}$$

Number literals such as 0,1 are allowed as function symbols without arguments that are always interpreted as the numbers they denote. Beyond differential symbols ${x}^{\prime }$, differential-form $\mathsf {d}\mathcal {L}$ allows differentials $(\theta )'$ of terms $\theta$ as terms for the purpose of axiomatically internalizing reasoning about differential equations.

Definition 2

(Hybrid program). Hybrid programs (HPs) are defined by the following grammar (with $\alpha ,\beta$ as HPs, program constant a, variable x, term $\theta$ possibly containing x, and formula $\psi$ of first-order logic of real arithmetic):

$$ \begin{aligned} \alpha ,\beta ~~{:}{:}\!\!=~ a~|~{{x\,}{:}{=}{\,\theta }} ~|~{{{x}^{\prime }\,}{:}{=}{\,\theta }} ~|~?{\psi } ~|~{{x}^{\prime }=\theta \,} \& {\,\psi } ~|~\alpha \cup \beta ~|~\alpha ;\beta ~|~{\alpha }^* \end{aligned}$$

Assignments ${{x\,}{:}{=}{\,\theta }}$ of $\theta$ to variable x, tests $?{\psi }$ of the formula $\psi$ in the current state, differential equations ${{x}^{\prime }=\theta \,} \& {\,\psi }$ restricted to the evolution domain constraint $\psi$, nondeterministic choices ${\alpha }\cup {\beta }$, sequential compositions $\alpha ;\beta$, and nondeterministic repetition ${\alpha }^*$ are as usual in $\mathsf {d}\mathcal {L}$ [4, 6]. The effect of the differential assignment ${{{x}^{\prime }\,}{:}{=}{\,\theta }}$ to differential symbol ${x}^{\prime }$ is similar to the effect of the assignment ${{x\,}{:}{=}{\,\theta }}$ to variable x, except that it changes the value of the differential symbol ${x}^{\prime }$ around instead of the value of x. It is not to be confused with the differential equation ${{x}^{\prime }=\theta }$, which will follow said differential equation continuously for an arbitrary amount of time. The differential assignment ${{{x}^{\prime }\,}{:}{=}{\,\theta }}$, instead, only assigns the value of $\theta$ to the differential symbol ${x}^{\prime }$ discretely once at an instant of time. Program constants a are uninterpreted, i.e. their behavior depends on the interpretation in the same way that the values of function symbols f and predicate symbols p depends on their interpretation.

Definition 3

( ${\mathbf {\mathsf{{d}}}}\mathcal {L}$ formula). The formulas of (differential-form) differential dynamic logic ($\mathsf {d}\mathcal {L}$) are defined by the grammar (with $\mathsf {d}\mathcal {L}$ formulas $\phi ,\psi$, terms $\theta ,\eta ,\theta _1,\dots ,\theta _k$, predicate symbol p, quantifier symbol C, variable x, HP $\alpha$):

$$\begin{aligned} \phi ,\psi ~~{:}{:}\!\!=~\theta \ge \eta ~|~p(\theta _1,\dots ,\theta _k) ~|~C(\phi ) ~|~\lnot \phi ~|~\phi \wedge \psi ~|~\forall {x}\,{\phi } ~|~\exists {x}\,{\phi } ~|~[{\alpha }]{\phi } ~|~\langle {\alpha }\rangle {\phi } \end{aligned}$$

Operators $>,\le ,<,\vee ,\rightarrow ,\leftrightarrow$ are definable, e.g., $\phi \rightarrow \psi$ as $\lnot (\phi \wedge \lnot \psi )$. Likewise $[{\alpha }]{\phi }$ is equivalent to $\lnot \langle {\alpha }\rangle {\lnot \phi }$ and $\forall {x}\,{\phi }$ equivalent to $\lnot \exists {x}\,{\lnot \phi }$. The modal formula $[{\alpha }]{\phi }$ expresses that $\phi$ holds after all runs of $\alpha$, while the dual $\langle {\alpha }\rangle {\phi }$ expresses that there is a run of $\alpha$ after which $\phi$ holds. Quantifier symbols C (with formula $\phi$ as argument), i.e. higher-order predicate symbols that bind all variables of $\phi$, are unnecessary but internalize contextual congruence reasoning efficiently.

2.2 Dynamic Semantics

A state is a mapping from variables $\mathcal {V}$ and differential symbols ${\mathcal {V}}^{\prime }$ to $\mathbb {R}$. The set of states is denoted $\mathcal {S}$. Let $\nu _{x}^{r}$ denote the state that agrees with state ${\nu }$ except for the value of variable $x$, which is changed to $r \in \mathbb {R}$, and accordingly for $\nu _{x^{\prime }}^{r}$. The interpretation of a function symbol f with arity n (i.e. with n arguments) is a smooth function $I(f):\mathbb {R}^n\rightarrow \mathbb {R}$ of n arguments.

Definition 4

(Semantics of terms). For each interpretation I, the semantics of a term $\theta$ in a state $\nu \in \mathcal {S}$ is its value in $\mathbb {R}$. It is defined inductively as follows

• 1. $[\![{x}]\!]^{I}\nu = \nu (x)$ for variable $x\in \mathcal {V}$

• 2. $[\![{{x}^{\prime }}]\!]^{I}\nu = \nu ({x}^{\prime })$ for differential symbol ${x}^{\prime }\in {\mathcal {V}}^{\prime }$

• 3. $[\![{f(\theta _1,\dots ,\theta _k)}]\!]^{I}\nu = I(f)\big ([\![{\theta _1}]\!]^{I}\nu ,\dots ,[\![{\theta _k}]\!]^{I}\nu \big )$ for function symbol f

• 4. $[\![{\theta +\eta }]\!]^{I}\nu = [\![{\theta }]\!]^{I}\nu + [\![{\eta }]\!]^{I}\nu$

• 5. $[\![{\theta \cdot \eta }]\!]^{I}\nu = [\![{\theta }]\!]^{I}\nu \cdot [\![{\eta }]\!]^{I}\nu$

• 6. $[\![{(\theta )'}]\!]^{I}\nu \displaystyle =\sum _x \nu ({x}^{\prime }) \frac{\partial [\![\theta ]\!]^I}{\partial x}(\nu ) = \sum _x \nu (x^\prime )\frac{\partial [\![\theta ]\!]^I\nu _x^X}{\partial X}$

Time-derivatives are undefined in an isolated state ${\nu }$. The clou is that differentials can still be given a local semantics: $[\![{(\theta )'}]\!]^{I}\nu$ is the sum of all (analytic) spatial partial derivatives of the value of $\theta$ by all variables x (or rather their values X) multiplied by the corresponding tangent described by the value ${\nu }({x}^{\prime })$ of differential symbol ${x}^{\prime }$. That sum over all variables $x\in \mathcal {V}$ has finite support, because $\theta$ only mentions finitely many variables x and the partial derivative by variables x that do not occur in $\theta$ is 0. The spatial derivatives exist since $[\![{\theta }]\!]^{I}\nu$ is a composition of smooth functions, so smooth. Thus, the semantics of $[\![{(\theta )'}]\!]^{I}\nu$ is the differential ² of (the value of) $\theta$, hence a differential one-form giving a real value for each tangent vector (i.e. vector field) described by the values ${\nu }({x}^{\prime })$. The values ${\nu }({x}^{\prime })$ of the differential symbols ${x}^{\prime }$ describe an arbitrary tangent vector or vector field. Along the flow of (the vector field of a) differential equation, though, the value of the differential $(\theta )'$ coincides with the analytic time-derivative of $\theta$ (Lemma 8). The interpretation of predicate symbol p with arity n is an n-ary relation $I(p)\subseteq \mathbb {R}^n$. The interpretation of quantifier symbol C is a functional I(C) mapping subsets $M\subseteq \mathcal {S}$ to subsets $I(C)(M)\subseteq \mathcal {S}$.

Definition 5

( ${\mathbf {\mathsf{{d}}}}\mathcal {L}$ semantics). The semantics of a $\mathsf {d}\mathcal {L}$ formula $\phi$, for each interpretation I with a corresponding set of states $\mathcal {S}$, is the subset $[\![\phi ]\!]^{I}\subseteq \mathcal {S}$ of states in which $\phi$ is true. It is defined inductively as follows

• 1. $[\![\theta \ge \eta ]\!]^{I} = \{{\nu } \in \mathcal {S} ~:~[\![{\theta }]\!]^{I}\nu \ge [\![{\eta }]\!]^{I}\nu \}$

• 2. $[\![p(\theta _1,\dots ,\theta _k)]\!]^{I} = \{{\nu } \in \mathcal {S} ~:~([\![{\theta _1}]\!]^{I}\nu ,\dots ,[\![{\theta _k}]\!]^{I}\nu )\in I(p)\}$

• 3. $[\![C(\phi )]\!]^{I} = I(C)\big ([\![\phi ]\!]^{I}\big )$ for quantifier symbol C

• 4. $[\![\lnot \phi ]\!]^{I} = {([\![\phi ]\!]^{I})}^{\complement } = \mathcal {S}\setminus [\![\phi ]\!]^{I}$

• 5. $[\![\phi \wedge \psi ]\!]^{I} = [\![\phi ]\!]^{I} \cap [\![\psi ]\!]^{I}$

• 6. $[\![\exists {x}\,{\phi }]\!]^{I} = \{{\nu } \in \mathcal {S} ~:~{\nu }_x^r \in [\![\phi ]\!]^{I} ~\text {for some}~r\in \mathbb {R}\}$

• 7. $[\![\langle {\alpha }\rangle {\phi }]\!]^{I} = [\![\alpha ]\!]^{I}\circ [\![\phi ]\!]^{I} =\{{\nu } ~:~\omega \in [\![\phi ]\!]^I ~\text {for some}~{\omega }~\text {such that}~(\nu , \omega )\in [\![\alpha ]\!]^I\}$

• 8. $[\![[{\alpha }]{\phi }]\!]^{I} = [\![\lnot \langle {\alpha }\rangle {\lnot \phi }]\!]^{I}$ $=\{{\nu } ~:~\omega \in [\![\phi ]\!]^I ~\text {for all}~\omega ~\text {such that}~(\nu , \omega )\in [\![\alpha ]\!]^I\}$

A $\mathsf {d}\mathcal {L}$ formula $\phi$ is valid in I, written ${I}\models {\phi }$, iff $[\![\phi ]\!]^{I}=\mathcal {S}$, i.e. ${\nu }\in [\![{\phi }]\!]^I$ for all ${\nu }$. Formula $\phi$ is valid, written $\models \phi$, iff $I\models {\phi }$ for all interpretations I.

The interpretation of a program constant a is a state-transition relation $I(a)\subseteq \mathcal {S}\times \mathcal {S}$, where $(\nu , \omega )\in I(a)$ iff a can run from initial state ${\nu }$ to final state $\omega$.

Definition 6

(Transition semantics of HPs). For each interpretation I, each HP $\alpha$ is interpreted semantically as a binary transition relation $[\![\alpha ]\!]^{I}\subseteq \mathcal {S}\times \mathcal {S}$ on states, defined inductively by

• 1. $[\![a]\!]^{I} = I(a)$ for program constants a

• 2. $[\![x:=\theta ]\!]^I = \{(\nu , \nu _x^r) ~:~r= [\![\theta ]\!]^I \nu \} = \{({\nu },\omega ) ~:~\omega ={\nu }~\text {except}~[\![x]\!]^I\omega =[\![{\theta }]\!]^{I}\nu \}$

• 3. $[\![x^{\prime }:=\theta ]\!]^I = \{(\nu , \nu _{x^{\prime }}^r) ~:~r= [\![\theta ]\!]^I \nu \} = \{({\nu },\omega ) ~:~\omega ={\nu }~\text {except}~[\![x^{\prime }]\!]^I\omega =[\![{\theta }]\!]^{I}\nu \}$

• 4. $[\![?\psi ]\!]^{I} = \{({\nu }, {\nu }) ~:~{\nu }\in [\![{\psi }]\!]^I\}$

• 5. $[\![x^\prime =\theta \, \& \,\psi ]\!]^{I} = \{({\nu },\omega ) ~:~I, \varphi , \models x^\prime = \theta \wedge \psi$, i.e. $\varphi (\zeta ) \in [\![ x' = \theta \wedge \psi ]\!]^I$ for all $0\le \zeta \le r$, for some function $\varphi :[0,r]\rightarrow \mathcal {S}$ of some duration r for which all $\varphi (\zeta )({x}^{\prime }) = \frac{\mathsf{d}\varphi (t)(x)}{\mathsf{d}t}(\zeta )$ exist and $\nu =\varphi (0)$ on ${\{{x}^{\prime }\}}^{\complement }$ and $\omega =\varphi (r)\}$; i.e., $\varphi$ solves the differential equation and satisfies $\psi$ at all times. In case $r=0$, the only condition is that ${\nu }=\omega$ on ${\{{x}^{\prime }\}}^{\complement }$ and $\omega ({x}^{\prime })=[\![\theta ]\!]^I \omega$ and $\omega \in [\![\psi ]\!]^I$.

• 6. $[\![{\alpha }\cup {\beta }]\!]^I = [\![\alpha ]\!]^I \cup [\![\beta ]\!]^I$

• 7. $[\![\alpha ;\beta ]\!]^I = [\![\alpha ]\!]^I \circ [\![\beta ]\!]^I = \{(\nu ,\omega ) : ({\nu },\mu ) \in [\![\alpha ]\!]^I, (\mu ,\omega ) \in [\![\beta ]\!]^I\}$

• 8. $[\![{\alpha }^*]\!]^I = ([\![\alpha ]\!]^I)^*= \bigcup \limits _{n\in \mathbb {N}} [\![\alpha ^n]\!]^{I} ~with~\alpha ^{n+1}\equiv \alpha ^{n}; \alpha \;and\;\alpha ^0 \equiv \,?true$

where ${\rho }^*$ denotes the reflexive transitive closure of relation $\rho$.

The initial values ${\nu }({x}^{\prime })$ of differential symbols ${x}^{\prime }$ do not influence the behavior of $(\nu , \omega )\in [\![x'= \theta \, \& \,\psi ]\!]^I$, because they may not be compatible with the time-derivatives for the differential equation, e.g. in ${{{x}^{\prime }\,}{:}{=}{\,1}};{{x}^{\prime }=2}$, with a ${x}^{\prime }$ mismatch.

Functions and predicates are interpreted by I and are only influenced indirectly by $\nu$ through the values of their arguments. So $p(e)\rightarrow [{{{x\,}{:}{=}{\,x+1}}}]{p(e)}$ is valid if x is not in e since the change in x does not change whether p(e) is true (Lemma 2). By contrast $p(x)\rightarrow [{{{x\,}{:}{=}{\,x+1}}}]{p(x)}$ is invalid, since it is false when $I(p)=\{d ~:~d\le 5\}$ and $\nu (x)=4.5$. If the semantics of p were to depend on the state ${\nu }$, then there would be no discernible relationship between the truth-values of p in different states, so not even $p\rightarrow [{{{x\,}{:}{=}{\,x+1}}}]{p}$ would be valid.

2.3 Static Semantics

The static semantics of $\mathsf {d}\mathcal {L}$ and HPs defines some aspects of their behavior that can be read off directly from their syntactic structure without running their programs or evaluating their dynamical effects. The most important aspects of the static semantics concern free or bound occurrences of variables. Bound variables x are those that are bound by $\forall {x}\,{}$or $\exists {x}\,{}$, but also those that are bound by modalities such as $[{{{x\,}{:}{=}{\,5y}}}]{}$ or $\langle {{{x}^{\prime }=1}}\rangle {}$ or $[{{{x\,}{:}{=}{\,1}}\cup {{{x}^{\prime }=1}}}]{}$ or $[{{{x\,}{:}{=}{\,1}}\cup {?{true}}}]{}$.

The notions of free and bound variables are defined by simultaneous induction in the subsequent definitions: free variables for terms ($\mathop {\textit{FV}}(\theta )$), formulas ($\mathop {\textit{FV}}(\phi )$), and HPs ($\mathop {\textit{FV}}(\alpha )$), as well as bound variables for formulas ($\mathop {\textit{BV}}(\phi )$) and for HPs ($\mathop {\textit{BV}}(\alpha )$). For HPs, there will be a need to distinguish must-bound variables ($\mathop {\textit{MBV}}(\alpha )$) that are bound/written to on all executions of $\alpha$ from (may-)bound variables ($\mathop {\textit{BV}}(\alpha )$) which are bound on some (not necessarily all) execution paths of $\alpha$, such as in $[{{{x\,}{:}{=}{\,1}}\cup {({{x\,}{:}{=}{\,0}};{{y\,}{:}{=}{\,x+1}})}}]{}$, which has bound variables $\{x,y\}$ but must-bound variables only $\{x\}$, because y is not written to in the first choice.

Definition 7

(Bound variable). The set $\mathop {\textit{BV}}(\phi )\subseteq \mathcal {V}\cup {\mathcal {V}}^{\prime }$ of bound variables of $\mathsf {d}\mathcal {L}$ formula $\phi$ is defined inductively as

$$\begin{aligned} \mathop {\textit{BV}}(\theta \ge \eta ) = \mathop {\textit{BV}}(p(\theta _1,\dots ,\theta _k))&= \emptyset \\ \mathop {\textit{BV}}(C(\phi ))&= \mathcal {V}\cup {\mathcal {V}}^{\prime }\\ \mathop {\textit{BV}}(\lnot \phi )&= \mathop {\textit{BV}}(\phi )\\ \mathop {\textit{BV}}(\phi \wedge \psi )&= \mathop {\textit{BV}}(\phi )\cup \mathop {\textit{BV}}(\psi )\\ \mathop {\textit{BV}}(\forall {x}\,{\phi }) = \mathop {\textit{BV}}(\exists {x}\,{\phi })&= \{x\}\cup \mathop {\textit{BV}}(\phi )\\ \mathop {\textit{BV}}([{\alpha }]{\phi }) = \mathop {\textit{BV}}(\langle {\alpha }\rangle {\phi })&= \mathop {\textit{BV}}(\alpha )\cup \mathop {\textit{BV}}(\phi ) \end{aligned}$$

Definition 8

(Free variable). The set $\mathop {\textit{FV}}(\theta )\subseteq \mathcal {V}\cup {\mathcal {V}}^{\prime }$ of free variables of term $\theta$, i.e. those that occur in $\theta$, is defined inductively as

$$\begin{aligned} \mathop {\textit{FV}}(x)&= \{x\}\\ \mathop {\textit{FV}}({x}^{\prime })&= \{{x}^{\prime }\}\\ \mathop {\textit{FV}}(f(\theta _1,\dots ,\theta _k))&= \mathop {\textit{FV}}(\theta _1)\cup \dots \cup \mathop {\textit{FV}}(\theta _k)\\ \mathop {\textit{FV}}(\theta +\eta ) = \mathop {\textit{FV}}(\theta \cdot \eta )&= \mathop {\textit{FV}}(\theta )\cup \mathop {\textit{FV}}(\eta ) \\ \mathop {\textit{FV}}((\theta )')&= \mathop {\textit{FV}}(\theta ) \cup {\mathop {\textit{FV}}(\theta )}^{\prime } \end{aligned}$$

The set $\mathop {\textit{FV}}(\phi )$ of free variables of $\mathsf {d}\mathcal {L}$ formula $\phi$, i.e. all those that occur in $\phi$ outside the scope of quantifiers or modalities binding it, is defined inductively as

$$\begin{aligned} \mathop {\textit{FV}}(\theta \ge \eta )&= \mathop {\textit{FV}}(\theta )\cup \mathop {\textit{FV}}(\eta )\\ \mathop {\textit{FV}}(p(\theta _1,\dots ,\theta _k))&= \mathop {\textit{FV}}(\theta _1)\cup \dots \cup \mathop {\textit{FV}}(\theta _k)\\ \mathop {\textit{FV}}(C(\phi ))&= \mathcal {V}\cup {\mathcal {V}}^{\prime }\\ \mathop {\textit{FV}}(\lnot \phi )&= \mathop {\textit{FV}}(\phi )\\ \mathop {\textit{FV}}(\phi \wedge \psi )&= \mathop {\textit{FV}}(\phi )\cup \mathop {\textit{FV}}(\psi )\\ \mathop {\textit{FV}}(\forall {x}\,{\phi }) = \mathop {\textit{FV}}(\exists {x}\,{\phi })&= \mathop {\textit{FV}}(\phi )\setminus \{x\}\\ \mathop {\textit{FV}}([{\alpha }]{\phi }) = \mathop {\textit{FV}}(\langle {\alpha }\rangle {\phi })&= \mathop {\textit{FV}}(\alpha )\cup (\mathop {\textit{FV}}(\phi )\setminus \mathop {\textit{MBV}}(\alpha )) \end{aligned}$$

Soundness requires that $\mathop {\textit{FV}}([{\alpha }]{\phi })$ is not defined as $\mathop {\textit{FV}}(\alpha )\cup (\mathop {\textit{FV}}(\phi )\setminus \mathop {\textit{BV}}(\alpha ))$, otherwise $[{{{{x\,}{:}{=}{\,1}}}\cup {{{y\,}{:}{=}{\,2}}}}]{x\ge 1}$ would have no free variables, but its truth-value depends on the initial value of x, demanding $\mathop {\textit{FV}}([{{{{x\,}{:}{=}{\,1}}}\cup {{{y\,}{:}{=}{\,2}}}}]{x\ge 1})=\{x\}$.

The static semantics defines which variables are free so may be read ($\mathop {\textit{FV}}(\alpha )$), which are bound ($\mathop {\textit{BV}}(\alpha )$) so may be written to somewhere in $\alpha$, and which are must-bound ($\mathop {\textit{MBV}}(\alpha )$) so must be written to on all execution paths of $\alpha$.

Definition 9

(Bound variable). The set $\mathop {\textit{BV}}(\alpha )\subseteq \mathcal {V}\cup {\mathcal {V}}^{\prime }$ of bound variables of HP $\alpha$, i.e. all those that may potentially be written to, is defined inductively:

$$ \begin{aligned} \mathop {\textit{BV}}(a)&= \mathcal {V}\cup {\mathcal {V}}^{\prime }&\text {for program constant }a \\ \mathop {\textit{BV}}({{x\,}{:}{=}{\,\theta }})&= \{x\} \\ \mathop {\textit{BV}}({{{x}^{\prime }\,}{:}{=}{\,\theta }})&= \{{x}^{\prime }\} \\ \mathop {\textit{BV}}(?{\psi })&= \emptyset \\ \mathop {\textit{BV}}({{x}^{\prime }=\theta \,} \& {\,\psi })&= \{x,{x}^{\prime }\} \\ \mathop {\textit{BV}}(\alpha \cup \beta ) = \mathop {\textit{BV}}(\alpha ;\beta )&= \mathop {\textit{BV}}(\alpha )\cup \mathop {\textit{BV}}(\beta ) \\ \mathop {\textit{BV}}({\alpha }^*)&= \mathop {\textit{BV}}(\alpha ) \end{aligned}$$

Definition 10

(Must-bound variable). The set $\mathop {\textit{MBV}}(\alpha )\subseteq \mathop {\textit{BV}}(\alpha )\subseteq \mathcal {V}\cup {\mathcal {V}}^{\prime }$ of must-bound variables of HP $\alpha$, i.e. all those that must be written to on all paths of $\alpha$, is defined inductively as

$$\begin{aligned} \mathop {\textit{MBV}}(a)&= \emptyset&\text {for program constant }a\\ \mathop {\textit{MBV}}(\alpha )&= \mathop {\textit{BV}}(\alpha )&\text {for other atomic }{\text {HPs}} \;\alpha \\ \mathop {\textit{MBV}}(\alpha \cup \beta )&= \mathop {\textit{MBV}}(\alpha )\cap \mathop {\textit{MBV}}(\beta )\\ \mathop {\textit{MBV}}(\alpha ;\beta )&= \mathop {\textit{MBV}}(\alpha )\cup \mathop {\textit{MBV}}(\beta )\\ \mathop {\textit{MBV}}({\alpha }^*)&= \emptyset \end{aligned}$$

Definition 11

(Free variable). The set $\mathop {\textit{FV}}(\alpha )\subseteq \mathcal {V}\cup {\mathcal {V}}^{\prime }$ of free variables of HP $\alpha$, i.e. all those that may potentially be read, is defined inductively as

$$ \begin{aligned} \mathop {\textit{FV}}(a)&= \mathcal {V}\cup {\mathcal {V}}^{\prime }&\text {for program constant }a\\ \mathop {\textit{FV}}({{x\,}{:}{=}{\,\theta }}) = \mathop {\textit{FV}}({{{x}^{\prime }\,}{:}{=}{\,\theta }})&= \mathop {\textit{FV}}(\theta ) \\ \mathop {\textit{FV}}(?{\psi })&= \mathop {\textit{FV}}(\psi ) \\ \mathop {\textit{FV}}({{x}^{\prime }=\theta \,} \& {\,\psi })&= \{x\}\cup \mathop {\textit{FV}}(\theta )\cup \mathop {\textit{FV}}(\psi ) \\ \mathop {\textit{FV}}({\alpha }\cup {\beta })&= \mathop {\textit{FV}}(\alpha )\cup \mathop {\textit{FV}}(\beta ) \\ \mathop {\textit{FV}}(\alpha ;\beta )&= \mathop {\textit{FV}}(\alpha )\cup (\mathop {\textit{FV}}(\beta )\setminus \mathop {\textit{MBV}}(\alpha )) \\ \mathop {\textit{FV}}({\alpha }^*)&= \mathop {\textit{FV}}(\alpha ) \end{aligned}$$

Unlike x, the left-hand side ${x}^{\prime }$ of differential equations is not added to the free variables of $\mathop {\textit{FV}}({{x}^{\prime }=\theta \,} \& {\,\psi })$, because its behavior does not depend on the initial value of differential symbols ${x}^{\prime }$, only the initial value of x. Free and bound variables are the set of all variables $\mathcal {V}$ and differential symbols ${\mathcal {V}}^{\prime }$ for program constants a, because their effect depends on the interpretation I, so may read and write all $\mathop {\textit{FV}}(a)=\mathop {\textit{BV}}(a)=\mathcal {V}\cup {\mathcal {V}}^{\prime }$ but not on all paths $\mathop {\textit{MBV}}(a)=\emptyset$. Subsequent results about free and bound variables are, thus, vacuously true when program constants occur. Corresponding observations hold for quantifier symbols.

The static semantics defines which variables are readable or writable. There may not be any run of $\alpha$ in which a variable is read or written to. If $x\not \in \mathop {\textit{FV}}(\alpha )$, though, then $\alpha$ cannot read the value of x. If $x\not \in \mathop {\textit{BV}}(\alpha )$, it cannot write to x.

The signature, i.e. set of function, predicate, quantifier symbols, and program constants in $\phi$ is denoted by $\varSigma (\phi )$ (accordingly for terms and programs). It is defined like $\mathop {\textit{FV}}(\phi )$ except that all occurrences are free. Variables in $\mathcal {V}\cup {\mathcal {V}}^{\prime }$ are interpreted by state ${\nu }$. The symbols in $\varSigma (\phi )$ are interpreted by interpretation I.

2.4 Correctness of Static Semantics

The following result reflects that HPs have bounded effect: for a variable x to be modified during a run of $\alpha$, x needs the be a bound variable in HP $\alpha$, i.e. $x\in \mathop {\textit{BV}}(\alpha )$, so that $\alpha$ can write to x. The converse is not true, because $\alpha$ may bind a variable x, e.g. by having an assignment to x, that never actually changes the value of x, such as ${{x\,}{:}{=}{\,x}}$ or because the assignment can never be executed.

Lemma 1

(Bound effect lemma). If $({\nu },{\omega }) \in [\![\alpha ]\!]^{I}$, then ${\nu }={\omega }$ on $BV(\alpha )^{\complement }$.

Similarly, only $\mathop {\textit{BV}}(\phi )$ change their value during the evaluation of formulas.

The value of a term only depends on the values of its free variables. When evaluating a term $\theta$ in two states ${\nu }$, $\tilde{\nu }$ that differ widely but agree on the free variables $\mathop {\textit{FV}}(\theta )$ of $\theta$, the values of $\theta$ in both states coincide. Accordingly for different interpretations I, J that agree on the symbols $\varSigma (\theta )$ that occur in $\theta$. Recall that all proofs and additional examples are in a companion report [9].

Lemma 2

(Coincidence lemma). If ${\nu }=\tilde{\nu }$ on $\mathop {\textit{FV}}(\theta )$ and $I =J$ on $\varSigma (\theta )$, then $[\![\theta ]\!]^{I}\nu =[\![\theta ]\!]^{J}\tilde{\nu }$.

By a more subtle argument, the values of $\mathsf {d}\mathcal {L}$ formulas also only depend on the values of their free variables. When evaluating $\mathsf {d}\mathcal {L}$ formula $\phi$ in two states ${\nu }$, $\tilde{\nu }$ that differ but agree on the free variables $\mathop {\textit{FV}}(\phi )$ of $\phi$, the (truth) values of $\phi$ in both states coincide. Lemmas 3 and 4 are proved by simultaneous induction.

Lemma 3

(Coincidence lemma). If ${\nu }=\tilde{\nu }$ on $\mathop {\textit{FV}}(\phi )$ and $I =J$ on $\varSigma (\phi )$, then $\nu \in [\![\phi ]\!]^{I} \text { iff } \tilde{\nu } \in [\![\phi ]\!]^{J}$.

In a sense, the runs of an HP $\alpha$ also only depend on the values of its free variables, because its behavior cannot depend on the values of variables that it never reads. That is, if ${\nu }=\tilde{\nu }$ on $\mathop {\textit{FV}}(\alpha )$ and $(\nu ,\omega ) \in [\![\alpha ]\!]^{I}$, then there is an $\tilde{\omega }$ such that $(\tilde{\nu },\tilde{\omega }) \in [\![\alpha ]\!]^{J}$ and $\omega$ and $\tilde{\omega }$ agree in some sense. There is a subtlety, though. The resulting states $\omega$ and $\tilde{\omega }$ will only continue to agree on $\mathop {\textit{FV}}(\alpha )$ and the variables that are bound on the particular path that $\alpha$ took for the transition $(\nu ,\omega ) \in [\![\alpha ]\!]^{I}$. On variables z that are neither free (so the initial states ${\nu }$ and $\tilde{\nu }$ have not been assumed to coincide) nor bound on the particular path that $\alpha$ took, $\omega$ and $\tilde{\omega }$ may continue to disagree, because z has not been written to. Yet, $\omega$ and $\tilde{\omega }$ agree on the variables that are bound on all paths of $\alpha$, rather than somewhere in $\alpha$. That is on the must-bound variables of $\alpha$. If initial states agree on (at least) all free variables $\mathop {\textit{FV}}(\alpha )$ that HP $\alpha$ may read, then the final states agree on those as well as on all variables that $\alpha$ must write, i.e. on $\mathop {\textit{MBV}}(\alpha )$.

Lemma 4

(Coincidence lemma). If ${\nu }=\tilde{\nu }$ on $V\supseteq \mathop {\textit{FV}}(\alpha )$ and $I =J$ on $\varSigma (\alpha )$ and $(\nu ,\omega ) \in [\![\alpha ]\!]^{I}$, then there is an $\tilde{\omega }$ such that $(\tilde{\nu },\tilde{\omega }) \in [\![\alpha ]\!]^{J}$ and $\omega =\tilde{\omega }$ on $V\cup \mathop {\textit{MBV}}(\alpha )$.

3 Uniform Substitutions

The uniform substitution rule ${\mathrm{US}_1}$ from first-order logic [2, §35,40] substitutes all occurrences of predicate $p(\varvec{\cdot })$ by a formula ${\psi }({\varvec{\cdot }})$, i.e. it replaces all occurrences of $p(\theta )$, for any (vectorial) term $\theta$, by the corresponding ${\psi }({\theta })$ simultaneously:

$$\begin{aligned} (\hbox {US}_{1})\quad \frac{\phi }{\phi _{{p}({\varvec{\cdot }})}^{\psi (\varvec{\cdot })}} \qquad \qquad (\hbox {US})\quad \frac{\phi }{\sigma (\phi )} \end{aligned}$$

Rule ${\mathrm{US}_1}$ [8] requires all relevant substitutions of ${\psi }({\theta })$ for $p(\theta )$ to be admissible and requires that no $p(\theta )$ occurs in the scope of a quantifier or modality binding a variable of $\psi ({\theta })$ other than the occurrences in $\theta$; see [2, §35,40].

This section considers a constructive definition of this proof rule that is more general: US. The $\mathsf {d}\mathcal {L}$ calculus uses uniform substitutions that affect terms, formulas, and programs. A uniform substitution $\sigma$ is a mapping from expressions of the form $f(\varvec{\cdot })$ to terms $\sigma f(\varvec{\cdot })$, from $p(\varvec{\cdot })$ to formulas $\sigma p(\varvec{\cdot })$, from $C(\_)$ to formulas $\sigma C({\_})$, and from program constants a to HPs $\sigma a$. Vectorial extensions are accordingly for uniform substitutions of other arities $k\ge 0$. Here $\varvec{\cdot }$ is a reserved function symbol of arity zero and _ a reserved quantifier symbol of arity zero. Figure 1 defines the result $\sigma (\phi )$ of applying to a $\mathsf {d}\mathcal {L}$ formula $\phi$ the uniform substitution $\sigma$ that uniformly replaces all occurrences of function f by a (instantiated) term and all occurrences of predicate p or quantifier  C by a (instantiated) formula as well as of program constant a by a program. The notation $\sigma f(\varvec{\cdot })$ denotes the replacement for $f(\varvec{\cdot })$ according to $\sigma$, i.e. the value $\sigma f(\varvec{\cdot })$ of function $\sigma$ at $f(\varvec{\cdot })$. By contrast, $\sigma (\phi )$ denotes the result of applying $\sigma$ to $\phi$ according to Fig. 1 (likewise for $\sigma ({\theta })$ and $\sigma (\alpha )$). The notation $f\in \sigma$ signifies that $\sigma$ replaces f, i.e. $\sigma f(\varvec{\cdot }) \ne f(\varvec{\cdot })$. Finally, $\sigma$ is a total function when augmented with $\sigma g(\varvec{\cdot }) = g(\varvec{\cdot })$ for all $g\not \in \sigma$. Accordingly for predicate symbols, quantifiers, and program constants.

Definition 12

(Admissible uniform substitution). The uniform substitution $\sigma$ is U-admissible for $\phi$ (or $\theta$ or $\alpha$, respectively) with respect to the set $U\subseteq \mathcal {V}\cup {\mathcal {V}}^{\prime }$ iff $\mathop {\textit{FV}}(\sigma |_{\varSigma (\phi )})\cap U=\emptyset$, where $\sigma |_{\varSigma (\phi )}$ is the restriction of $\sigma$ that only replaces symbols that occur in $\phi$ and $\mathop {\textit{FV}}(\sigma )=\bigcup _{f\in \sigma } \mathop {\textit{FV}}({\sigma }{f(\varvec{\cdot })}) \cup \bigcup _{p\in \sigma } \mathop {\textit{FV}}({\sigma }{p(\varvec{\cdot })})$ are the free variables that $\sigma$ introduces. The uniform substitution $\sigma$ is admissible for $\phi$ (or $\theta$ or $\alpha$, respectively) iff all admissibility conditions during its application according to Fig. 1 hold, which check that the bound variables U of each operator are not free in the substitution on its arguments, i.e. $\sigma$ is U-admissible. Otherwise the substitution clashes so its result $\sigma ({\phi })$ ($\sigma ({\theta })$ or $\sigma ({\alpha })$) is not defined.

US is only applicable if $\sigma$ is admissible for $\phi$. In all subsequent results, all applications of uniform substitutions are required to be defined (no clash).

Fig. 1.

Recursive application of uniform substitution $\sigma$

3.1 Correctness of Uniform Substitutions

Let $I_{p}^{R}$ denote the interpretation that agrees with interpretation I except for the interpretation of predicate symbol p, which is changed to $R \subseteq \mathbb {R}$. Accordingly for predicate symbols of other arities, for function symbols f, and quantifiers C.

Corollary 1

(Substitution adjoints). The adjoint interpretation $\sigma _{\nu }^*I$ to substitution $\sigma$ for $I, \nu$ is the interpretation that agrees with I except that for each function symbol $f\in \sigma$, predicate symbol $p\in \sigma$, quantifier $C\in \sigma$, and program constant $a\in \sigma$:

If $\nu =\omega$ on $\mathop {\textit{FV}}(\sigma )$, then $\sigma _{\nu }^*I=\sigma _{\omega }^{*}I$. If $\sigma$ is U-admissible for $\phi$ (or $\theta$ or $\alpha$, respectively) and $\nu =\omega$ on ${U}^{\complement }$, then

$$\begin{aligned}{}[\![\theta ]\!]^{\sigma _{\nu }^*I}&= [\![\theta ]\!]^{\sigma _{\omega }^*I} ~\text {i.e.}~ [\![\theta ]\!]^{\sigma _{\nu }^*I} \mu = [\![\theta ]\!]^{\sigma _{\omega }^*I} \mu ~\text {for all}~\mu \\ [\![\phi ]\!]^{\sigma _{\nu }^*I}&= [\![\phi ]\!]^{\sigma _{\omega }^*I}\\ [\![\alpha ]\!]^{\sigma _{\nu }^*I}&= [\![\alpha ]\!]^{\sigma _{\omega }^*I} \end{aligned}$$

Substituting equals for equals is sound by the compositional semantics of $\mathsf {d}\mathcal {L}$. The more general uniform substitutions are still sound, because interpretations of uniform substitutes correspond to interpretations of their adjoints. The semantic modification of adjoint interpretations has the same effect as the syntactic uniform substitution, proved by simultaneous induction.

Lemma 5

(Uniform substitution lemma). The uniform substitution $\sigma$ and its adjoint interpretation $\sigma _\nu ^* I, \nu$ to $\sigma$ for $I, \nu$ have the same term semantics:

$$\begin{aligned}{}[\![{\sigma (\theta )}]\!]^{I}\nu = [\![{\theta }]\!]^{\sigma _{\nu }^{*}I}\nu \end{aligned}$$

Lemma 6

(Uniform substitution lemma). The uniform substitution $\sigma$ and its adjoint interpretation $\sigma _{\nu }^{*}I, \nu$ to $\sigma$ for $I, \nu$ have the same formula semantics:

$$\begin{aligned} {\nu }\in [\![{\sigma (\phi )}]\!]^I ~\text {iff}~ \nu \in [\![\phi ]\!]^{\sigma _\nu ^*I} \end{aligned}$$

Lemma 7

(Uniform substitution lemma). The uniform substitution $\sigma$ and its adjoint interpretation $\sigma _\nu ^*I, \nu$ to $\sigma$ for $I, \nu$ have the same program semantics:

$$\begin{aligned} (\nu , \omega ) \in [\![\sigma (\alpha )]\!]^I ~\text {iff}~ (\nu , \omega ) \in [\![\alpha ]\!]^{\sigma _\nu ^*I} \end{aligned}$$

3.2 Soundness

The uniform substitution lemmas are the key insights for the soundness of US. US is only applicable if the uniform substitution is defined (does not clash).

Theorem 1

(Soundness of uniform substitution). US is sound and so is its special case ${\text {US}_1}$. That is, if their premise is valid, then so is their conclusion.

4 Differential Dynamic Logic Axioms

Proof rules and axioms for a Hilbert-type axiomatization of $\mathsf {d}\mathcal {L}$ from prior work [6] are shown in Fig. 2, except that, thanks to rule US, axioms and rules now comprise the finite list of $\mathsf {d}\mathcal {L}$ formulas in Fig. 2 as opposed to an infinite collection of axioms from a finite list of axiom schemata along with schema variables, side conditions, and implicit instantiation rules. Soundness of the axioms in Fig. 2 follows from the soundness of corresponding axiom schemata [6], but would be easier to prove standalone, because it is a finite list of formulas without the need to prove soundness for all their instantiations. The rules in Fig. 2 are axiomatic rules, i.e. pairs of concrete formulas instantiated by US. Further, $\bar{x}$ is the vector of all relevant variables, which is finite-dimensional, or, in practice, considered as a built-in vectorial term. Proofs in the uniform substitution $\mathsf {d}\mathcal {L}$ calculus use US (and bound renaming such as $\forall {x}\,{p(x)}\leftrightarrow \forall {y}\,{p(y)}$) to instantiate the axioms from Fig. 2 to the required form. CT,CQ,CE are congruence rules, which are included for efficiency to use axioms in any context even if not needed for completeness.

Fig. 2.

Differential dynamic logic axioms and proof rules

Real Quantifiers. Besides (decidable) real arithmetic (whose use is denoted ), complete axioms for first-order logic can be adopted to express universal instantiation $\forall \hbox {i}$, distributivity $\forall \rightarrow$, and vacuous quantification $\hbox {V}_{\forall }$.

• $(\forall \hbox {i})$ $(\forall {x}\,{p(x)})\rightarrow p(f)$

• $(\forall {\rightarrow })$ $\forall {x}\,{(p(x)\rightarrow q(x))} \rightarrow (\forall {x}\,{p(x)} \rightarrow \forall {x}\,{q(x)})$

• $(\hbox {V}_\forall )$ $p \rightarrow \forall {x}\,{p}$

The Significance of Clashes. US clashes for substitutions that introduce a free variable into a bound context. Even an occurrence of p(x) in a context where x is bound does not allow mentioning x in the replacement except in the $\varvec{\cdot }$ places:

US can directly handle even nontrivial binding structures, though, e.g. from $[:=]$ with the substitution $\sigma =\{f\mapsto x^2, p(\varvec{\cdot })\mapsto [{{(z:=\varvec{\cdot }+z)}^*; z:=\varvec{\cdot }+yz}]{y\ge \varvec{\cdot }}\}$:

$$\begin{aligned} \textsc {us}\frac{[{{{x}:={f}}}]{p(x)} \leftrightarrow p(f)}{[{x:=x^2}]{[{{(z:=x{+}z)}^*;z:=x{+}yz}]{y{\ge }x}} \leftrightarrow [{{(z:=x^2{+}z)}^*;z:=x^2{+}yz}]{y{\ge }x^2}} \end{aligned}$$

5 Differential Equations and Differential Axioms

Section 4 leverages the first-order features of $\mathsf {d}\mathcal {L}$ and US to obtain a finite list of axioms without side-conditions. They lack axioms for differential equations, though. Classical calculi for $\mathsf {d}\mathcal {L}$ have axioms for replacing differential equations with a quantifier for time $t\ge 0$ and an assignment for their solutions $\bar{x}(t)$ [4, 6]. Besides being limited to simple differential equations, such axioms have the inherent side-condition “if $\bar{x}(t)$ is a solution of the differential equation ${{x}^{\prime }=\theta }$ with symbolic initial value x”. Such a side-condition is more difficult than occurrence and read/write conditions, but equally soundness-critical. This section leverages US and the new differential forms in $\mathsf {d}\mathcal {L}$ to obtain a logically internalized version of differential invariants and related proof rules for differential equations [5, 7] as axioms (without schema variables and free of side-conditions). These axioms can prove properties of more general “unsolvable” differential equations. They can also prove all properties of differential equations that can be proved with solutions [7] while guaranteeing correctness of the solution as part of the proof.

5.1 Differentials: Invariants, Cuts, Effects, and Ghosts

Figure 3 shows axioms for proving properties of differential equations (DW–DS) as well as axioms for differential substitutions ($[':=]$), and differential axioms for differentials (${+ ',\cdot ',\circ '}$). Axioms identifying $(x)'={x}^{\prime }$ for variables $x\in \mathcal {V}$ and $(f)'=0$ for functions f and number literals of arity 0 are used implicitly. Some axioms use reverse implications $(\phi \leftarrow \psi )\equiv (\psi \rightarrow \phi )$ for emphasis.

Fig. 3.

Differential equation axioms and differential axioms

Differential weakening axiom DW internalizes that differential equations can never leave their evolution domain q(x). DW implies³ ${[{{{x}^{\prime }=f(x)\,} \& {\,q(x)}}]{p(x)}} \leftrightarrow {[{{{x}^{\prime }=f(x)\,} \& {\,q(x)}}]{(q(x)\rightarrow p(x))}}$ also called DW, whose (right) assumption is best proved by G. The differential cut axiom DC is a cut for differential equations. It internalizes that differential equations staying in r(x) stay in p(x) iff p(x) always holds after the differential equation that is restricted to the smaller evolution domain ${\,} \& {\,q(x)\wedge r(x)}$. DC is a differential variant of modal modus ponens K.

Differential effect axiom DE internalizes that the effect on differential symbols along a differential equation is a differential assignment assigning the right-hand side f(x) to the left-hand side ${x}^{\prime }$. Axiom DI internalizes differential invariants, i.e. that a differential equation stays in p(x) if it starts in p(x) and if its differential $(p(x))'$ always holds after the differential equation ${{x}^{\prime }=f(x)\,} \& {\,q(x)}$. The differential equation also vacuously stays in p(x) if it starts outside q(x), since it is stuck then. The (right) assumption of DI is best proved by DE to select the appropriate vector field ${x}^{\prime }=f(x)$ for the differential $(p(x))'$ and a subsequent DW,G to make the evolution domain constraint q(x) available as an assumption. For simplicity, this paper focuses on atomic postconditions for which $(\theta \ge \eta )' \equiv (\theta >\eta )' \equiv (\theta )'\ge (\eta )'$ and $(\theta =\eta )' \equiv (\theta \ne \eta )' \equiv (\theta )'=(\eta )'$, etc. Axiom DG internalizes differential ghosts, i.e. that additional differential equations can be added if their solution exists long enough. Axiom DS solves differential equations with the help of DG,DC. Vectorial generalizations to systems of differential equations are possible for the axioms in Fig. 3.

The following proof proves a property of a differential equation using differential invariants without having to solve that differential equation. One use of US is shown explicitly, other uses of US are similar for DI,DE,[$':=$] instances.

Previous calculi [5, 7] collapse this proof into a single proof step with complicated built-in operator implementations that silently perform the same reasoning in an opaque way. The approach presented here combines separate axioms to achieve the same effect in a modular way, because they have individual responsibilities internalizing separate logical reasoning principles in differential-form $\mathsf {d}\mathcal {L}$.

5.2 Differential Substitution Lemmas

The key insight for the soundness of DI is that the analytic time-derivative of the value of a term $\eta$ along a differential equation ${{x}^{\prime }=\theta \,} \& {\,\psi }$ agrees with the values of its differential $(\eta )'$ along the vector field of that differential equation.

Lemma 8

(Differential lemma). If $I,\varphi \models {{x}^{\prime }=\theta \wedge \psi }$ holds for some flow $\varphi :[0,r]\rightarrow \mathcal {S}$ of any duration $r>0$, then for all $0\le \zeta \le r$:

$$\begin{aligned}{}[\![(\eta )']\!]^{I} \varphi (\zeta ) = \frac{\mathsf{d}[\![\eta ]\!]^I \varphi (t)}{\mathsf{d}t} (\zeta ) \end{aligned}$$

The key insight for the soundness of differential effects DE is that differential assignments mimicking the differential equation are vacuous along that differential equation. The differential substitution resulting from a subsequent use of $[':=]$ is crucial to relay the values of the time-derivatives of the state variables x along a differential equation by way of their corresponding differential symbol ${x}^{\prime }$. In combination, this makes it possible to soundly substitute the right-hand side of a differential equation for its left-hand side in a proof.

Lemma 9

(Differential assignment). If $I, \varphi \models {{x}^{\prime }=\theta \wedge \psi }$ holds for some flow $\varphi :[0,r]\rightarrow {\mathcal {S}}$ of any duration $r\ge 0$, then

$$\begin{aligned} I,\varphi \models \phi \leftrightarrow [{{{{x}^{\prime }\,}{:}{=}{\,\theta }}}]{\phi } \end{aligned}$$

The final insights for differential invariant reasoning for differential equations are syntactic ways of computing differentials, which can be internalized as axioms (${+ ', \cdot ', \circ '}$), since differentials are syntactically represented in differential-form $\mathsf {d}\mathcal {L}$.

Lemma 10

(Derivations). The following equations of differentials are valid:

$$\begin{aligned} (f)'&= 0&\text {for arity 0 functions/numbers}~f \end{aligned}$$

(1)

$$\begin{aligned} (x)'&= {x}^{\prime }&\text {for variables}~x\in \mathcal {V} \end{aligned}$$

(2)

$$\begin{aligned} (\theta +\eta )'&= (\theta )' + (\eta )' \end{aligned}$$

(3)

$$\begin{aligned} (\theta \cdot \eta )'&= (\theta )'\cdot \eta + \theta \cdot (\eta )' \end{aligned}$$

(4)

$$\begin{aligned} \left[ y :={\theta }\right] [{{{{y}^{\prime }\,}{:}{=}{\,1}}}] {}&\big ((f(\theta ))' = (f(y))'\varvec{\cdot }(\theta )'\big )&\text {for }y,{y}^{\prime }\not \in \theta \end{aligned}$$

(5)

5.3 Soundness

Theorem 2

(Soundness). The $\mathsf {d}\mathcal {L}$ axioms and proof rules in Figs. 2 and 3 are sound, i.e. the axioms are valid formulas and the conclusion of a rule is valid if its premises are. All US instances of the proof rules (with $\mathop {\textit{FV}}(\sigma )=\emptyset$) are sound.

6 Conclusions

With differential forms for local reasoning about differential equations, uniform substitutions lead to a simple and modular proof calculus for differential dynamic logic that is entirely based on axioms and axiomatic rules, instead of soundness-critical schema variables with side-conditions in axiom schemata. The US calculus is straightforward to implement and enables flexible reasoning with axioms by contextual equivalence. Efficiency can be regained by tactics that combine multiple axioms and rebalance the proof to obtain short proof search branches. Contextual equivalence rewriting for implications is possible when adding monotone quantifiers C whose substitution instances limit to positive polarity.