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 and then . For an arbitrary commutative ring , 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 is a ring of polynomials of some variety . For each element and the evaluations are elements of a field, and so if and then . It follows that for any ideal in if and then . Finally, by Nullstellensatz this is the same as saying that if then , an purely algebraic fact that can be proven for an arbitrary commutative ring .
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 is equivalent to since the schemes corresponding to these equations are different.
Perhaps this can be reconciled if we work in a logic where is not equivalent to . Then we can say that implies , but the former is not implied by . Indeed we do not have such an implication for the multiplicative conjunction 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.