# Questions tagged [descriptive-complexity]

Descriptive complexity classifies problems based on how hard it is to express the problem in some logical formalism.

14 questions with no upvoted or accepted answers
Filter by
Sorted by
Tagged with
0answers
264 views

### Descriptive complexity characterization of TimeSpace classes

Are there descriptive complexity characterizations for TimeSpace complexity classes like $\mathsf{SC^i}= \mathsf{DTimeSpace}(n^{O(1)},O(\lg^i n))$?
0answers
494 views

Denote the $k$-variable fragment of logic $L$ by $L^{(k)}$. The model-checking problem for a logic $L$ with respect to a class of structures $C$, denoted $MC(L,C)$, is the decision problem $MC(L,C)... 0answers 479 views ### To what extent MSO = WS1S, when adding relations? [This question has been asked on MathOverflow with no luck a month ago.] Let me first clarify my definitions. For a word$w \in \Sigma^*$, with$\Sigma =\{a_1, \ldots, a_n\}$, I define two ... 0answers 301 views ### Proof assistant formalizations of Finite Model Theory I'm wondering if anyone knows of a formalization (even limited) of any part of finite model theory in any of the major proof assistants. (I'm most familiar with Coq, but Isabelle, Agda, etc. would ... 0answers 166 views ### Descriptive Complexity characterzation of BPP We know of descriptive complexity characterizations of classes such as P, and NP, which use First Order logic, and operators. Does BPP have a characterization under descriptive complexity, too(any ... 0answers 349 views ### Collapsing of exptime and alternation bounded turing machine This question was already asked on math overflow, but I did not find any answer to my question (or let say the answer was that up to the knowledge of those people, no answer were known) Let C be a ... 0answers 199 views ### reference request: deciding validity of higher-order quantified boolean formulas is not Kalmar-elementary$\newcommand\iddots{⋰}$In "A simple proof of a theorem of Statman" (TCS 1992), Harry Mairson gives a simple proof of Statman's result that deciding$\beta\eta$-equality of terms in simply typed lambda ... 0answers 196 views ### Logic capturing automorphism-invariant$\mathsf{AC^0}$properties Q1. Is there a logic that is computable in polynomial-time which contains all order-invariant properties computable in smaller classes like$\mathsf{AC^0}$(or$\mathsf{TC^0}$)? Motivation As you ... 0answers 61 views ### Inexpressibility of Second order In finite model theory, Ehrenfeucht-Fraïssé games gives us tools to prove inexpressibility results for FOL. Pebble games do the same for infinitary logic with finitely many variables. Do we have such ... 0answers 61 views ### Complexity class name for the class of languages that are$\Sigma^1_1$-definable over finite domains Let${\cal L}=\{Y_1,..., Y_k, X\}$be a finite relational language such that$X$is a unary relation name. Let$\phi(X,\bar{Y})\in{\cal L}$be a first-order formula (the formula can have the equality ... 0answers 117 views ### Proof of SAT is complete for NP via first-order reductions So I have been reading this: https://people.cs.umass.edu/~immerman/book/ch7.pdf I do not understand the proof of theorem 7.16, which says that SAT is complete for NP via first-order reductions. My ... 0answers 136 views ### Do problems have to be statable in$\Pi_1\$ to use Levin's universal search to find short proofs if P=NP

In If P=NP, could we obtain proofs of Goldbach's Conjecture etc.? it talks about the hypothetical world where P=NP and using the proof of it to prove a problem/theorem assuming that it has a short ...
0answers
86 views

### Does Descriptive Complexity techniques have the naturalisation barrier?

I wished to know if the proof attempts at separation of complexity classes via the methods outlined by Descriptive Complexity theorists naturalise? By naturalise I'm talking about the Idea of Natural ...
0answers
154 views

### Questions about the definition of the Quantum Turing Machine

I am trying to have a better understanding of the definition of the Quantum Turing Machine. My questions: If the output of a quantum program is the eigenvalue of the ground state of a Hamiltonian ...