24
votes
Accepted
Why should you "never resort to polymorphism when initiality would do"?
Initiality comes with a powerful universal property which allows you to, internally, prove statements about the constructions you perform. If you give me an element of ...
- 1,264
18
votes
What are the advantages to impredicativity?
All impredicativity means is that propositions form a complete lattice! This is a basic principle of mathematics.
So if you want to be able to use the architecture of mathematics developed in the last ...
- 2,053
10
votes
Which proof assistant would you advise me to learn (in 2022) considering my interests?
There is no single right answer and all of this will be highly subjective. Before I get into the details based on the subjects you want to learn, I would just say, pick something, play around with it,...
- 9,653
8
votes
Accepted
What are the advantages to impredicativity?
There are some tricks that only work when you have access to an impredicative universe. They tend to construct "the smallest object" of some kind, without an explicit construction, i.e. a ...
- 2,353
7
votes
Could Prop be the top universe?
I am going to interpret your + as "is an element of", i.e., you are asking for a hierachy of universes that looks like this:
$$\mathsf{Set} : \mathsf{Type}...
- 10k
7
votes
Counterexamples in Type Theory
Coq maintains a document of historical proofs of absurdity, including brief explanations of the flaw that allowed them to pass. Most of these are more "counter-examples in type theory ...
- 1,547
7
votes
Inductive vs. recursive definitions
Defining recursive properties by fixpoint is possible, but it is usually easier to reason on inductively defined ones. Mostly because they come with their own induction principles. If you use fixpoint ...
- 146
7
votes
Accepted
Pragmatic encodings of inductive inductive types
Your example signature is negative recursive in the second field of Sigma so it can't be encoded in total languages.
For internal universes, the usual solution is ...
- 2,077
6
votes
Figures on computer proof assistant usage
I don't have answers to most of your questions but another way to look at this question is which proof systems have formalized the most theorems. The largest scale effort that I know of to track ...
- 231
6
votes
Accepted
How can you represent a dependent type visually?
I addressed some of these questions in my lecture “Spartan Type Theory” (PDF slides) at the UniMath 2017 school in Birmingham. In particular, slide 18 looks like this:
Please look at the slides for ...
- 10k
6
votes
Why is it hard to formalize informal proofs?
Are there any theoretical obstacles in formalizing what we actually do when we mentally verify equations, etc?
Yes: we don't know what we actually do when we mentally verify equations!
This is a glib ...
- 2,053
6
votes
Accepted
Naming conventions (letter case, underscores, &c) for Coq
A similar question was recently discussed in the Coq Zulip chat (regular link, no-login-needed link), of which this answer is a summary.
The vstyle project is working on building / collecting Coq ...
- 946
5
votes
Accepted
Could we speed up ATP or ATD using a directed graph that appears to work like a gigantic brain?
Building that gigantic proof graph as an explicit graph would probably be a very bad idea, given its size and the complexity of "connecting inputs to outputs". Indeed, as you can have an ...
- 5,620
4
votes
Counterexamples in Type Theory
Making this a community wiki. Here are a few that come to mind, some more obvious than others, with a theme, and not described in detail. May add more later.
A simply typed $\lambda$-term whose ...
4
votes
Inductive vs. recursive definitions
Let me just mention a third possibility which is sometimes called "small inversion". This is some kind of middle ground between the two possibilities you present, which gives you some of the ...
- 5,620
3
votes
Counterexamples in Type Theory
As mentioned in this answer on this site, so-called "positive coinductive types" break subject reduction.
3
votes
Accepted
Figures on computer proof assistant usage
I think one has to be a bit careful here. I wouldn't say the primary users of proof assistants would self identify as mathematicians. I think many use proof assistants for software and hardware ...
- 9,653
3
votes
Pragmatic encodings of inductive inductive types
To complement András' answer, and especially if you want to stay in Coq, you can also define such an internal universe using indexed inductive types only. Basically, you replace the definitions of ...
- 5,620
3
votes
Accepted
How does Lean4 (or a typical PA) represent lambda functions or in other words arbitrary expressions?
(This answer assumes you already know some of the basics of Lean as in Theorem Proving in Lean 4.)
In a typical first logic class or set theory class in college, first order logic is presented as ...
- 9,653
3
votes
Which proof assistant would you advise me to learn (in 2022) considering my interests?
I really cannot improve on Jason Rute's answer, but one suggestion I would have: after playing around with whatever theorem prover you decided to use, dabble around with a few others.
In particular, ...
- 1,574
2
votes
Inductive vs. recursive definitions
Inductive allows you to express non-deterministic, non-terminating computations, while Fixpoint computations can be ...
- 301
1
vote
Which proof assistant would you advise me to learn (in 2022) considering my interests?
I can't (yet) recommend AutoMath, except for historical interest. But, I resurrected it here AutoMath (GitHub) on GitHub, with upgrade on its syntax.
Its biggest weakness, by far, is its inability to ...
- 111
Only top scored, non community-wiki answers of a minimum length are eligible