47
$\begingroup$

Many mathematical subfields often use the axiom of choice and proofs by contradiction. I heard from people supporting constructive mathematics that often one can rewrite the definitions and theorems so that both the axiom of choice and proofs by contradiction aren't needed anymore.

An example is the theory of locales. This is a reformulation of topology that doesn't need the axiom of choice to prove analogues of results that classically need some form of choice, such as Tychonoff's theorem.

I wonder: Are there some tricks behind this "reformulation"? When I have a theorem with a classical proof, how can I reformulate it so that it is provable constructively?

In case this question is too broad, I would be interested in the following example: The usual proof of Gödel's completeness theorem by Henkin isn't constructive. Is there some easy way to reformulate the theorem and the proof constructively? Or is it necessary to define, with much non-trivial work, categorical semantics and state the theorem in this new context?

$\endgroup$
2
  • 2
    $\begingroup$ If you want a more classical treatise about analysis have a look into P. Lorenzen: Differential und Integral. Eine konstruktive Einführung in die klassisische Analysis. Akademische Verlagsgesellschaft (1965). Unfortunately its written in German and I don't know if there is a translation into English, $\endgroup$ Commented Jan 22, 2021 at 19:05
  • 4
    $\begingroup$ Completeness theorem cannot be constructivized: McCarty proved that Heyting arithmetic has the unique model over the Kleene realizability model of $\mathsf{IZF}$. Thus if $\mathsf{IZF}$ proves the completeness theorem, then Heyting arithmetic is not recursive. On the same line, I do not expect there is an easy way to reformulate the completeness theorem constructively. $\endgroup$
    – Hanul Jeon
    Commented Jan 23, 2021 at 4:17

4 Answers 4

61
$\begingroup$

If you want a "general method" that "always works" to turn a classical theorem into a constructive one, there are double-negation translations: if you add enough $\neg\neg$s to a classical theorem, you can make a constructively provable statement. However, this rarely produces a constructively meaningful result. Aside from this, there are no fully general methods, but there are general heuristic (and, in some cases, formalizable) techniques and tricks that can be applied.

The most basic technique is learning to recognize when uses of excluded middle, proof by contradiction, and choice are totally unnecessary. This involves inspecting definitions as well as theorems and proofs, looking for occurences of negated statements that can be turned into classically-equivalent positive ones. For instance, if you defined an injective function to be one such that if $x\neq y$ then $f(x)\neq f(y)$, then using that definition is going to involve a lot of excluded middle; but if you remove the unnecessary contrapositive and define it to mean that if $f(x)=f(y)$ then $x=y$, many proofs immediately become more constructive.

Another technique is to replace a negated statement by a classically-equivalent positive one. For instance, if $x$ and $y$ are real numbers, then in constructive analysis we generally replace $x\neq y$ by $x \mathrel{\#} y$ ("$x$ is apart from $y$"), meaning that they are at least some positive rational distance apart. To a certain extent, this can even be formalized: in Linear logic for constructive mathematics I showed that if a proof can be written in a certain variant of affine logic, then it can automatically be interpreted constructively if enough negative statements are replaced by positive ones in this way.

A third technique is to avoid asking for the bare existence of "ideal" objects, such as ultrafilters, prime ideals, zeros of functions, etc. Instead we can replace these by appropriate "approximating systems". For instance, without some form of choice we may not be able to prove that some spectrum has enough points (filters or ideals) to be a nontrivial topological space; but we can instead consider the frame in which those filters would exist as representing a point-free space (locale). Somewhat analogously, without excluded middle we can't prove the usual Intermediate Value Theorem about the actual existence of some zero; but instead we can approximate such a zero by finding a point whose image is as close to zero as desired.

These replacements aren't always classically equivalent. For instance, there are also constructive versions of the intermediate value theorem in which the hypotheses on the function are strengthened, e.g. to say that it never "hovers" around zero. Such strengthenings can often be found by inspecting the proof to see what is "really used" once excluded middle is pared away; often it happens that these stronger hypotheses are satisfied by most practical applications anyway.

These are just a few of the ideas that occur to me; other more dedicated constructivists will probably be able to list many more. Note that a common theme in many of these techniques is to pay attention to computability. Mathematics (even constructive mathematics) always involves idealizations and infinite objects (unless you're a dyed-in-the-wool finitist/predicativist), but certain kinds of "completed infinity" are impossible to compute with, so we can make them more constructive by thinking about how we might represent an approximation computationally, or what actual data would witness the truth of some negative statement.

Finally, regarding Gödel's completeness theorem, as you may know it is equivalent to either weak König's lemma (if the language is countable) or the Boolean Prime Ideal Theorem (if the language is arbitrary). Since these are known to be unprovable constructively, so is the completeness theorem as Gödel stated it. I would say that the version in categorical semantics is the "correct" constructive completeness theorem; sometimes it's unavoidable that a certain amount of nontrivial work is required to turn something into a constructive version (for instance, locales also require some work vis-a-vis topological spaces). This can be regarded as an instance of the general method of "avoiding ideal objects": instead of a single ideal set-model that requires non-constructive principles for its existence, we consider the collection of more concrete categorical models.

$\endgroup$
5
  • $\begingroup$ Do you have a reference to recommend for the completeness theorem that you mention? $\endgroup$
    – user44143
    Commented Jan 22, 2021 at 21:25
  • 4
    $\begingroup$ @MattF. You mean the version using categorical semantics? One is in D1.4 of Sketches of an Elephant. It's probably also in Makkai-Reyes Introduction to First-Order Categorical Logic (which might even be the original reference? I'm not sure), but I don't have that in front of me to check. $\endgroup$ Commented Jan 22, 2021 at 21:31
  • 1
    $\begingroup$ Thank you very much for this great answer! Concerning your suggestion of replacing ideal objects by approximating systems: This suggestion seems to work only if one wants to constructivize a theorem about ideal objects. In this case, one can reformulate the theorem by replacing these ideal objects by approximating systems, fine. But if one wants to constructivize a theorem whose proof uses ideal objects as a tool (such as ultrafilters in the proof of the compactness theorem), this suggestion doesn't seem to help much. Am I missing something? $\endgroup$
    – user877505
    Commented Jan 23, 2021 at 19:58
  • 1
    $\begingroup$ I would say that the compactness theorem is also a theorem about ideal objects, namely "ideal models". Of course there are also non-ideal models (just as a non-spatial locale can have some points), but the models that the compactness theorem claims to exist are of the ideal sort. $\endgroup$ Commented Jan 23, 2021 at 21:42
  • $\begingroup$ Alright, thanks. $\endgroup$
    – user877505
    Commented Jan 24, 2021 at 13:38
15
$\begingroup$

Errett Bishop gave some principles in his book on Constructive Analysis:

“The task of making analysis constructive is guided by three basic principles.

  • First, to make every concept affirmative. (Even the concept of inequality is affirmative.)
  • Second, to avoid definitions that are not relevant. (The concept of a pointwise continuous function is not relevant; a continuous function is one that is uniformly continuous on compact intervals.)
  • Third, to avoid pseudogenerality . (Separability hypotheses are freely employed.)”

Those are so openly stated in the founding text of modern constructive mathematics that I don’t think they qualify as tricks. They may not even qualify as helpful advice for a novice, but they are actually reasonable focal points for someone with some experience in the art of constructivizing.

As for the completeness theorem, I never saw a constructive version that I found satisfying, because there is usually no constructive content to the hypothesis that a theory is consistent. But here is a line of thought: What can we do constructively with consistency? Sometimes we have decision procedures. What can we do constructively with a model? Sometimes we build another model. So maybe there is a theorem: If $R$ is a ring with quantifier elimination, then $R[x]/(p)$ also has quantifier elimination. And some version of this for more general algebraic objects could be a distant constructive analog of the completeness theorem....but the line of thought gets so distant so quickly that you might decide that the completeness theorem is not a good place to look for constructivity.

$\endgroup$
1
  • $\begingroup$ Thanks! Especially the Bishop quote is quite enlightening. $\endgroup$
    – user877505
    Commented Jan 24, 2021 at 13:39
7
$\begingroup$

Are you aware that the (semantic) completeness theorem for countable first-order languages is equivalent over RCA0 (a weak subsystem of second-order arithmetic) to WKL0? Essentially the non-constructive part of this lies in the fact that you want to obtain an infinite path from an infinite binary tree. This principle is truly non-constructive, since there is a computable infinite tree with no computable infinite path. So even in the countable realm, which arguably is what truly constructive mathematics should be about, the completeness theorem is non-constructive. But it is not that bad; we can obtain a model of any consistent computable FOL theory that is computable from the first Turing jump.

If you are interested in the use of AC in the uncountable case, the issue lies entirely with whether the theory can be well-ordered. The completeness theorem holds for any theory over a well-orderable language. In general you can find that almost every theorem that invokes AC or Zorn's lemma can be rephrased as theorems about well-ordered stuff whose proofs need no choice. For example, every well-orderable field has an algebraic closure, and every vector space with a well-orderable spanning set has a basis. So even in the usual setting of Zermelo set theory you can easily extract the 'more constructive' version just by adding well-orderability conditions.

$\endgroup$
6
$\begingroup$

I wrote a guide to constructivizing proofs at https://us.metamath.org/ileuni/mmil.html#intuitionize . The notation and to some extent the content is specific to IZF (Intuitionistic Zermelo–Fraenkel) as formalized in metamath. But much of what is covered there applies more broadly: use apartness rather than negated equality, for ordinals think in terms of ∅ ∈ 𝐴 rather than 𝐴 ≠ ∅ , replace nonempty set with inhabited set, and others. The links on that page provide examples (which in many cases will let you compare a constructive proof with the corresponding non-constructive proof by comparing the Intuitionistic Logic Explorer with the Metamath Proof Explorer).

$\endgroup$

You must log in to answer this question.

Not the answer you're looking for? Browse other questions tagged .