Skip Navigation



Journal of Logic and Computation Advance Access published online on September 23, 2009
Journal of Logic and Computation, doi:10.1093/logcom/exp055
This Article
Right arrow Abstract Freely available
Right arrow Full Text (PDF)
Right arrow Alert me when this article is cited
Right arrow Alert me if a correction is posted
Services
Right arrow Email this article to a friend
Right arrow Similar articles in this journal
Right arrow Alert me to new issues of the journal
Right arrow Add to My Personal Archive
Right arrow Download to citation manager
Right arrowRequest Permissions
Google Scholar
Right arrow Articles by Avron, A.
Social Bookmarking
Add to CiteULike   Add to Connotea   Add to Del.icio.us  
What's this?

© The Author, 2009. Published by Oxford University Press. All rights reserved. For Permissions, please email: journals.permissions@oxfordjournals.org

Original Papers

A Simple Proof of Completeness and Cut-admissibility for Propositional Gödel Logic

Arnon Avron

School of Computer Science, Tel-Aviv University, Tel-Aviv, Israel.
E-mail: aa{at}tau.ac.il

Received 24 August 2008.

We provide a constructive, direct and simple proof of the completeness of the cut-free part of the hypersequential calculus HG for Gödel logic (thereby proving both completeness of the calculus for its standard semantics, and the admissibility of the cut rule in the full calculus). We then extend the results and proofs to derivations from assumptions, showing that such derivations can be confined to those in which cuts are made only on formulas which occur in the assumptions. The article is self-contained, and no previous knowledge concerning HG (or even Gödel logic) is needed for understanding it.

Keywords: Propositional Gödel Logic; Hypersequents; Strong cut-elimination; Completeness



References

  1. Avellone A, Ferrari M, Miglioli P. Duplication-free tableaux calculi together with cut-free and contraction-free sequent calculi for the interpolable propositional intermediate logics. Logic Journal of the IGPL (1999) 7:447–480.[CrossRef]
  2. Avron A. Using hypersequents in proof systems for non-classical logics, Annals of Mathematics and Artificial Intelligence (1991) 4:225–248.[CrossRef]
  3. Avron A. Gentzen-type systems, resolution and tableaux. Journal of Automated Reasoning (1993) 10:265–281.[CrossRef][Web of Science]
  4. Avron A, Konikowska B. Decomposition proof systems for Gödel logics. Studia Logica (2001) 69:197–219.[CrossRef]
  5. Baaz M, Ciabattoni A, Fermüller CG. Hypersequent calculi for Gödel logics - a survey. Journal of Logic and Computation (2003) 13:835–861.[Abstract/Free Full Text]
  6. Baaz M, Preining N, Zach R. First-order Gödel logics. Annals of Pure and Applied Logic (2007) 147:23–47.[CrossRef][Web of Science]
  7. Baaz M, Zach R. Hypersequent and the proof theory of intuitionistic fuzzy logic. Springer. 187–201. In Proceedings of CSL 2000, vol. 1862 of Lecture Notes in Computer Science.
  8. Ciabattoni A, Galatos N, Terui K. From axioms to analytic rules in nonclassical logics. In: Proceedings of LICS 2008. IEEE Computer Society Press. 229–240.
  9. Corsi G. Semantic trees for Dummett's logic LC. Studia Logica (1986) 45:199–206.[CrossRef]
  10. Corsi G. A cut-free calculus for Dummett's LC quantified. Zeitschrift für Mathematische Logik und Grundlagen der Mathematik (1989) 35:289–301.[CrossRef][Web of Science]
  11. Dyckhoff D. A deterministic terminating sequent calculus for Gödel-Dummett logic. Logic Journal of the IGPL (1999) 7:319–326.[CrossRef]
  12. Dyckhoff D, Negri S. Decision methods for linearly ordered heyting algebras. Archive for Mathematical Logic (2006) 45:411–422.[CrossRef][Web of Science]
  13. Dummett M. A propositional calculus with a Denumerable matrix. Journal of Symbolic Logic (1959) 24:96–107.
  14. Gödel K. On the intuitionistic propositional calculus. In: Collected Work—Feferman S, et al, eds. (1933) 1. Oxford University Press.
  15. Hájek P. Metamathematics of Fuzzy Logic (1998) Kluwer Academic Publishers.
  16. Metcalfe G, Olivetti N, Gabbay D. Proof Theory for Fuzzy Logics (2009) Springer.
  17. Sonobe O. A Gentzen-type formulation of some intermediate propositional logics. Journal of Tsuda College (1975) 7:7–14.

Add to CiteULike CiteULike   Add to Connotea Connotea   Add to Del.icio.us Del.icio.us    What's this?



This Article
Right arrow Abstract Freely available
Right arrow Full Text (PDF)
Right arrow Alert me when this article is cited
Right arrow Alert me if a correction is posted
Services
Right arrow Email this article to a friend
Right arrow Similar articles in this journal
Right arrow Alert me to new issues of the journal
Right arrow Add to My Personal Archive
Right arrow Download to citation manager
Right arrowRequest Permissions
Google Scholar
Right arrow Articles by Avron, A.
Social Bookmarking
Add to CiteULike   Add to Connotea   Add to Del.icio.us  
What's this?