# Questions tagged [constructive]

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

13 questions
Filter by
Sorted by
Tagged with
658 views

### In a dependently typed language, are all types statements?

In dependently typed languages such as Agda, Lean, Coq, Idris (and Pie), a mathematical or logical statement can be expressed as a type, and then proven by writing a program that creates an instance ...
• 141
268 views

### Determining why my proof depends on the axiom of choice

I would like to write constructive proofs in Lean 4, so I don't want my proofs to depend on Classical.choice, the axiom of choice. However, one of my proofs does, ...
• 161
183 views

### Which proof assistants implement Church's rule?

Church's rule (CR) is one of the hallmarks of constructive mathematics, and is an admissible rule in a wide variety of constructive theories (you might consider CR to be a requirement for constructive ...
447 views

### LEM, the halting problem, the curry-howard correspondence -> deep connection?

I posted the following on the math stackexchange, but it occurs to me that this might be a more (or at least equally?) appropriate forum: It was recently said to me by a prominent mathematician, who I ...
245 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
808 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 ...
• 1,051
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 ...
• 8,685
319 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 ...
• 901
406 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,967
359 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,025
303 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