# Differential equations → predicate logic mapping

I was watching Tom LaGatta's talk on category theory recently, and one of the audience brought up a statement that caught my attention (around the 56:15 mark):

I was gonna say, there was a book I read, and they claim that some fella discovered there was a functor between differential equations and [...] logic with quantifiers.

I tried searching for some pointers in Google, MO and nLab, but came up with nothing relevant. Does anyone have any idea what result specifically he was talking about?

• Also, I wasn't sure whether to post this on math.SE or here, so please, do correct me if it's not appropriate here. – Matěj G. Apr 14 '16 at 20:09
• How do these things even form a category? – Thomas Rot Apr 14 '16 at 21:26
• @MatějG. I think this is far above the limit of "research level", and it definitely belongs here. – Amir Sagiv Apr 16 '16 at 9:04

Very roughly sketching SDG and considering only first-order (autonomous) ordinary differential equations, we model the "real line" as a rig object $R$ in our (Grothendieck) topos, $\mathcal{E}$, and we characterize a subobject of $R$, $D$, via the following axiom (the simplest form of the Kock-Lawvere axiom): the map $(x,y) \mapsto (d \mapsto x + dy) : R^2 \to R^D$ is an isomorphism. In particular, we can write the inverse map as $f \mapsto (f(0), f'(0))$. We think of the elements $d \in D$ as the elements of $R$ such that $d^2 = 0$. We see that every map in $D \to R$ is affine. (Objects which have this property are generally called "microlinear" which includes any powers of $R$.) The tangent bundle of $X$ is represented by the arrow $\pi_X \equiv f \mapsto f(0) : X^D \to X$. A vector field (i.e. an autonomous first-order ODE) on $X$ can be viewed as an arrow $v : X \to X^D$ which satisfies $v(x)(0) = x$. We can form the category of $(-)^D$-coalgebras (not comonad coalgebras) and the category of vector fields will be a subcategory of that, namely coalgebras that are sections of $\pi$.
As a generality, the category of coalgebras for a right adjoint endofunctor on a Grothendieck topos is itself a Grothendieck topos and has an essential geometric surjection from the base topos to it. Now here's where things get interesting. In (at least some forms of) SDG, $(-)^D$ has a right adjoint written $(-)^{\frac{1}{D}}$. To get the category of 1ODEs to be a Grothendieck topos, we need to show that the subcategory they correspond to is still a Grothendieck topos. In the fractional exponents paper, this is done by proving a general result (Theorem 2) about certain equifiers. Second order ODEs arise from arrows $X^D \to X^{D_2}$ for which we use the transpose $X \to X^{D_2/D}$ and then essentially the same argument. Grothendieck toposes enable geometric logic, so categories of 1ODEs and 2ODEs (as well as the underlying topos $\mathcal{E}$) support finitary conjuction, infinitary disjunction, and existential quantification in a way that will be preserved by the inverse image functor of the geometric surjection. Grothendieck toposes are also elementary toposes and so support additionally universal quantification and implication (and are models of an intuitionistic set theory), but this additional structure won't be preserved by geometric morphisms. (As an aside, elementary toposes also support a dependent product type and (global) sections of bundles are just global elements of dependent products, i.e. a vector field on $X$ is a (global) element of $\prod x\!:\!X.\{ f : X^D\ |\ f(0) = x \}$ using a type theoretic notation.)
• @MatějG. So there are, at least, three things going on. The logical formulae in the internal language of the topos that 1/2ODEs form are, like everything in the topos, ODEs and maps between them, in exactly the CH way. There's also a mapping of 1/2ODEs into $\mathcal{E}$ which has it's own internal language with quantification. Finally, as I alluded to at the end, if we take the right adjoint of pullback along the unique map $X\to 1$ and apply it to the tangent bundle $\pi_X : X^D\to X$, we get a "type" of vector fields on $X$ (including the section constraint!). – Derek Elkins left SE Apr 19 '16 at 3:28