15 problems

The language and proof system of non-hypothetical logic are considered over the axioms of Peano Arithmetic, denoted by $\mathsf{PA}$, in a purely relational language. One may also…

Let $\mathbf{QS5}$ be the quantified modal logic QS5, and consider its fragment using two individual variables and a single unary predicate letter. Decidability conjecture. The fra…

Let $\mathbf{QS5}$ be the quantified modal logic QS5, and consider its fragment using two individual variables and two unary predicate letters. Undecidability conjecture. The fragm…

Let $(\mathcal{F},\le)$ be a well-quasi-order (wqo), and suppose there are algorithms for basic problems related to $\le$, including deciding whether $X\le Y$ and, given $X$, findi…

Undecidability conjecture. The first-order theory of $(\mathbb{Z};<,+,g)$ is undecidable.

Undecidability conjecture. It is undecidable to check whether $\rho\geq 1$ for the joint spectral radius $\rho$.

Decidability equivalence. The following are equivalent:

Deficiency-one decidability conjecture. If $|A|-|R|=1$, then the Diophantine problem in $G$ is decidable.

The conjecture. Given a strongly terminating game $\mathcal{G}$, it is undecidable whether the winning positions of $\mathcal{G}$ form a regular language.

Let $\alpha$ be a non-quadratic scalar. Undecidability conjecture. $\alpha$-Presburger arithmetic sentences with three alternating blocks of quantifiers are undecidable. The paper…

Let $\psi$ be an $\textnormal{\textsf{MLSP}}$-formula, let $\mathrm{Vars}(\psi)$ be its set of variables, and let $M$ be a model of $\psi$. The subtheory…

Let $\mathcal{F}$ and $\mathcal{F}'$ be forbidden sets of permutation patterns with $|\mathcal{F}|=|\mathcal{F}'|=1$. Single-permutation decidability conjecture. Both the parity pr…

Let $X$ be a countable quasiminimal recursive subshift. The model-checking problem asks whether the language of $X$ intersects a given formal language. Locally testable decidabilit…

Disjunctive-binding decidability conjecture. The fragment $db$ enjoys a decidable satisfiability problem.

Conjunctive-binding positive-properties conjecture. The fragment $cb$ enjoys the finite-model property and has a decidable satisfiability problem.