First some definitions to make it clear what I'm talking about:
A deductive system is a set $J$ of judgments together with a set $R$ of inference rules each of the form $ j_0 \leftarrow j_1, j_2, \ldots, j_k \qquad\qquad(k\ge 0)$ where $j_0$ is a judgment called the conclusion of the rule and the other $j_i$s are premises.
(For my present purposes I'm not interested in the internal structure of judgments, though it is usual to assume that $J$ is a easily recognizable formal language over some alphabet and that $R$ is a the union of finitely many easily decidable subsets of $J\times J^*$. An "axiom" in this definition is just an inference rule with zero premises).
When $A$ is any (possibly infinite) set of judgments and $j$ is some judgment, we say that $j$ can be derived from A, written $A\vdash j$ iff there is a finite sequence of judgments ending with $j$, such that each element in the sequence is a member of $A$ or is the conclusion of a inference rule whose premises all appear earlier in the sequence. (In the notation $A \vdash j$ we can write $A$ as a list without set brackets, so in particular "$\vdash j$" means $\varnothing\vdash j$.)
(Equivalently, $A\vdash j$ if there is a tree (or pointed dag) whose interior nodes are labeled with (concrete) inference rules and leaves with elements of $A$, and the edges connect premises with conclusions in the obvious way, and the root concludes $j$).
This framework works well to describe Hilbert-style logics. Then the "judgments" are just well-formed formulas, and the inference rules are all instances of modus ponens, the logical axioms, primitive rules for quantifiers and so forth. If we have a particular theory in the logic, we have a choice between elevating its non-logical axioms to nullary inference rules (thus fusing the logic and the theory into a single deductive system), or to put the set of non-logical axioms to the left of the turnstile and saying that $\phi$ is a thorem iff $T\vdash\phi$ in the deductive system of pure logic.
The framework also allows natural deduction (with environments) or sequent calculus to be deductive systems. In the latter case the judgments are sequents, and the majority of inferences rules are not axioms. But there is a notational problem here, because sequents themselves are written with a turnstile symbols, which clashes with the above use of a turnstile to assert the existence of a formal proof for a judgment.
My question: Is there a well-established symbolic way to distinguish between "outer" turnstiles that assert that some judgments can be derived from other ones, and the "inner" turnstiles that are "just punctuation" in the syntax of sequents? Are there better words to explain the difference between these two roles than the long cumbersome description I've given here?
As one example of what I'd like to express, suppose that we write the outer turnstiles as $\Vdash$. Then we could speak about a "meta-deduction theorem" for sequent calculus:
$\Vdash (\Gamma, \phi \vdash \psi)$ if and only if $(\Gamma \vdash \phi)\Vdash(\Gamma \vdash\psi)$.