Skip to main content

Questions tagged [constructive]

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

Filter by
Sorted by
Tagged with
4 votes
2 answers
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 ...
Mars's user avatar
  • 141
3 votes
1 answer
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, ...
Robin Green's user avatar
4 votes
2 answers
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 ...
Christopher King's user avatar
2 votes
5 answers
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 ...
user avatar
2 votes
0 answers
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 ...
Gavin Dooley's user avatar
7 votes
2 answers
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 ...
Neil Strickland's user avatar
27 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 ...
Jason Rute's user avatar
  • 8,685
14 votes
4 answers
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 ...
Will Sawin's user avatar
13 votes
1 answer
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 ...
Trebor's user avatar
  • 3,967
12 votes
3 answers
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 ...
James Martin's user avatar
  • 1,025
9 votes
1 answer
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 ...
Nico's user avatar
  • 722
15 votes
1 answer
264 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 ...
Greg Nisbet's user avatar
  • 2,771
14 votes
1 answer
267 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 ...
Bruno Le Floch's user avatar