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