{'fraction_non_alphanumeric': 0.055952704539276976, 'fraction_numerical': 0.009567817341668932, 'mean_word_length': 3.5468083791633194, 'pattern_counts': {'":': 0, '<': 0, '<?xml version=': 0, '>': 26, 'https://': 0, 'lorem ipsum': 0, 'www.': 0, 'xml': 0}, 'pii_count': 0, 'substrings_counts': 0, 'word_list_counts': {'cursed_substrings.json': 50, 'profanity_word_list.json': 0, 'sexual_word_list.json': 0, 'zh_pornsignals.json': 0}}
Definable Ellipsoid Method, Sums-of-Squares Proofs, and the Isomorphism Problem

The ellipsoid method is an algorithm that solves the (weak) feasibility and linear optimization problems for convex sets by making oracle calls to their (weak) separation problem. We observe that the previously known method for showing that this reduction can be done in fixed-point logic with counting (FPC) for linear and semidefinite programs applies to any family of explicitly bounded convex sets. We use this observation to show that the exact feasibility problem for semidefinite programs is expressible in the infinitary version of FPC. As a corollary we get that, for the isomorphism problem, the Lasserre/Sums-of-Squares semidefinite programming hierarchy of relaxations collapses to the Sherali-Adams linear programming hierarchy, up to a small loss in the degree.


Introduction
Besides the well-known fact of being the first algorithm to be discovered that could solve linear programs (LPs) in polynomial time, the ellipsoid method has at least two other aspects that make it an important tool for the computer science theoretician. The first is that the algorithm is able to handle not only high-dimensional explicit LPs, but also certain implicitly given LPs that are described by exponentially many, or even infinitely many, linear inequalities. These include some of the most celebrated groundwork pieces of combinatorial optimization, such as the weighted matching problem on general graphs, and the submodular function minimization problem, among others. The second important feature of the ellipsoid method is that its polynomial running time in the bit-model of computation, taking into account potential issues of numeric instability, is since a long time ago well understood [9].
There is a third emerging and to some extent surprising feature of the ellipsoid method that is of particular significance for the logician and the descriptive complexity theorist. The starting point is the important breakthrough result of Anderson, Dawar and Holm [2] who developed a method called folding for dealing with symmetries in an LP. They used this method for showing that, for the special case of LPs, the ellipsoid method can be implemented in fixed-point logic with counting (FPC), and hence in polynomial time, but choicelessly, i.e., in a way that the symmetries from the input are respected all along the computation, as well as in the output. As the main application of their result, they proved that the class of graphs that have a perfect matching could be defined in FPC, thus solving one of the well-known open problems raised by Blass, Gurevich and Shelah in their work on Choiceless Polynomial Time [6]. The method of folding was extended further by Dawar and Wang for dealing with explicitly bounded and full-dimensional semidefinite programs (SDPs) [8].
The first contribution of our work is the observation that the abovementioned method of folding from [2] is general enough to capture the power of the ellipsoid method in its full strength. We observe that the fully general polynomial-time reduction that solves the weak feasibility problem given a weak separation oracle for an explicitly bounded convex set can be implemented, choicelessly, in FPC. As in the earlier works that employed the folding method, our implementation also uses the reduction algorithm as described in [9] as a black-box. The black-box is made into a choiceless procedure through a sequence of runs of the algorithm along a refining sequence of suitable quotients of the given convex set. It should be pointed out that while all the main ideas for doing this were already implicit in the earlier works by Anderson, Dawar and Holm, and by Dawar and Wang, working out the details requires a certain degree of care. For one thing, when we started this work it was not clear whether the earlier methods would be able to deal with separation oracles for families of convex sets that are not closed under the folding-quotient operations. We observe that such closure conditions, which happen to hold for LPs and SDPs, are indeed not required.
With this first observation in hand, we proceed to develop three applications. Our first application concerns the semidefinite programming exact feasibility problem. A semidefinite set, also known as a spectrahedron, is a subset of Euclidean space that is defined as the intersection of the cone of positive semidefinite matrices with an affine subspace. Thus, semidefinite sets are the feasible regions of SDPs, and the SDP exact feasibility problem asks, for an SDP given as input, whether its feasible region is non-empty. While the approximate and explicitly bounded version of this problem is solvable in polynomial-time by the ellipsoid method, the computational complexity of exact feasibility is a well-known open problem in mathematical programming; it is decidable in polynomial space, by reduction to the existential theory of the reals, but its precise position in the complexity hierarchy is unknown. It has been shown that the problem is at least as hard as PosSLP, the positivity problem for integers represented as arithmetic circuits [16], and hence at least as hard as the famous square-root sum problem, but the exact complexity of these two problems is also largely unknown (see [1]). Our result on the SDP exact feasibility problem is that, when its input is represented suitably as a finite structure, it is definable in the logic C ω ∞ω , i.e. boundedvariable infinitary logic with counting. In more recent terminology, we say that the SDP exact feasibility problem has bounded counting width: there is a fixed bound k so that the set of YES (and NO) instances of the problem is closed under indistinguishability by formulas of k-variable counting logic. This is perhaps an unexpected property for the SDP exact feasibility problem to have.
Although this definability result does not seem to have any direct algorithmic conse-quences for the SDP exact feasibility problem itself, we are able to use the gained knowledge
Vectors and matrices. If I is a non-empty index set, then an I-vector is an element of R I . The components of u ∈ R I are writen u(i) or u i , for i ∈ I. We identify R n with R [n] . For Ivectors u and v, the inner product of u and v is u, v = i∈I u i v i . We write u 1 = i∈I |u i | for the L 1 -norm, u 2 = u, u for the L 2 -norm, and u ∞ = max{|u i | : i ∈ I} for the L ∞ -norm. For K ⊆ R I and δ > 0, we define the δ-ball around K by S(K, δ) := {x ∈ R I : x−y 2 ≤ δ for some y ∈ K}. We define also S(K, −δ) := {x ∈ R I : S(x, δ) ⊆ K}. Holder's inequality states that if p, q ∈ N ∪ {∞} satisfy 1/p + 1/q = 1, then | u, v | ≤ u p v q . The special case p = q = 2 is the Cauchy-Schwartz inequality.
If I and J are two non-empty index sets, then an I × J-matrix is simply an I × J-vector; i.e., an element of R I×J . Accordingly, the components of X ∈ R I×J are written X(i, j), or X i,j , or X ij . The L 1 -, L 2 -and L ∞ -norms of a matrix X ∈ R I×J are defined as the respective norms of X seen as an I × J-vector, and the inner product of the matrices X, Y ∈ R I×J is X, Y = i∈I j∈J X ij Y ij . Matrix product is written by concatenation. The Hadamard product of matrices X, Y ∈ R I×J is the matrix X • Y defined by (X • Y ) ij = X ij Y ij for all i and j. A square matrix X ∈ R I×I is positive definite, denoted X ≻ 0, if it is symmetric and satisfies z T Xz > 0, for every non-zero z ∈ R I . If it is symmetric but satisfies the weaker condition that z T Xz ≥ 0, for every z ∈ R I , then it is positive semidefinite, which we denote by X 0. Equivalently, X is positive semidefinite if and only if X = Y T Y for some matrix Y ∈ R J×I if and only if all its eigenvalues are non-negative. By I we denote the square identity matrix of appropriate dimensions, i.e., I ij = 1 if i = j and I ij = 0 if i = j. By J we denote the square all-ones matrix of appropriate dimensions, i.e., J ij = 1 for all i and j. For I and J we omit the reference to the index set in the notation (particularly so if the index set is called I or J, for obvious reasons).
Let I and J be two non-empty index sets and let σ : I → J be a function. If v is a J-vector, then we write [v] −σ for the I-vector defined by [v] −σ (i) = v(σ(i)) for every i ∈ I. The notation extends to sets S of J-vectors in the natural way: If P is a set of I-vectors and Q is a set of J-vectors, then we say that P and Q are isomorphic, denoted P ∼ = Q, if there exists a bijection σ : I → J such that P = [Q] −σ .
Vocabularies, structures and logics. A many-sorted (relational) vocabulary L is a set of sort symbols D 1 , . . . , D s together with a set of relation symbols R 1 , . . . , R m . Each relation symbol R in the list has an associated type of the form D i 1 × · · · × D ir , where r ≥ 0 is the arity of the symbol, and i 1 , . . . , i r ∈ [s] are not necessarily distinct. A structure A of vocabulary L, or an L-structure, is given by s disjoint sets D 1 , . . . , D s called domains, one for each sort symbol D i ∈ L, and one relation R ⊆ D i 1 × · · · × D ir for each relation symbol R ∈ L of type D i 1 × · · · × D ir . We use D(A) or D to denote the domain associated to the sort symbol D, and R(A) or R to denote the relation associated to the relation symbol R.
In practice, the overloading of the notation should never be an issue. The domain of a sort symbol is also called a sort.
A logic for a many-sorted vocabulary L has an underlying set of individual variables for each different sort in L. When interpreted on an L-structure, the variables are supposed to range over the domain of its sort; i.e., the variables are typed. Besides the equalities x = y between variables of the same type, the atomic L-formulas are the formulas of the form R(x 1 , . . . , x r ), where R is a relation symbol of arity r and x 1 , . . . , x r are variables of types that match the type of R. The formulas of first-order logic over L are built from the atomic formulas by negations, disjunctions, conjunctions, and existential and universal quantification of individual variables.
The syntax of First-Order Logic with Counting FOC is defined by adjoining one more sort N to the underlying vocabulary, adding one binary ternary relation symbol ≤ of type N × N and two ternary relation symbols + and × of types N × N × N, as well as extending the syntax to allow quantification of the form ∃ ≥y x(ϕ), where y is a variable of type N. In the semantics of FOC, each L-structure A is expanded to an L ∪ {N, ≤, +, ×}-structure with N(A) = {0, . . . , n}, where n = max{|D i (A)| : i = 1, . . . , s}, and ≤, +, and × are interpreted by the standard arithmetic relations on {0, . . . , n}. The meaning of ∃ ≥y x(ϕ), for a concrete assignment y → i ∈ {0, . . . , n}, is that there exist at least y many witnesses a for the variable x within its sort such that assignment x → a satisfies the formula ϕ.
The syntax of Fixed-Point Logic with Counting FPC extends the syntax of FOC by allowing the formation of inflationary fixed-point formulas ifp x,X ϕ(x, X). On a structure A of the appropriate vocabulary, such formulas are interpreted as defining the least fixedpoint of the monotone operator A → A ∪ {a ∈ D i 1 × · · · × D ir : A |= ϕ(a, A)}, where D i 1 × · · · × D ir is the type of the relation symbol X in ϕ(x, X). The syntax of Infinitary Logic with Counting C ∞ω extends the syntax of FOC by allowing infinite disjunctions and conjunctions; i.e., formulas of the form i∈I φ i and i∈I φ i where I is a possibly infinite index set, and {φ i : i ∈ I} is an indexed set of formulas. The fragment of C ∞ω with k variables is the set of formulas that use at most k variables of any type. In the formulas of C k ∞ω the variables can be reused and hence there is no finite bound on the quantification depth of the formulas. It is well-known that if we care only for finite structures, then C k ∞ω could have been defined equivalently by disallowing the numeric sort and replacing the quantification ∃ ≥y x(ϕ), where y is a numeric variable, by all quantifiers of the form ∃ ≥i x(ϕ), where i is a (concrete) natural number; see [14]. We write C ω ∞ω for the union of the C k ∞ω over all natural numbers k. It is also known that for every natural number k, every many-sorted vocabulary L, and every L-formula ϕ of FPC that uses k variables, there exists an L-formula ψ of C k ∞ω such that ϕ and ψ define the same relations over all finite L-structures. While all the published proofs that we are aware of give the statement for single-sorted vocabularies (e.g. [14]), it is clear that the same proof applies to many-sorted vocabularies.
Interpretations and reductions. Let L and K be two many-sorted vocabularies, and let Θ be a class of K-formulas. A Θ-interpretation of L in K is given by: two Θ-formulas δ D (x) and ǫ D (x, y) for each sort symbol D of L, and one Θ-formula ψ R (x 1 , . . . , x r ) for each relation symbol R ∈ L of arity r. In all these formulas, the displayed x's and y's are tuples of distinct variables of the same length m, called the arity of the interpretation. We say that the interpretation takes a K-structure A as input and produces an L-structure B as output if for each sort symbol D in L there exists a surjective partial map f D : . .×f Dr and D 1 ×· · ·×D r is the type of R. The composition of two interpretations, one of L in K, and another one of K in J, is an interpretation of L in J defined in the obvious way. Similarly, the composition of an interpretation of L in K with an L-formula is a K-formula defined in the obvious way. In all these compositions, the number of variables in the resulting formulas multiply. For example, the composition of a C k ∞ω -interpretation with a C ℓ ∞ω -formula is a C kℓ ∞ω -formula. A reduction from a problem to another is an interpretation that takes (a representation of) an input x for the first problem and produces (a representation of) an input y for the second problem, in such a way that (a representation of) a solution for y is also (a representation of) a solution for x. The reduction is called a Θ-reduction if it can be produced by a Θ-interpretation.
Numbers, vectors and matrices as structures. We represent natural numbers, integers and rational numbers as finite relational structures in the following way. A natural number n ∈ N is represented by a finite structure, with a domain {0, . . . , N − 1} of bit positions where N ≥ ⌊log 2 (n + 1)⌋, of a vocabulary L N that contains a binary relation symbol ≤ for the natural linear order on the bit positions, and a unary relation symbol P for the actual bits, i.e., the bit positions i that carry a 1-bit in the unique binary representation of n of length N. Single bits b ∈ {0, 1} are represented as natural numbers with at least one bit position. Thus L B is really the same as L N , but we still give it a separate name. Integers z ∈ Z are represented by structures of the vocabulary L Z = L B∪ L N , with a domain {0, . . . , N − 1} of bit positions, where N ≥ ⌊log 2 (|z| + 1)⌋. If z = (−1) b n, where b ∈ {0, 1} and n ∈ N, then the P -relation from L B encodes the sign b, and the P -relation from L N encodes the actual bits of the magnitude n. Both copies of ≤ are interpreted by the natural linear order on the bit positions. Rationals q ∈ Q are represented by structures of the vocabulary L Q = L B∪ L N∪ L N , with a domain {0, . . . , N − 1} that is large enough to encode both the numerator and the denominator of q in binary. If q = (−1) b n/d, where b ∈ {0, 1} and n, d ∈ N, then the P -relation from L B is used to encode the sign b, the P -relation from the first copy of L N is used to encode the bits of the numerator n, and the P -relation from the second copy of L N is used to encode the bits of the denominator d. As always each ≤ is the natural linear order on the bit positions. We use zero denominator to represent ±∞.
An I-vector u ∈ Q I is represented by a two-sorted structure, where the first sortĪ is the index set I and the second sortB is a domain {0, . . . , N − 1} of bit positions, where N is large enough to encode all the numerators and denominators in the entries of u in binary. The vocabulary L vec of this structure has one unary relation symbol I forĪ, one binary relation symbol ≤ for the natural linear order onB, and three binary relation symbols P s , P n and P d , each of typeĪ ×B, that are used to encode the entries of u in the expected way: P s (i, 0) if and only if u(i) is positive, P n (i, j) if and only if the j-th bit of the numerator of u(i) is 1, and P d (i, j) if and only if the j-th bit of the denominator of u(i) is 1.
More generally, if I 1 , . . . , I d denote index sets that are not necessarily pairwise distinct, then the corresponding tensors u ∈ Q I 1 ×···×I d are represented by many-sorted structures, with one sortĪ for each index set I for as many different index sets as there are in the list I 1 , . . . , I d , plus one sortB for the bit positions. The vocabulary L vec,d of these structures has one unary relation symbol I for each index sortĪ, one binary relation symbol ≤ for the natural linear order on the bit positionsB, and three d + 1-ary relation symbols P s , P n and P d , each of typeĪ 1 × · · · ×Ī d ×B, for encoding the signs and the bits of the numerators and the denominators of the entries of the tensor. Matrices A ∈ Q I×J and square matrices A ∈ Q I×I are special cases of these, and so are indexed sets of vectors {u i : i ∈ K} ⊆ Q I and index sets of matrices {A i : i ∈ K} ⊆ Q I×J .

Definable Ellipsoid Method
In this section we show that the ellipsoid method can be implemented in FPC for any family of explicitly bounded convex sets. We begin by defining the problems involved.

Geometric problems and the ellipsoid method
Let C be a class of convex sets, each of the form K ⊆ R I for some non-empty index set I. The class C comes with an associated encoding scheme. We assume that the encoding of a set K ⊆ R I carries within it enough information to determine the set I. If the encoding also carries information about a rational R satisfying K ⊆ S(0 I , R), then we say that K is circumbscribed, and we write (K; I, R) to refer to it. We write (K; n, R) whenever I = [n].
The exact feasibility problem for C takes as input the encoding of a set K ⊆ R I in C and asks for a bit b ∈ {0, 1} that is 1 if K is non-empty, and 0 if K is empty. The weak feasibility problem for C takes as input the encoding of a set K ⊆ R I in C and a rational ǫ > 0 and asks for a bit b ∈ {0, 1} and a vector x ∈ Q I such that: 1. b = 1 and x ∈ S(K, ǫ), or 2. b = 0 and vol(K) ≤ ǫ.
The reason why the exact feasibility problem is formulated as a decision problem and does not ask for a feasible point is that K could well be a single point with non-rational components. In the weak feasibility problem this is not an issue because if K is non-empty, then the ball S(K, ǫ) surely contains a rational point. The (not-so-)weak separation problem for C takes as input the encoding of a set K ⊆ R I in C , a vector y ∈ Q I , and a rational δ > 0 and asks as output for a bit b ∈ {0, 1} and a vector s ∈ Q I such that ||s|| ∞ = 1 and: 1. b = 1 and y ∈ S(K, δ), or 2. b = 0 and s, y + δ ≥ sup{ s, x : x ∈ K}.
The problems carry the adjective weak in their name to stress on the fact that in both cases the more natural requirement of membership in K is replaced by the looser requirement of membership in S(K, γ) for a given γ > 0. For the weak separation problem, the additional qualification not-so-(weak) serves the purpose of distinguishing it from the weak(er) version in which condition 2. is replaced by the looser requirement that s, y + δ ≥ sup{ s, x : x ∈ S(K, −δ)}. It turns out that the main procedure of the ellipsoid method, as stated in the monograph [9] and in Theorem 1 below, requires the not-so-weak version. Recall that an ellipsoid in R I is a set of form E(A, a) = {x ∈ R I : (x − a) T A(x − a) ≤ 1}, where a ∈ R I is the center, and A is an I × I positive definite matrix.
Theorem 1 (Theorem 3.2.1 in [9]). There is an oracle polynomial-time algorithm, the central-cut ellipsoid method (CC), that solves the following problem: Given a rational number ǫ > 0 and a circumscribed closed convex set (K; n, R) given by an oracle that solves the notso-weak separation problem for K, outputs one of the following: either a vector x ∈ S(K, ǫ), or a positive definite matrix A ∈ Q n×n and a vector a ∈ Q n such that K ⊆ E(A, a) and vol(E(A, a)) ≤ ǫ.
We plan to use algorithm CC from Theorem 1 almost as a black-box, except for the three aspects of it stated below. Although they are not stated in Theorem 3.2.1 in [9], inspection of the proof and the definitions in the book shows that they hold: 1. input to the algorithm is the triple given by ǫ, n and R, 2. the rationals ǫ and R are represented in binary, the natural n is represented in unary, 3. the algorithm makes at least one oracle query, and the output is determined by the answer to the last oracle call in the following way: if this last call was (y, δ) and the answer was the pair (b, s), then δ ≤ ǫ and the output vector x of CC is y itself whenever b = 1, and there exists a positive definite matrix A and a vector a so that K ⊆ E(A, a) and vol(E(A, a)) ≤ ǫ whenever b = 0.
The last point implies, in particular, that CC solves the weak feasibility problem for the given K. However, note also that the theorem states a notably stronger claim than the existence of a polynomial-time oracle reduction from the weak feasibility problem for a class C of sets to the not-so-weak separation problem for the same class C of sets: indeed, CC solves the feasibility problem for K by making oracle calls to the separation problem for the same K.

Definability of ellipsoid
In our case, since we want to refer to definability in a logic, the encoding scheme for C will encode each set K through a finite relational structure, and we will require it to be invariant under isomorphisms. Such encodings we call representations. Formally, a representation of C is a surjective partial map r from the class of all finite L-structures onto C , where L is a finite vocabulary that contains at least one unary relation symbol I, that satisfies the following conditions:

for every A ∈ Dom(r) it holds that r(A) ⊆ R I where I = I(A).
A circumscribed representation of C is a surjective partial map r from the class of all finite L-structures onto C , where L is a finite vocabulary that contains at least one unary relation symbol I as well as a copy of the vocabulary L Q , that satisfies the following conditions:

for every
Note that a circumscribed representation of C exists only if every K in C is bounded. For a given representation r of C , any of the existing preimages A ∈ r −1 (K) of a set K ∈ C is called a representation of K. If L is the vocabulary of the representation, then we say that C is represented in vocabulary L. If C has a representation in some vocabulary L, then we say that C is a represented class of sets, and if it has a circumscribed representation, then we say that it is a represented class of circumscribed sets.
If C is a represented class of convex sets and Φ is a class of logical formulas, then we say that the weak feasibility for C is Φ-definable if there exists a Φ-interpretation that, given an input represented as a structure over the vocabulary of the input, produces a valid output represented also as a structure over the vocabulary of the output. For example, if L is the vocabulary in which C is represented, then an interpretation for the weak feasibility problem for C would take as input a structure over L∪L Q and produce as output a structure over L B∪ L vec . It is required in addition that the represented K ⊆ R I from the input and the vector x ∈ Q I from the output share the same sortĪ with the same relation symbol I interpreted by the same set. For the not-so-weak separation problem, the input would be a structure over L∪ L Q∪ L vec and the output would be a structure over L B∪ L vec . Again, the represented K ⊆ R I and the vector y ∈ Q I from the input, and the vector s ∈ Q I from the output, share the same sortĪ with the same relation symbol I interpreted by the same set.
The following is the main result of this section.
Theorem 2. Let C be a represented class of circumscribed closed convex sets. If the notso-weak separation problem for C is FPC-definable, then the weak feasibility problem for C is also FPC-definable.
Although all the main ideas of the proof that we are going to present were already present in the works [2] and [8], we present a detailed proof for completeness.
At an intuitive level, the main difficulty for simulating the ellipsoid method within a logic is that one needs to make sure that the execution of the algorithm stays canonical ; i.e., invariant under the isomorphisms of the input structure. The principal device to achieve this is the following clever idea from [2]: instead of running the ellipsoid method directly over the given set K ⊆ R I , the algorithm is run over certain folded versions [K] σ ⊆ R σ(I) of K, where σ(I) is an ordered subset of I. If the execution of the ellipsoid does not detect the difference between K and the folded [K] σ , then an appropriately defined unfolding of the solution for [K] σ will give the right solution for K. If, on the contrary, the ellipsoid detects the difference in the form of a vector u ∈ Q I whose folding [u] σ does not unfold appropriately, then the knowledge of u is exploited in order to refine the current folding into a strictly larger ordered σ ′ (I) ⊆ I, and the execution is restarted with the new [K] σ ′ ⊆ R σ ′ (I) . After no more than |I| many refinements the folding will be indistinguishable from K, and the execution will be correct.
The crux of the argument that makes this procedure FPC-definable is that the ellipsoid algorithm is always operating over an ordered set σ(I). In particular, the algorithm stays canonical, and the polynomially many steps of its execution are expressible in fixed-point logic FP by the Immerman-Vardi Theorem. Indeed, the counting ability of FPC is required only during the folding/unfolding/refining steps.
Before we move to the actual proof, we discuss the required material for the method of foldings.

Folding operations
Let I and J be non-empty index sets. Let σ : I → J be an onto map. The folding [u] σ of an I-vector u and the unfolding [v] −σ of a J-vector v are the vectors defined by for every j ∈ J and every i ∈ I, respectively. For sets K ⊆ R I and L ⊆ R J , define The following lemma collects a few important properties of foldings. See Propositions 17 and 18 in [8] in which properties (4) and (5) from the lemma are also proved for all sets but stated only for convex sets.
Lemma 1. Let σ : I → J be an onto map, let u and v be I-vectors, and let K be a set of I-vectors. Then the following hold: which is the special case of the Cauchy-Schwartz inequality x, y ≤ x 2 y 2 where y is the d-dimensional all-ones vector. Property (3) is an immediate consequence of (2). Property (4) follows from (1) and (2) follows from the fact that the map u → [u] σ is linear.
There is one further important property of foldings that we will need. Recall that the ellipsoid given by a positive definite matrix A ∈ R J×J and a vector a ∈ R J is the set We extend the definition of the set E(A, a) to arbitrary positive semidefinite matrices A. It should be noted that if A is positive semidefinite but not positive definite, then at least one of the semi-axes of E(A, a) is infinite and hence the set is unbounded. In this case we call E(A, a) an unbounded ellipsoid. Lemma 2. Let K ⊆ R I be a set, let σ : I → J be an onto map, and let R ∈ R J×I and L ∈ R I×J be the matrices that define the linear maps u → We have: with the first equality following from the linearity of R, the second equality following from the easily verified fact that [[a] −σ ] σ = a, and the inequality following from the fact that For the second part of the proof, observe that the matrix R T AR = (BR) T (BR) is positive semidefinite. Let λ 1 ≥ · · · ≥ λ n ≥ 0 be the eigenvalues of R T AR, let V = {u 1 , . . . , u n } be an orthonormal basis of corresponding eigenvectors, and let (b 1 , . . . , b n ) be the coordinates of La with respect to the basis V . The axes of symmetry of the (possibly unbounded) ellipsoid E(R T AR, La) correspond to the vectors in V . As we show below, λ 1 > 0 and therefore the shortest axis of E(R T AR, La) has a finite length 2(1/λ 1 ) 1/2 . It follows that E(R T AR, La) is contained in the set of points whose coordinates, with respect to the basis V , are given by Since the r-ball S(0, r) is inscribed in the n-dimensional hypercube [−r, r] n , where the coordinates are again given with respect to the basis V , this We will finish the proof by showing that vol(E(A, a)) where V k denotes the volume of a 1-ball in the kdimensional real vector space (for the volume of an ellipsoid see, e.g., [9]). Therefore, if vol(E(A, a)) ≤ ǫ, then µ 1 ≥ (V k /ǫ) 2/k > k −2 (1/ǫ) 2/k , where the last inequality follows from the fact that V k > k −k . Now, let y ∈ R J be an eigenvector of A corresponding to the eigenvalue µ 1 , and let x = Ly. Note that x T x ≤ ny T y. Hence, Since y = 0 also x = 0, and the Rayleigh quotient principle implies that λ 1 ≥ µ 1 /n. Hence λ 1 ≥ k −2 (1/ǫ) 2/k /n, which gives (1/λ 1 ) 1/2 ≤ n 1/2 kǫ 1/k ≤ nkǫ 1/k . From now on, all maps σ : I → J will be onto and have J = [k] for some positive integer k. Such maps define a preorder ≤ σ on I with exactly k equivalence classes and is defined by Since any bijective map respects any vector, observe that if σ does not respect v, then there exists a least one proper refinement of σ that does respect v. We aim for a canonical such refinement, that we denote σ v , and that is definable in FPC. We define it as follows.
In words, n(j) is the number of distinct v-values in the j-th equivalence class of ≤ σ , and m(i) is the number of distinct v-values in the equivalence class of i that are no bigger than On the other hand: Although not strictly needed, it is useful to note that σ v is a coarsest refinement of σ that respects v. The final lemma before we proceed to the proof of Theorem 2 collects a few computation tasks about foldings that are FPC-definable: Proof. All five cases are straightforward given the ability of FPC to perform the basic arithmetic of rational numbers, compute sums of sets of rationals indexed by definable sets, and compute cardinalities of definable sets.

Proof of Theorem 2
Let Ψ be an FPC-interpretation that witnesses that the not-so-weak separation problem for C is FPC-definable. We start by showing that there is an FPC-interpretation Ψ ′ that takes as input a representation of a set K ⊆ R I in C , an onto mapping σ : I → [k] where k is an integer that satisfies 1 ≤ k ≤ |I|, a vector y ∈ Q k , and a rational δ > 0 and outputs an integer b ∈ {−1, 0, 1} and a vector s ∈ Q I such that s ∞ = 1 and: 1. b = 1 and σ respects s and [y] −σ ∈ S(K, δ) and y ∈ S([K] σ , δ), or 2. b = 0 and σ respects s and [s] σ , y + δ ≥ sup{ [s] σ , x : x ∈ [K] σ }, or 3. b = −1 and σ does not respect s.
Concretely, let Ψ ′ be the interpretation that does the following: The claim that Ψ ′ is FPC-definable follows from points 3. and 4. in Lemma 3. The claim that Ψ ′ satisfies the required conditions follows from the correctness of Ψ, together with the fact that [[y] −σ ] σ = y, and properties (4) and (5) in Lemma 1. For later use, let us note that if the given σ : I → [k] is a bijection, then the third type of output b = −1 cannot occur.
compute [s] σ and take the pair (b, [s] σ ) as a valid output to the query (y, δ), 08.
if the run of CC makes a new query (y, δ), go back to step 05, 09.
if the run of CC makes no more queries, go to step 13, 10. else 11.
abort the run of CC and go back to step 04 with σ := σ s and k := k ′ , 13. let (b, s) be the output of Ψ ′ for the last oracle call (y, δ), A key aspect of CC that makes this algorithm well-defined is that, for steps 04, 05, 08 and 09, the only knowledge that the algorithm needs about the targeted set [K] σ are its dimension k, its bounding radius R, and correct answers to earlier queries (see point 1. immediately following the statement of Theorem 1). In particular, the algorithm will be welldefined even if the class C is not closed under foldings, as long as the gathered knowledge about the alleged [K] σ remains consistent with the assumption that the convex set given by the oracle is [K] σ . Note that properties (2), (4), and (5) in Lemma 1 guarantee so, as long as all s-vectors are respected by σ. As soon as this is detected to not be the case, σ is refined, and the run of CC is restarted with the new k and γ for the new σ (and the same R).
After no more than |I| many refinements of σ, the simulation of the run of CC will be executed until the end. Indeed, this happens at latest once σ becomes the totally refined map because at that point σ is a bijection that surely respects every s. Whenever the run is executed until the end, the algorithm reaches step 13 with a pair (b, s) and a σ that respects s. We use this to show that CC' solves the weak feasibility problem for C , and that it can be implemented in FPC.
The claim that CC' solves the weak feasibility problem for C is proved as follows. Let (b, s) be the output of Ψ ′ for the last oracle call (y, δ) of the execution of CC. As noted above, σ : I → [k] respects s and hence b ∈ {0, 1} by Property 3 in the description of Ψ ′ . If b = 1, then [y] −σ ∈ S(K, δ) by Property 1 in the description of Ψ ′ , and S(K, δ) ⊆ S(K, ǫ) because δ ≤ γ ≤ ǫ. This shows that (b, [y] −σ ) is a correct output for the weak feasibility problem for ǫ and K in case b = 1. In case b = 0 we have [K] σ ⊆ E(A, a) for a positive definite matrix A and a vector a, with vol(E(A, a)) ≤ γ ≤ (ǫ/(2 n R n−1 nk)) k , by point 3. immediately following the statement of Theorem 1. Since K ⊆ S(0, R), by Lemma 2 this means that the volume of K is at most ǫ and the answer b = 0 is a correct output.
For the implementation in FPC, we note that CC' is a relational WHILE algorithm that halts after at most |I| iterations all whose steps can be computed through FPCinterpretations without quotients.
Step 01 is the description of the input.
Step 02 follows from the fact that K has a circumsbribed representation: just take the L Q -reduct of the representation of K, where L Q is the copy of the vocabulary that is used for representing the rational radius R.
Step 03 is point 1. in Lemma 3. Step 04 follows from the Immerman-Vardi Theorem on the fact that the representation of [k] is an ordered structure and the computation of CC in between oracle calls runs in polynomial time.
Step 05 is just a control statement.
Step 06 follows from point 4. in Lemma 3. Step 07 follows from the fact σ respects s and point 5. in Lemma 3.
Step 08 follows, again, from the Immerman-Vardi Theorem on the fact that the representation of [k] is an ordered structure and the computation of CC in between oracle calls runs in polynomial time.
Step 09 follows from the same reason as Step 08.
Step 10 is a control statement.
Step 11 follows from point 5. in Lemma 3.
Step 12 and 13 are just control statements. Step 14 follows from point 3. in Lemma 3.
This completes the proof of Theorem 2, and this section.

Feasibility of SDPs
In this section we use Theorem 2 to show that the exact feasibility of semidefinite programs is definable in C ω ∞ω .

Semidefinite sets
A semidefinite set K A,b ⊆ R I is the set of matrices X ∈ R J×J that satisfy where A ∈ R M ×(J×J) is an indexed set of J × J matrices, b ∈ R M is an indexed set of reals, X is a J × J symmetric matrix of formal variables x ij = x ji = x {i,j} for i, j ∈ J, and I = {{i, j} : i, j ∈ J} is the set of variable indices. A circumscribed semidefinite set is a pair The representation of the circumscribed semidefinite set (K A,b ∈ R I , R) is a structure over the vocabulary L SDP∪ L Q whose L SDP -reduct is the representation of K A,b ∈ R I , and whose L Q -reduct is the representation of R.
The class of semidefinite sets together with the representation defined above form a represented class of sets, which we denote by C SDP . Similarly, the class of circumscribed semidefinite sets form a represented class of circumscribed sets denoted C C SDP . In [8] Dawar and Wang show the following: . The weak feasibility problem for circumscribed semidefinite sets is FPCdefinable.
In order to do so they prove Theorem 2 for the special case of semidefinite sets and propose an FPC-interpretation for the not-so-weak separation oracle. For completeness, we work out the details of a variant of their construction, indicating the precise place where our procedures differ, and why.

Separation oracle
We show that the not-so-weak separation problem is FPC-definable for the class C SDP of all semidefinite sets. This clearly implies the FPC-definability of the not-so-weak separation problem for C C SDP , which is what is needed for the proof of Theorem 3. We begin with a few definitions and lemmas.
A polytope K u,b ⊆ R I is defined by a system of linear inequalities: Linear programs of the form: where x, u and b are as specified above and c is an I-vector, are represented similarly as polytopes. The vocabulary L optLP contains three additional binary symbols P c,s , P c,n , P c,d that encode the vector c.

Theorem 4 ([2]). There exists an FPC-interpretation that takes as input a linear program
and outputs an integer b ∈ {−1, 0, 1}, a vector s ∈ Q I and a rational r ∈ Q, such that: 1. b = 1 and P is feasible but unbounded below, or 2. b = 0 and P has as an optimal feasible solution of value r, and s is one, or 3. b = −1 and P is infeasible.
We also need the following lemma from [8] showing that the smallest eigenvalue of a given symmetric matrix can be approximated in FPC:

Lemma 4 ([8]). There exists an FPC-interpretation that takes as input a symmetric matrix
A ∈ Q I×I and a rational δ > 0 and outputs a rational λ, such that λ is the approximate value of the smallest eigenvalue of A up to precision δ.
We are now ready to show the following: The not-so-weak separation problem for C SDP is FPC-definable.
Proof. If K A,b ⊆ R I is a non-empty semidefinite set and Y ∈ R J×J is a symmetric matrix outside K A,b , then either Y violates at least one of the linear inequalities that describe K A,b , or fails to be positive semidefinite. In the former case, we get a separating hyperplane by taking the normal of the violated inequality, and a canonical one by taking the sum of all of them, as in [2]. In the latter case, the smallest eigenvalue λ of Y is negative, and if v is an eigenvector of this eigenvalue, then vv T is a valid separating hyperplane (after normalization). Such an eigenvector would be found if we were able to find an optimal solution to the optimization problem inf y (Y − λI)y 1 s.t. y ∞ = 1.
Unfortunately, this optimization problem cannot be easily phrased into an LP because the constraint y ∞ = 1 cannot be expressed by linear inequalities. Here is where we differ from [8]: first we relax the constraint y ∞ = 1 to y ∞ ≤ 1, but then we add the condition that some component y l is 1, and we do this for each l ∈ J separately. Thus, for each l ∈ J, let P (Y, λ, l) be the following optimization problem: inf y (Y − λI)y 1 s.t. y ∞ ≤ 1, y l = 1.
This we can formulate as an LP. The problem P (Y, λ, l) may be feasible for some l ∈ J and infeasible for some other l ∈ J, but at least one is guaranteed to be feasible. We take a solution for each feasible one and add them together to produce a canonical separating hyperplane. All this would be an accurate description of what our separation oracle does except for the fact that we cannot compute λ exactly, but only an approximationλ. Still, if the approximation is good enough, usingλ in place of λ in the P (Y, λ, l)'s will do the job. We provide the details. Let Ψ be the interpretation that takes as input a symmetric matrix Y ∈ Q J×J , a rational δ > 0, and a representation of K A,b ⊆ R I in C SDP , where A ∈ Q M ×(J×J) and b ∈ Q M , does the following: 01. given Y , δ, and K A,b ⊆ R I as specified, 02. compute L : if D = 0, compute S := i∈L A i /D, and output (0, S), 06.

Let us show that Ψ is FPC-definable and satisfies the required conditions.
Step 01 is the description of the input. Steps 07 and 11 are control steps. FPC-definability of Steps 02, 03, 04, 05, 06, 08, 10, 14 and 15 follow from the ability of FPC to perform the basic arithmetic of rational numbers, compare rational numbers, and compute cardinalities of definable sets.
Step 09 follows from Lemma 4. Below we argue that Steps 12 and 13 are FPC-definable and that the output is always correct.
Suppose that L = {i ∈ M : A i , Y > b i } = ∅ and let us prove that the output in Steps 05 an 06 is correct. If i∈L A i is the zero matrix then we have that Therefore, the feasibility region K A,b is empty. Indeed, every X ∈ K A,b satisfies which is a contradiction. Hence, for any matrix whose L ∞ -norm is 1, in particular for the identity matrix I, the output (0, I) is correct. If i∈L A i is not the non-zero matrix, let D = i∈L A i ∞ and S = i∈L A i /D. Then for every X ∈ K A,b we have that Moreover, the matrix S has L ∞ -norm 1. So the output is correct. Suppose that L = {i ∈ M : A i , Y > b i } = ∅, n = |J| andλ > δ/2n 2 , and let us argue that the output in Step 10 is correct. Observe that, for every i ∈ M, the matrix Y satisfies A i , Y ≤ b i , and its smallest eigenvalue λ is positive, which means that the matrix Y is positive semidefinite. Hence, Y is in the feasibility region K A.b and the output is correct.
Finally, let us assume thatλ > δ/2n 2 . In this case, for every l ∈ J, the FPC interpretation needs to compute the optimal value and an optimal solution of the optimisation problem P (Y,λ, l). To show that this is possible, we define an essentially equivalent linear program P ′ (l) and use Theorem 4 to conclude.
To perform Steps 12 and 13 the FPC interpretation takes, for each l ∈ J, the linear program P ′ (l) with variables {x i : i ∈ J} ∪ {y i : i ∈ J}, defined by: for every i ∈ J y l = 1.
In the following, since Y andλ are fixed, let us write P (l) instead of P (Y,λ, l).

Claim 1. The program P (l) is feasible if and only if the program P ′ (l)
is feasible and the optimal values of P (l) and P ′ (l) are the same. Moreover, if a vector {x i : i ∈ J}∪{y i : i ∈ J} is an optimal solution to P ′ (l), then the vector {y i : i ∈ J} is an optimal solution to P (l).
Proof. Suppose that the feasibility region of P (l) is non-empty. For every vector y = {y i : i ∈ J} in the feasibility region of P (l), the vector {x i : i ∈ J} ∪ {y i : i ∈ J}, where x i = |(Y y −λy) i |, belongs to the feasibility region of P ′ (l) and its value i∈J x i = (Y −λI)y 1 is the same as the value of {y i : i ∈ J} for P (l). Therefore, the feasibility region of P ′ (l) is non-empty and the optimal value opt ′ of P ′ (l) is smaller or equal to the optimal value opt of P (l).
Suppose that the feasibility region of P ′ (l) is non-empty, and take an optimal solution {x i : i ∈ J} ∪ {y i : i ∈ J} for P ′ (l). Let y = {y i : i ∈ J}. It holds that y ∞ = 1 and y l = 1, so the vector y is in the feasibility region of P (l). Therefore, the feasibility region of P (l) is non-empty, and opt ≤ (Y −λI)y 1 . Moreover, for every i ∈ J, we have that Hence, the vector y is an optimal solution for P (l) and the optimal values are the same.
To perform Steps 12 and 13 the FPC interpretation computes, for every l ∈ J, an optimal solution and the optimal value of the optimisation problem P (l), by computing an optimal solution and the optimal value of the linear program P ′ (l) via Theorem 4, and projecting the output to the variables {y i : i ∈ J}.
We will now show that T , as defined in Step 12, is nonempty, and that l∈T v l v T l ∞ = 0. It follows that the output matrix S in Step 14 is well defined.
Proof. Let v be an eigenvector of Y with the smallest eigenvalue λ, and let v ∞ = 1. We have the following If there exists l ∈ J such that v l = 1, then v ∈ P (l) and T = ∅. Otherwise, there exists l ∈ J such that v l = −1. Then −v ∈ P (l) and we are done as well.
On the other hand, where v l • v l denotes the Hadamard product. The first inequality follows from the fact that all coefficients of each of the vectors v l • v l are squares and therefore non negative.
Finally, let us show that the output (0, S) in Step 15 is correct.
Claim 4. For every l ∈ T , let v l be the optimal solution of P (l). Then for every X ∈ K A,b , where the last but one inequality is a consequence of Holder's inequality. It follows that Hence, −λv T l v l + δ/2n ≥ −δ/2n + δ/2n = 0. We finish the proof by showing that for every X ∈ K A,b , S, Y + δ ≥ S, X .
Let X be any matrix in K A,b . From now on, let D = l∈T v l v T l ∞ . It holds that where the last inequality follows from the fact that |T | ≤ n and D ≥ 1.

Exact feasibility
We use Theorem 3 to prove the main result of this section: Theorem 5. The exact feasibility problem for semidefinite sets is C ω ∞ω -definable.
We begin the proof by relating the problem of exact feasibility to the subject of Theorem 3, i.e., the weak feasibility problem for circumscribed semidefinite sets.
For any R > 0, the R-restriction of a semidefinite set K A,b is the set of all those points in K A,b whose L ∞ -norm is bounded by R, i.e., it is the semidefinite set given by: For any ǫ > 0, the ǫ-relaxation of a semidefinite set K A,b is the semidefinite set given by: The question of emptiness for ǫ-relaxations of R-restrictions of semidefinite sets is closely linked to the exact feasibility problem under consideration. Recall the Cantor Intersection Theorem: If K 1 ⊇ K 2 ⊇ · · · is a decreasing nested sequence of non-empty compact subsets of R n , then the intersection i≥1 K i is non-empty. We use it for the following lemma.

Lemma 5. A semidefinite set K A,b is non-empty if and only if there exists a positive rational R such that for every positive rational ǫ it holds that the ǫ-relaxation of the R-restriction of K A,b is non-empty.
Proof. Assume that K A,b is non-empty and let x be a point in it. Let R be a rational bigger than x ∞ . Then x is also in the R-restriction of K A,b , and therefore in the ǫ-relaxation of the R-restriction of K A,b for every positive rational ǫ.
Assume now that R is a positive rational such that the ǫ-relaxation of the R-restriction of K A,b is non-empty for every positive rational ǫ. For each positive integer m, let K m be the 1/m-relaxation of the R-restriction of K A,b . Each K m is closed and bounded, hence compact. Moreover K 1 ⊇ K 2 ⊇ · · · , i.e., the sets K m form a decreasing nested sequence of non-empty subsets of R I . It therefore follows from the Cantor Intersection Theorem that m≥1 K m is non-empty. The claim follows from the observation that m≥1 K m is indeed the R-restriction of K A,b .
It follows from Theorem 3 that the emptiness problem for ǫ-relaxations of R-restrictions of semidefinite sets is definable in FPC in the following sense. Proof. Let Φ be an FPC-interpretation that witnesses that the weak feasibility problem for the class of circumscribed semidefinite sets is FPC-definable. The formula ψ takes as input the representation of a semidefinite set K A,b ⊆ R I , a rational ǫ > 0 and a rational R > 0, and does the following: 01. given K A,b ⊆ R I , ǫ and R as specified, 02. compute k := |I|, 03. compute R ′ := ⌈ k(R + ǫ) 2 ⌉, 04. compute a representation of K, the ǫ-relaxation of the R-restriction of K A,b , 05. compute m : This procedure is clearly FPC-definable. In order to prove correctness we will need the following lemma.
For any ǫ > 0, if the semidefinite set K A,b ∈ R I is nonempty, then its ǫ-relaxation has volume greater than Proof. Take ǫ 1 = ǫ/2km. Let Y be an element of K A,b . We will show that S(Y + ǫ 1 I, ǫ 1 ) is included in the ǫ-relaxation of K A,b . It will follow that the volume of the ǫ-relaxation of K A,b is at least ǫ k 1 V k , where V k is the volume of a 1-ball in the k-dimensional real vector space. Since V k > 1/k! this finishes the proof.
Suppose that T ∈ S(Y + ǫ 1 I, ǫ 1 ). This means that T = Y + ǫ 1 I + Z, where Z 2 ≤ ǫ 1 . Let v be a vector whose L 2 -norm is 1. We have Moreover, for every i ∈ M, we have where the one to last inequality follows from the fact that m = max { A i 2 : i ∈ M} ∪ {1}, and the last inequality follows from the fact that k = |I| ≥ 1.
We are now ready to conclude the proof. Observe that the L ∞ -norm of any point that belongs to the ǫ-relaxation of the R-restriction of a semidefinite set is bounded by R + ǫ, therefore the pair (K, R ′ ) computed in Steps 03 and 04 is a representation of a circumscribed semidefinite set. Let (b, x) be the pair computed in Step 07.
If b = 1 then there exists a point in S(K, δ), which in particular means that K is nonempty, so the output in Step 08 is correct. If b = 0, then we know that the volume of K is at most δ. The inequalities that define K have the form A i , X ≤ b i + ǫ for i ∈ M, and X {i,j} ≤ R + ǫ or −X {i,j} ≤ R + ǫ for i, j ∈ J. The maximum 2-norm of the normals of these inequalities and 1 is m = max { A i 2 : i ∈ M} ∪ {1}, so Lemma 6 applies. This means that K is empty, and the output in Step 09 is correct.
To finish the proof of Theorem 5 we show a technical lemma that may sound a bit surprising at first: it sounds as if it was stating that C k ∞ω -definability is closed under secondorder quantification over unbounded domains, which cannot be true. However, on closer look, the lemma states this only if the vocabularies of the quantified and the body parts of the formula are totally disjoint. In particular, this means that the domains of the sorts in the quantified and body parts of the formula stay unrelated except through the counting mechanism of C k ∞ω . Note for the record that if L and K are two many-sorted vocabularies with disjoint sorts, then obviously the vocabulary L ∪ K does not contain any relation symbol whose type mixes the sorts of L and K. If A is a class of L ∪ K-structures and B is a class of K-structures, we use the notation ∃B · A to denote the class of all finite L-structures A for which there exists a structure B ∈ B such that A∪ B ∈ A . Similarly, we use ∀B · A to denote the class of all finite L-structures A such that for all structures B ∈ B we have that A∪ B ∈ A . Lemma 7. Let L and K be many-sorted vocabularies with disjoint sorts, let A be a class of finite L ∪ K-structures, and let B be a class of finite K-structures. If A is C k ∞ω -definable, then the classes of L-structures ∃B · A and ∀B · A are also C k ∞ω -definable.
Proof. The proof is a simple Booleanization trick to replace the finite quantifiers ∃ ≥i over the sorts in K by finite propositional formulas, followed by replacing ∃B and ∀B by infinite disjunctions and conjunctions, respectively, indexed by the structures in B. We provide the details. Let φ be a formula of the many-sorted vocabulary L ∪ K with all variables of the L-sorts among x 1 , . . . , x k , and all variables of the K-sorts among y 1 , . . . , y k . Note that since L and K have disjoint sorts, all the atomic subformulas of φ have all its variables among x 1 , . . . , x k or all its variables among y 1 , . . . , y k . In other words, there are no atomic subformulas with mixed x-y variables. For every finite K-structure B with domain B and every b = (b 1 , . . . , b k ) ∈ B k , let φ(B, b) be the Booleanization of φ with respect to the atomic interpretation of K given by B, the domain of quantification B for the variables of the Ksorts, and the free-variable substitution x := b. Formally, using the notation [E] for the truth value of the statement E, the formula φ(B, b) is defined inductively as follows: θ(B, b)), Since there are no atomic subformulas with mixed x-y variables, the definition covers all cases. The construction of φ(B, b) was designed so that for every finite (L ∪ K)-structure C with L-and K-reducts A and B with domains A and B, respectively, every a ∈ A k and It follows from the definitions that φ ∃ defines ∃B · A . Similarly, defining φ ∀ := B∈B φ(B) works for ∀B · A .
We put everything together in the proof of Theorem 5.
Proof of the Theorem 5. Let ψ be the L SDP∪ L Q∪ L Q -formula of FPC defined in Proposition 2. Let l be the number of variables in ψ. By the translation from l-variable FPC to C l ∞ω (see Section 2), there exists an L SDP∪ L Q∪ L Q -formula τ of C l ∞ω defining the same class A of finite structures. The vocabulary of A has disjoint sorts. Let B R be the class of finite structures which are representations of positive rational numbers over the first copy of L Q , and let B ǫ be the class of finite structures which are representations of positive rational numbers over the second copy of L Q . By Lemma 7 the class ∀B ǫ ·A , and hence ∃B R ·∀B ǫ ·A , is also C l ∞ω -definable. Let φ be the L SDP -formula of C l ∞ω defining this last class. Lemma 5 implies that φ defines the exact feasibility problem for semidefinite sets.

Sums-of-Squares Proofs and Lasserre Hierarchy
In this section we develop the descriptive complexity of the problem of deciding the existence of Sums-of-Squares proofs. Along the way we discuss the relationship between the Lasserre hierarchy of SDP relaxations and SOS, and how 0/1-valued variables ensure strong duality. We use the strong duality to argue the equivalence between the existence of SOS refutations and the existence of a notion of SOS approximate refutations that we introduce.

Descriptive Complexity of SOS Proofs
Let x 1 , . . . , x n be a set of variables. In the following whenever we talk about polynomials or monomials we mean polynomials and monomials over the set of variables x 1 , . . . , x n and real or rational coefficients. For a set Q = {q 1 , . . . , q k } of polynomials and a further polynomial q, a Sums-of-Squares proof of q ≥ 0 from Q is an identity: where, for every j ∈ [m], the polynomial s j is a sum of squares of polynomials, and the polynomial p j is either in Q or in the set B n defined as follows: The inequalities p ≥ 0 for p ∈ B n are called Boolean axioms. If q = −1, then the proof is called a refutation of Q. Sometimes we allow the system to include equations q i = 0, which we think of as the set of two inequalities q i ≥ 0 and −q i ≥ 0. The degree of the proof is defined as max{deg(p j s j ) : j ∈ [m]}, where, for a polynomial p, the notation deg(p) denotes the degree of p.
We consider the problem of deciding the existence of SOS proofs and refutations of a fixed degree 2d for a set of polynomials given as input. The first easy observation is that the proof-existence problem can be reduced to the exact feasibility problem for semidefinite sets, and the reduction can be done in FPC. Then we ask whether the exactness condition in the feasibility problem for semidefinite sets can be relaxed, and we achieve this for refutations. In other words: 1. Proof-existence reduces in FPC to exact feasibility for semidefinite sets.
2. Refutation-existence reduces in FPC to weak feasibility for semidefinite sets.
We note that, in both cases, the semidefinite sets in the outcome of this reduction are not circumbscribed. As stated, point 1. above is almost a reformulation of the problem. In order to prove point 2. we need to develop a notion of approximate refutation, and combine it with a strong duality theorem that characterizes the existence of SOS refutations in terms of so-called pseudoexpectations. We note that the strong duality theorem that we need relies on the assumption that the Boolean axioms are allowed for free in the definition of SOS.
Finally, we combine these FPC reductions with the results of the previous section in order to get the following: Corollary 1. For every fixed positive integer d, the problems of deciding the existence of SOS proofs of degree 2d, and SOS refutations of degree 2d, are C ω ∞ω -definable. Moreover, there exists a constant c, independent of d, such that the defining formulas are in C cd ∞ω . As usual with descriptive complexity results like these, we need to fix some encoding of the input as finite relational structures. In this case the inputs are indexed sets of polynomials. The exact choice of encoding is not very essential, but we propose one for concreteness.
Let I be an index set and let {x i : i ∈ I} be a set of formal variables. A monomial is a product of variables. We use the notation x α , where α ∈ N I , to denote the monomial that has degree α i on variable x i . We write |α| for the degree i∈I α i of the monomial x α . A polynomial α c α x α is a finite linear combination of monomials, i.e. all but finitely many of the coefficients c α are zero. A polynomial p with rational coefficients is represented by a three-sorted structure, with a sortĪ for the index set I, a second sortM for the finite set of monomials that have non-zero coefficient in p, and a third sortB for a domain {0, . . . , N −1} of bit positions, where N is large enough to encode all the coefficients of p and all the degrees of its monomials in binary. The vocabulary L pol of this structure has one unary relation symbol I forĪ, one binary relation symbol ≤ for the natural linear order onB, three binary relations symbols P s , P n , and P d of typeM ×B that encode, for each monomial, the sign, the bits of the numerator, and the bits of the denominator of its coefficient, respectively, and a ternary relation symbol D of typeM ×Ī ×B that encodes, for each monomial and each variable, the bits of the degree of this variable in the monomial.

Lasserre hierarchy
For a set of polynomials {q 0 , q 1 , . . . , q k }, by POP(q 0 ; {q 1 , . . . , q k }) we denote the polynomial optimisation problem : Take d > 0. By M d we denote the matrix indexed by monomials of degree at most d over the variables x 1 , . . . , x n where (M d ) α,β = x α+β . For every monomial x α , we introduce a variable y α and by M d (y) we denote the corresponding matrix of variables, i.e., (M d (y)) α,β = y α+β . More generally, for any polynomial q = γ c γ x γ , the matrix M q,d , indexed by monomials of degree at most d, is defined by M q,d = qM d , i.e., (M q,d ) α,β = qx α+β . The corresponding matrix M q,d (y) is defined by (M q,d (y)) α,β = γ c γ y α+β+γ . Observe that the entries of the matrix M q,d are polynomials of degree at most 2d + deg q, while the entries of the matrix M q,d (y) are the corresponding linear combinations of variables. Note also that M 1,d = M d and M 1,d (y) = M d (y). For every variable y α , consider the coefficients of y α in the matrix M q,d (y). Those coefficients form a matrix which we denote by A q,d,α . Formally, for |α| ≤ 2d + deg q, the matrices A q,d,α are defined as the real matrices satisfying M q,d (y) = α y α A q,d,α or equivalently M q,d = α x α A q,d,α . Finally, for any polynomial q, by d q we denote the biggest integer satisfying 2d q + deg q ≤ 2d.
Let Q be a set of polynomials. For any positive integer d, the Lasserre SDP relaxation of the polynomial optimisation problem POP( α a α x α ; Q) of order d is the pair of semidefinite programs (P d , D d ), where P d is the primal semidefinite program: inf y α a α y α y ∅ = 1 M q,dq (y) 0, for every q ∈ Q and D d is the dual semidefinite program: Weak SDP duality implies that the optimal value of P d is always greater or equal to the optimal value of D d . In [10] the authors establish a condition which guarantees strong duality for primal and dual SDP problems in the Lasserre hierarchy. Proof. Let q 0 = α a α x α and let d be some positive integer. The primal P ′ d is the following semidefinite program: inf y α a α y α y ∅ = 1 M q,dq (y) 0, for every q ∈ Q M p,dp (y) 0 (20) Let P = {q ∈ Q : c q > 0}. Note that since deg p = max{deg q : q ∈ P }, for every q ∈ P , we have d p ≤ d q . For each q ∈ P , by M ′ q,dq (y) let us denote the principal submatrix of M q,dq (y) obtained by removing the rows and columns indexed by monomials of degree greater than d p . Observe that M p,dp (y) = q∈P c q M ′ q,dq (y). Since the constraints {M q,dq (y) 0 : q ∈ P } imply the constraint M p,dp (y) = q∈P c q M ′ q,dq (y) 0, the feasibility regions, and therefore also the optimal values, of P d and P ′ d are the same.
The dual D ′ d is the following semidefinite program: sup z,Z z q∈Q A q,dq,∅ , Z q + A p,dp,∅ , Z p = a ∅ − z q∈Q A q,dq,α , Z q + A p,dp,α , Z p = a α , for 1 ≤ |α| ≤ 2d Z q 0, for every q ∈ Q Z p 0 (21) Any solution to the program D d can be extended to a solution to the program D ′ d with the same optimal value by taking Z p to be the zero matrix. On the other hand, any solution (z, {Z q } q∈Q , Z p ) to the program D ′ d gives rise to a solution (z, {Z q } q∈Q ) to the program D d with the same optimal value by settingz := z,Z q := Z q +c q Z p , for each q ∈ P , andZ q := Z q , for each q ∈ Q \ P . This follows form the fact that A p,dp,α = q∈P c q A q,dq,α .

SOS proofs as semidefinite sets
Fix a set of polynomials Q and a further polynomial p = α a α x α . LetQ = Q ∪ B n . A polynomial s of degree at most 2t is a sum of squares if and only if there exists a positive semidefinite matrix Z indexed by monomials of degree at most t such that s = M t , Z . Therefore, there exists a degree-2d SOS proof of the polynomial inequality p ≥ 0 from Q if and only if, for every q ∈Q, there exists a positive semidefinite matrix Z q indexed by monomials of degree at most d q such that Observe that the existence of a set of positive semidefinite matrices {Z q : q ∈Q} satisfying the identity (22) is exactly the same as non-emptiness of the semidefinite set K d (Q, p) ⊆ R I d given by: q∈Q A q,dq,α , Z q = a α for |α| ≤ 2d and X 0, where is a set of variable indices, and for every q ∈Q, the matrix Z q is the principal submatrix of X corresponding to the rows and columns indexed by {(q, x α ) : |α| ≤ d q }. Indeed, from every feasible point X ∈ K d (Q, p) we get a set of positive semidefinite matrices {Z q : q ∈Q} satisfying the identity (22) by setting Z q be the principal submatrix of X corresponding to the rows and columns indexed by {(q, x α ) : |α| ≤ d q }. On the other hand, any set of positive semidefinite matrices {Z q : q ∈Q} satisfying the identity (22) can be extended to a point in K d (Q, p) by setting all remaining variables to 0.
The representation of the semidefinite set K d (Q, p) can be easily obtained from the representation of the set of polynomials Q and the polynomial p by means of FPC-interpretations: Fact 2. For every fixed positive integer d, there is an FPC-interpretation that takes a set of polynomials Q and a polynomial p as input and outputs a representation of the semidefinite set K d (Q, p). Moreover, there exists a constant c, independent of d, such that the formulas in the FPC interpretation have at most cd variables.
Therefore, as a consequence of Theorem 5 we obtain Corollary 1. Indeed, let us fix a positive integer d and let Φ be the FPC-interpretation from Fact 2. We compose Φ with the C ω ∞ω -sentence from Theorem 5 that decides the exact feasibility of semidefinite sets. The resulting sentence ψ decides the existence of an SOS proof of degree 2d. It is a sentence of C k ∞ω , where k = cd, for an integer c that is independent of d. A C ω ∞ω -sentence deciding the existence of an SOS refutation of degree 2d is obtained analogously by starting with an FPC-interpretation which takes as input a set of polynomials Q and outputs the semidefinite set K d (Q, −1).

Approximate SOS refutations
For any ǫ > 0, an ǫ-approximate degree-2d SOS refutation of a set of polynomials Q is an identity: where for every q ∈Q, the polynomial s q is a sum of squares, for each α of degree at least 1, we have |a α | ≤ ǫ, and |1 + a ∅ | ≤ ǫ. In the same way as the degree-2d SOS refutations correspond to the points in the semidefinite set K d (Q, −1), the ǫ-approximate degree-2d SOS refutations correspond to the points in the ǫ-relaxation of K d (Q, −1).
We will now relate the existence of SOS refutations to the primal and dual problems in the Lasserre hierarchy for the polynomial optimisation problem POP(0;Q). The goal is to use strong SDP duality for showing that, for small enough ǫ depending on the degree and the number of variables, the existence of SOS refutations is equivalent to the existence of ǫ-approximate ones. It follows that the problem of deciding the existence of SOS refutations of a fixed degree reduces, by means of FPC-interpretations, to the weak feasibility problem for semidefinite sets.
For any set of polynomials Q, the polynomial optimisation problem POP(0;Q) will be denoted by SOL(Q): Clearly, the optimisation problem SOL(Q) is feasible if and only if the system of polynomial inequalities {q ≥ 0 : q ∈ Q} has a 0/1-solution.
For a positive integer d, by (P d (Q), D d (Q)) we denote Lasserre SDP relaxation of the polynomial optimisation problem SOL(Q) of order d, i.e., P d (Q) is the semidefinite program: and D d (Q) is the semidefinite program: Observe that degree-2d SOS refutations of Q correspond precisely to the feasible solutions to D d (Q) with value 1 (see identity (22)). The following lemma summarizes the relationship between degree-2d SOS refutations of Q and solutions to the program D d (Q). The second equivalence follows from the fact that by multiplying a solution to D d (Q) with value v by any p ≥ 0 we obtain another solution with value pv. For a system of polynomials Q, a pseudoexpectation of degree 2d is a linear mapping F from the set of polynomials of degree at most 2d over the set of variables x 1 , . . . , x n to the reals such that F (1) = 1, and for every q ∈Q and every sum of squares polynomial s of degree at most 2d q , we have F (qs) ≥ 0.
A linear mapping from the set of polynomials of degree at most 2d to the reals is uniquely defined by its restriction to monomials. Therefore, there is a natural one-to-one correspondence between linear functions from the set of polynomials of degree at most 2d to the reals and assignments to the set of variables {y α : |α| ≤ 2d} of the program P d (Q), given by G(y α ) = F (x α ). It is easy to see that an assignment G to the variables of P d (Q) is a feasible solution if and only if F is a pseudoexpectation of degree 2d.

Lemma 10. There exists a degree-2d pseudoexpectation for Q if and only if the program
Proof. Let F be a linear functions from the set of polynomials of degree at most 2d to the reals and let G be the corresponding assignment to the variables of P d (Q). The statement of the lemma follows by showing that for every q ∈Q, the matrix M q,dq (G(y)) is positive semidefinite if and only if for every sum of squares polynomial s of degree at most 2d q , we have F (qs) ≥ 0.
Let us take some q ∈Q. Observe that for every matrix Z indexed by monomials of degree at most d q , we have M q,dq (G(y)), Z = F (M q,dq ), Z ) = F ( qM dq , Z ) = F (q M dq , Z ).
The matrix M q,dq (G(y)) is positive semidefinite if and only if for every positive semidefinite matrix Z indexed by monomials of degree at most d q , it holds M q,dq (G(y)), Z = F (q M dq , Z ) ≥ 0 if and only if F (qs) ≥ 0 for every sum of squares polynomial s of degree at most 2d q . The last equivalence follows from the fact that a polynomial s of degree at most 2t is a sum of squares if and only if there exists a positive semidefinite matrix Z indexed by monomials of degree at most t such that s = M t , Z .
Note that by summing the inequalities 1 − x 1 ≥ 0, . . . , 1 − x n ≥ 0, together with the inequalities x 1 − x 2 1 ≥ 0, . . . , x n − x 2 n ≥ 0 one obtains an inequality n − i∈[n] x 2 ≥ 0, which witnesses the fact that the problem SOL(Q) is encircled. Therefore, by Lemma 8 for the problem SOL(Q) there is no duality gap between primal and dual SDP problems in the Lasserre hierarchy and the optimal value of D d (Q) is +∞ if and only if P d (Q) is infeasible. As a consequence of Lemmas 9 and 10 we get the following. Suppose that Q has no degree-2d SOS refutation. By strong duality this implies the existence of a degree-2d pseudoexpectation. This in turn, as we will show now, precludes even the existence of ǫ-approximate refutations, for small enough ǫ. The key is the following lemma, which says that in the presence of boolean axioms the absolute values of a pseudoexpectation on the set of monomials are bounded by 1.
Lemma 11. If F is a degree-2d pseudoexpectation for Q, then 0 ≤ F (m) ≤ 1 for every monomial m of degree at most d, and −1 ≤ F (m) ≤ 1 for every monomial m of degree at most 2d.
Proof. First we show that if m is a monomial of degree at most 2d andm denotes its multilinearization, then F (m) = F (m). We do this by showing that F (x 2 m) = F (xm) for every variable x and every monomial m of degree at most 2d−2. Fix such a monomial m and let r and s be monomials of degree at most d − 1 such that m = rs. Note that m = p 2 − q 2 where p = (r + s)/2 and q = (r − s)/2, and both p 2 and q 2 have degree at most 2d − 2. It holds that This shows F ((x 2 − x)m) = 0 and hence F (x 2 m) = F (xm). Now we show that 0 ≤ F (m) ≤ 1 for every monomial m of degree at most d. By the previous paragraph we have F (m) = F (m 2 ), and F (m 2 ) ≥ 0 because m 2 is a square of degree at most 2d. The other inequality will be shown by induction on the degree. For the empty monomial 1 we have F (1) = 1. Now let m be a monomial of degree at most d − 1 such that F (m) ≤ 1 and let x be a variable. It holds that F (m) − F (xm) = F ((1 − x)m) = F ((1 − x)m 2 ) ≥ 0, and hence F (xm) ≤ F (m) ≤ 1.
The number of monomials of degree 2d over the set of n variables is n+2d−1 2d . Let ǫ n,d = 1/(3 n+2d−1 2d ). We are now ready to show that the existence of a degree-2d SOS refutation of a system of polynomial inequalities with n variables is equivalent to the existence of an ǫ n,d -approximate such refutation. Proof. If Q has an SOS refutation of degree 2d, then clearly it has an ǫ n,d -approximate refutation of degree 2d Now assume that Q has no SOS refutation of degree 2d. Therefore, by Corollary 2 there exists a pseudoexpectation of degree 2d. Let us denote it by F . Suppose that Q has an ǫ n,d -approximate SOS refutation of degree 2d, i.e., there exists a set of sum of squares polynomials {s q : q ∈Q} such that where for each α of degree at least 1, we have |a α | ≤ ǫ n,d , and |1 + a ∅ | ≤ ǫ n,d . Now, observe that F q∈Q qs q = q∈Q F (qs q ) ≥ 0, while F ( α a α x α ) = F (a ∅ ) + α a α F (x α ) ≤ −1 + ǫ n,d + n + 2d − 1 2d ǫ n,d ≤ − 1 3 .
The obtained contradiction finishes the proof.
An ǫ-relaxation of a convex set K is either empty, which clearly implies the emptiness of the set K itself, or it has volume greater than δ, where δ can be easily computed by means of FPC-interpretations from the representation of K and ǫ (see Lemma 6). We therefore get the following: Proof. The reduction is an FPC-interpretation which takes a set of polynomials Q with n variables as input and outputs the ǫ n,d -relaxation of K d (Q, −1) and a rational δ > 0, such that either the ǫ n,d -relaxation of K d (Q, −1) is empty, or it has volume greater than δ. Theorem 8. There exist an integer constant c such that, for all pairs of graphs G and H and all positive integers d, if there is a degree-2d SOS proof that G and H are not isomorphic, then there is a degree-cd SA proof that G and H are not isomorphic.
Proof. Fix a positive integer d. Let Φ be the FPC-interpretation from Fact 3 and compose it with the C ω ∞ω -sentence from Corollary 1 that decides the existence of an SOS proof of degree 2d. The resulting sentence φ is a sentence of C k ∞ω , where k = cd for an integer c that is independent of d. The sentence φ was designed in such a way that for every pair of graphs G and H it holds that (G, H) |= φ if and only if there is a degree-2d SOS proof that G and H are not isomorphic. In particular, since there certainly is no degree-2d SOS proof that G is not isomorphic to itself, we have (G, G) |= ¬φ. Now assume that there is no degree-k SA proof that G and H are not isomorphic. We get G ≡ k H by Theorem 7, from which it follows that (G, H) ≡ k (G, G). Since φ is a C k ∞ω -sentence and (G, G) |= ¬φ we get (G, H) |= ¬φ. Therefore, by design of φ, there is no degree-2d SOS proof that G and H are not isomorphic.
Next we use the following recent result of Berkholz [4] unexpectedly showing that SOS simulates PC; we remark that this result holds only for systems of equations with 0/1-values.
Theorem 9. Let Q be a system of polynomial equations over R with 0/1-valued variables. If Q has a PC refutation of degree d, then Q has an SOS refutation of degree 2d.
For two non-isomorphic graphs G and H, let sos(G, H), sa(G, H), monpc(G, H) and pc(G, H) denote the smallest degrees for which SOS, SA, monomial PC and PC can prove that G and H are not isomorphic, respectively. For isomorphic graphs let us take all three quantities to be ∞. Combining Theorems 9, 7, 8, we get the following full cycle of implications: where c is the constant in Theorem 8. By returning to the primals, the same results can be stated in terms of the number of levels that are required for the Lasserre [11] and the Sherali-Adams [15] hierarchies to become infeasible. The result says that, for any pair of graphs G and H, the first levels at which the relaxations for ISO(G, H) become infeasible are separated by no more than a constant c/2-factor.