The most nonelementary theory (a direct lower bound proof)

Vorobyov, Sergei

Item

ITEM ACTIONSEXPORT

Add to Basket

Local TagsRelease HistoryDetailsSummary

Released

Report

The most nonelementary theory (a direct lower bound proof)

MPS-Authors

/persons/resource/persons45677

Vorobyov, Sergei
Programming Logics, MPI for Informatics, Max Planck Society;

External Resource

No external resources are shared

Fulltext (restricted access)

There are currently no full texts shared for your IP range.

Fulltext (public)

MPI-I-98-2-007.pdf
(Any fulltext), 392KB

Supplementary Material (public)

There is no public supplementary material available

Citation

Vorobyov, S.(1998). The most nonelementary theory (a direct lower bound proof) (MPI-I-1998-2-007). Saarbrücken: Max-Planck-Institut für Informatik.

Cite as: https://hdl.handle.net/11858/00-001M-0000-0014-7A8A-2

Abstract

We give a direct proof by generic reduction that a decidable rudimentary theory of finite typed sets [Henkin 63, Meyer 74, Statman 79, Mairson 92] requires space exceeding infinitely often an exponentially growing stack of twos. This gives the highest currently known lower bound for a decidable logical theory and affirmatively answers to Problem 10.13 of [Compton & Henson 90]: Is there a `natural' decidable theory with a lower bound of the form $\exp_\infty(f(n))$, where $f$ is not linearly bounded? The highest previously known lower and upper bounds for `natural' decidable theories, like WS1S, S2S, are `just' linearly growing stacks of twos.