[FOM] 618: Adventures in Formalization 4

[Anthony Coulter]

We may be talking at cross purposes, but I would suggest that a general-
purpose constructive proof checker probably cannot rely on the
decidability of the first-order theory of the reals.

In Bishop-style analysis, the real numbers do *not* form a totally
ordered field. That is, Bishop would not admit "for all real a, b:
a <= b or b <= a" as an axiom. In its place he offered the weaker
assumption that for all a,b, and c, a < b implies that either a < c or
c < b. Since Bishop started with a different set of axioms, his first-
order theory of the reals comes out different from the first-order
theory everyone else is used to. (The fact that Bishop restricted
himself to intuitionistic logic makes the first-order part of this
theory even more different.) So Tarski's celebrated decision procedure
(which was written for a totally-ordered field under classical logic)
does not apply to Bishop's constructive theory. The fact that the first-
order theory of the reals provides only enough symbols to construct
algebraic numbers is immaterial here because you aren't allowed to
assume that all numbers are algebraic when you try to prove the
inequalities.

In these situations it's the predicates (not the functions) that turn
out to cause computability problems. Bishop identified real numbers with
rational Cauchy sequences. Computing sums and products of Cauchy
sequences is straight- forward enough, but determining whether a Cauchy
sequence converges to a number which is just above, just below, or
exactly equal to zero is not. So equality and order relations turn out
to be uncomputable in that system. But if you can't tell whether a
number is zero or not, then a definition by cases will also fail: you
can't say "1/x = {if x = 0, then 0, otherwise perform the usual
algorithm for reciprocals of Cauchy sequences}" because the "if x = 0"
is not computable. If you disregard this fact and allow the definition
by cases *anyway*, then you run into the problem I described earlier in
this thread, where assuming that this reciprocal exists *prior* to being
shown a proof of x != 0 leads you to prove an existential claim that is
intuitionistically invalid.

I'll admit that the term "constructivism" also applies to formalisms
other than Bishop's, and in these situations you might not run into this
sort of problem. But like I stated in my last post, if your notion of
constructivism involves intuitionistic logic, you must either allow
functions to be defined on decidable domains only, or use free logic to
avoid that problem with existential quantifiers.

Regards,
Anthony