On Different Intuitionistic Calculi and Embeddings from Int to S4 |
| |
Authors: | Egly Uwe |
| |
Affiliation: | (1) Institut f[uuml, TU Wien, Favoritenstr. 9-11, A-1040 Wien, Austria |
| |
Abstract: | In this paper, we compare several cut-free sequent systems for propositional intuitionistic logic Intwith respect to polynomial simulations. Such calculi can be divided into two classes, namely single-succedent calculi (like Gentzen's LJ) and multi-succedent calculi. We show that the latter allow for more compact proofs than the former. Moreover, for some classes of formulae, the same is true if proofs in single-succedent calculi are directed acyclic graphs (dags) instead of trees. Additionally, we investigate the effect of weakening rules on the structure and length of dag proofs.The second topic of this paper is the effect of different embeddings from Int to S4. We select two different embeddings from the literature and show that translated (propositional) intuitionistic formulae have sometimes exponentially shorter minimal proofs in a cut-free Gentzen system for S4than the original formula in a cut-free single-succedent Gentzen system for Int. Moreover, the length and the structure of proofs of translated formulae crucially depend on the chosen embedding. |
| |
Keywords: | propositional intuitionistic logic modal embeddings proof translations polynomial simulations |
本文献已被 SpringerLink 等数据库收录! |
|