Return to Question

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 an answer by Emil Jeřábek.)

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.)

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] Emil Jeřábek pointed out that there is a predicate $x\in{\mathbb N}$ in the form $$\forall X(0\in X\wedge \forall y(y\in X\to y+1\in X)\to x\in X).$$ Originally, I though about restricting (or forbidding) quantifiers over sets to avoid something like this, but now I think it may be unnecessary. This predicate is useless (for its intended purpose) if we cannot prove existence of sufficiently many sets $X$ with this property, and I think it might be the case.

[EDIT] Following Jeřábek, denote the above predicate by $N(x)$. If we have $$(N(x)\wedge x\neq 0)\to N(x-1),$$ then we already have Robinson arithmetic (which is undecidable). The thing is, I do not see how to prove this implication by the means available.

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 an answer by Emil Jeřábek.)

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] Emil Jeřábek pointed out that there is a predicate $x\in{\mathbb N}$ in the form $$\forall X(0\in X\wedge \forall y(y\in X\to y+1\in X)\to x\in X).$$ Originally, I though about restricting (or forbidding) quantifiers over sets to avoid something like this, but now I think it may be unnecessary. This predicate is useless (for its intended purpose) if we cannot prove existence of sufficiently many sets $X$ with this property, and I think it might be the case.

Let me elaborate. Denote by $N$ the set of "natural numbers" defined by the above predicat. Let $\phi(x)$ be a formula. Can we prove the induction $$\phi(0)\wedge \forall y\in N(\phi(y)\to \phi(y+1))\to \forall n\in N\, \phi(n)?$$ I think, no (without some more axioms). Let us assume that the conclusion is false, that is, $\neg \phi(n)$ for some $n\in N$. The problem is, this $n$ is not given explicitely (say, $n=10000$), all we know about it is that $n\in X$ for any $X$ as above. To arrive at a contradiction, we need to show that there is $y\in N$ such that $\phi(y)$ but $\neg \phi(y+1)$; essentially, we need a proof that $N$ is well ordered. If I am not mistaken, we do not have means for that.

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] Emil Jeřábek pointed out that there is a predicate $x\in{\mathbb N}$ in the form $$\forall X(0\in X\wedge \forall y(y\in X\to y+1\in X)\to x\in X).$$ Originally, I though about restricting (or forbidding) quantifiers over sets to avoid something like this, but now I think it may be unnecessary. This predicate is useless (for its intended purpose) if we cannot prove existence of sufficiently many sets $X$ with this property, and I think it might be the case.

[EDIT] Following Jeřábek, denote the above predicate by $N(x)$. If we have $$(N(x)\wedge x\neq 0)\to N(x-1),$$ then we already have Robinson arithmetic (which is undecidable). The thing is, I do not see how to prove this implication by the means available.