3
$\begingroup$

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)?

$\endgroup$
2
  • $\begingroup$ I could imagine having intuitionistically provable theorems in the Isabelle library depending on classically proven theorems just because the library was assumed to be "classical forever anyway". (No offense at Isabelle developers intended.) $\endgroup$
    – ComFreek
    Sep 30, 2019 at 7:41
  • $\begingroup$ I’m sure much of the library is not set up to easily constructivize that which can be constructivized, just because people just use whatever is easiest to prove something and that might not be the constructive(izable) proof. My question is more if there is a fundamental impediment to making Isabelle/HOL “constructive friendly”, so that things can be constructive if they want to be or classical if that makes sense, more like real math. $\endgroup$ Oct 1, 2019 at 1:06

1 Answer 1

1
$\begingroup$

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.

$\endgroup$

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.