A uniform method for proving lower bounds on the computational complexity of logical theories

A new method for obtaining lower bounds on the computational complexity of logical theories is presented. It extends widely used techniques for proving the undecidability of theories by interpreting models of a theory already known to be undecidable. New inseparability results related to the well known inseparability result of Trakhtenbrot and Vaught are the foundation of the method. Their use yields hereditary lower bounds . By means of interpretations lower bounds can be transferred from one theory to another. Complicated machine codings are replaced by much simpler definability considerations, viz., the kinds of binary relations definable with short formulas on large finite sets. Numerous examples are given, including new proofs of essentially all previously known lower bounds for theories, and lower bounds for various theories of finite trees, which turn out to be particularly useful
Keywords No keywords specified (fix it)
Categories (categorize this paper)
DOI 10.1016/0168-0072(90)90080-L
Edit this record
Mark as duplicate
Export citation
Find it on Scholar
Request removal from index
Revision history

Download options

Our Archive

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

On Computable Numbers, with an Application to the Entscheidungsproblem.Alan Turing - 1936 - Proceedings of the London Mathematical Society 42 (1):230-265.
On the Complexity of the Theories of Weak Direct Powers.Charles Rackoff - 1976 - Journal of Symbolic Logic 41 (3):561-573.
Sentences True in All Constructive Models.R. L. Vaught - 1960 - Journal of Symbolic Logic 25 (1):39-53.

View all 21 references / Add more references

Citations of this work BETA

Algorithmic Uses of the Feferman–Vaught Theorem.J. A. Makowsky - 2004 - Annals of Pure and Applied Logic 126 (1-3):159-213.
Automatic Structures of Bounded Degree Revisited.Dietrich Kuske & Markus Lohrey - 2011 - Journal of Symbolic Logic 76 (4):1352-1380.

View all 10 citations / Add more citations

Similar books and articles

The Complexity of Propositional Proofs.Nathan Segerlind - 2007 - Bulletin of Symbolic Logic 13 (4):417-481.
Some Upper and Lower Bounds on Decision Procedures in Logic.Jeanne Ferrante - 1974 - Project Mac, Massachusetts Institute of Technology.
Sharpened Lower Bounds for Cut Elimination.Samuel R. Buss - 2012 - Journal of Symbolic Logic 77 (2):656-668.
More About Uniform Upper Bounds on Ideals of Turing Degrees.Harold T. Hodes - 1983 - Journal of Symbolic Logic 48 (2):441-457.
Logical Aspects of Rates of Convergence in Metric Spaces.Eyvind Martol Briseid - 2009 - Journal of Symbolic Logic 74 (4):1401 - 1428.
Uniform Bounds on Growth in o-Minimal Structures.Janak Ramakrishnan - 2010 - Mathematical Logic Quarterly 56 (4):406-408.
The Complexity of Analytic Tableaux.Noriko H. Arai, Toniann Pitassi & Alasdair Urquhart - 2006 - Journal of Symbolic Logic 71 (3):777 - 790.


Added to PP index

Total downloads
4 ( #774,351 of 2,287,730 )

Recent downloads (6 months)
1 ( #393,085 of 2,287,730 )

How can I increase my downloads?

Monthly downloads

Sorry, there are not enough data points to plot this chart.

My notes

Sign in to use this feature