Double-exponential inseparability of robinson subsystem

Lavinia Egidi, Giovanni Faglia

Research output: Contribution to journalArticlepeer-review

Abstract

In this work a double exponential time inseparability result is proven for a finitely axiomatizable first order theory Q+. The theory, subset of Presburger theory of addition S+, is the additive fragment of Robinson system Q. We prove that every set that separates Q+ from the logically false sentences of addition is not recognizable by any Turing machine working in double exponential time. The lower bound is given both in the non-deterministic and in the linear alternating time models. The result implies also that any theory of addition that is consistent with Q+-in particular any theory contained in S+-is at least double exponential time difficult. Our inseparability result is an improvement on the known lower bounds for arithmetic theories. Our proof uses a refinement and adaptation of the technique that Fischer and Rabin used to prove the difficulty of S +. Our version of the technique can be applied to any incomplete finitely axiomatizable system in which all of the necessary properties of addition are provable.

Original languageEnglish
Pages (from-to)94-124
Number of pages31
JournalJournal of Symbolic Logic
Volume76
Issue number1
DOIs
Publication statusPublished - Mar 2011

Fingerprint

Dive into the research topics of 'Double-exponential inseparability of robinson subsystem'. Together they form a unique fingerprint.

Cite this