Question: Is there a decidable theory sufficient to formulate and prove (many) theorems of classical analysis?

What I have in mind is a theory with two kinds of objects, reals (which are introduced as a Dedekind complete ordered field) and subsets of ${\mathbb R}^n$. For each ${\mathbb R}^n$ there are axioms of Extensionality and Specification but not Adjunction (https://en.wikipedia.org/wiki/General_set_theory).

If I am not mistaken, this is not sufficient to introduce arithmetic, neither algebraically (writing down a predicate for $x\in{\mathbb Z}$) nor logically. So, the theory must be fairly weak. On the other hand, this must be enough to build up quite a bit of analysis, although I am not sure how much exactly. Chain rule, mean value theorem, intermediate value theorem - no doubt. Taylor's theorem - yes, but for each degree separately (we do not have induction.) Riemann integral - probably, but I am not certain.

Did I get it right?

[EDIT] To avoid misunderstanding, there are in fact two different questions, is there any decidable theory on the basis of which some analysis can be built, and if such a theory can be constructed along the lines suggested above.

[EDIT] About the second question: no, this approach does not work. (See the answer by Emil Jeřábek.)

  • 1
    $\begingroup$ With these axioms alone, you cannot prove the existence of any set at all. (And if you add the axiom that a set exists, you cannot prove the existence of any nonempty set.) So, clearly you need more than that. $\endgroup$ – Emil Jeřábek 3.0 Jun 5 '18 at 8:20
  • $\begingroup$ Not a problem, just declare the whole ${\mathbb R}^n$ a set. (For each $n$ . By the way, I did not mean to list all the axioms, so it is not a precise description of a theory anyway.) $\endgroup$ – Alex Gavrilov Jun 5 '18 at 8:44
  • $\begingroup$ Following Friedman, Simpson, and others working in reverse mathematics, there are now many ways of developing weak systems where fragments of analysis and other fields can be handled. It may be helpful to reorient your question in this context, and also update the relevant tags. $\endgroup$ – Mikhail Katz Jun 5 '18 at 10:21
  • 1
    $\begingroup$ The thing is, the formula $N(x)$ given as $\forall X\,(0\in X\land\forall y\,(y\in X\to y+1\in X)\to x\in X)$ defines natural numbers. It is not hard to show this way that any consistent theory in your language that includes the theory of ordered rings and comprehension for quantifier-free formulas is undecidable. I have no idea how to avoid this. $\endgroup$ – Emil Jeřábek 3.0 Jun 5 '18 at 10:31
  • 4
    $\begingroup$ @MikhailKatz All theories used in reverse mathematics include fairly strong fragments of arithmetic, and are undecidable as well. $\endgroup$ – Emil Jeřábek 3.0 Jun 5 '18 at 10:35

I say this is impossible: any expansion of the theory of reals by anything vaguely resembling sets is doomed to undecidability.

Theorem: Let $T$ be a two-sorted theory with one sort for reals, and the second sort for sets of reals, which includes the theory of ordered rings (on the first sort). Assume that for each standard $n\in\mathbb N$, it is consistent with $T$ that the set $\{0,1,\dots,n\}$ exists.

Then it is undecidable if $T$ proves a given formula $\phi(X)$, where $X$ is a set variable, but $\phi$ contains no set quantifiers.

(The assumptions could still be weakened. For example, it would be enough if $T$ does not disprove the existence of a set whose intersection with the interval $[0,n]$ is $\{0,1,\dots,n\}$.)

This can be shown by mimicking the usual proof that consistency of $\Sigma_1$ sentences with theories containing Robinson’s $R$ (not to be confused with Robinson’s arithmetic $Q$) is undecidable, using a definition of $\mathbb N$ in $\mathbb R$ by a formula with an existential set quantifier.

Specifically, let us fix a recursively inseparable pair of disjoint r.e. sets $A_0,A_1\subseteq\mathbb N$. By the MRDP theorem, we can write $$x\in A_i\iff\mathbb N\models\exists\vec y\,p_i(x,\vec y)=0$$ for some integer polynomials $p_0,p_1$. Define $$\begin{align} N(X)&\iff\begin{aligned}[t]&0\in X\land1\in X\land\forall x\in X\,(x=0\lor1\le x)\\ &\land\forall x,y\in X\,\bigl(y\le x\to x-y\in X\bigr),\end{aligned}\\ W_i(X,x,w)&\iff\exists\vec y\in X\,\bigl(x\le w\land\vec y\le w\land p_i(x,\vec y)=0\bigr),\\ \phi(X,x)&\iff N(X)\land\exists w\in X\,\bigl(W_0(X,x,w)\land\neg W_1(X,x,w)\bigr). \end{align}$$ (The intention is that $N(X)$ means “$X$ is an initial segment of $\mathbb N$”, $W_i(X,x,w)$ means “in $X$, there are witnesses for $x\in A_i$ below $w$”, and $\phi(X,x)$ means “in the initial segment $X$, there are witnesses for $x\in A_0$ smaller than any witnesses for $x\in A_1$”.)

The result now follows from the next two claims, which imply that $$\{n\in\mathbb N:T\vdash\neg\phi(X,n)\}$$ is undecidable.

Claim 0: If $n\in A_0$, then $T+\exists X\,\phi(X,n)$ is consistent.

Proof: Fix $\vec a\in\mathbb N$ such that $p_0(n,\vec a)=0$, and let $m=\max\{n,\vec a,1\}$. By assumption, it is consistent with $T$ that $$X=\{0,1,\dots,m\}$$ is a set. Then we verify in $T$ easily that $N(X)$, $W_0(X,n,m)$, and $\neg W_1(X,n,m)$: in particular, there are no witnesses for “$n\in A_1$” in $\{0,\dots,m\}$, as there are in fact no witnesses in $\mathbb N$ by disjointness of $A_0$ and $A_1$.

Claim 1: If $n\in A_1$, then $T+\exists X\,\phi(X,n)$ is inconsistent.

Proof: As above, fix $\vec a\in\mathbb N$ such that $p_1(n,\vec a)=0$, and let $m=\max\{n,\vec a\}$. Work in $T$, and assume for contradiction that $X$ and $w\in X$ satisfy $N(X)$, $W_0(X,n,w)$, and $\neg W_1(X,n,w)$.

First, assume $w\ge m$. The definition of $N(X)$ easily implies $0,1,\dots,m\in X$. But then in particular, $\vec a\in X$, hence $W_1(X,n,w)$, a contradiction.

On the other hand, assume $w\le m$. The definition of $N(X)$ implies that the only elements of $X$ below $m$ are $0,1,\dots,m$. However, “$n\in A_0$” has no witnesses among $\{0,\dots,m\}$, as it has no witnesses in $\mathbb N$. Thus, we obtain a contradiction with $W_0(X,n,w)$.

  • $\begingroup$ Thank you! It looks like my attempt was rather naive. Apparently, devising "decidable analysis" is not that simple (if possible at all). $\endgroup$ – Alex Gavrilov Jun 6 '18 at 6:30

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.