stratification (typage) of logic and syntax at the same time: is such a dream feasible? This post is more philosophical than formal, yet I think it's an important question.
There's an idea I have for long times already that would consist, in some sense, in doing a "theory of theories". What I mean by that, is a (semi)-formal system in which all meta-thinking would be internalized, and could even be studied more or less formally.
This "framework" would, in some sense, be a theory of the process of abstraction (or say, a formalization of it). Let me explain the motivations.
Call foundational formal theory (FFT) any system consisting of a collection of formal rules about syntax, some axioms and logic. If one calls natural language $\mathcal{N}_0$, an FFT $\mathcal{F}$ can be seen as a formalization of "some ideas" of natural language. Call $\mathcal{N}_0$-ideas such ideas of natural language (for example, the idea of set, the idea of membership, the idea of relation, or even the idea of chair and computer, $\ldots$) 
Example: ZF(C) is a foundational formal theory that is trying to formalize the $\mathcal{N}_0$-ideas of "collections" and binary relation of "membership" $\in$.
On the contrary, category theory seen as an FFT (not well founded as far as I know) is a formalization of the $\mathcal{N}_0$-idea of composition. 
Note that it is really important to understand that an FFT is internalized inside a natural language $\mathcal{N}_0$. Indeed, an FFT is never defined formally because it is constructed and expressed with $\mathcal{N}_0$-ideas. It allows us to do formal work, but it involves some choices at some points, and these choices are arbitrary (for formalists), or philosophically motivated to make sense of some "real life" phenomenon (where I put everything related to concepts into real life).
In this respect, if $\mathcal{F}$ is constructed with a language $\mathcal{L}$, a logic $\mathcal{I}$, and some formal axioms $\mathcal{A}$ expressed within the language $\mathcal{L}$, then one has to understand that $\mathcal{L}$, $\mathcal{A}$, and $\mathcal{I}$ expressed more or less with $\mathcal{N}_0$-ideas in order to construct $\mathcal{F}$. 
Now that $\mathcal{F}$ is constructed, one could give this formal system to a computer and demonstrate all the properties of the objects described by $\mathcal{F}$. Still, this way of doing mathematics is not at all what people are doing because it is
1) pure phenomenology of $\mathcal{F}$ that does not explain anything,
2) brute forcing and won't work in any case (not speaking about incompleteness).
What people usually do, is trying to make sense of the "phenomenon" described by $\mathcal{F}$. In this respect, people are going to define $\mathcal{L}$-ideas in order to make sense of the objects of $\mathcal{F}$, and try to demonstrate some of their properties by using the axioms $\mathcal{A}$ and the logic $\mathcal{I}$.
An $\mathcal{L}$-idea can be seen as an idea over $\mathcal{F}$. It is perfectly conceivable that some expressible ideas in $\mathcal{L}$ have no models in $\mathcal{F}$, but would the idea be meaningless? Syntax allows it, so it's damn meaningful.
Now, what people do is even more than that. They also define theories over $\mathcal{F}$ in order to explain what happens inside $\mathcal{F}$. If an FFT is a level-0 theory, people are going to define level-1 theories over this FFT, using only the objects/definitions of $\mathcal{F}$ and their properties.
Example: if ZFC is an FFT, we know that it admits, for example, the integer $(\mathbb{Z},+,0)$ constructed explicitly, or some $S_n$. Then, group theory would be a level-1 theory over ZFC whose purpose is precisely to abstract the phenomenon encountered in the "daily life" of ZFC. That is, to explain them. 
Similarly, topology would also be a level-1 theory over ZFC. Now, these level-1 theories  come with their ideas and properties. It is in my opinion dishonest to consider that a property of group theory (seen as a level-1 theory over ZFC) has the same status as a property of ZFC. In this respect, one would want to type syntax and would want to have level-0 definitions and propositions that belongs to some FFT (say, ZFC), that are distinct to level-1 definitions and propositions belonging to some level-1 theory over ZFC (and so on). 
One could even be tempted to define topological group theory, not as a theory over group theory and topology, but as some sort of "pushout" of them (if it makes sense because definitions are now typed).
Anyway, the important thing to notice is the stratification of abstraction. Starting with an FFT seen as a level-0 theory, to abstract is to see the ideas of such an FFT as objects by "creating" a level-1 theory over it, whose purpose is to make sense of them. These level-1 ideas over such an FFT produces, in their turn, some "phenomenon" we would like to understand too. We are therefore always free to create a level-2 theory that is both above the FFT and the previous level-1 theory in order to explain these phenomenon that were hard to see without our level-1 theory. This might continue up to infinity. There's indeed no reason to believe that being an idea or being an object is an objective distinction free from any theory (for the ones who like philosophy, it might help to see an object as an idea on which we glued "the idea of being an object", so it's all ideas and the ideas we put on them). 
The ideas/objects of a level-$n$ theory takes as objects the $m$-ideas/objects with $m < n$ that are under it. It would therefore be necessary to type both the objects and the syntax (they are actually the same thing. What we call the integers in an FFT, say ZFC, are nothing else than pure syntax).
One would also want to be able to make $n$-propositions about the $m$-propositions with $m < n$. Indeed, it is striking that first order theory can't make formal such sentences as "If $F$ is a closure operator that preserves some proposition $P$, then ..." while such phenomenon are encountered everywhere (Clearly, to avoid being crushed by diagonal argument, one needs to stratify syntax). One would maybe want to quantify over variables in order to make sense of syntactic phenomenon : this is impossible in FOL.
One might also want to see  formally what happens if we take proposition P of say, group theory, that starts with a quantifier $\forall$ and substitute it with a $\exists$. That is, one would like meta-mathematics to be formalizable explicitly. This requires stratification of syntax. 
In such a framework, the existence of a model from a level-$n$ theory to a level-$m$ theory with $m < n$ would be nothing else than the existence of a morphism that preserves (some) syntactic/logical operations (some sort of morphism of syntax). 
In particular, one would like to be able to see how the level-$n$ theories that are not necessarily comparable for the relation of being above interacts (if it makes sense).
Anyone knows if there are some work done in this respect? Feel free to discuss any of these philosophical ideas and their feasibility.
PS for the philosophers: if the goal of maths is to find deeper and deeper FFTs (that are able to describe more and more mathematical things in a clearer and deeper way), considering that any FFT is a theory over a natural language $\mathcal{N}_0$, shouldn't we look for a deeper and deeper natural language to begin with?
edit: Some precisions about the need to stratify syntax from scratch: if my foundational formal theory $\mathcal{F}$ is built up from a language $\mathcal{L}$, a logic $\mathcal{I}$ and some axioms $\mathcal{A}$, then the propositions described by the internalization of $\mathcal{I}$ inside $\mathcal{F}$, say $\mathcal{I}_\mathcal{F}$, are by no mean the same thing as the propositions of $\mathcal{F}$. 
If $Prop(\mathcal{F})$ denotes the “collection” (in natural language) of propositions of 
$\mathcal{F}$, then it is by no mean trivial that Prop(analytic theory with logic $\mathcal{I}_\mathcal{F}$, axioms $\mathcal{A}$ + something and language $\mathcal{L}$ with underlying FFT $\mathcal{F}$) is equivalent to $Prop(\mathcal{F})$.
Example: a group object in Grp is necessarily abelian. Thus, one shouldn’t trust such internalizations. One needs a way to speak “naturally” of $Prop(\mathcal{F})$ as a theory over $\mathcal{F}$ that comes from scratch with $\mathcal{F}$. (Then, one could also make sense of $PropProp(\mathcal{F})$, and so on…)
One could even be tempted to believe that some proofs of incompleteness are just a result of such internalization process (please, don't think that I want to deny Godel's theorems, thanks).
 A: Some precisions about my claim that internalization procedure might fool us about what "really" is our theory.
An FFT $\mathcal{F}$ is defined inside natural language. So is the logic $\mathcal{I}$ you're "associating" with it. An FFT is defined by some string of symbols one can write explicitly on some piece of paper. The propositions one can show about this theory are the propositions one can write on a piece of paper manipulating these strings of symbols explicitly too. Let us call "writable" what one can write explicitly on a piece of paper (where by explicit we really do mean explicitly, with no abuse of notations or shortcut).
Call $Prop(\mathcal{F})$ the "collection" of writable propositions of $\mathcal{F}$ (those are nothing else than the potential propositions one is able to write down). If $\mathcal{F}$ is strong enough, it can internalize its own logic and syntax, call it $\mathcal{I}_F$. One can then show some propositions satisfied by $\mathcal{I}_F$. Yet, the previous propositions are by no mean the same as $Prop(\mathcal{F})$ for the simple reason that to show them, one will usually quantify over all natural numbers. Quantification over all natural number is "too strong", because most integers are actually non writable (indeed, one would need more energy, space, and time, than what is actually accessible from us in real life). 
Therefore, it is totally conceivable that many propositions one is going to show (or that fails) about $\mathcal{I}_F$ using a quantification over the integers doesn't belong at all to $Prop(\mathcal{F})$. Quantification clearly sees "way too far" (in the length of the formula) as what is actually possible to write down for real. 
As an example, one could even conclude that Godel incompleteness theorems are a "bug" resulting from this too strong quantification over all natural numbers. By seeing "too far" that what is actually writable, we have to conclude that there are formula one could never prove. One could believe (not firmly) that incompleteness doesn't hold for the collection of writable propositions $Prop(\mathcal{F})$. 
PS: I believe that incompleteness is a fact of formal systems, but the way it is proven doesn't convince me anymore. It is a necessity to build a theory of theories in which such proof would be much more convincing (we don't want to internalize the syntax and logic inside the FFT we are considering. This way of doing thing is really bad for two reasons: 
1) quantification allows you to see too far that what really makes sense
2) it loses information: a group object in Grp is necessarily abelian.)
A: Let us consider category theory as a (non well founded) model of the idea I have of a theory of theories. See any category with some good properties as a foundational theory (maybe a topos?).
We are going to define formally what is a definition, and a printing.
Definition (Formal definition of level $1$): A formal definition of level 1 is a finite $1$-category
Ex: Let us define $Def_1(Prod)$ as the category with diagram $A \leftarrow A \times B \rightarrow B$, where the arrows are interpreted as projections, and where we also add universal arrows (the diagonal) and a terminal object $1$. We can also define $Def_1(coProd)$ as $Def_1(Prod)^{op}$. 
One can also define $Def_1(Grp)$ as the category that is nothing else (and almost no more) than the diagram of a group object where we also add all the universal arrows coming from the different products.
Definition (printing of level 1): A printing of level 1 is a (co)limit (maybe more?) preserving 1-functor from a finite 1-category to any category $\mathcal{C}$.
Ex: A printing of level 1 of a group of level 1 is a functor $F: Def_1(Grp) \rightarrow \mathcal{C}$ that is a functor with group object image in $\mathcal{C}$.
A printing of $Def_1(Prod)$ is a functor with product image in $\mathcal{C}$.
One could also define the category of all printing to a category $\mathcal{C}$ and interpret them as all "representations"/"models" in $\mathcal{C}$, and where morphisms are obviously natural transformations.
Now, let us interpret FinCat as the 2-category of all formal definitions of level $1$. Call it $1$-Def.
Definition (Homomorphism of definitions of level 1): An homomorphism of two formal definitions of level 1 $Def_1(A)$ to $Def_1(B)$ is a functor from $Def_1(A)$ to $Def_1(B)$.
Definition (Equivalence of definitions): Two formal definitions of level 1 are equivalent iff they are equivalents as 1-categories in $1$-Def.
Ex: Let $Def_1(Grpd$ $of$ $one$ $object)$, seen as the diagram of an internal category with $C_0 = 1$ the terminal object. One can show that this category is equivalent with $Def_1(Grp)$.
Definition (fusion of level 1): Let $Def_1(A) \leftarrow Def_1(B) \rightarrow Def_1(C)$ be three formal definitions. Their pushout in 1-Def is said to be a fusion of $Def_1(A)$ and $Def_1(C)$.
Ex: The fusion of $Def_1(Prod)$ and $Def_1(coProd)$ is $Def_1(biProd)$, where we glue $A$, $B$, and $A \times B$ to $A$, $B$ and $A +B$, 1 to 0, with obvious injection functors.  To show: the fusion of $Def_1(Grp)$ with $Def_1(coGrp)$ is $Def_1(biGrp)$.
Definition (compatibility of level 1): Let $Def_1(A) \rightarrow Def_1(B) \leftarrow Def_1(C)$ be three formal definitions of level 1. Their pullback in 1-Def is said to be a compatibility of $Def_1(A)$ and $Def_1(C)$.
Ex: One can do an axiom removal of level 1 by taking an equalizer (still in Def-1) between, say, the identity functor $Id : Def_1(Grp) \rightarrow Def_1(Grp)$ to $Rmv$(Associativity) $: Def_1(Grp) \rightarrow Def_1(Grp)$ that is sending the associativity square to $G \leftarrow G \times G \leftarrow 1 \rightarrow G\times G \rightarrow G$.
Definition (formal definition of level 2): A formal definition of level $2$ is a finite 2-subcategory of 1-Def seen as a 2-category.
Definition (formal homomorphism of level 1): A formal homomorphism of definition of level 1 is a definition of level 2 whose diagram is $A \rightarrow B$. We call it $Def_2(Homomorphism$ $of$ $1-Def)$.
One could then create the 3-category 2-Def whose objects are formal definitions of level two and arrows are 2-Functors.
Definition (homomorphism of level 2): An homomorphism of level two is a 2-functor in 2-Def.
One could continue like that and discriminate each layers of definitions to study them formally, for example, formal printing of level 1, then printing of level two, formal natural transformation of level two, formal printing of level two, $\ldots$.
Note that in this framework, one has to discriminate the "natural ideas" (in the sense of primitive and defined at the foundations of the theory, not inside) like functors, natural transformations, $n$-category, to their formal definitions.
In particular, I'll try to edit this post in order to show that there exists an operation of specification that allows to go to the lower layer of definitions.
Indeed, informally a groupoid with one object can be said to be a $Def_0(Grp)$, that is, the level 0 definition of what is a group because it depends on "elements". There must exists a link between Def_n(Grp) and Def_{n-1}(Grp). Hence, once would have an operation that shows you at which layer of " algebraic deepness" the definition relies. Level 0 definitions are "element wises", they are dumb and bad. Level 1 definitions are purely algebraic, they are good. Higher algebra definition might be even better.
produit d'une $Def_1(A)$ avec $Def(0 -> 1)$
