7
$\begingroup$

The language of ordered rings is a first-order language with operators for $+$, $-$, and $\cdot$, constants for $0$ and $1$, and relations for $<$, $=$ and $>$.

To decide whether such a statement can be classically proven (in, say, ZFC) for the real numbers is easy:

But now consider the problem of deciding whether such a statement is provable about the (Dedekind) reals in, say, neutral constructive mathematics. The above algorithm no longer works on the input $\forall x. \forall y. (x = y) \lor \lnot (x = y)$. The algorithm above will state that it is provable since CAD says it is true, but it is in fact not constructively provable since it is the analytic WLPO, which is a constructive taboo. A correct algorithm would declare this statement to be not provable. (See aws's comment for a description of this set of sentences using topos theory.)

So my question is does such an algorithm exist?

I have a feeling though that this should still be computable. Constructive algebra is basically just "fuzzy" classical algebra.

Note though that for first-order arithmetic, the answer is no. A $\Sigma^0_1$ statement is provable iff it is true (whether considering classical or constructive proofs), and deciding this would let you solve the halting problem.

Also note that, constructively, formulas do not in general have a Prenex normal form.

Improve this question
$\endgroup$
21
  • 1
    $\begingroup$ Are we talking about decidability of a theory, or about the decidability of validity in a particular model? Whatever it is, you should not be saying things like "classically proven for real numbers" because "proven" makes sense with respect to a theory but "real numbers" is not a theory, it's a model (or a structure). And then a little later you say "use CAD to compute whether it is true or not". So which is it going to be, "prove" or "true"? Do you understand what confuses me? $\endgroup$
    – Andrej Bauer
    Commented Apr 11 at 23:39
  • 1
    $\begingroup$ Are we talking about Tarski's theorem that the theory of a real closed field is decidable? If so, that result is purely proof-theoretic. In the context of Tarski's result CAD is not about "truth" but about proving theorems in the theory of real-closed field. Mentioning ZFC just causes confusion, because it has nothing to do with Tarski's result. I speak formally and I am nit-picking but I am really trying to understand what the question is. Also,, as a logician I feel entitled to nitpick more than normal mathematicians. $\endgroup$
    – Andrej Bauer
    Commented Apr 12 at 5:34
  • 6
    $\begingroup$ According to the paper doi.org/10.2307/2271730 the intuitionistic theory of real closed fields is not decidable, although the proof doesn't apply to the set of sentences in the language that hold for $\mathbb{R}_d$, because it goes via adding a fairly strong version of division that doesn't hold constructively for the reals. $\endgroup$
    – aws
    Commented Apr 12 at 8:21
  • 5
    $\begingroup$ @AndrejBauer if I understand right, the precise question would be "which sentences in the language of ordered rings hold for the Dedekind real number object in every topos with n.n.o." $\endgroup$
    – aws
    Commented Apr 12 at 14:53
  • 2
    $\begingroup$ @AndrejBauer vouching for why this question is interesting: (1) what makes Tarski's result interesting isn't that some oddly specific set of axioms implies all the first-order properties of the reals, but the corollary that the first-order properties of the reals are computable (2) you can quickly check if something is a constructive taboo and (3) an algorithm like this would be a pretty cool feature in a constructive proof assistant $\endgroup$
    – Christopher King
    Commented Apr 12 at 15:28

0

Reset to default

You must log in to answer this question.