16
votes
Accepted
Incorporating Markov's principle in various proof assistants
There are different ways to implement Markov's principle, and they're not equivalent. I know of at least three techniques to implement MP.
MP as a loop
I personally find this to be a hack inherited ...
- 2,353
12
votes
How usable is Lean for constructive mathematics?
First, a quick disclaimer: I am not a constructivist! However, I am a logician and I care about aspects of constructive mathematics and I really care about computability in general.
As Jason mentioned,...
12
votes
How usable is Lean for constructive mathematics?
I think given the other two positive answers, I want to temper expectations.
Lean 4 is designed for classical mathematics in mind, and the developers don't have any current plans to support ...
- 9,653
10
votes
Accepted
Are there automated theorem provers for constructive logics? What strategy do they use?
The firstorder tactic in Coq is an "experimental extension of tauto to first-order reasoning." The tauto tactic &...
- 1,547
10
votes
Accepted
Lean: dubious noncomputability
The purpose of the noncomputability checker is to (try to) determine whether or not the VM compiler will succeed in making executable bytecode, which can be evaluated more efficiently (by ...
- 506
9
votes
How usable is Lean for constructive mathematics?
It's worth noting that there are roughly two different standards of "constructivity" in Lean:
classical.choice: if ...
- 971
6
votes
In a dependently typed language, are all types statements?
To make the basics clear: languages don't mean anything before you assign them meanings manually, and you can interpret the same language different ways. So if you want to interpret a dependent type ...
- 4,077
6
votes
Lean: dubious noncomputability
(assuming Lean 3): There is a command called environment.decl_noncomputable_reason
in Lean 3.35c or later that may help you diagnose the reason for noncomputability, or at least the declaration in ...
- 635
6
votes
How usable is Lean for constructive mathematics?
It is reasonable to ask, "what does constructive mathematics even mean in 2022?"
It certainly owes nothing at all to Brouwer and Heyting's "intuitionism" beyond the rejection of ...
- 806
6
votes
Why does it matter if canonicity holds for irrelevant types?
Consider the following type theory:
\begin{gather}
\frac{ }{\vdash G \; \mathsf{type}} \qquad
\frac{ }{\vdash \Lambda \; \mathsf{type}} \\[2ex]
\frac{\vdash g : G \qquad \vdash e_1 : \Lambda \qquad \...
- 9,931
5
votes
Converting between formulations of reals in Coq
I apologize, but the correct answer is “you do not want to convert between different formulations of reals”. As a rule of thumb, you should pick one formalization of reals and run with it. Trying to ...
- 9,931
5
votes
Algorithms obtained through constructive formalization
Cubical type theory, or any constructive interpretation of HoTT implies the computability of various aspects of algebraic topology. That means, you can encode concepts of homotopy theory into $\lambda$...
- 680
5
votes
Algorithms obtained through constructive formalization
The logic group in Munich has worked on program extraction in the past decades. Most notably, they extracted a program computing the transitive closure of a relation from a graph-theoretic proof and a ...
- 665
5
votes
Accepted
Why does it matter if canonicity holds for irrelevant types?
I will focus here on a universe of definitionally irrelevant types; let's call it SProp. In short, we can postulate any consistent SProp axiom, without breaking any constructive metatheoretic property....
- 2,077
5
votes
Accepted
LEM, the halting problem, the curry-howard correspondence -> deep connection?
Is it correct that the omission of LEM is the distinguishing characteristic of constructive logic as opposed to classical?
Yes.
Is it correct that the Curry-Howard correspondence is conditioned on ...
- 1,639
4
votes
In a dependently typed language, are all types statements?
You can look at the ways to define types as ways to define propositions.
One simple definition of Nat is its Boehm-Berarducci encoding: ...
- 2,087
4
votes
Why does it matter if canonicity holds for irrelevant types?
One answer is that (judgmental) proof irrelevance does not correspond to computational irrelevance. Proof irrelevance means that every proof is equal in some sense. But that doesn't mean the values ...
- 982
4
votes
Type Theory research groups
External links
The following pages mention researchers interested in the foundations or applications of proof assistants:
Authors participating in the TYPES international conference on Types for ...
4
votes
Algorithms obtained through constructive formalization
In structural proof theory, a nice example of an algorithm arising from a constructive proof is the technique of hereditary substitution.
In 1995, Frank Pfenning wrote a paper, Structural Cut ...
- 2,053
4
votes
Which proof assistants implement Church's rule?
Not the answer you would like to hear, but that would be "no proof assistant" (to my knowledge). The first reason is that Church's rule does not hold for classical theories but the ...
- 9,931
3
votes
LEM, the halting problem, the curry-howard correspondence -> deep connection?
Complexity theory in general has very low logical complexity. Almost all of it can be expressed in Peano arithmetic, and often in much weaker fragments of arithmetic. Furthermore, the most interesting ...
- 9,931
3
votes
Determining why my proof depends on the axiom of choice
I tried to replace parts of the proof with sorry, but I was getting confused by the results of doing so, so I made a small ...
- 161
2
votes
Accepted
Which proof assistants implement Church's rule?
You might want to give a look at A Certifying Extraction with Time Bounds from Coq to Call-By-Value Lambda Calculus by Yannick Forster and Fabian Kuntze. They define a set-up in Coq where using ...
- 5,620
2
votes
LEM, the halting problem, the curry-howard correspondence -> deep connection?
I'll just try and address some of the more basic points, I'll let others deal with the more technical details related to proof assistants (see Mario Carneiro's answer for example):
Is it correct that ...
- 258
1
vote
Algorithms obtained through constructive formalization
I don’t think you can exactly call that a useful algorithm, but being able to actually compute with the proof that there exists an $n$ such that $\pi_4(S^3)$ is isomorphic to $\mathbb{Z}/n\mathbb{Z}$ ...
- 5,620
Only top scored, non community-wiki answers of a minimum length are eligible