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?
I'm not sure what "book" prompted them to say this, but the ideas sound like the ideas from Synthetic Differential Geometry (SDG) (see also Synthetic Geometry of Manifolds) and Fractional Exponential Functors and Categories of Differential Equations, and the "fella" was probably Anders Kock (probably via Bill Lawvere). Lawvere has a brief, informal set of seminar notes that sketches the idea (unfortunately the PDF is somewhat broken) and led to the fractional exponential functors paper.
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.)
