Questions tagged [constructive]
For questions about constructive or intuitionistic logic. Constructive proofs can be extracted as programs.
9
questions
2
votes
0
answers
192
views
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 ...
- 121
5
votes
2
answers
644
views
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 ...
- 997
25
votes
4
answers
2k
views
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 ...
- 6,995
14
votes
4
answers
305
views
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 ...
- 891
12
votes
1
answer
320
views
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 ...
- 3,688
12
votes
3
answers
315
views
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 ...
- 1,015
9
votes
1
answer
291
views
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 ...
- 722
15
votes
1
answer
236
views
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 ...
- 2,711
14
votes
1
answer
241
views
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 ...
- 492