Are there any constructive higher order logics? In particular, could one take the foundation of Isabelle/HOL remove excluded middle and choice and still have a powerful foundation of constructive math? It seems Isabelle's usage of structured proofs makes its syntax preferable to Coq but Isabelle/HOL, the by far largest Isabelle library, is entirely classical. What would the impediments be to making Isabelle/CHOL (Constructive HOL) in which all the classical theorems (T) could be rephrased as (excluded middle ==> choice ==> T)?
Is there a constructive version of the logic of Isabelle/HOL
foundationslogicproof-verification
Related Solutions
I apologize if this answer ends up a little vague.
There is no one definition of what "constructive" or "non-constructive" means. Even in the community of mathematical constructivism, there are many disagreements. Just the title of one classic book, "Varieties of constructive analysis", already suggests this.
I can point out two common issues with constructive or non-constructive proofs.
Constructiveness depends on proof methods. For example, the classical inference rule of double negation elimination ("From $\lnot \lnot P$ derive $P$") is usually viewed as nonconstructive. But a somewhat similar rule of ex falso quodlibet ("From $P$ and $\lnot P$ derive any sentence $Q$") was viewed as acceptable to proponents of intuitionism. The status of the axiom of choice varies greatly from one program of constructive mathematics to another.
Constructiveness depends on representations. The things that can be done constructively with a mathematical object depend on how the object is represented. For example, in general one cannot prove constructively that for any real number $a$ either $a < 0$, $a = 0$, or $a > 0$. This is because the usual system for representing real numbers does not allow this question to be answered in constructive manner just given a representation for $a$. On the other hand, it is possible in many constructive systems to prove that any integer is "negative, 0, or positive", because the representation of an integer used in such systems is sufficiently nice to allow the answer to be constructively determined from the representation. Note that for some constructivists the "representation" that matters is the mental representation they have.
These two items are related because the constructively permissible proof methods depend greatly on the representations being used. For example, the appropriate forms of the axiom of choice are non-constructive relative to CZF set theory but are constructive relative to Martin-Löf type theory.
Back to the original question. There are many constructive proofs that do not use any methods that imply the entire law of the excluded middle. For example the proof might just use the so-called "lesser limited principle of omniscience" which does not imply excluded middle. In fact I do not know whether there is any one sentence in the language of Heyting arithmetic that implies the entire law of the excluded middle over the rest of HA.
Here is a partial answer.
Godel's theorem connects logic and set theory. Syntax is the part of the logic, it's where the formulas and proofs live; set theory is the part of the semantics, where the interpretations and models live. Of course one can have them relocated to other contexts, but classically I think that it's a theorem about logic and set theory.
It is provable without the axiom of choice that if we have an infinite tree whose nodes are the natural numbers, and every level of the tree is finite, then there is a branch in that tree. If we omit the requirement that the nodes of the tree are the natural numbers, it won't be true anymore and counterexamples do exist (by which I mean, consistent with $\sf ZF$, of course).
Similarly, given a countable language we write the proof of the completeness theorem for that language, and all our uses of the axiom of choice will be mitigated by the fact that we have a uniform enumeration of all the objects of interest. Therefore some fragment of the completeness theorem is in fact provable without any appeal to the axiom of choice.
On the other hand, the completeness theorem is not about countable languages. It is about any language of first-order logic. So we can have a lot of function symbols, or constants, or so on. So what about the above proof? Well, it can be shown that if the language is well-orderable, then indeed we can repeat the same arguments and everything is well-orderable uniformly and everything is fine.
But alas, without the axiom of choice, not every set can be well-ordered. And that where the non-constructive nature of the proof sneaks in. Let me give a particular counterexample.
Example:
We say that a set $A$ is amorphous if it is infinite, and cannot be written as a disjoint union of two infinite sets. One can show that if $A$ is an amorphous set, then there is no way to linearly order $A$. That is, there is no $R\subseteq A\times A$ such that $(A,R)$ is a linearly ordered set.
Suppose that $A$ is an amorphous set (and it is consistent that such set exists), and let $\mathcal L$ be the language in which $<$ is a binary relation symbol, and for every $a\in A$ there is a constant symbol $c_a$.
We write the axioms, $\varphi$ is the conjuction of the statements $<$ is a linear order, and for every distinct $a,b\in A$ we write $\varphi_{a,b}:=c_a\neq c_b$. This theory is consistent, because if it were to prove a contradiction there would be a finite number of $a\in A$ whose constants appear in the proof, but then we can construct a finite linear order which will be an interpretation of these axioms. This is impossible of course.
However, the theory as a whole, despite being consistent, does not have a model. Because in any model of the theory, reducing just to the constants will have defined a linear order of $A$, and $A$ itself is an amorphous set, so it cannot be linearly ordered.
So where is the axiom of choice coming into the play? When we construct models we need to make some arbitrary choices along the way. When the language is well-ordered then we can delegate these choices to the well-ordered and uniformly make them all; but when the language is an arbitrary set which may not be well-orderable to begin with, then the axiom of choice is needed.
In fact, one can prove that the completeness theorem (and its equivalent, the compactness theorem) is equivalent to the ultrafilter lemma, stating that every filter can be extended to an ultrafilter. These all are also equivalent to many other weak choice principles such as Tychonoff theorem for Hausdorff spaces, or the Boolean Prime Ideal theorem.
So what is missing from this answer? Well, I don't know about contexts where the WKL is not provable, so I cannot help in that aspect. But hopefully this answer shed some light on where the theorem is using fragments of choice and non-constructiveness.
Best Answer
The answer to "are there any constructive higher-order logics" is yes. Martin-Löf type theory and its many descendants and variants are the examples that first come to mind.
However, you seem to be particularly interested in versions of simple type theory as implemented in Isabelle/HOL. In principle, the HOL logic as implemented in Isabelle is the same as that implemented in the other theorem provers in the HOL family (HOL IV, HOL Light, ProofPower, ...). John Harrison's HOL Light presents the logic in a way that clearly separates out the intuitionistic fragment (see his paper HOL Light: an overview). I suspect it would require some significant restructuring of Isabelle/HOL to adopt the HOL Light formulation. If that's something you'd like to happen, then I suggest you raise this on the Isabelle mailing list rather than here.
As a small aside: the axiom of choice implies the axiom of excluded middle in higher-order logic.