Logica Universalis 8 (1):25-60 (2014)

Proofs and countermodels are the two sides of completeness proofs, but, in general, failure to find one does not automatically give the other. The limitation is encountered also for decidable non-classical logics in traditional completeness proofs based on Henkin’s method of maximal consistent sets of formulas. A method is presented that makes it possible to establish completeness in a direct way: For any given sequent either a proof in the given logical system or a countermodel in the corresponding frame class is found. The method is a synthesis of a generation of calculi with internalized relational semantics, a Tait–Schütte–Takeuti style completeness proof, and procedures to finitize the countermodel construction. Finitizations for intuitionistic propositional logic are obtained through the search for a minimal derivation, through pruning of infinite branches in search trees by means of a suitable syntactic counterpart of semantic filtration, or through a proof-theoretic embedding into an appropriate provability logic. A number of examples illustrates the method, its subtleties, challenges, and present scope
Keywords Non-classical logics  completeness  correspondence  countermodels  proof search  labelled sequent calculi  intuitionistic logic  provability logic  multi-modal logics  geometric rules  Sahlqvist
Categories (categorize this paper)
DOI 10.1007/s11787-014-0097-1
Edit this record
Mark as duplicate
Export citation
Find it on Scholar
Request removal from index
Revision history

Download options

PhilArchive copy

Upload a copy of this paper     Check publisher's policy     Papers currently archived: 70,079
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

Proof Analysis in Modal Logic.Sara Negri - 2005 - Journal of Philosophical Logic 34 (5-6):507-544.
Labelled Deductive Systems: Volume 1.Dov M. Gabbay - 1996 - Oxford, England: Oxford University Press.
Proof Analysis in Intermediate Logics.Roy Dyckhoff & Sara Negri - 2012 - Archive for Mathematical Logic 51 (1-2):71-92.
Labelled Non-Classical Logics.Luca Viganò - 2000 - Boston, MA, USA: Kluwer Academic Publishers.

View all 27 references / Add more references

Citations of this work BETA

Proof Analysis for Lewis Counterfactuals.Sara Negri & Giorgio Sbardolini - 2016 - Review of Symbolic Logic 9 (1):44-75.
Geometrisation of First-Order Logic.Roy Dyckhoff & Sara Negri - 2015 - Bulletin of Symbolic Logic 21 (2):123-163.

View all 12 citations / Add more citations

Similar books and articles

Proof Analysis in Intermediate Logics.Roy Dyckhoff & Sara Negri - 2012 - Archive for Mathematical Logic 51 (1-2):71-92.
Propositional Mixed Logic: Its Syntax and Semantics.Karim Nour & Abir Nour - 2003 - Journal of Applied Non-Classical Logics 13 (3-4):377-390.
Labeled Sequent Calculi for Modal Logics and Implicit Contractions.Pierluigi Minari - 2013 - Archive for Mathematical Logic 52 (7-8):881-907.
Completeness and Incompleteness for Intuitionistic Logic.Charles McCarty - 2008 - Journal of Symbolic Logic 73 (4):1315-1327.
Kripke Completeness of Infinitary Predicate Multimodal Logics.Yoshihito Tanaka - 1999 - Notre Dame Journal of Formal Logic 40 (3):326-340.


Added to PP index

Total views
53 ( #213,996 of 2,506,121 )

Recent downloads (6 months)
1 ( #416,984 of 2,506,121 )

How can I increase my downloads?


My notes