# Gentzen-style proof system with global states?

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$.