I am working on a framework for metamathematics which uses structures of type (U, F, R), to which I refer as "universes" (short for "universe of discourse"), where U is a collection called "support" (or, better, "basis" so that one can say that the universe in "based on" U), F is a subcollection of U called "foundation", and R is a binary relation on U called "reduction" relation. Sure, all three notions are correlated with the universe, like this: "support/basis of universe", "foundation of universe", "reduction relation of universe".
This structure captures what is essential for this research from both axiomatic theories and (maybe) from universes of discourse, treated on the same footing. Here are 2 examples of universes.
The universe of discoure of a set theory with atoms: foundation is the set of atoms and reduction is membership, or inverse to membership
A universe based of the set of lists of formulas of an axiomatic theory, with the list of its axioms as foundation, and a list L is considered as reducible to another list L' iff the sequent L -> L' is deducible in this theory. The theory is supposed to be based on a sequent calculus - in would be more difficult to capture what is called here "universe" from a theory based on a Hilbert-style presented calculus.
The collection U\F is very often used in discourse and it would be really useful to have a term for it.
To refer to U\F as "superstructure of F" does not sound correct because this is a collection and not a "structure".
To call U\F "co-foundation" is not correct, since in precise terms, "co-foundation" is a sub-collection of U\F.
Once I called "basis" the collection F, which I call now "foundation", and referred to U\F as "over-basis" (which is similar to ""overbase"/"base"). But there is a reasons why "foundation" is a better term for "F" than the term "basis" -- the notion "basis" seems to be mostly used with the meaning "basis of generators", and thus, this term implies that the elements of U\F are all reducible to elements of F (which is not true for all universes - this is not true for what I call "non-well-founded" universes).
Since "theorems" are the things which reduce to axioms, one would try to figure out a new term for U\F proceeding from the term "theorem" (versus "axiom"), but the use of this term presupposes that the discussion is only about theories and, also, an axiom is also a theorem (and is there a term with meaning "theorem, which is not an axiom"!?). To coin a term proceeding from the word "theorem" applicable to U\F for a universe of discourse of a set theory does not seem possible, since what kind of class could be called something close in meaning with "theorem"!?
Would really appreciate a good term for U\F and any critical comments on other terms. Also, I would mention your name as credits for a good term in a paper I am working on.