In a logical system (which may or might not be the first order logic system), given a set $\Phi$ of formulas (or sentences),
is there a name for $\{\text{formula }\phi\text{ | }\Phi \models \phi \}$?
is there a name for $\{\text{formula }\phi\text{ | }\Phi \vdash \phi \}$?
Are they both called the "theories" of $\Phi$?
Is $\Phi$ called a set of axioms of the two?
Some thoughts and observations:
The set of formulas satisfied by a structure is called the theory of the structure. (somewhere in Ebbinghaus' logic book.)
On p111 In Enderton's logic book, if $Φ⊢$, then $$ is called a theorem of $Φ$.
On p128 in Enderton's book, "Such a book would first state the logical axioms and the rules of inference and would explain that they are acceptable to reasonable people. Then it would proceed to show that many formulas were deducible (or deducible from certain nonlogical axioms, such as axioms for set theory)."
Is it correct that a theory is a set of theorems, and a theorem is a member of some theory or theories?
Thanks.
To make this question most significant, we want to work with a notion of "logical system" more-or-less along the following lines: a tuple $(Sent, \models, \vdash)$ where $\models$ is a relation between structures and sentences, $\vdash$ is a relation between sets of sentences and sentences, and $\models$ and $\vdash$ need not be connected by a completeness theorem (that is, it need not be the case that $\Gamma\vdash\varphi$ iff for every $\mathcal{M}$ with $\mathcal{M}\models\gamma$ for each $\gamma\in\Gamma$ we have $\mathcal{M}\models\varphi$).
The relevant term is "deductive closure." When $\models$ and $\vdash$ coincide (e.g. with first-order logic) there's nothing more to say. However, when $\models$ and $\vdash$ don't coincide - or are not known to coincide at this stage in the argument - this terminology has to be elaborated on. I don't think there's a standard terminology here, but here are the usages I've heard:
"Deductive closure" for the $\vdash$-version and "entailment closure" for the $\models$-version.
"Semantic deductive closure" and "syntactic deductive closure" for the $\models$-version and $\vdash$-version, respectively.
Re: your suggested terminology, "theory" is often used to refer to any set of sentences (or even formulas sometimes), so it would of course be inappropriate for this. When we add a closure condition, we can indeed talk about $T$ being generated by $\Gamma$ and we can talk about $\Gamma$ axiomatizing $T$. (We can do the latter using the looser meaning of "theory" too: we can say that $T_0$ axiomatizes $T_1$ iff they have the same deductive closures.)
However, we still have to distinguish between $\vdash$ and $\models$: does "theory" mean "$\vdash$-closed" or "$\models$-closed?"
Since the vast majority of logic takes place in the first-order context where we do have a completeness theorem, and more generally in logics whose $\models$ and $\vdash$ coincide, this point is largely ignorable; when it's important, my experience is that there is no really standard terminology and texts have to specify what language they're using.