Jump to ContentJump to Main Navigation
Handbook of Logic in Computer Science: Volume 5. Algebraic and Logical Structures$
Users without a subscription are not able to see the full content.

S. Abramsky, Dov M. Gabbay, and T. S. E. Maibaum

Print publication date: 2001

Print ISBN-13: 9780198537816

Published to Oxford Scholarship Online: November 2020

DOI: 10.1093/oso/9780198537816.001.0001

Show Summary Details
Page of

PRINTED FROM OXFORD SCHOLARSHIP ONLINE (oxford.universitypressscholarship.com). (c) Copyright Oxford University Press, 2021. All Rights Reserved. An individual user may print out a PDF of a single chapter of a monograph in OSO for personal use. date: 15 June 2021

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

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

Chapter:
(p.129) A uniform method for proving lower bounds on the computational complexity of logical theories
Source:
Handbook of Logic in Computer Science: Volume 5. Algebraic and Logical Structures
Author(s):

Kevin J. Compton

C. Ward Henson

Publisher:
Oxford University Press
DOI:10.1093/oso/9780198537816.003.0003

In this chapter we present a method for obtaining lower bounds on the computational complexity of logical theories, and give several illustrations of its use. This method is an extension of widely used procedures for proving the recursive undecidability of logical theories. (See Rabin [1965] and Eršov et al. [1965].) One important aspect of this method is that it is based on a family of inseparability results for certain logical problems, closely related to the well-known inseparability result of Trakhtenbrot (as refined by Vaught), that no recursive set separates the logically valid sentences from those which are false in some finite model, as long as the underlying language has at least one non-unary relation symbol. By using these inseparability results as a foundation, we are able to obtain hereditary lower bounds, i.e., bounds which apply uniformly to all subtheories of the theory. The second important aspect of this method is that we use interpretations to transfer lower bounds from one theory to another. By doing this we eliminate the need to code machine computations into the models of the theory being studied. (The coding of computations is done once and for all in proving the inseparability results.) By using interpretations, attention is centred on much simpler definability considerations, viz., what kinds of binary relations on large finite sets can be defined using short formulas in models of the theory. This is conceptually much simpler than other approaches that have been proposed for obtaining lower bounds, such as the method of bounded concatenations of Fleischmann et al. [1977]. We will deal primarily with theories in first-order logic and monadic second-order logic.

Keywords:   actual variables, atomic formula, complete, depth, elementary recursive, explicit definition, formal variables, hard, height, hereditary, implicit definitions, interpretation, iterative definition, monadic second-order logics, only positively, operator formula, prenex definition

Oxford Scholarship Online requires a subscription or purchase to access the full text of books within the service. Public users can however freely search the site and view the abstracts and keywords for each book and chapter.

Please, subscribe or login to access full text content.

If you think you should have access to this title, please contact your librarian.

To troubleshoot, please check our FAQs , and if you can't find the answer there, please contact us .