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

1 Answer 1


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!

  • $\begingroup$ Thank you very much for the recommendation. I will check out the book! :-) $\endgroup$
    – Trung Ta
    Apr 17, 2016 at 5:36

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.