User emil jeřábek - MathOverflow

Answer by Emil Jeřábek for Reference request: Minimal Axiomatizations of PA over (+,x,<=).

2013-05-20T17:39:24Z

I can’t say I understand the rationale for using minimization instead of induction, but the following works:

$x+0=x$
$x+S(y)=S(x+y)$
$x\cdot0=0$
$x\cdot S(y)=x\cdot y+x$
$x=0\lor\exists y\,x=S(y)$
$S(x)\le y\to x< y$
$\phi(x)\to\exists z\,(\phi(z)\land\forall y\,(\phi(y)\to z\le y))$

where in 6 and below, $x< y$ is a short-hand for $x\le y\land x\ne y$.

By applying 7 to the formula $x=u\lor x=v$, we get $$\tag{8}u\le v\lor v\le u,$$ and specializing to $u=v$ gives $$\tag{9}u\le u.$$ Since $x=x$ and a fortiori $x\nless x$, 6 implies $$S(x)\nleq x.\tag{10}$$ We can prove the induction schema $$\phi(0)\land\forall x\,(\phi(x)\to\phi(S(x)))\to\forall x\,\phi(x)\tag{11}$$ as follows: assume for contradiction $\neg\phi(x)$, and let $x$ be the smallest such, as given by 7. We cannot have $x=0$, hence $x=S(y)$ for some $y$ by 5. Then $\neg\phi(y)$ by the premise of the induction axiom, hence $x=S(y)\le y$ by the minimality of $x$, contradicting 10.

We can prove $$x\le 0\to x=0\tag{12}$$ by induction on $x$ using 6. Also, 8 and 12 imply $$0\le x\tag{13}.$$ Finally, assume for contradiction that there are $x,y$ such that $$x< y< S(x).\tag{$*$}$$ Let $x$ be the smallest for which such a $y$ exist, and let $y$ be the smallest for this $x$. We cannot have $y=0$ by 12, hence $y=S(z)$ for some $z$. We have $z< S(x)$ by 6, but $y\nleq z$ by 10, hence the minimality of $y$ implies $x\nless z$, thus $z\le x$ by 8. If $x=z$, then $y=S(x)$ contradicts the assumption $y< S(x)$. Otherwise $z< x< S(z)$, hence the minimality of $x$ implies $x\le z$, thus $x< z$, a contradiction.

In view of 8, the impossibility of $(*)$ implies the converse of 6: $$x< y\to S(x)\le y.\tag{14}$$ By the Appendix of http://math.cas.cz/~jerabek/papers/t02.pdf, 1–4,6,11,13,14 imply the remaining axioms of PA.

Answer by Emil Jeřábek for Basic results with three or more hypotheses

2013-05-16T10:43:52Z

Let $K$ be an ordered field, and $v$ a valuation on $K$ with convex valuation ring. If $(K,v)$ is henselian, the value group is divisible, and the residue field is real-closed, then $K$ itself is a real-closed field.

There is also an analogous statement for algebraically closed fields of characteristic $0$.

Answer by Emil Jeřábek for Verifying the correctness of a Sudoku solution

2013-05-06T19:12:38Z

$\DeclareMathOperator\span{span}$Here is an argument which works for general $n\times n$ Sudokus, $n\ge 2$, using some ideas from the other answers (namely, casting the problem in terms of linear algebra as in François Brunault’s answer, and the notion of alternating paths below is related to the even sets as in Tony Huynh’s answer, attributed to Zack Wolske).

I will denote the cells as $s_{ijkl}$ with $0\le i,j,k,l< n$, where $i$ identifies the band, $j$ the stack, $k$ the row within band $i$, and $l$ the column within stack $j$. Rows, columns, and blocks are denoted $r_{ik},c_{jl},b_{ij}$ accordingly. Let $X=\{r_{ik},c_{jl},b_{ij}:i,j,k,l< n\}$ be the set of all $3n^2$ checks. For $S\subseteq X$ and $x\in X$, I will again denote by $S\models x$ the consequence relation “every Sudoku grid satisfying all checks from $S$ also satisfies $x$”.

Let $V$ be the $\mathbb Q$-linear space with basis $X$, and $V_0$ be the span of the vectors $\sum_kr_{ik}-\sum_jb_{ij}$ for $i< n$, and $\sum_lc_{jl}-\sum_ib_{ij}$ for $j< n$.

Lemma 1: If $x\in\span(S\cup V_0)$, then $S\models x$.

Proof: A grid $G$ induces a linear mapping $\phi_G$ from $V$ into an $n^2$-dimensional such that for any $x'\in X$, the $i$th coordinate of $\phi_G(x')$ gives the number of occurrences of the number $i$ in $x'$. We have $\phi_G(V_0)=0$, and $G$ satisfies $x'$ iff $\phi_G(x')$ is the constant vector $\vec 1$. If $x=\sum_i\alpha_ix_i+y$, where $x_i\in S$ and $y\in V_0$, then $\phi_G(x)=\vec\alpha$ for $\alpha:=\sum_i\alpha_i$. The same holds for every grid $G'$ satisfying $S$; in particular, it holds for any valid grid, which has $\phi_{G'}(x)=\vec1$, hence $\alpha=1$. QED

We intend to prove that the converse holds as well, so assume that $x\notin\span(S\cup V_0)$. We may assume WLOG $x=r_{00}$ or $x=b_{00}$, and we may also assume that $r_{i0}\notin S$ whenever $r_{ik}\notin S$ for some $k$, and $c_{j0}\notin S$ whenever $c_{jl}\notin S$ for some $l$. By assumption, there exists a linear function $\psi\colon V\to\mathbb Q$ such that $\psi(S\cup V_0)=0$, and $\psi(x)\ne0$. The space of all linear functions on $V$ vanishing on $V_0$ has dimension $3n^2-2n$, and one checks easily that the following functions form its basis:

$\omega_{ik}$ for $0\le i< n$, $0< k< n$: $\omega_{ik}(r_{ik})=1$, $\omega_{ik}(r_{i0})=-1$.
$\eta_{jl}$ for $0\le j< n$, $0< l< n$: $\eta_{jl}(c_{jl})=1$, $\eta_{jl}(c_{j0})=-1$.
$\xi_{ij}$ for $i,j< n$: $\xi_{ij}(r_{i0})=\xi_{ij}(c_{j0})=\xi_{ij}(b_{ij})=1$.

(The functions are zero on basis elements not shown above.) We can thus write $$\psi=\sum_{ik}u_{ik}\omega_{ik}+\sum_{jl}v_{jl}\eta_{jl}+\sum_{ij}z_{ij}\xi_{ij}.$$ If $r_{ik}\in S$, $k\ne0$, then $0=\psi(r_{ik})=u_{ik}$, and similarly $c_{jl}\in S$ for $l\ne0$ implies $v_{jl}=0$. Thus, the functions $\omega_{ik}$ and $\eta_{jl}$ that appear in $\psi$ with a nonzero coefficient individually vanish on $S$. The only case when they can be nonzero on $x$ is $\omega_{0k}$ if $x=r_{00}$ and $r_{00},r_{0k}\notin S$, but then taking any valid grid and swapping cells $s_{0000}$ and $s_{00k0}$ shows that $S\nvDash x$ and we are done. Thus we may assume that the first two sums in $\psi$ vanish on $S\cup\{x\}$, and therefore the third one vanishes on $S$ but not on $x$, i.e., WLOG $$\psi=\sum_{ij}z_{ij}\xi_{ij}.$$ That $\psi$ vanishes on $S$ is then equivalent to the following conditions on the matrix $Z=(z_{ij})_{i,j< n}$:

$z_{ij}=0$ if $b_{ij}\in S$,
$\sum_jz_{ij}=0$ if $r_{i0}\in S$,
$\sum_iz_{ij}=0$ if $c_{j0}\in S$.

Let us say that an alternating path is a sequence $e=e_p,e_{p+1},\dots,e_q$ of pairs $e_m=(i_m,j_m)$, $0\le i_m,j_m< n$, such that

$i_m=i_{m+1}$ if $m$ is even, and $j_m=j_{m+1}$ if $m$ is odd,
the indices $i_p,i_{p+2},\dots$ are pairwise distinct, except that we may have $e_p=e_q$ if $q-p\ge4$ is even,
likewise for the $j$s.

If $m$ is even, the incoming line of $e_m$ is the column $c_{j_m0}$, and its outgoing line is the row $r_{i_m0}$. If $m$ is odd, we define it in the opposite way. An alternating path for $S$ is an alternating path $e$ such that $b_{i_mj_m}\notin S$ for every $m$, and either $e_p=e_q$ and $q-p\ge4$ is even ($e$ is an alternating cycle), or the incoming line of $e_p$ and the outgoing line of $e_q$ do not belong to $S$.

Every alternating path $e$ induces a matrix $Z_e$ which has $(-1)^m$ at position $e_m$ for $m=p,\dots,q$, and $0$ elsewhere. It is easy to see that if $e$ is an alternating path for $S$, then $Z_e$ satisfies conditions 1, 2, 3.

Lemma 2: The space of matrices $Z$ satisfying 1, 2, 3 is spanned by matrices induced by alternating paths for $S$.

Proof: We may assume that $Z$ has integer entries, and we will proceed by induction on $\|Z\|:=\sum_{ij}|z_{ij}|$. If $Z\ne 0$, pick $e_0=(i_0,j_0)$ such that $z_{i_0j_0}>0$. If the outgoing line of $e_0$ is outside $S$, we put $q=0$, otherwise condition 2 guarantees that $z_{i_0,j_1}< 0$ for some $j_1$, and we put $i_1=i_0$, $e_1=(i_1,j_1)$. If the outgoing line of $e_1$ is outside $S$, we put $q=1$, otherwise we find $i_2$ such that $z_{i_2j_1}>0$ by condition 3, and put $j_2=j_1$. Continuing in this fashion, one of the following things will happen sooner or later:

The outgoing line of the last point $e_m$ constructed contains another point $e_{m'}$ (and therefore two such points, unless $m'=0$). In this case, we let $p$ be the maximal such $m'$, we put $q=m+1$, $e_q=e_p$ to make a cycle, and we drop the part of the path up to $e_{p-1}$.
The outgoing line of $e_m$ is outside $S$. We put $q=m$.

In the second case, we repeat the same construction going backwards from $e_0$. Again, either we find a cycle, or the construction stops with an $e_p$ whose incoming line is outside $S$. Either way, we obtain an alternating path for $S$ (condition 1 guarantees that $b_{i_mj_m}\notin S$ for every $m$). Moreover, the nonzero entries of $Z_e$ have the same sign as the corresponding entries of $Z$, thus $\|Z-Z_e\|<\|Z\|$. By the induction hypothesis, $Z-Z_e$, and therefore $Z$, is a linear combination of some $Z_e$s. QED

Now, Lemma 2 implies that we may assume that our $\psi$ comes from a matrix $Z=Z_e$ induced by an alternating path $e=e_p,\dots,e_q$. Assume that $G$ is a valid Sudoku grid that has $1$ in cells $s_{i_mj_m00}$ for $m$ even, and $2$ for $m$ odd. Let $G'$ be the grid obtained from $G$ by exchanging $1$ and $2$ in these positions. Then $G'$ violates the following checks:

$b_{i_mj_m}$ for each $m$.
If $e$ is not a cycle, the incoming line of $e_p$, and the outgoing line of $e_q$.

Since $e$ is an alternating path for $S$, none of these is in $S$. On the other hand, $\psi(x)\ne0$ implies that $x$ is among the violated checks, hence $S\nvDash x$.

It remains to show that such a valid grid $G$ exists. We can now forget about $S$, and then it is easy to see that every alternating path can be completed to a cycle, hence we may assume $e$ is a cycle. By applying Sudoku permutations and relabelling the sequence, we may assume $p=0$, $i_m=\lfloor m/2\rfloor$, $j_m=\lceil m/2\rceil$ except that $i_q=j_q=j_{q-1}=0$. We are thus looking for a solution of the following grid: $$\begin{array}{|ccc|ccc|ccc|ccc|ccc|} \hline 1&&&2&&&&&&&&&&&&\\ \strut&&&&&&&&&&&&&&&\\ \strut&&&&&&&&&&&&&&&\\ \hline &&&1&&&2&&&&&&&&&\\ &&&&&&&&&&&&&&\cdots&\\ &&&&&&&&\ddots&&&&&&&\\ \hline 2&&&&&&&&&1&&&&&&\\ \strut&&&&&&&&&&&&&&&\\ \strut&&&&&&&&&&&&&&&\\ \hline \strut&&&&&&&&&&&&&&&\\ \strut&&&&\vdots&&&&&&&&&&&\\ \strut&&&&&&&&&&&&&&&\\ \hline \end{array}$$ where the upper part is a $q'\times q'$ subgrid, $q'=q/2$.

If $q'=n$, we can define the solution easily by putting $s_{ijkl}=(k+l,j-i+l)$, where we relabel the numbers $1,\dots,n^2$ by elements of $(\mathbb Z/n\mathbb Z)\times(\mathbb Z/n\mathbb Z)$, identifying $1$ with $(0,0)$ and $2$ with $(0,1)$. In the general case, we define $s_{ijkl}=(k+l+a_{ij}-b_{ij},l+a_{ij})$. It is easy to check that this is a valid Sudoku if the columns of the matrix $A=(a_{ij})$ and the rows of $B=(b_{ij})$ are permutations of $\mathbb Z/n\mathbb Z$. We obtain the wanted pattern if we let $a_{ij}=b_{ij}=j-i\bmod{q'}$ for $i,j< q'$, and extend this in an arbitrary way so that the columns of $A$ and the rows of $B$ are permutations.

This completes the proof that $x\notin\span(S\cup V_0)$ implies $S\nvDash x$. This shows that $\models$ is a linear matroid, and we get a description of maximal incomplete sets of checks by means of alternating paths.

We can also describe the minimal dependent sets. Put $$D_{R,C}=\{r_{ik}:i\in R,k< n\}\cup\{c_{jl}:j\in C,l< n\}\cup\{b_{ij}:(i\in R\land j\notin C)\lor(i\notin R\land j\in C)\}$$ for $R,C\subseteq\{0,\dots,n-1\}$. If $R$ or $C$ is nonempty, so is $D_{R,C}$, and $$\sum_{i\in R}\Bigl(\sum_kr_{ik}-\sum_jb_{ij}\Bigr)-\sum_{j\in C}\Bigl(\sum_lc_{jl}-\sum_ib_{ij}\Bigr)\in V_0$$ shows that $D_{R,C}$ is dependent. On the other hand, if $D$ is a dependent set, there is a linear combination $$\sum_i\alpha_i\Bigl(\sum_kr_{ik}-\sum_jb_{ij}\Bigr)-\sum_j\beta_j\Bigl(\sum_lc_{jl}-\sum_ib_{ij}\Bigr)\ne0$$ where all basic vectors with nonzero coefficients come from $D$. If (WLOG) $\alpha:=\alpha_{i_0}\ne0$, put $R=\{i:\alpha_i=\alpha\}$ and $C=\{j:\beta_j=\alpha\}$. Then $R\ne\varnothing$, and $D_{R,C}\subseteq D$.

On the one hand, this implies that every minimal dependent set is of the form $D_{R,C}$. On the other hand, $D_{R,C}$ is minimal unless it properly contains some $D_{R',C'}$, and this can happen only if $R'\subsetneq R$ and $C=C'=\varnothing$ or vice versa. Thus $D_{R,C}$ is minimal iff $|R|+|C|=1$ or both $R,C$ are nonempty.

This also provides an axiomatization of $\models$ by rules of the form $D\smallsetminus\{x\}\models x$, where $x\in D=D_{R,C}$ is minimal. It is easy to see that if $R=\{i\}$ and $C\ne\varnothing$, the rules for $D_{R,C}$ can be derived from the rules for $D_{R,\varnothing}$ and $D_{\varnothing,\{j\}}$ for $j\in C$, hence we can omit these. (Note that the remaining sets $D_{R,C}$ are closed, hence the corresponding rules have to be included in every axiomatization of $\models$.)

To sum it up:

Theorem: Let $n\ge2$.

$S\models x$ if and only if $x\in\span(S\cup V_0)$. In particular, $\models$ is a linear matroid.
All minimal complete sets of checks have cardinality $3n^2-2n$. (One such set consists of all checks except for one row from each band, and one column from each stack.)
The closed sets of $\models$ are intersections of maximal closed sets, which are complements of Sudoku permutations of the sets
- $\{b_{00},b_{01},b_{11},b_{12},\dots,b_{mm},b_{m0}\}$ for $0< m< n$
- $\{c_{00},b_{00},b_{01},b_{11},b_{12},\dots,b_{mm},r_{m0}\}$ for $0\le m< n$
- $\{c_{00},b_{00},b_{01},b_{11},b_{12},\dots,b_{m-1,m},c_{m1}\}$ for $0\le m< n$
The minimal dependent sets of $\models$ are the sets $D_{R,C}$, where $R,C\subseteq\{0,\dots,n-1\}$ are nonempty, or $|R|+|C|=1$.
$\models$ is the smallest consequence relation such that $D_{R,C}\smallsetminus\{x\}\models x$ whenever $x\in D_{R,C}$ and either $|R|,|C|\ge2$, or $|R|+|C|=1$.

Answer by Emil Jeřábek for Smallest base to reach partial recursive functions as a closure of unbound search

2013-05-06T13:24:43Z

$\def\dotm{\mathbin{\dot-}}$It follows from the MRDP theorem that every partial recursive function $f(\vec x)$ can be written as $f(\vec x)\simeq l(\mu z\,[p(\vec x,l(z),l(r(z)),\dots,l(r^{k-1}(z)),r^k(z))=0])$, where $p(\vec x,y_0,\dots,y_k)$ is a polynomial with integer coefficients, and $l(z)$ and $r(z)$ are the left and right inverse of a pairing function. If we take the Cantor pairing function $[x,y]=\frac12(x+y)(x+y+1)+x$, we can express $l(z)=z-[0,g(z)]$, $r(z)=g(z)-l(z)$, where $g(z)=\mu u\,[2z\dotm(u+1)(u+2)=0]$. Thus, partial recursive functions are the closure of projections, successor, multiplication, and limited subtraction under minimization and composition. (Note that $x+y=S(x)S(y)\dotm ((S(x)S(y)\dotm x)\dotm y)$.)

Answer by Emil Jeřábek for Verifying the correctness of a Sudoku solution

2013-05-02T13:58:45Z

I couldn’t find all my original notes, but I have reconstructed the gist of it.

First, validity of Sudoku grids is preserved by transposition, permutations of bands, permutations of rows within bands, permutations of stacks, and permutations of columns within stacks. Below I will use “Sudoku permutation” as a short-hand for permutations from the group generated by these transformations. Also, I will write “blocks” instead of what is called “squares” in the question, since the latter is commonly used to denote single cells.

Let us say that a set of checks $S\subseteq\{r_1,\dots,r_9,c_1,\dots,c_9,b_1,\dots,b_9\}$ is complete if every Sudoku grid satisfying the checks from $S$ satisfies all checks (i.e., it is a valid grid). One can characterize complete sets of checks by describing either minimal complete sets, or maximal incomplete sets. I will mostly refer to complements of these sets, as they have less elements.

As was already observed in the question, there are complete sets of 21 checks. (I prefer the following symmetric solution: check all blocks, two rows in each band, and two columns in each stack.) It follows from the description below that this number is optimal, as all minimal complete sets of checks have 21 elements.

Proposition 1. The following are equivalent:

$S$ is complete.
All checks can be derived from $S$ by means of the following rule: if $S$ includes all but one of the 6 checks contained in a given band or stack, add the remaining one to $S$.
$S$ is not included in the complement of a Sudoku permutation of one of the following sets:

a) $\{r_1,r_2\}$

b) $\{r_1,c_1,b_1\}$

c) $\{b_1,b_2,b_4,b_5\}$

d) $\{r_1,r_4,b_1,b_4\}$

e) $\{r_1,c_1,b_2,b_4,b_5\}$

f) $\{b_2,b_3,b_4,b_6,b_7,b_8\}$

g) $\{r_1,r_4,b_1,b_5,b_7,b_8\}$

h) $\{r_1,c_1,b_3,b_5,b_6,b_7,b_8\}$
$S$ includes the complement of a Sudoku permutation of one of the following sets (there may well be some errors in the list, but the only relevant information is that they all have 6 elements): $\{r_1,r_4,r_7,c_1,c_4,c_7\}$, $\{r_1,r_4,c_1,c_4,c_7,b_7\}$, $\{r_1,r_4,c_1,c_4,b_6,b_9\}$, $\{r_1,r_4,c_1,c_4,b_6,b_8\}$, $\{r_1,c_1,c_4,c_7,b_6,b_9\}$, $\{r_1,c_1,c_4,c_7,b_6,b_8\}$, $\{r_1,c_1,c_4,b_3,b_6,b_9\}$, $\{r_1,c_1,c_4,b_3,b_6,b_8\}$, $\{r_1,c_1,c_4,b_3,b_5,b_8\}$, $\{r_1,c_1,c_4,b_3,b_5,b_7\}$, $\{r_1,c_1,c_4,b_5,b_6,b_9\}$, $\{r_1,c_1,c_4,b_5,b_6,b_8\}$, $\{r_1,c_1,b_2,b_3,b_4,b_7\}$, $\{r_1,c_1,b_2,b_3,b_6,b_7\}$, $\{r_1,c_1,b_2,b_3,b_6,b_8\}$, $\{r_1,c_1,b_2,b_3,b_6,b_9\}$, $\{r_1,c_1,b_3,b_6,b_7,b_8\}$, $\{r_1,c_1,b_3,b_6,b_8,b_9\}$, $\{r_1,c_1,b_3,b_5,b_7,b_8\}$, $\{r_1,c_1,b_3,b_5,b_8,b_9\}$, $\{c_1,c_4,c_7,b_1,b_4,b_7\}$, $\{c_1,c_4,c_7,b_1,b_4,b_8\}$, $\{c_1,c_4,c_7,b_1,b_5,b_9\}$, $\{c_1,c_4,b_2,b_3,b_5,b_8\}$, $\{c_1,c_4,b_2,b_3,b_5,b_9\}$, $\{c_1,c_4,b_2,b_3,b_6,b_9\}$, $\{c_1,c_4,b_2,b_3,b_6,b_7\}$, $\{c_1,c_4,b_2,b_5,b_6,b_7\}$, $\{c_1,b_1,b_2,b_3,b_4,b_7\}$, $\{c_1,b_1,b_2,b_3,b_4,b_8\}$, $\{c_1,b_1,b_2,b_3,b_5,b_9\}$, $\{c_1,b_1,b_2,b_3,b_6,b_9\}$, $\{c_1,b_1,b_2,b_4,b_6,b_7\}$, $\{c_1,b_2,b_3,b_4,b_6,b_9\}$, $\{c_1,b_2,b_3,b_6,b_7,b_8\}$, $\{c_1,b_3,b_4,b_6,b_7,b_8\}$, $\{c_1,b_2,b_3,b_4,b_7,b_8\}$.

Proof (part):

$2\to1$ follows from the soundness of the rule: if, say, a grid satisfies 3 block checks and two row checks incident with the same band, each number occurs three times in the band, and twice in the checked rows, hence it occurs once in the remaining row.

$4\to2$: draw 37 pictures, and chase applications of the rule.

$1\to3$: For each of the cases a–h, we need to find an invalid grid which satisfies checks outside the given set.

a) Take any valid grid, and swap the elements in cells 1:1 and 2:1 (that’s row and column number).

b) Take a valid grid, and modify cell 1:1.

c) There exists a valid grid with 1 in cells 1:1, 4:4, and 2 in cells 1:4, 4:1. Exchange 1 and 2 in these four cells.

d) Take a valid grid, and swap the elements in cells 1:1 and 4:1.

e) Do the same as in c), but leave 1 in cell 1:1.

f) There exists a valid grid with 1 in cells 1:4, 4:7, 7:1, and 2 in cells 1:7, 4:1, and 7:4. Exchange 1 and 2 in these six cells. $$\begin{array}{|ccc|ccc|ccc|} \hline 3&4&5&\color{green}1&6&7&\color{green}2&8&9\\ 6&7&8&3&2&9&4&1&5\\ 9&1&2&4&5&8&3&6&7\\ \hline \color{green}2&3&4&5&7&6&\color{green}1&9&8\\ 5&6&9&8&1&2&7&3&4\\ 7&8&1&9&3&4&5&2&6\\ \hline \color{green}1&9&6&\color{green}2&4&5&8&7&3\\ 4&2&7&6&8&3&9&5&1\\ 8&5&3&7&9&1&6&4&2\\ \hline \end{array}$$

g) Do the same as in f), but leave cells 1:7 and 4:7 unchanged. This is g) up to permutation.

h) Do the same as in f), but leave one of the six cells unchanged. (Again, up to permutation.)

$3\to4$: This is a tedious but straightforward case analysis, much easier done with pictures than with words, so I’m omitting it.

Let us consider a more general problem: a set of checks $S$ implies a check $x$, written $S\models x$, if every Sudoku grid satisfying all checks from $S$ also satisfies $x$. Thus defined $\models$ is a consequence relation (or closure operator). Note that $S$ is complete iff $S\models x$ for every $x$ (i.e., iff $S$ is inconsistent in the usual consequence relation terminology).

Let $\mathcal D$ be the set of all Sudoku permutations of the following sets:

(i) $\{r_1,r_2,r_3,b_1,b_2,b_3\}$,

(ii) $\{r_1,\dots,r_9,c_1,\dots,c_9\}$,

(iii) $\{r_1,\dots,r_9,c_1,\dots,c_6,b_3,b_6,b_9\}$,

(iv) $\{r_4,\dots,r_9,c_4,\dots,c_9,b_2,b_3,b_4,b_7\}$.

(I don’t know how to draw decent pictures this time, as everything overlaps everything else.) Define $S\vdash x$ to be the consequence relation axiomatized by rules of the form $D\smallsetminus\{x\}\vdash x$, where $x\in D\in\mathcal D$.

Let $\mathcal M$ be the set of all complements of Sudoku permutations of the sets a, ..., h above. The third consequence relation is defined as follows: $S\Vdash x$ iff $S\subseteq M$ implies $x\in M$ for every $M\in\mathcal M$. (In other words, closed sets of $\Vdash$ are exactly the intersections of subfamilies of $\mathcal M$.)

Proposition 2: ${\models}={\vdash}={\Vdash}$.

Proof:

$S\vdash x\implies S\models x$:

This amounts to showing that $D\smallsetminus\{x\}\models x$ for $x\in D\in\mathcal D$. For example, let $D$ be the set in (iv), and $x=b_3$. Fix a Sudoku grid satisfying $\{r_4,\dots,r_9,c_4,\dots,c_9,b_2,b_4,b_7\}$, and let $n=1,\dots,9$. The number $n$ occurs 3 times in the bottom band by $r_7,r_8,r_9$, one of which occurrences is in $b_7$, hence it occurs twice in $b_8\cup b_9$. The same argument shows that it occurs twice in $b_5\cup b_6$ and in $b_5\cup b_8$, hence it occurs twice in $b_6\cup b_9$. Since there are three occurrences in the rightmost stack by $c_7,c_8,c_9$, $n$ occurs once in $b_3$. As $n$ was arbitrary, this means that $b_3$ is correct.

$S\models x\implies S\Vdash x$:

This means that for every set $M\in\mathcal M$ and $x\notin M$, there exists a grid satisfying $M$ and not $x$. We have verified this in the proof of Proposition 1.

$S\Vdash x\implies S\vdash x$:

We need to show that if $S$ is a maximal set such that $S\nvdash x$, there is $M\in\mathcal M$ such that $S\subseteq M$ and $x\notin M$. This is again done by a case analysis. By symmetry, it suffices to consider the cases $x=r_1$ and $x=b_1$. I will briefly write down the proof so that it does not appear that I’m making unjustified claims all the time.

Case $x=r_1$: We have $r_1\notin S$. If $r_2\notin S$ or $r_3\notin S$, we are done by a), hence assume $r_2,r_3\in S$. As $S$ is closed under the (i) rule, some block from the first band is missing from $S$. By symmetry, we may assume $b_1\notin S$. If some column incident with $b_1$ is missing, we are done by b), hence assume $c_1,c_2,c_3\in S$. By (i) for the first stack, WLOG $b_4\notin S$. If some row from the middle band is missing, we are done by d), hence assume $r_4,r_5,r_6\in S$. By (i) for the middle band, WLOG $b_5\notin S$. If some column in the middle stack is missing, e) applies, hence assume $c_4,c_5,c_6\in S$.

Case 1: $r_7,r_8,r_9\in S$. Then some column, WLOG $c_7$, is missing from $S$ by (ii). If $b_3\notin S$ or $b_6\notin S$, we are done by b) or e), respectively. Thus $b_3,b_6\in S$, hence $b_9\notin S$ by (iii). By (iv), $b_7\notin S$ or $b_8\notin S$, hence e) or h) applies.

Case 2: some row, WLOG $r_7$, is missing. Then $b_7,b_8\in S$ unless d) or g) applies. By (iv), $b_3\notin S$ or $b_6\notin S$, hence we are done by d) or g), respectively, unless $b_9\in S$. Then WLOG $c_7\notin S$ by (iii), hence we are done by b) or e).

Case $x=b_1$: If some row and column incident with $b_1$ are missing from $S$, we are done by b), hence WLOG $r_1,r_2,r_3\in S$. By (i), WLOG $b_2\notin S$. If columns are missing in both the first two stacks, we are done by d), hence WLOG $c_1,c_2,c_3\in S$. Then WLOG $b_4\notin S$ by (i). If $b_5\notin S$, we are done by c), hence assume $b_5\in S$. If $b_6,b_8\notin S$, then $b_3,b_7,b_9\in S$ unless c) or f) applies, thus some row and column incident with $b_9$ are missing by (i), hence we are done by h). If $b_6,b_8\in S$, some row and column incident with $b_5$ are missing by (i), hence we are done by e). Thus, we can assume $b_6\in S$ and $b_8\notin S$. By (i), WLOG $r_4\notin S$. Then $r_7,r_8,r_9\in S$ unless g) applies, and $c_4,c_5,c_6\in S$ unless e) applies. If $b_7\notin S$, c) applies, otherwise $b_9\notin S$ by (i). By (iii), WLOG $c_7\notin S$, hence we are done by h).

QED

I know next to nothing about matroid theory so I let others to figure it out, but the symmetric form of the rules defining $\vdash$ makes me suspect that the closure operator is in fact a matroid.

Answer by Emil Jeřábek for Weakest choice principle required for Robertson-Seymour Graph Minor Theorem?

2013-04-30T12:04:44Z

As far as I can see, the Robertson–Seymour theorem is provable in plain ZF.

First, the restricted version of the theorem for graphs whose vertices are natural numbers can be written as a $\Pi^1_1$ second-order arithmetical sentence, hence its provability in ZF follows from its provability in ZFC by the Schoenfield absoluteness theorem. (Note that the set of all such finite graphs is countable, hence well-orderable, thus all the common definitions of wqo coincide in this case without the need for any choice.)

Second, ZF proves that the general case is equivalent to the restricted case. I will take the definition of wqo requiring that every subset has a finite basis: this is the most natural formulation in set theory without choice, and it implies in ZF both the property given in the original question, and the property that for every sequence $\{x_i:i\in\mathbb N\}$, there exist $i< j$ with $x_i\le x_j$.

So, assume that $X$ is a set of finite graphs. Let $X'$ be the set of all graphs with integer vertices isomorphic to some graph in $X$. By the restricted version of the theorem, we can find a finite basis $B'\subseteq X'$, say $B'=\{G_i':i< n\}$. In ZF, we have choice for finite families, hence we can find $B:=\{G_i:i< n\}\subseteq X$ such that $G_i\simeq G_i'$ for each $i< n$. Then $B$ is a finite basis for $X$: if $G\in X$, there exists $G'\in X'$ isomorphic to $G$ (as the vertex set of $G$ is finite, it is in bijection with some $\{0,\dots,m-1\}\subseteq\mathbb N$, and we can lift the graph along this bijection). Since $B'$ is a basis of $X'$, some $G_i'\in B'$ is a minor of $G'$, hence $G_i\in B$ is a minor of $G$.

Answer by Emil Jeřábek for Zeros of polynomials in discretely ordered rings

2013-04-24T15:21:28Z

The answer is no. The argument below is essentially due to Kaye [1] (Lemmas 2.1 and 5.8). Put $$p(a,x,y)=x^2-2axy+y^2-1.$$

Lemma 1: In any discretely ordered ring (DOR), if $p(a,x,y)=0$, $0< x\le y$, and $a>0$, then $y\le 2ax\le x+y$ and $p(a,2ax-y,x)=0$.

Proof: Straightforward computation.

Lemma 2: Let $n\in\mathbb N$. In any DOR, if $p(a,x,y)=0$, $0\le x\le y$, $n\le b\le a-2$, $x\equiv b\pmod{a-1}$, and $y\equiv b+1\pmod{a-1}$, then $y\ge a^n$.

Proof: By induction on $n$. For $n=1$, $y< a$ together with the congruences implies $x=b$ and $y=b+1$, whence $-p(a,x,y)=2b^2(a-1)+2ab+1>0$. Assume the statement holds for $n$, we prove it for $n+1$. The assumption $p(a,x,y)=0$ together with Lemma 1 gives $p(a,2ax-y,x)=0$, where $0\le2ax-y\le x$ and $2ax-y\equiv b-1\pmod{a-1}$. By the induction hypothesis, $x\ge a^n$, hence by Lemma 1, $y\ge(2a-1)a^n\ge a^{n+1}$.

Now, let $q(\vec w)$ be an integer polynomial that has no roots in $\mathbb Z$, but has roots in some model of, say, PA (or rather the ring obtained from a model of PA by adding a negative part). Then the polynomial $r(a,\vec w)=\bigl(a-\sum_iw_i^2\bigr)^2+q^2(\vec w)$ is also solvable in a model $M$ of PA, but any its root in a DOR must have $a$ larger than every integer. Put \begin{multline}f(a,\vec w,u_0,u_1,u_2,u_3,v_0,v_1,v_2,v_3)=\\ \textstyle r^2(a,\vec w)+p^2\bigl(a,(1+\sum_iu_i^2)(a-1)-1,(1+\sum_iu_i^2+\sum_iv_i^2)(a-1)\bigr).\end{multline} If we take a root of $f$ in a DOR $R$, then $a>n$ for every $n\in\mathbb N$. Putting $b=a-2$, $x=(1+\sum_iu_i^2)(a-1)-1$, $y=(1+\sum_iu_i^2+\sum_iv_i^2)(a-1)$, Lemma 2 implies that $y\ge a^n$ for every $n\in\mathbb N$, hence $R$ does not have rank 1.

On the other hand, PA (or even much weaker theories, see Lemma 2.2, 2.3 in [1]) proves that for every $a\ge b+2$ there are $x,y$ satisfying the properties in Lemma 2, and it also proves Lagrange’s four-square theorem, hence $f$ has a root in $M$.

Reference:

[1] Richard Kaye, Diophantine induction, Annals of Pure and Applied Logic 46 (1990), no. 1, pp. 1–40.

Answer by Emil Jeřábek for Does any lower bound on proofs of FLT improve Shepherdson 1965?

2013-04-16T13:46:06Z

Leszek Kołodziejczyk has devised a method how to extend some type of Shepherdson-like models of IOpen into models of Buss’s theory $T^0_2$ (a weak subsystem of $I\Delta_0+\Omega_1$). In particular, he has shown that $T^0_2$ does not prove that $x^3+y^3=z^3$ has no nontrivial solution.

Answer by Emil Jeřábek for When does $ZFC \vdash\ ' ZFC \vdash \varphi\ '$ imply $ZFC \vdash \varphi$?

2013-04-12T10:14:14Z

$\def\zfc{\mathrm{ZFC}}\def\pr{\operatorname{Prov}\nolimits}$The statement

$\zfc\vdash\pr_\zfc(\ulcorner\varphi\urcorner)$ implies $\zfc\vdash\varphi$ for every sentence $\varphi$ in the language of $\zfc$

is equivalent to the statement that $\zfc$ is either inconsistent or $\Sigma^0_1$-sound: the latter means that every $\Sigma^0_1$-sentence provable in $\zfc$ is true in standard integers. One direction is obvious as $\pr_\zfc(\ulcorner\varphi\urcorner)$ is a $\Sigma^0_1$-sentence, and its truth in $\mathbb N$ says exactly that $\varphi$ is provable in $\zfc$. The converse follows from the Friedman–Goldfarb–Harrington principle: if $T$ is a recursively axiomatized theory containing Robinson’s arithmetic and $\sigma$ a $\Sigma^0_1$-sentence, there exists a sentence $\varphi$ (that can also be taken $\Sigma^0_1$) such that

$$I\Delta_0+\mathit{EXP}\vdash\pr_T(\ulcorner\varphi\urcorner)\leftrightarrow(\sigma\lor\pr_T(\ulcorner0=1\urcorner)).$$

$\Sigma^0_1$-soundness is stronger than consistency, but weaker than $\omega$-consistency. If you are wondering about foundational issues, it is best to consider it as a separate assumption on its own.

Answer by Emil Jeřábek for Definability in a language with a single binary predicate

2013-04-08T14:51:40Z

No, the structure is definitionally equivalent with $(\mathbb Z,0,S)$ (that is, you make the successor function a function rather than a predicate), which is well-known to have elimination of quantifiers: every formula is equivalent to a Boolean combination of formulas of the form $y=S^n(x)$, where $x,y$ are either variables or $0$, and $n$ is a natural number. For formulas with one free variable, this means that the only definable subsets are finite or cofinite.

In fact, the set of positive integers is not even definable in the structure $(\mathbb Z,0,1,+)$, which also has a form of elimination of quantifiers: every formula $\phi(x_1,\dots,x_k)$ is equivalent to a Boolean combination of linear equalities $n_1x_1+\dots+n_kx_k=n_0$ with $n_0,n_1,\dots,n_k\in\mathbb Z$, and formulas of the form $x_i\equiv n\pmod m$ with $n,m\in\mathbb Z$, $0\le n< m$. Its unary definable subsets are those that are periodic up to finitely many exceptions.

EDIT: In view of the comments, let me clarify how $(\mathbb Z,0,S)$ is definable in $(\mathbb Z,P)$:

$$\begin{align*} x=0&\iff\forall y\,\neg P(y,x),\\ x=1&\iff\forall y\,\neg P(x,y),\\ y=S(x)&\iff P(y,x)\lor(x=0\land y=1). \end{align*}$$

The converse is obvious: $$P(x,y)\iff x=S(y)\land x\ne0.$$

Answer by Emil Jeřábek for Asymptotics of the Number of Non-Isomorphic Equivalence Relations and the Number of Non-Isomorphic Relations

2013-04-10T16:01:06Z

You don’t need either of the two fancy formulas. Since every equivalence relation is the kernel of a function from the $n$-element set into itself, their number is at most $n^n$ (and taking them up to isomorphism can only make it smaller). On the other hand, there are $2^{n^2}$ binary relations in total, and each isomorphism class has at most $n!$ elements, hence there are at least $2^{n^2}/n!$ nonisomorphic relations. Thus, $$\frac{p(n)}{a(n)}\le\frac{n^nn!}{2^{n^2}}=2^{O(n\log n)-n^2}\to0.$$

Answer by Emil Jeřábek for What metatheory proves $\mathsf{ACA}_0$ conservative over PA?

2013-04-10T12:26:37Z

The conservativity of $\mathrm{ACA}_0$ over $\mathrm{PA}$ is provable in $I\Delta_0+\mathit{SUPEXP}$ by a cut elimination argument. It is not provable in $I\Delta_0+\mathit{EXP}$, since $\mathrm{ACA}_0$ has superexponential speedup over $\mathrm{PA}$ (due to Solovay).

Answer by Emil Jeřábek for dense orders are saturated

2013-04-08T13:51:29Z

This characterization for dense linear orders can be found as Proposition 16.1 in Sachs’ Saturated model theory. Note that he defines $\kappa$-density differently than you (this property is also known as orders of type $\eta_\alpha$ in the literature, by the way). I can’t find a discussion of saturated real-closed fields in the book, but the fact that a rcf is $\kappa$-saturated iff its underlying order is is included e.g. as Exercise 4.5.18 in Marker’s Model theory: an introduction.

Answer by Emil Jeřábek for Is the product of closed subgroups in a locally compact group locally compact?

2013-04-03T13:53:06Z

The is not true in general. For example, if $G=\mathbb R$, $A=\mathbb Z$, and $H=h\mathbb Z$ for some $h\in\mathbb R\smallsetminus\mathbb Q$, then $AH$ (that is, $\mathbb Z+h\mathbb Z$) is a countable dense subgroup of $\mathbb R$, and as such it is not locally compact.

Furthermore, as pointed out by Misha, the product $AH$ need not even be a subgroup: for instance, take $G$ to be the discrete free group on two generators $a,h$, and $A$ and $H$ the cyclic subgroups generated by $a$ and $h$, respectively. Instead of $A$ being abelian, you should require that $AH=HA$; a sufficient condition is that one of the subgroups is normal (or more generally, that one of the subgroups is included in the normalizer of the other).

If $AH=HA$ and both subgroups are compact, then $AH$ is a compact subgroup of $G$, being a continuous image of a compact space.

Answer by Emil Jeřábek for The existential theory of the reals

2013-03-08T12:40:59Z

In order for this to be a computational problem in the first place, you have to fix a representation of the coefficients by finite strings (which in particular implies that the field is countable). The answer will in general depend on the representation.

For the most obvious case, if the coefficients are taken from the field of real algebraic numbers, and are represented in a common way (minimal polynomial + an isolating interval or a BKR sign condition), then the problem is equivalent to the one with rational coefficients, because we can just plug the definitions of the coefficients into the formula.

Answer by Emil Jeřábek for ERA, PRA, PA, transfinite induction and equivalences

2013-03-06T12:34:00Z

This entirely depends on what exactly you mean by TI, as there are several options (I actually do not understand what the $\{\alpha\in\epsilon_0\}$ part of the notation is supposed to mean either, but I will assume it just means transfinite induction up to $\epsilon_0$):

$TI\{\alpha\in\epsilon_0\}$ is the schema $$\forall x\,(\forall y\prec x\,\phi(y)\to\phi(x))\to\forall x\,\phi(x),$$ where $\phi$ is an arbitrary formula, and $\prec$ the standard ordering of type $\epsilon_0$. It is easy to see that transfinite induction implies ordinary induction over a weak base theory (say, $I\Delta_0$), hence in this case, $I\Delta_0+TI\{\alpha\in\epsilon_0\}=\mathrm{PA}+TI\{\alpha\in\epsilon_0\}$ (and the same holds for any base theory in between).
$TI\{\alpha\in\epsilon_0\}$ is the same schema restricted to formulas of bounded complexity $\Gamma$. Typically used choices for $\Gamma$ include $\Pi^0_2$, $\Pi^0_1$, or open formulas in the language of PRA or EA (also called ERA or EFA). In all these cases, $\mathrm{PRA}+TI\{\alpha\in\epsilon_0\}$ is strictly weaker than $\mathrm{PA}+TI\{\alpha\in\epsilon_0\}$, since the former theory can be axiomatized by formulas of bounded complexity, and no consistent set of formulas of bounded complexity can imply full ordinary induction (which is equivalent to the full uniform reflection schema). In the case where $\Gamma$ are open EA-formulas, $\mathrm{EA}+TI\{\alpha\in\epsilon_0\}$ is likewise strictly weaker than $\mathrm{PRA}+TI\{\alpha\in\epsilon_0\}$. On the other hand, if $\Gamma\supseteq\Pi^0_1$, then $TI\{\alpha\in\epsilon_0\}$ implies $I\Sigma_1\supseteq\mathrm{PRA}$ over a weak base theory.
$TI\{\alpha\in\epsilon_0\}$ is the second-order induction axiom $$\forall X\,\forall x\,(\forall y\prec x\,y\in X\to x\in X)\to\forall x\,x\in X.$$ Then one needs to include some comprehension schema in the base theory to make any sense, and its strength determines the strength of the $TI\{\alpha\in\epsilon_0\}$. In particular, if we take at least $\Sigma^0_1$-comprehension, we are in the same situation as in 1. If we take recursive comprehension, it is the same as 2 with $\Gamma=\Delta^0_1$.

Answer by Emil Jeřábek for Defining definite integral using indefinite integral.

2013-03-05T19:53:33Z

To add to Gerald Edgar’s answer:

1) Kurzweil–Henstock integral satisfies $\int_a^bf(x)\,dx=F(b)-F(a)$ even under the weaker assumptions that $F$ is continuous and $F'(x)=f(x)$ for all but countably many $x\in[a,b]$, hence it fully subsumes the integral you want to define. It is, however, strictly more general: if $A\subseteq[a,b]$ is a null set and $f$ its characteristic function, then $\int_a^bf(x)=0$ (as a Kurzweil–Henstock or Lebesgue integral), so the only choice would be $F$ constant, but then $0=F'(x)=f(x)$ only holds outside $A$. Thus, in general, the set of exceptions may be an arbitrary null set. (It cannot be any worse: the Lebesgue differentiation theorem mentioned by Gerald Edgar holds for Kurzweil–Henstock integral as well.) In particular, your integral (unlike Kurzweil–Henstock integral) does not extend Lebesgue integral. It does not even extend Riemann integral, as we can take for $A$ a closed set.

3) If we allow $C$ to be an arbitrary null set, then the definition no longer makes sense: if we take for $F$ the Cantor function, then $F$ is continuous and $F'(x)=0$ almost everywhere, so we would be forced to put $0=\int_0^10\,dx=F(1)-F(0)=1$.

One can salvage the definition by making stronger requirements on the function $F$. That is, we can put $\int_a^bf(x)\,dx=F(b)-F(a)$ if $F'(x)=f(x)$ for all $x\in[a,b]$ except a null set, and $F$ is an admissible indefinite integral function. One can obtain a characterization of Lebesgue integral in this way by taking $F$ absolutely continuous. For Kurzweil–Henstock integral, one needs a broader class of functions, whose description is a bit more delicate, see e.g. http://link.springer.com/article/10.1007%2Fs10587-008-0081-0 .

Answer by Emil Jeřábek for Size-limited oracles

2013-02-28T15:27:39Z

Computational problems that can be efficiently (i.e., polynomial-time) computed from solutions of the problem on shorter instances are known as (downward) self-reducible. A classical example is SAT: given a CNF $\phi$ in variables $x_0,\dots,x_n$, let $\phi_0$ and $\phi_1$ be the CNFs in variables $x_0,\dots,x_{n-1}$ obtained by setting $x_n$ to 0 or 1 (respectively), and simplifying the formula accordingly. Then $\phi$ is satisfiable iff $\phi_0$ or $\phi_1$ is satisfiable. For a discussion of the self-reducibility phenomenon and pointers to the literature, see e.g. ftp://ftp.cs.rutgers.edu/cs/pub/allender/cie.plenary.pdf or http://www.thi.uni-hannover.de/fileadmin/forschung/arbeiten/selke-ma.pdf .

Answer by Emil Jeřábek for Is there any o-minimal expansion of the real field with functions of growth higher than exponential?

2013-02-07T11:21:06Z

This is a well-known open problem, see e.g. http://www1.maths.leeds.ac.uk/maloa/lecturenotes/lyon.pdf . All currently known o-minimal expansions of the reals (such as the pfaffian closure of $\mathbb R$) are exponentially bounded.

Answer by Emil Jeřábek for What logic is modelled by generalized boolean algebra?

2013-01-30T15:15:04Z

The question is not quite well posed. In algebraic logic, logics are not defined by algebras, but by logical matrices: these are pairs $\langle A,D\rangle$, where $D$ is a subset of $A$, termed the set of designated values. The logic of a class $K$ of matrices is then the consequence relation $\models_K$ such that for any formula $\phi$ and a set of formulas $\Gamma$, $\Gamma\models_K\phi$ holds iff for every $\langle A,D\rangle\in K$ and every homomorphism $v$ from the algebra of formulas to $A$: if $v(\Gamma)\subseteq D$, then $v(\phi)\in D$. In the most important situations, $D$ is equationally definable in $A$: $D=\{x\in A:A\models E(x)\}$ for a set of equations $E$, which reduces matrices back to pure algebraic language. However, there may be many different choices of $E$, hence it is not sufficient to specify just a class of algebras.

For example, the matrices for classical logic are $\langle A,\{1\}\rangle$, where $A$ is a Boolean algebra. Here, $\{1\}$ is definable by $E(x)=\{x\approx1\}$.

See R. Jansana’s SEP article Propositional consequence relations and algebraic logic for a comprehensive introduction to algebraic propositional logic.

Since you didn’t specify which sets of designated values to take in generalized Boolean algebras (and the most obvious choice doesn’t work as GBA do not need to have a top), the question does not necessarily admit a unique answer. Let me give some specific examples. For the following, I assume GBA formulated in the signature $\{\land,\lor,0,-\}$, where $x-y$ is the relative complement of $y$ in $[0,x]$:

Let $K$ be the class of matrices $\langle A,D\rangle$, where $A$ is a GBA, and $D$ is a nonempty filter in $A$. Then the logic of $K$ is the $\{\land,\lor,0,-\}$-fragment of classical logic.
Let $K$ be the class of matrices $\langle A,\{0\}\rangle$, where $A$ is a GBA. Then the logic of $K$ is a notational variant of the positive fragment (i.e., $\{\lor,\land,1,\to\}$) of classical logic, where the connectives have been renamed to their duals as indicated by the order in which I have written them.
Let $K$ be the class of matrices $\langle A,\varnothing\rangle$, where $A$ is a GBA. Then the logic of $K$ is the maximal logic with no theorems, i.e., $\Gamma\models_K\phi$ iff $\Gamma\ne\varnothing$.
Let $K$ be the class of matrices $\langle A,A\rangle$, where $A$ is a GBA. Then the logic of $K$ is the inconsistent logic, i.e., $\Gamma\models_K\phi$ for every $\Gamma,\phi$.

Choice #2 is better behaved than the other three as the matrices in question are (equationally definable and) reduced, and in particular, the logic obtained is (finitely, strongly, and regularly) algebraizable, with GBA being its equivalent semantics. (See Jansana’s article for the basic definitions.) While in principle the condition of algebraizability still does not lead to a unique logic from a given class of algebras, it means that the upside-down positive fragment of classical logic corresponds to GBA in as good a sense as the full classical logic corresponds to BA.

[EDIT 2: Let me qualify the previous sentence. It’s true that in general, more than one logic can be algebraizable wrt the same variety of algebras. However, in the case of GBA, there are not that many possible choices for $E(x)$, and it is in fact easy to check that positive classical logic is the unique logic algebraized by GBA (and the translations given below are also unique up to equivalence). Thus, the question does have a well-defined unique answer after all.]

EDIT: I will spell out explicitly what algebraizability of the positive fragment means, and how it provides a logic modelled by GBA. Consider the propositional logic $\vdash$ defined by the following Hilbert calculus: $$\begin{gather} (\phi-\psi)-\phi\\ ((\chi-\phi)-(\psi-\phi))-((\chi-\psi)-\phi)\\ \phi-(\phi-(\psi-\phi))\\ 0\\ \phi-(\phi\lor\psi)\\ \psi-(\phi\lor\psi)\\ ((\phi\lor\psi)-\phi)-\psi\\ (\phi\land\psi)-\phi\\ (\phi\land\psi)-\psi\\ ((\chi-(\phi\land\psi))-(\chi-\psi))-(\chi-\phi)\\ \phi,\psi-\phi\vdash\psi \end{gather}$$ Let $\let\sd\vartriangle\phi\sd\psi:=(\phi-\psi)\lor(\psi-\phi)$, and let $\models$ denote validity in GBA. Then we have:

$\phi_1\approx\psi_1,\dots,\phi_n\approx\psi_n\models\phi\approx\psi$ iff $\phi_1\sd\psi_1,\dots,\phi_n\sd\psi_n\vdash\phi\sd\psi$
$\phi_1,\dots,\phi_n\vdash\psi$ iff $\phi_1\approx0,\dots,\phi_n\approx0\models\psi\approx0$
$\phi\approx\psi\models(\phi\sd\psi)\approx0$, $(\phi\sd\psi)\approx0\models\phi\approx\psi$
$\phi\vdash\phi\sd0$, $\phi\sd0\vdash\phi$

Thus, the mappings $\phi\approx\psi\mapsto\phi\sd\psi$ and $\phi\mapsto\phi\approx0$ provide a bi-interpretation of the quasiequational theory of GBA with the logic given by $\vdash$. (This is what distinguishes this case from other choices of matrices based on GBA, such as #1,3,4 above. These choices give logics modeled in GBA’s, but they do not have matching translations of algebra into logic, hence passing from GBA to such logics is losing structure and information.)

Answer by Emil Jeřábek for Can FPA really prove its consistency?

2013-01-29T14:18:00Z

In principle, the answer can depend on the proof system, but as long as you stick to some of the usual Hilbert-style or sequent proof systems, this shouldn’t matter.

First, as explained in http://mathoverflow.net/questions/120106, the question is equivalent to provability of the consistency of FPA in $I\Delta_0+\Omega_1$. (The fact that you are using second order objects to encode proofs and formulas corresponds to using all numbers instead of just the logarithmically small ones in $I\Delta_0+\Omega_1$, hence you end up with the usual consistency statement.)

Now, working in $I\Delta_0+\Omega_1$ (or equivalently, Buss’s $S_2$), the consistency of FPA is equivalent to the consistency of the second-order theory of the model with one-element first-order universe (in whatever finite language, it’s all equivalent), since the two theories are interpretable in each other. This in turn can be reduced to the quantified propositional calculus: since there is only one first-order element (and only one $n$-tuple of elements for every $n$), you can ignore first-order quantifiers and variables, and replace second-order variables with propositional variables both in second-order quantifiers and in atomic formulas. (Purely first-order atomic formulas such as $t=s$ can be replaced with the constant $\top$ for truth.) Thus, the question becomes whether $I\Delta_0+\Omega_1$ proves the consistency of the quantified propositional calculus ($G$).

The answer is that this is one of the major open problems in the area, but it is conjectured to be false. There is a kind of correspondence of subsystems of bounded arithmetic to propositional proof systems; in particular, the fragments $T^i_2$ of $S_2$ (${}=I\Delta_0+\Omega_1$) correspond to the fragments $G_i$ of the quantified propositional calculus, obtained by restricting all formulas in the proof (or alternatively, all cut formulas in the sequent calculus formulation) to $\Sigma^q_i$ or $\Pi^q_i$ formulas (= formulas in prenex form with at most $i$ quantifier blocks). This means:

$T^i_2$ proves the consistency (and even some form of reflection principle) of $G_i$.
Conversely, $\mathrm{Con}_{G_i}$ implies over a weak base theory all $\forall\Delta^b_1$-consequences of $T^i_2$ (and more complex consequences of $T^i_2$ can be xiomatized by an appropriate reflection principle). A related fact is that if $T^i_2$ proves a $\forall\Sigma^b_i$ statement, one can translate it into a sequence of quantified propositional tautologies which will have polynomially bounded proofs in $T^i_2$.
If $P$ is any propositional proof system whose consistency is provable in $T^i_2$, then $G_i$ polynomially simulates $P$.

$S_2$ is the union of its finitely axiomatizable fragments $T^i_2$. This means that $S_2$ proves the consistency of each fragment $G_i$, but on the other hand, if it proved the consistency of the full quantified propositional calculus $G$, it would imply that $G_i$ polynomially simulates $G$ for some $i$, and this is assumed to be false. To put it differently, the $\forall\Delta^b_1$-consequences of $S_2$ (as well as $S_2$ itself) are not assumed to be finitely axiomatizable.

The correspondence of theories and propositional proof systems also extends to complexity classes. Sets definable by $\Sigma^b_i$ formulas in the standard model of arithmetic are exactly those computable in the $i$-level $\Sigma^P_i$ of the polynomial hierarchy. The theories $T^i_2$ have induction for $\Sigma^b_i$ formulas, and their provably total $\Sigma^b_{i+1}$-definable functions are $\mathrm{FP}^{\Sigma^P_i}$, so these theories correspond to levels of the polynomial hierarchy. On the propositional side, satisfiability of $\Sigma^q_i$ formulas is a $\Sigma^P_i$-complete problem. Taking the union, $S_2$ corresponds to the full polynomial hierarchy $\mathrm{PH}$. However, the complexity class corresponding to $G$ is $\mathrm{PSPACE}$, as satisfiability of unrestricted quantified propositional formulas is $\mathrm{PSPACE}$-complete. Thus, asking $S_2$ to prove the consistency of $G$ is in the same spirit as collapsing $\mathrm{PSPACE}$ to $\mathrm{PH}$ (and therefore to some its fixed level). (Don’t quote me on this. While the collapse of the $T^i_2$ hierarchy does imply the collapse of $\mathrm{PH}$, for propositional proof systems this becomes only a loose analogy.)

In order to give also an upper bound on the consistency strength, the consistency of $G$, and therefore of FPA, is provable in theories corresponding to $\mathrm{PSPACE}$. The best known such theory is Buss’s theory $U^1_2$, which is a “second-order” extension of $S_2$ with comprehension for bounded sets defined by bounded formulas without second-order quantifiers, and length induction for bounded $\Sigma^1_1$-formulas. Notice that things get really messy here, as the first-order objects of $U^1_2$ correspond to second-order objects of FPA, and second-order objects of $U^1_2$ have no analogue in FPA. Alan Skelley formulated an equivalent (technically, RSUV-isomorphic) theory $W^1_1$. This is syntactically a third-order arithmetic, and it is more directly comparable to FPA (as numbers of one theory correspond to numbers of the other, and sets correspond to sets). $W^1_1$ proves the consistency of $G$, and thus of FPA.

Answer by Emil Jeřábek for Provability in Second-Order Arithmetic without the Successor Axiom

2013-01-28T13:20:19Z

As I already mentioned in another thread for a slightly different theory, it is possible to give a complete description of models of FPA (I mean all models, giving a complete semantics for the many-sorted first-order theory, not just proper second-order models, which abo lists in the question and which I will henceforth call “standard”) in terms of more familiar theories:

Models where successor is total are exactly the models of $Z_2$.
Models where successor is not total. If $M\models I\Delta_0+\Omega_1$ and $0< a\in M$ is such that $M\models{}$ “$2^a$ exists”, we can form the following model $A_{M,a}$: its “first-order” sort consists of the submodel $[0,a)_M$ of $M$ (where successor, addition, and multiplication are considered as relations, not functions), and for every $n$, its “second-order” universe of $n$ary relations consists of $[0,2^{a^n})_M$, where $r< 2^{a^n}$ represents the relation $$\{\langle u_0,\dots,u_{n-1}\rangle\in[0,a)^n:M\models\mathrm{bit}(r,a^{n-1}u_{n-1}+\dots+au_1+u_0)=1\},$$ where $\mathrm{bit}(x,u)$ is the $u$th bit in the binary representation of $x$. (Note that the existence of $2^a$ implies the existence of $2^{a^n}$ by $\Omega_1$.) Then $A_{M,a}\models\mathrm{FPA}$: the main thing is that the validity of any (second-order) formula in $A_{M,a}$ translates to a formula in $M$ whose all quantifiers are bounded by some $2^{a^n}$, and $I\Delta_0+\Omega_1$ proves bit-comprehension for $\Delta_0$-definable subsets of logarithmically small intervals, which implies full comprehension in $A_{M,a}$.
Conversely, every model $A\models\mathrm{FPA}$ where successor is not total is isomorphic to $A_{M,a}$ for some $M,a$ as above. I will sketch the argument below. FPA proves that $A$ has a largest element, and satisfies full first-order induction; this first-order theory is called $\mathrm{PA^{top}}$, and it is well-known that every its model $A$ can be extended into a model $B$ of $I\Delta_0$ so that $A$ is its submodel of the form $[0,a)$, and the standard powers $\{a^n:n\in\omega\}$ are cofinal in $B$ (unless $a=1$). The construction works as follows: for every $n$, elements of the interval $[0,a^n)$ in $B$ can be represented by $n$tuples of elements of $A$; one can define in $\mathrm{PA^{top}}$ the arithmetic operations on such $n$tuples in such a way that these $[0,a^n)$ form an increasing chain of models whose union is taken as $B$. In our case, we also have the second-order universes of $n$-ary relations, and these can be used to represent exponentially larger numbers: an $n$-ary relation from $A$ (i.e., a subset of $[0,a^n)$) will represent a number below $2^{a^n}$ in binary. In this way, we can extend $B$ into a model $M$ such that $B=\{x\in M:M\models2^x\text{ exists}\}$. Since any bounded formula in $M$ translates into a second-order formula in $A$, $M$ will satisfy $\Delta_0$ induction up to logarithmically small numbers (this is called length induction), which implies $I\Delta_0$. $M\models\Omega_1$ follow from the fact that $\{2^{a^n}:n\in\omega\}$ is cofinal in $M$. By the construction, $A\simeq A_{M,a}$.
(The second part of the argument, viz. a correspondence of “second-order” models of arithmetic with bounded sets to “first-order” models with exponentially larger numbers is known as the RSUV isomorphism.)

This gives a characterization of provability in FPA: for any (second-order) sentence $\phi$, the construction above implicitly gives a first-order formula $\phi^*$ such that

$\mathrm{FPA}\vdash\phi$ iff $Z_2\vdash\phi$ and $I\Delta_0+\Omega_1\vdash\phi^*$.

Note that $\phi^*$ is a $\Pi^0_1$-sentence; conversely, every $\Pi^0_1$-sentence is equivalent to one of this form. Note that the standard models of FPA with non-total successor are $A_{\mathbb N,n}$ for some $n\in\mathbb N$, hence the question reduces to: find sentence $\phi$ such that $Z_2\vdash\phi$, $\mathbb N\models\phi^*$, but $I\Delta_0+\Omega_1\nvdash\phi^*$.

An example of such a statement is $\mathrm{Con}_Q$ (the formal consistency of Robinson arithmetic), formulated as a $\Pi^0_1$-formula of the form $\forall x\,\theta(x)$, where $\theta(x)$ is a formula whose all quantifiers are bounded to $x$, and atomic formulas are reformulated in such a way that they do not refer to any numbers above $x$. The translation $\phi^*$ is then essentially equivalent to $\forall x\,\theta(|x|)$, where $|x|$ is the length function, that is, the statement that $Q$ has no logarithmically short proofs of contradiction. This is not provable in $I\Delta_0+\Omega_1$. Thus, $\mathrm{Con}_Q$ is not provable in FPA, but it holds in all its standard models, and it is provable in $Z_2$.

Independent $\Pi^0_1$ statements (for weak or strong arithmetic) in the literature are mostly variants of consistency statements. While this is not a precise question, it is a sort of an open problem to find natural combinatorial $\Pi^0_1$ statements independent of particular fragments of arithmetic. Let me mention two principles which are conjectured to be unprovable in $I\Delta_0+\Omega_1$, and therefore would give the wanted example for FPA:

$\Delta_0$-$\mathrm{PHP}$: the pigeonhole principle. In the language of FPA, it is the following schema: for every formula $\phi(u,X,Y)$ (possibly with other parameters not shown), $$\begin{align}\forall u\,\neg[&\forall X\subseteq[0,u]\,\exists Y\subsetneq[0,u]\,\phi(u,X,Y)\\&{}\land\forall X_0,X_1,Y\subseteq[0,u]\,\neg(\phi(u,X_0,Y)\land\phi(u,X_1,Y))].\end{align}$$ (I.e., $\phi$ does not define an injective (multi-)function from $\mathcal P([0,u])$ into itself minus one set.)
$\mathrm{Count}_2(\Delta_0)$: the counting principle modulo $2$. In the language of FPA, it is the schema $$\begin{align}\forall u\,\neg[&\forall X\subsetneq[0,u]\,\exists!Y\subsetneq[0,u]\,\phi(u,X,Y)\\&{}\land\forall X,Y\subsetneq[0,u]\,(\phi(u,X,Y)\to X\ne Y\land\phi(u,Y,X))]\end{align}$$ for every formula $\phi(u,X,Y)$. (I.e., $\phi$ does not define a fixpoint-free involution on $\mathcal P([0,u])$ minus one set. In general, the mod $k$ counting principle would state that some canonical class of finite cardinality not divisible by $k$ cannot be partitioned into $k$-element subclasses, but it’s easier to state it just for $k=2$.)

Answer by Emil Jeřábek for Even XOR Odd Infinities?

2013-01-23T14:17:19Z

The answer is no. It is enough to find a model of MA which is an integral domain of characteristic $0$ (whence O1 is true and E1 false) such that $2$ is not invertible (whence E2 is true and O2 false).

One example of such a model is the ring of $2$-adic integers $\mathbb Z_2$. This is clearly a domain, and $2$ is not a unit, hence it suffices to show

Theorem: For any prime $p$, the ring $\mathbb Z_p$ is a model of MA.

Proof: The only problem is to verify that induction holds. Assume $\mathbb Z_p\models\phi(0)\land\forall x\,(\phi(x)\to\phi(x+1))$, where $\phi$ is an arithmetic formula with parameters from $\mathbb Z_p$, and put $\phi(\mathbb Z_p):=\{a\in\mathbb Z_p:\mathbb Z_p\models\phi(a)\}$.

Since $\phi(\mathbb Z_p)$ is definable in $\mathbb Z_p$, it is also definable in the field $\mathbb Q_p$ endowed with a unary predicate for $\mathbb Z_p$. Macintyre [1] proved that such structures admit a form of quantifier elimination, and as a corollary (Thm. 2 on p. 609), every infinite definable set has a nonempty interior. Thus, there is $a_0\in\phi(\mathbb Z_p)$ and $k\ge0$ such that $a_0+p^k\mathbb Z_p\subseteq\phi(\mathbb Z_p)$. Let $a\in\mathbb Z_p$ be arbitrary, and let $b< p^k$ be a natural number such that $b\equiv a-a_0\pmod{p^k}$. Since $\phi(\mathbb Z_p)$ is closed under successor, we have $a\in b+a_0+p^k\mathbb Z_p\subseteq\phi(\mathbb Z_p)$. Thus, $\phi(\mathbb Z_p)=\mathbb Z_p$, i.e., $\mathbb Z_p\models\forall x\,\phi(x)$. QED

I suspect the following may work as additional countermodels (they are domains where $2$ is not a unit, the issue is whether they satisfy induction):

The ring of algebraic integers $\tilde{\mathbb Z}$. A form of quantifier elimination for $\tilde{\mathbb Z}$ was proved by van den Dries [2] and Prestel and Schmid [3], but the basic formulas are somewhat messy, so it is not immediately clear to me whether this implies induction.
The localization of $\tilde{\mathbb Z}$ at a maximal ideal containing $2$. Elimination of quantifiers for this (and similar) rings is reported as Fact 3 in [2], where it is attributed to [4]. It seems it could imply induction by a similar argument as for $\mathbb Z_p$.

[1] Angus Macintyre, On definable subsets of $p$-adic fields, Journal of Symbolic Logic 41 (1976), no. 3, pp. 605–610.

[2] Lou van den Dries, Elimination theory for the ring of algebraic integers, Journal für die reine und angewandte Mathematik 388 (1988), pp. 189–205.

[3] A. Prestel and J. Schmid, Existentially closed domains with radical relations, Journal für die reine und angewandte Mathematik 407 (1990), pp. 178–201.

[4] Angus Macintyre, Kenneth McKenna, Lou van den Dries, Elimination of quantifiers in algebraic structures, Advances in Mathematics 47 (1983), no. 1, pp. 74–87.

Answer by Emil Jeřábek for Is metatheory, providing proof of the incompleteness theorem, consistent?

2013-01-17T11:23:50Z

As already pointed out by Steven Landsburg, there are plenty of such theories if you stick to conventional mathematics. If you are some sort of an ultrafinitist, the incompleteness theorem is provable in weak fragments of bounded arithmetic, such as $PV$ or $S^1_2$. These theories are interpretable in Robinson’s arithmetic $Q$, so as long as you accept that $Q$ is consistent, there is such a theory. Do you believe that for every natural numbers $n,m$, the number $\underbrace{2^{2^{\cdot^{\cdot^{\cdot^{2^m}}}}}}_n$ exists? Then $Q$ is consistent.

Answer by Emil Jeřábek for What can we infer about the size of a complete Boolen algebra, given it is $\kappa$-c.c.?

2013-01-07T15:51:07Z

The $\kappa$-cc condition by itself does not put any bound on the cardinality of the algebra. For example, for each $\lambda$, the Cohen algebra of regular open subsets of $2^\lambda$ is ccc, but it has cardinality $\lambda^\omega$. However, one can bound the size of $B$ using additional cardinal characteristics: for a simple bound, if $B$ is $\kappa$-cc and has a dense subset $P$ of cardinality $\lambda$, then $|B|\le\lambda^{<\kappa}$, as every element of $B$ can be written as the join of an antichain in $P$.

Answer by Emil Jeřábek for Collection from Replacement in ZFC-extensionality

2012-12-20T12:19:25Z

Collection is not provable in ZFC minus extensionality, a simple countermodel is described in http://mathoverflow.net/questions/54328 . (That the model cannot provably satisfy collection follows from Gödel’s theorem. For a specific instance of collection which fails, let $\bar\omega$ denote one of the many representations of $\omega$ in the model, and $\bar0\in\bar\omega$ the corresponding empty set: then the model satisfies “for every $n\in\bar\omega\smallsetminus\{\bar0\}$, there exists a function $f$ with domain $n$ such that $f(\bar0)=\bar\omega$, and $f(x)\in f(y)$ whenever $x\in y\in n$”, but there is no set collecting such functions for every $n\in\bar\omega\smallsetminus\{\bar0\}$.)

Answer by Emil Jeřábek for Existential instantiation in Hilbert-style deduction systems

2012-12-18T12:51:27Z

First, the standard definition of semantic entailment is neither the “simple” one nor the “complicated” one, but the following: $T\models U$ iff for every $M$, if $M,A\models T$ for every $A$, then $M,A\models U$ for every $A$.

First-order Hilbert-style usually employ some form of a generalization rule: the simplest one is $$\phi\vdash\forall x\,\phi,$$ other common variants include $$\begin{align} \psi\to\phi\vdash\psi\to\forall x\,\phi,\\ \phi\to\psi\vdash\exists x\,\phi\to\psi, \end{align}$$ where $x$ must not occur free in $\psi$. (The choice of the rules depends on other axioms of the system, and of course on the logic, if you are dealing with non-classical systems.) Notice that these rules are not sound with respect to either your “simple” or “complicated” definition, but they are sound with respect to the semantics I gave above. (Note also that the system on the Wikipedia page, with no generalization rules, is quite unconventional.)

The way to simulate existential instantiation in Hilbert systems is by means of a “meta-rule”, much like you’d use the deduction theorem to simulate the implication introduction rule. The most common formulation is:

Lemma 1: If $T\vdash\phi(c)$, where $c$ is a constant not appearing in $T$ or $\phi$, then $T\vdash\forall x\,\phi(x)$.

A version with explicit existential quantifiers may look like this:

Lemma 1’: If $T\vdash\psi(c)\to\phi$, where $c$ is a constant not appearing in $T$, $\phi$, or $\psi$, then $T\vdash\exists x\,\psi(x)\to\phi$.

Both lemmas follow easily by replacing the constant everywhere with a fresh variable, and applying an appropriate version of the generalization rule. In order to simulate the natural deduction existential elimination rule, you are in a situation where you have already derived (or assume) $\exists x\,\psi(x)$. You add $\psi(c)$ as an extra assumption, where $c$ is a fresh constant, and derive the desired result $\phi$. By deduction theorem (you have to make sure to satisfy its hypotheses, such as by not using generalization rules in the proof snippet, or by assuming $\psi(c)$ is a sentence), this implies the provability of $\psi(c)\to\phi$, and therefore of $\exists x\,\psi(x)\to\phi$ by Lemma 1’.

In particular, the construction of a Henkin completion of a theory basically needs that if $T+\exists x\,\psi(x)$ is consistent, where $\psi(x)$ has no other free variable, then $T+\psi(c)$ is consistent, where $c$ is a fresh constant. This follows from Lemma 1’ and the deduction theorem in the way I indicated.

Answer by Emil Jeřábek for SAT and Arithmetic Geometry

2012-12-06T16:16:23Z

As for the first question, solvability of a system of polynomial equations is NP-complete over every finite field, and NP-hard for every integral domain. The reduction was already mentioned in David Speyers’s answer: add $x_i^2-x_i$ to your system for every variable $x_i$.

The exact complexity of solvability over infinite domains is not so easy to answer. To begin with, it may significantly depend on the representation of the polynomial and its coefficients.

Solvability over $\mathbb Z$ is undecidable ($\Sigma^0_1$-complete). This is the MRDP theorem. The decidability of solvability over $\mathbb Q$ is an open problem.
Solvability of polynomials with rational coefficients over $\mathbb R$ or $\mathbb C$ is in PSPACE, and it is not known whether one can do better. Assuming the generalized Riemann hypothesis, solvability of rational polynomials over $\mathbb C$ is in AM, and therefore in the second level of the polynomial hierarchy. Note that AM = NP under some plausible assumptions from circuit complexity.
Solvability over the algebraic closure of a finite field is also decidable, though I do not know offhand what are the complexity bounds (but it should be again something in the vicinity of EXP or PSPACE). The keyword is “effective Nullstellensatz”.

Answer by Emil Jeřábek for Non-uniform complexity of the halting problem

2012-12-03T12:58:32Z

Every r.e. language is polynomial-time reducible to the halting problem. Since there are computable languages (indeed, in $\Delta^E_3$) having the maximum possible circuit complexity for every length $n$ (which is asymptotically $2^n/n$), the halting problem also has exponential circuit complexity. The exact complexity will depend on the particular representation of algorithms in the definition of the halting problem, and specifically, on the complexity of the reduction function which hardwires an input string into a fixed algorithm. In the most obvious representations, this function blows up the input length only linearly and can be made computable by linear-size circuits, hence we get $2^{\Theta(n)}$ as the circuit complexity of the halting problem. If the halting problem is formulated directly for algorithms accepting an input, the reduction function increases the input length by an additive constant and has essentially constant complexity, so the circuit complexity of the halting problem is $\Theta(2^n/n)$ in such a formulation.

Answer by Emil Jeřábek for If NP=EXPTIME, does every DTM have a succinct "execution proof"?

2012-11-29T15:54:32Z

Q1: Yes (except that the certificates you get may have size polylogarithmic in $n$, not just logarithmic, and you need to apply the argument to both HALTS-IN-N and its complement, as pointed out by Andreas).

Q2: Well, NP = EXP contradicts all kinds of conjectures from complexity theory: it makes the polynomial hierarchy collapse to NP = coNP, it makes NP = PSPACE, and PSPACE = EXP, all of which are assumed to be false. On the other hand, it also implies P ≠ NP. We cannot rule out NP = EXP with the present state of knowledge (nor the even stronger collapse ZPP = EXP), but the time hierarchy theorem implies that $\mathrm P\ne\mathrm{EXP}$ and $\mathrm{NP}\ne\mathrm{NEXP}\cap\mathrm{coNEXP}$. Existence of succinct certificates also shows up in other similar situations: for example, if EXP has polynomial-size Boolean circuits, then membership in any EXP language has succinct certificates verifiable in randomized polynomial time (that is, EXP = MA).

Vis-à-vis the last but one paragraph of your question, note that an exhaustive deterministic search for a short certificate takes time exponential in the size of the certificate, so you don’t save here anything in terms of deterministic running time.

I don’t follow the last paragraph. EXP = NP implies $\mathrm{DTIME}(2^{t(n)})\subseteq\mathrm{NTIME}\bigl(t(n)^{O(1)}\bigr)$ for every time-constructible function $t(n)$ of at least polynomial growth, if that’s what you mean, but this does not lead to a contradiction.

EDIT: It may be worth mentioning that there is nothing particularly revolting about the idea that the existence of an exponentially long computation can be proved using a polynomial amount of data. In fact, Babai, Fortnow, and Lund have shown that NEXP = MIP, which means that two (computationally unlimited) agents presenting polynomial-size evidence who cannot communicate with each other can reliably convince a randomized polynomial-time verifier that such an exponentially long halting computation (even nondeterministic) exists. (Here, polynomial and exponential is measured in terms of the length of the input, which is logarithmic in the $n$ from the original question.)

EDIT 2: Yes, the running times for primitive recursive functions (or predicates) are enormous. More precisely, a function is primitive recursive if and only if it is computable in time $A(k,n)$ for some constant $k$, where $A$ is the Ackermann function. Plugging an extra exponential or logarithm in this characterization makes no difference. In view of the latter fact, whether NP = EXP or not has not much to do with the argument: we know unconditionally that the version of HALTS-IN-N where $n$ is given in unary is in P.

Comment by Emil Jeřábek

2013-05-22T11:45:23Z

Except that you should really do as you say and use a hyphen (fixed-point, U+002D, TeX: -), not a minus sign (fixed−point, U+2212, TeX: dollar-dollar).

Comment by Emil Jeřábek

2013-05-17T15:45:57Z

The definition of a measurable function is that preimages of Borel sets are measurable. Preimages of general measurable sets needn’t be. Of course, intervals are Borel.

Comment by Emil Jeřábek

2013-05-17T14:25:16Z

Yes, if it is undecidable in a half-decent theory, then it is true. Yes, you cannot prove in, say, ZFC that it is undecidable in ZFC, but then again, you cannot prove in ZFC that anything is undecidable in ZFC. However, it is conceivable that the undecidability of the conjecture in ZFC is provable by assuming some stronger hypothesis, such as the consistency of ZFC.

Comment by Emil Jeřábek

2013-05-17T13:59:42Z

Whatever. The point is that you question was deleted because it is not appropriate for this site, and reposting it again won’t change that.

Comment by Emil Jeřábek

2013-05-17T13:42:25Z

I experience a déja vu. Wsp, in case you didn’t manage to read the comment below your previous question (mathoverflow.net/questions/130650) before it got deleted: the popular knowledge is that $\Gamma(z)$ is not analytic, as it has simple poles at all nonpositive integers.

Comment by Emil Jeřábek

2013-05-17T10:36:52Z

Thanks, it was fun.

Comment by Emil Jeřábek

2013-05-16T16:06:07Z

@Tom: My comment concerned the first version of the question, where it was impossible to guess that the OP is actually talking about ideals. It looked like a plain identity between two numbers (which were actually distinct).

Comment by Emil Jeřábek

2013-05-16T15:07:38Z

False statements tend to be hard to prove.

Comment by Emil Jeřábek

2013-05-15T20:28:18Z

Obviously not, unless $p=q$. If you meant the two $1$s to be different constants, apply a Möbius transformation.

Comment by Emil Jeřábek

2013-05-15T19:34:26Z

Duplicate of mathoverflow.net/questions/130750

Comment by Emil Jeřábek

2013-05-14T11:07:40Z

$\gcd(15-2,17-4)$

Comment by Emil Jeřábek

2013-05-07T14:59:04Z

I’m sorry for the number of edits. I’m going to stop here.

Comment by Emil Jeřábek

2013-05-07T10:10:14Z

Kalmár elementary will certainly do, and so will polynomial time, or even uniform $\mathit{AC}^0$ (by a different argument). (Not that it would matter, but the formula for addition actually gives $1+0=2\cdot1\dot-((2\cdot1\dot-1)\dot-0)=2\dot-((2\dot-1)\dot-0)=2\dot-1=1$. The point of the expression is that $x+y=z-((z-x)-y)$, and if we take $z\ge x+y$, then one can replace $-$ with limited subtraction. Now, $S(x)S(y)=xy+x+y+1\ge x+y$.)

Comment by Emil Jeřábek

2013-05-07T10:01:31Z

You don’t need Pell’s equation. You can prove that for every $b\le a-2$ there exist $y\ge x\ge0$ such that $p(a,x,y)=0$ satisfying the two congruences in Lemma 2 by a straightforward induction on $b$ (keeping $a$ fixed). The induction step follows from an inverse version of Lemma 1, whose conclusion reads $2ay\ge x+y$ and $p(a,y,2ay-x)=0$.

Comment by Emil Jeřábek

2013-05-06T19:27:19Z

The DOR is the model $M$ of Peano arithmetic from the answer. Peano arithmetic proves (hence every its model satisfies) that for any $a$ and $b=a-2$, there are $y\ge x\ge a-1$, $x\equiv-1\pmod{a-1}$, $y\equiv0\pmod{a-1}$ such that $p(a,x,y)=0$. Moreover, it proves the Lagrange four-square theorem, hence $(x-1)/(a-1)-1$ and $(y-x-1)/(a-1)$ can be written as sums of four squares. These are the $u$'s and $v$'s.