231
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 ...
41
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 ...
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 ...
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 ...
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 ...
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 "...
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 ...
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 ...
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, ...
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. ...
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 ...
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 ...
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 ...
20
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 ...
19
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 ...
18
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 ...
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 ...
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 ...
Community wiki
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 ...
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 ...
14
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 ...
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 ...
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 ...
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 ...
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, ...
Community wiki
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 ...
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 ...
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 ...
12
votes
Formalizations of the idea that something is a function of something else?
The situation here seems very analogous to that in probability, where there is also a state space $\Omega$ (which is the underlying set of a probability space $(\Omega, {\mathcal B}, {\bf P})$) which ...
12
votes
Accepted
A peculiarity of Henkin's 1950 proof of completeness for higher order logic
Henkin's completness proof for first order logic (using his method of constants) and Henkin's work on the completeness of type theory were both carried out in his doctoral 1947 dissertation written ...
Only top scored, non community-wiki answers of a minimum length are eligible
Related Tags
type-theory × 204lo.logic × 119
homotopy-type-theory × 50
ct.category-theory × 47
reference-request × 24
foundations × 24
set-theory × 23
lambda-calculus × 19
constructive-mathematics × 18
proof-theory × 15
soft-question × 9
computability-theory × 9
categorical-logic × 9
computer-science × 8
mathematical-philosophy × 8
proof-assistants × 7
new-foundations × 7
homotopy-theory × 6
higher-category-theory × 5
topos-theory × 5
universal-algebra × 5
intuitionism × 5
model-theory × 4
terminology × 4
formal-languages × 4