Journal of Symbolic Logic Volume 76, Issue 1, March 2011, Pages 94-124 Double-exponential inseparability of robinson subsystem (Article) Egidi, L. , Faglia, G. Dipartimento di Informatica, Università del Piemonte Orientale A. Avogadro, Viale T. Michel.11, 15121 Alessandria, Italy View references (20) 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.

Double exponential inseparability of Robinson subsystem Q+

EGIDI, Lavinia;
2011-01-01

Abstract

Journal of Symbolic Logic Volume 76, Issue 1, March 2011, Pages 94-124 Double-exponential inseparability of robinson subsystem (Article) Egidi, L. , Faglia, G. Dipartimento di Informatica, Università del Piemonte Orientale A. Avogadro, Viale T. Michel.11, 15121 Alessandria, Italy View references (20) 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.
File in questo prodotto:
Non ci sono file associati a questo prodotto.

I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.

Utilizza questo identificativo per citare o creare un link a questo documento: https://hdl.handle.net/11579/15868
Citazioni
  • ???jsp.display-item.citation.pmc??? ND
  • Scopus 0
  • ???jsp.display-item.citation.isi??? 0
social impact