230
votes
Accepted
What makes dependent type theory more suitable than set theory for proof assistants?
I apologize for writing a lengthy answer, but I get the feeling the discussions about foundations for formalized mathematics are often hindered by lack of information.
I have used proof assistants for ...
- 48k
40
votes
What makes dependent type theory more suitable than set theory for proof assistants?
EDIT: Since this question has gotten so much interest, I have decided to substantially rewrite my answer, stating explicitly here on MO some of the more important points rather than forcing the reader ...
- 78.6k
40
votes
Top-down mathematics, or "Where it all begins"
One approach, mentioned by Pace Nielsen in the comments, is to start with what I call strict formalism. The only substantive assumption required for strict formalism is that you are capable of ...
- 78.6k
32
votes
What makes dependent type theory more suitable than set theory for proof assistants?
I still find it very surprising that this random talk I gave attracts so much attention, especially as not everything I said was very well thought out. I am more than happy to engage with people in ...
- 40.8k
30
votes
How do we construct the Gödel’s sentence in Martin-Löf type theory?
I think we can assume MLTT is a formal system of the usual kind. Therefore, in formal arithmetic using Gödel numbering we can formulate the arithemetic statement con(MLTT), stating the consistency of ...
- 309
29
votes
Accepted
Formalizations of the idea that something is a function of something else?
First of all, it seems to me as though the real question here is "what is a variable quantity?" Most of the definitions you quote from pre-20th century mathematicians assume that the notion of "...
- 65.1k
27
votes
Accepted
How can the simply typed lambda calculus be Turing-incomplete, yet stronger than second-order logic?
The simply-typed $\lambda$-calculus is not stronger than second-order logic.
The simply-typed $\lambda$-calculus has:
product types $A \times B$, with corresponding term formers (pairing and ...
- 48k
23
votes
Accepted
Why would the category of sets be intuitionistic?
You wrote:
Suppose our intuition for the phrase "subset of $X$" comes from the idea of having an effective total function $X \rightarrow \{0,1\}$ that returns an answer in a finite amount ...
- 48k
23
votes
Two interpretations of implication in categorical logic?
There are two concepts here, which are tightly connected. Logically, this corresponds to the distinction between $\vdash$ and $\Rightarrow$.
(A) Morphisms $t : \Gamma \to A$ represent (well-formed, ...
- 8,755
22
votes
Accepted
In constructive mathematics, why does the category of abelian groups fail to be abelian?
There are many different flavors of constructive mathematics. The theory that was used in this paper is weak, it lacks some useful constructions from the usual set theory such as quotient sets. ...
- 4,410
21
votes
How do we construct the Gödel’s sentence in Martin-Löf type theory?
There is a generalization of Gödel's incompleteness theorem that is more naturally applicable to MLTT: Löb's theorem says that to prove $P$, it suffices to prove that $P$ is true whenever $P$ is ...
- 695
21
votes
Accepted
Coinduction for all?
This is a question that I've puzzled about myself, and I don't pretend to have The Answer. But here's one thought that I've found illuminating. Let's start by comparing the behavior of induction and ...
- 65.1k
20
votes
Accepted
History of the notation for substitution
Some early examples of the form $[t/x]$ are due to Haskell Curry.
See:
Haskell Curry & Robert Feys & William Craig, Combinatory Logic. Volume I (1958), page 54:
Let $a$ and $b$ be obs and ...
- 1,681
20
votes
Can you have a type theory where there is type of all types?
Of course you can have $\mathsf{Type} : \mathsf{Type}$, the consequence of that is that all types are inhabited (by Girard's paradox). Some people call this an inconsistency, but that only makes sense ...
- 48k
20
votes
Top-down mathematics, or "Where it all begins"
Here is a possible viewpoint to contemplate:
Foundations of mathematics do not begin anywhere.
This happens to be my (current) personal belief. I agree with Monroe that the answer to the question ...
- 48k
19
votes
Accepted
What kind of category is generated by Cubical type theory?
There are two kinds of answers as to what kind of category a "homotopy type theory" is the internal language of. On the one hand there is a kind of $(\infty,1)$-category that is the semantic object ...
- 65.1k
17
votes
Accepted
Why are W-types called "W"?
You write:
Probably "W" means either "wellordered" or "wellfounded". […] But these are notions associated to order theory, whereas W-types don't directly have to do with ...
- 19.2k
16
votes
Accepted
Why the reflection rule trivializes higher paths in Martin-Löf Extensional Type theory?
The point is that the reflection rule makes $p = \mathsf{refl}_x$ a well-formed expression. This turns out to be incredibly dangerous: now we can prove it by induction on equality.
More precisely:
...
- 14.9k
16
votes
Good introductory book to type theory?
Here are some resources:
UniMath school teaching materials, and in particular:
Spartan type theory, an introduction to type theory (slides)
Introduction to Univalent Foundations of Mathematics with ...
16
votes
Accepted
3 questions about basics of Martin-Löf type theory
Universe levels usually trip up newcomers to type theory since there is no straightforward intuition for them. What I found helpful is to think of them as a merely technical device to prevent ...
- 308
15
votes
Accepted
What do we call this quantifier ("binder")?
You are describing the regular tree grammars. Here is the basic idea.
It is useful to think of syntactic expressions as abstract syntax trees. In our case we are looking for a tree $\alpha$ which ...
- 48k
15
votes
Accepted
Homotopy type theory: Are the hierarchy of Type_k universes isomorphic?
This question is about type theory in general and is not specific to homotopy type theory. $\newcommand{\Type}{\mathtt{Type}}$
The thing you are missing is that a universe $\Type_k$ contains very ...
- 48k
14
votes
Practical Benefits of HTT/univalent foundations for assisted proofs
You didn't specify exactly what "claimed benefits" for non-univalent type theory in general you're referring to, and I happen to believe that even non-univalent type theory does have ...
- 65.1k
13
votes
How do we construct the Gödel’s sentence in Martin-Löf type theory?
Maria Emilia Maietti starts her http://www.sciencedirect.com/science/article/pii/S1571066104805693 by saying that "André Joyal constructed arithmetic universes to provide a categorical proof of ...
- 179
13
votes
Accepted
Are there types with nontrivial paths in all dimensions? (HoTT)
$\prod_{n\in\mathbb{N}} S^n$ certainly has nontrivial structure at all levels (i.e. "is not a homotopy $n$-type for any finite $n$"). In classical homotopy theory, even $S^2$ by itself has nontrivial ...
- 65.1k
13
votes
Good introductory book to type theory?
I am far from being an expert. I will make a few suggestions.
Per Martin-Löf. Intuitionistic type theory. (Notes by Giovanni Sambin of a series of lectures given in Padua, June 1980). Napoli, ...
13
votes
What types are to mathematical proofs as types à la Martin-Löf are to constructive proofs, and what's wrong with them?
A good starting point to learn about type theories for classical logic is the $\lambda\mu$-calculus introduced in 1992 by Parigot in λμ-Calculus: An algorithmic interpretation of classical natural ...
- 48k
13
votes
What does the ramified in ramified type theory mean?
As far as I know, the word "ramified", in reference to type theory, means that one pays attention not only to the ranks of sets (where sets of rank $n$ have members of rank $n-1$) but also ...
- 72.3k
12
votes
Identity types: What makes Intuitionistic Type Theory *intuitionistic*?
As far as I can tell Martin-Löf's analysis of identity and his formulation of the identity types is the intuitionistic explanation of identity. In terms of BHK it would be an algorithmic version of ...
- 48k
12
votes
Accepted
What exactly is a judgement?
I highly recommend reading Martin-Löf's paper referenced by Ulrik Buchholtz in the comments to your question. Apart from that, here are a couple of point that might help, some of which were already ...
- 48k
Only top scored, non community-wiki answers of a minimum length are eligible