scholarly journals On the quantifier complexity of definable canonical Henselian valuations

2015 ◽  
Vol 61 (4-5) ◽  
pp. 347-361 ◽  
Author(s):  
Arno Fehm ◽  
Franziska Jahnke
Keyword(s):  
Quantifier Complexity

DIRECT AND LOCAL DEFINITIONS OF THE TURING JUMP

2007 ◽  
Vol 07 (02) ◽  
pp. 229-262 ◽  
Author(s):  
RICHARD A. SHORE
Keyword(s):  
Lower Bound ◽  
Second Order ◽  
Turing Degrees ◽  
Second Order Arithmetic ◽  
Ideal Formula ◽  
Quantifier Complexity ◽  
Order Arithmetic ◽  
Models Of Arithmetic

We show that there are Π5 formulas in the language of the Turing degrees, [Formula: see text], with ≤, ∨ and ∧, that define the relations x″ ≤ y″, x″ = y″ and so {x ∈ L2(y) = x ≥ y|x″ = y″} in any jump ideal containing 0(ω). There are also Σ6&Π6 and Π8 formulas that define the relations w = x″ and w = x', respectively, in any such ideal [Formula: see text]. In the language with just ≤ the quantifier complexity of each of these definitions increases by one. For a lower bound on definability, we show that no Π2 or Σ2 formula in the language with just ≤ defines L2 or L2(y). Our arguments and constructions are purely degree theoretic without any appeals to absoluteness considerations, set theoretic methods or coding of models of arithmetic. As a corollary, we see that every automorphism of [Formula: see text] is fixed on every degree above 0″ and every relation on [Formula: see text] which is invariant under the double jump or under join with 0″ is definable over [Formula: see text] if and only if it is definable in second order arithmetic with set quantification ranging over sets whose degrees are in [Formula: see text].

scholarly journals EXISTENTIALLY CLOSED MODELS IN THE FRAMEWORK OF ARITHMETIC

2016 ◽  
Vol 81 (2) ◽  
pp. 774-788 ◽  
Author(s):  
ZOFIA ADAMOWICZ ◽  
ANDRÉS CORDÓN-FRANCO ◽  
F. FÉLIX LARA-MARTÍN
Keyword(s):  
Closed Model ◽  
Existentially Closed ◽  
Quantifier Complexity

AbstractWe prove that the standard cut is definable in each existentially closed model of IΔ0 + exp by a (parameter free) П1–formula. This definition is optimal with respect to quantifier complexity and allows us to improve some previously known results on existentially closed models of fragments of arithmetic.

scholarly journals First-Order Interpolation and Interpolating Proof Systems

10.29007/1qb8 ◽  
2018 ◽  
Author(s):  
Laura Kovács ◽  
Andrei Voronkov
Keyword(s):  
Proof System ◽  
First Order ◽  
Proof Systems ◽  
Quantifier Complexity ◽  
Non Local ◽  
Additional Constraints ◽  
Superposition Calculus

It is known that one can extract Craig interpolants from so-called localproofs. An interpolant extracted from such a proof is a booleancombination of formulas occurring in the proof. However, standard completeproof systems, such as superposition, for theories having the interpolationproperty are not necessarily complete for local proofs: there are formulashaving non-local proofs but no local proof.In this paper we investigate interpolant extraction from non-local refutations(proofs of contradiction) in the superposition calculus and prove a numberof general results about interpolant extraction and complexity of extractedinterpolants. In particular, we prove that the number of quantifier alternationsin first-order interpolants of formulas without quantifier alternations isunbounded. This result has far-reaching consequences for using local proofsas a foundation for interpolating proof systems: any such proof system shoulddeal with formulas of arbitrary quantifier complexity.To search for alternatives for interpolating proof systems, we consider severalvariations on interpolation and local proofs. Namely, we give an algorithm forbuilding interpolants from resolution refutations in logic without equality anddiscuss additional constraints when this approach can be also used for logicwith equality. We finally propose a new direction related to interpolation vialocal proofs in first-order theories.

scholarly journals A definable Henselian valuation with high quantifier complexity

2015 ◽  
Vol 61 (4-5) ◽  
pp. 362-366
Author(s):  
Immanuel Halupczok ◽  
Franziska Jahnke
Keyword(s):  
Quantifier Complexity ◽  
Henselian Valuation

scholarly journals On the quantifier complexity of ? n+1 (T)? induction

2004 ◽  
Vol 43 (3) ◽  
pp. 371-398 ◽  
Author(s):  
A. Cord�n-Franco ◽  
A. Fern�ndez-Margarit ◽  
F.F. Lara-Mart�n
Keyword(s):  
Quantifier Complexity

Local Definitions in Degree Structures: The Turing Jump, Hyperdegrees and Beyond

2007 ◽  
Vol 13 (2) ◽  
pp. 226-239 ◽  
Author(s):  
Richard A. Shore
Keyword(s):  
Second Order ◽  
The Other ◽  
Turing Degrees ◽  
Second Order Arithmetic ◽  
Other Hand ◽  
Quantifier Complexity ◽  
Order Arithmetic ◽  
Models Of Arithmetic

AbstractThere are Π5 formulas in the language of the Turing degrees, D, with ≤, ⋁ and ⋀, that define the relations x″ ≤ y″, x″ = y″ and so x ∈ L2(y) = {x ≥ y ∣ x″ = y″} in any jump ideal containing 0(ω). There are also Σ6 & Π6 and Π8 formulas that define the relations w = x″ and w = x′, respectively, in any such ideal I. In the language with just ≤ the quantifier complexity of each of these definitions increases by one. On the other hand, no Π2 or Σ2 formula in the language with just ≤ defines L2 or x ∈ L2(y). Our arguments and constructions are purely degree theoretic without any appeals to absoluteness considerations, set theoretic methods or coding of models of arithmetic. As a corollary, we see that every automorphism of I is fixed on every degree above 0″ and every relation on I that is invariant under double jump or joining with 0″ is definable over I if and only if it is definable in second order arithmetic with set quantification ranging over sets whose degrees are in I. Similar direct coding arguments show that every hyperjump ideal I is rigid and biinterpretable with second order arithmetic with set quantification ranging over sets with hyperdegrees in I. Analogous results hold for various coarser degree structures.

Sign in / Sign up

Export Citation Format

Share Document