Questions tagged [constructive]

For questions about constructive or intuitionistic logic. Constructive proofs can be extracted as programs.

Filter by
Sorted by
Tagged with
2 votes
0 answers

Proof of a certain proposition not using classical logic

I'm self-studying the textbook Theorem Proving in Lean, and there's one exercise from Section 3.7 that I'm stuck on. The exercise asks for a proof of the proposition ¬(p ↔ ¬p) that does not use ...
Gavin Dooley's user avatar
5 votes
2 answers

Lean: dubious noncomputability

In Lean, some definitions must be marked as noncomputable, for example if they depend on the law of the excluded middle or other nonconstructive choice principles. Usually, the reason for ...
Neil Strickland's user avatar
25 votes
4 answers

How usable is Lean for constructive mathematics?

In my answer explaining the differences between Lean and Coq, I emphasized that Lean is "essentially classical" mostly due to sociological norms. Nonetheless, even after posting that, I ...
Jason Rute's user avatar
  • 6,995
14 votes
4 answers

Algorithms obtained through constructive formalization

Formal proofs in proof systems that avoid the law of the excluded middle and certain other principles can be automatically converted into algorithms. What useful new algorithms have been produced by ...
Will Sawin's user avatar
12 votes
1 answer

Incorporating Markov's principle in various proof assistants

The Markov's principle states that if a Turing machine does not run forever, then it halts. Equivalently, if I have a function $f : \mathbb N \to \mathrm{Bool}$, such that I have proved that $\neg\neg ...
Trebor's user avatar
  • 3,688
12 votes
3 answers

Why does it matter if canonicity holds for irrelevant types?

Suppose you were to add a non-constructive axiom which only applies to irrelevant types, such as the irrelevance axiom. To my understanding canonicity and strong normalization are defining features of ...
James Martin's user avatar
  • 1,015
9 votes
1 answer

Type Theory research groups

Research about type theory, internal languages, intuitionism, constructivism, and proof assistants is, at the moment, not as fashionable as other branches of mathematics are, say for example algebraic ...
Nico's user avatar
  • 722
15 votes
1 answer

Are there automated theorem provers for constructive logics? What strategy do they use?

I know of a handful of automated theorem provers for classical first-order logic such as Vampire (source code). Internally, I think most of these provers work by translating premises and the negated ...
Greg Nisbet's user avatar
  • 2,711
14 votes
1 answer

Converting between formulations of reals in Coq

While trying to answer more concretely a question on floating points, I tried proving a simple statement using the Flocq library of Coq. However, I got stuck before really exercising it because I am ...
Bruno Le Floch's user avatar