The bridge between logic and geometry - motivating the work of Olivia Caramello

There are several beautiful and profound foundational papers (many from the 1970s) on inituitionistic higher-order logic within the framework of topos theory. Papers by Lawvere, D. Scott, M. Fourman, G. E. Reyes and others which focus on the philosophical aspects of formal presentations of higher order intuitionistic logic inspired by the structure of elementary topoi: partial domains, sorts and types, definite descriptions, definability, non-classical truth values, the interpretation of bounded quantifiers, the axiom of infinity (NNOs), the Russell-Prawitz translation (Scott claims to have discovered this in the 50s), etc.
There is an elegant Hilbert-style formal presentation of intuitionistic higher-order logic employed by Fourman in his paper in the Handbook of Mathematical Logic.

In our paper "Hegel and Modern Topology" we proposed an interpretation of the the Logic of Concept wherein the stages of Subjective Concept and Objective Concept and their integration are interpreted in terms of the duality between theories and models (understood as a geometrically inspired category theoretic framework for general systems theory) and the problem of finding a bridge between the two - something which partakes of the essence of both, perhaps in the style of algebraic logic.

In the paper by Fourman he uses only the most rudimentary notions of category theory. The main result is that any (elementary) topos is equivalent (via a logical morphism) to the topos of a definitionally complete theory E(T) and that any theory T gives rise to a topos E(T). Thus the objects E(T) -  bearing in mind their universal property (theorem 8.9 in the paper by Fourman) - would seem to be a candidate for a bridge between theories and models. E(T) classifies models of T: there is a correspondence between models M of T and logical morphisms E(T) -> M.

But Fourman remarks (he terms it an "embarassement") that this still does not constitute a bridge between (higher-order) logic and geometry (i.e. Objective Concept), between theories and Grothendieck topoi and their geometric morphisms. Fourman mentions a paper by Reyes in which Grothendieck topoi are described in terms of adding to Set a "generic model" for a possibly infinitary first-order theory. 

As I see it some of the main problems with topos theory are the following:

1) Some of the toposes that I find most interesting, such as the Hyland's Effective Topos (a model of higher-order computable mathematics) are not Grothendieck toposes.
2) Even the Effective Topos still depends crucially on the category of sets (it is an enrichment of Set) - so it does not seem to provide in itself an alternative foundations for mathematics. However Fourman and Scott's theory of Omega-sets may provide a different perspective...
3) This needs to be checked, but I think that for a general topos with a Natural Number Object we cannot prove that there is no mono m: P(N) -> N. But for a Grothendieck topos the situation may be different...

A nice application of Grothendieck toposes is provided by Moerdijk and MacLane's treatment of forcing models in Sheaves in Geometry and Logic. I like to think of the underlying poset P as a kind of training data (partial information, not always consistent) and the construction of the sheaf model Sh(P) for the dense topology as analogous to models constructed by machine learning (a kind of passage to the limit, extrapolation and smoothing out of the data of P).

We have written in Ocaml a minimal proof assistant based on the logical system presented by Fourman in his paper The Logic of Topoi:

https://github.com/owl77/Intuitionistic-Higher-Order-Logic-and-Topos-Theory

Very short note on formal concepts in science

From whence do we get the impression that some mathematical models are closer to physical and spatio-temporal intuition,  more down to earth and intimately tied to concrete applications, while others hover close to the heights of allegedly less useful  'abstract-nonsense' ? The real numbers and differential equations, these are seen as tied to dynamic-geometric intuition and of vast applicability and interest in engineering and science.  But abstract algebra and category theory appear to have no direct relevance to applicable mathematical models or to their kind of concrete geometric-dynamic intuition. We present here a few short speculations.

Perhaps the abstract models do capture fundamental levels of reality (maybe even more fundamental than the so-called concrete spatio-temporal ones) and what is required is first of all the methodic development of a special kind of intuition or cognition to grasp the planes of reality which they model (maybe something like Goethe's method is called for?). And then further models are required which can effect a mediation or transfer between these two levels, or at least allow a continuity or gradual deformation between concrete spatio-temporal reality and higher levels of reality.

A beautiful illustration of such a meditation and construction is furnished by the double fibration in Penrose's twistor theory which allows a mediation and transfer between physically significant objects on Minkowski space and abstract cohomological objects on the complex algebraic variety $\mathbb{P}^3$.This operation allows solutions to conformally invariant differential equations on spacetime (e.g., Maxwell's equations, Yang-Mills, or linearized gravity) to be identified exactly with Cech or Dolbeault cohomology classes on specific regions of twistor space. This appears to have been Penrose's attempt to give a geometric (topological) interpretation of quantum non-locality. 

Another illustration is the theory of $\mathcal{D}$-modules which presents a mediation between derived categories (and monoidal categories) and concrete models of systems of partial differential equations.

The idea of Kant's schematism of the pure concepts of the understanding can be interpreted as finding the mediation between logic and geometry (including mathematical physics). This is of immense contemporary significance as we find versions of Kantian schematism in topos theory, homotopy type theory and in areas involving monoidal categories in algebra, geometry and physics and in linear logic and computer science. 

There is also apparently a mediation and transition between the theory of bifurcations of smooth vector fields, fundamental  and ubiquitous in concrete applied mathematics,  and monoidal category and operad theory. See also Physics, Topology, Logic and Computation: A Rosetta Stone by John C. Baez and Mike Stay.

An objection can be raised that our concrete allegedly intuitive mathematical models are themselves quite abstract but are only perceived as immediate and intuitive in our present cultural context by a deliberate forgetting of the complexity of their cognitive-historical past and genesis. For instance real numbers are constructed from the rationals by quite abstract, cardinality increasing, procedures involving equivalence classes and identification. And the same goes for the concepts of continuity, differentiability and so forth. Surely the ancient Greeks had other forms of intuitive perception and concreteness in their geometry, physics and engineering. We answer this objection by our arguments that the fundamental dynamic and geometric-topological intuitions of modern science were in fact identical to those of ancient Greece. It is the modern foundations in terms of Dedekind cuts and $\epsilon$s and $\delta$s that can be critiqued from a philosophical and logical point of view and alternative foundations (locales, realizability topoi, synthetic differential geometry, homotopy type theory) can be defended which are also more aligned to the theory of space and change found for instance in Aristotle's Physics.