I'm sorry if my question looks stupid or does not make sense. However, I want to ask if it is normal/common to have a global state, which is shared by all inference rules, in a Gentzen-style proof system?
In particular, the inference rule may maintain a local state L and a global state G. Any update to the local state L of a rule is local only in the scope of this rule and the sub proof tree derived from this rule. Any update to the global state G in a rule can be accessed by other rules as well.
For example, G and L are illustrated in the following Cut rule,
where an update that adding C to L ∪ {A} is local and perceptible.
G, L ∪ {A} ⊢ C G, L ∪ {A,C} ⊢ B
---------------------------------- Cut
G, L ∪ {A} ⊢ B
Let say if this rule is used inside a proof tree, and I also want to update C to G, so that the new G can be used in other part of a proof tree, is this possible to do it?
In particular, in the following proof tree, I want to update C into G of the Cut rule, to have an updated G* and this G* can be used later to in the application of Rule2. Does this make sense when doing this?
G*, L ∪ {A} ⊢ C G*, L ∪ {A,C} ⊢ B G*, L ∪ {A} ⊢ E
------------------------------------ Cut ----------------- Rule2
G, L ∪ {A} ⊢ B G, L ∪ {A} ⊢ E
----------------------------------------------------------------- Rule1
..... something here ........
If I get you right, then what you refer to as global state is usually just called an axiom system. Such an axiom system is simply a set of formulas, which are assumed to hold without any further proof needed. Now if we have a sequent $$ \Gamma_0 , \Gamma \to \Delta $$ where $\Gamma_0$ is a sequence of formulas from an axiom system $G$, then we say that $$ \Gamma \to \Delta $$ is provable from $G$ in $\mathbf{LK}$. An interesting fact, by the way, is that $\Gamma_0 , \Gamma \to \Delta$ is provable in $\mathbf{LK}$ if and only if $\Gamma \to \Delta$ is provable in $\mathbf{LK}_G$, which is the $\mathbf{LK}$ extended with axiom $\to g$ for each formula $g \in G$.
If you want to know more about this, then check out section 4 in part 1 of the book about proof theory by Takeuti: http://www.amazon.com/Proof-Theory-Dover-Books-Mathematics-ebook/dp/B00FAUEB32/ref=sr_1_1?ie=UTF8&qid=1460709504&sr=8-1&keywords=takeuti+proof+theory
I'm not entirely sure what you mean with your last paragraph, but note that an axiom system cannot be altered within a proof.
Hope this helps anyway!