Linear Logic, Topos Theory, and Algebraic Geometry

Note: The stuff below is some idle thought without much backing to it and extremely speculative. Don’t take it seriously.

Something seems right about linear logic: Both classical logic and intuitionistic logic embed in it, and although sequent calculus loses duality symmetry going from classical logic to intuitionistic logic this symmetry is regained in linear logic. It seems to me like intuitionistic logic is more fundamental than classical logic, and although there’s no good theory for how to fully do mathematics in linear logic (as Bishop did in intuitionistic logic), I suspect that linear logic is more fundamental still.

The category of sheaves over a topological space or a site is a model of intuitionistic set theory. Conversely, given a model of intuitionistic set theory we can try to interpret it as being a category of sheaves over some kind of space. We can construct a dictionary of logical equivalents of geometric concepts and vice versa. This is the core idea of topos theory. If linear logic is more fundamental than intuitionistic logic then a natural generalization of this idea is to geometrically interpret models of linear dependent type theory to get a more general notion of space. As far as I’m aware a good theory of linear dependent type doesn’t exist yet.

A speculative idea I have for how to apply this is that it can reconcile to conflicting intuitions in algebraic geometry: On one hand, algebra laws over a field say that if a \neq 0 and b \neq 0 then a b \neq 0. For an arbitrary commutative ring R, even though this statement is no longer true it is still sometimes useful to think of it as holding in some “local” sense. For example, suppose R is a ring of polynomials of some variety X. For each element x \in X and f, g \in R the evaluations f (x), g (x) are elements of a field, and so if f (x) \neq 0 and g (x) \neq 0 then f (x) g (x) \neq 0. It follows that for any ideal I in R if V (I) \subseteq D (f) and V (I) \subseteq D (g) then V (I) \subseteq D (f g). Finally, by Nullstellensatz this is the same as saying that if I + (f) = I + (g) = R then I + (fg) = R, an purely algebraic fact that can be proven for an arbitrary commutative ring R.

On the other hand, scheme theory makes use of nilpotent elements of a ring and these elements contain significant geometric information. That is, we cannot say that x^2=0 is equivalent to x=0 since the schemes corresponding to these equations are different.

Perhaps this can be reconciled if we work in a logic where P \land P is not equivalent to P. Then we can say that x \neq 0 \land x \neq 0 implies x^2 \neq 0, but the former is not implied by x \neq 0. Indeed we do not have such an implication for the multiplicative conjunction \land of linear logic. So maybe the right way to think of a scheme with nilpotent functions over it is as a space where the logic over the space is intrinsically linear.