David Bourget (Western Ontario)
David Chalmers (ANU, NYU)
Rafael De Clercq
Jack Alan Reynolds
Learn more about PhilPapers
Journal of Symbolic Logic 71 (2):399 - 424 (2006)
We give resource bounded versions of the Completeness Theorem for propositional and predicate logic. For example, it is well known that every computable consistent propositional theory has a computable complete consistent extension. We show that, when length is measured relative to the binary representation of natural numbers and formulas, every polynomial time decidable propositional theory has an exponential time (EXPTIME) complete consistent extension whereas there is a nondeterministic polynomial time (NP) decidable theory which has no polynomial time complete consistent extension when length is measured relative to the binary representation of natural numbers and formulas. It is well known that a propositional theory is axiomatizable (respectively decidable) if and only if it may be represented as the set of infinite paths through a computable tree (respectively a computable tree with no dead ends). We show that any polynomial time decidable theory may be represented as the set of paths through a polynomial time decidable tree. On the other hand, the statement that every polynomial time decidable, relative to the tally representation of natural numbers and formulas, is equivalent to P = NP. For predicate logic, we develop a complexity theoretic version of the Henkin construction to prove a complexity theoretic version of the Completeness Theorem. Our results imply that that any polynomial space decidable theory △ possesses a polynomial space computable model which is exponential space decidable and thus △ has an exponential space complete consistent extension. Similar results are obtained for other notions of complexity
|Keywords||No keywords specified (fix it)|
|Categories||categorize this paper)|
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.
Citations of this work BETA
No citations found.
Similar books and articles
Peter Lohmann & Heribert Vollmer (2013). Complexity Results for Modal Dependence Logic. Studia Logica 101 (2):343-366.
Maria Bulińska (2009). On the Complexity of Nonassociative Lambek Calculus with Unit. Studia Logica 93 (1):1 - 14.
Andreas Blass, Yuri Gurevich & Saharon Shelah (2002). On Polynomial Time Computation Over Unordered Structures. Journal of Symbolic Logic 67 (3):1093-1125.
Thomas Strahm (1997). Polynomial Time Operations in Explicit Mathematics. Journal of Symbolic Logic 62 (2):575-594.
Lauri Hella (1996). Logical Hierarchies in PTIME. Information And Computation 129 (1):1--19.
Erich Grädel & Yuri Gurevich (1995). Tailoring Recursion for Complexity. Journal of Symbolic Logic 60 (3):952-969.
Stephen A. Fenner, Stuart A. Kurtz & James S. Royer (2004). Every Polynomial-Time 1-Degree Collapses If and Only If P = Pspace. Journal of Symbolic Logic 69 (3):713-741.
Douglas Cenzer & Andre Nies (2001). Initial Segments of the Lattice of Π01 Classes. Journal of Symbolic Logic 66 (4):1749 - 1765.
Barbara F. Csima (2004). Degree Spectra of Prime Models. Journal of Symbolic Logic 69 (2):430 - 442.
Samuel Coskey & Joel David Hamkins (2010). Infinite Time Decidable Equivalence Relation Theory. Notre Dame Journal of Formal Logic 52 (2):203-228.
Barbara F. Csima, Denis R. Hirschfeldt, Julia F. Knight & Robert I. Soare (2004). Bounding Prime Models. Journal of Symbolic Logic 69 (4):1117 - 1142.
Leon Horsten & Philip Welch (2007). The Undecidability of Propositional Adaptive Logic. Synthese 158 (1):41 - 60.
Harry Deutsch (1979). The Completeness of S. Studia Logica 38 (2):137 - 147.
Erich Grädel (1999). On the Restraining Power of Guards. Journal of Symbolic Logic 64 (4):1719-1742.
Added to index2010-08-24
Total downloads17 ( #140,569 of 1,696,616 )
Recent downloads (6 months)4 ( #144,179 of 1,696,616 )
How can I increase my downloads?