On different intuitionistic calculi and embeddings from int to S

Studia Logica 69 (2):249-277 (2001)
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
Categories (categorize this paper)
DOI 10.1023/A:1013869924088
 Save to my reading list
Follow the author(s)
My bibliography
Export citation
Find it on Scholar
Edit this record
Mark as duplicate
Revision history Request removal from index
Download options
PhilPapers Archive

Upload a copy of this paper     Check publisher's policy on self-archival     Papers currently archived: 24,463
External links
Setup an account with your affiliations in order to access resources via your University's proxy server
Configure custom proxy (use this if your affiliation does not provide a proxy)
Through your library
References found in this work BETA

No references found.

Add more references

Citations of this work BETA
Sara Negri (2011). Proof Theory for Modal Logic. Philosophy Compass 6 (8):523-538.

Add more citations

Similar books and articles

Monthly downloads

Added to index


Total downloads

22 ( #214,053 of 1,925,507 )

Recent downloads (6 months)

2 ( #308,589 of 1,925,507 )

How can I increase my downloads?

My notes
Sign in to use this feature

Start a new thread
There  are no threads in this forum
Nothing in this forum yet.