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?
Best Answer
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.