Timeline for What makes dependent type theory more suitable than set theory for proof assistants?
Current License: CC BY-SA 4.0
48 events
| when toggle format | what | by | license | comment | |
|---|---|---|---|---|---|
| Jun 20, 2023 at 8:49 | comment | added | Andrej Bauer | @DaxFohl: if you intended such a crazy definition, you could arrange it in existing proof assistants by defining suitable $\in$ and $\subseteq$ relations. That is, instead of using the type-theoretic judgement "$a$ has type $B$" you would have to define your own "$x \in y$" and "$x \subseteq y$". People actually do this when they formalize set theory. The point is this: it's a bad idea to design a proof assistant so that 99% suffer because 1% want something special. Let the 1% put in some extra effort instead. | |
| Jun 19, 2023 at 22:40 | comment | added | Dax Fohl | I'm confused why the "mistake" is rejected, if it's a formally meaningful statement. What if you actually intended it? Would you have to find another proof assistant? | |
| Jun 2, 2021 at 6:46 | comment | added | Andrej Bauer | @PeterGerdes: I am not sure I understand you. You say at the same time that "$V$ needs some kind of type system" and that "it doesn't seem obvious that you would want the statements in $V$ to be type judgements in that system". I do not see how to take reconcile these statements. | |
| Jun 1, 2021 at 18:52 | comment | added | Peter Gerdes | When you say that V must enforce something like type theory I don't follow what you mean. Sure, it seems like V needs some kind of type system as a programming language would but it doesn't seem obvious that you would want the statements in V to be type judgements in that system. Why assume that we should put our type system to the both the use of ensuring we express precisce concepts and as the underlying logic we are manipulating? Is it just you haven't seen one? | |
| Dec 9, 2020 at 6:32 | comment | added | Alex Gavrilov | Personally, I am not entirely happy with the idea that "A (any) suitable variant of set theory or type theory fits these criteria". If we are talking about some mathematicians sometimes using a proof assistant somehow, then no problem. But if we have in mind a more ambitious goal of formalizing mathematics as a whole, then chosing a kernel stops being just a matter of convenience and becomes a matter of principle. In this case, it should be something to be done very carefully. | |
| Dec 7, 2020 at 8:28 | history | edited | Andrej Bauer | CC BY-SA 4.0 |
added 69 characters in body
|
| Dec 1, 2020 at 12:59 | comment | added | user95393 | Yes, one could say dogmatism is the problem. | |
| Nov 27, 2020 at 9:08 | comment | added | Andrej Bauer |
I have grown tired of dogmatism surrounding foundations. Just a techinical point: Isabelle is a simple type theory within which one can formulate other formalisms. For instance, ZF_base says that membership mem is a map of type [i, i] ⇒ o where i stands for the type of individuals and o for the type of truth values. This is the sense in which I meant that Isabelle/ZF formalizes set theory in type theory.
|
|
| Nov 26, 2020 at 16:23 | comment | added | user95393 | @AndrejBauer: then we might have different notions of what a type-theoretic proof assistant is. Isabelle/ZF adopts set theory as a foundation, not on type theory. And the departure from Isabelle/HOL is partly motivated by the reasons I pointed out originally. I don't know about Flypitch, which looks interesting: thanks for the pointer. I still disagree about the irrationality forcing types from the start by making them a foundational aspect, with no way of escaping them. Again, I wasn't claiming anything, I was merely pointing out a possible reason to bother about these things. Thanks. | |
| Nov 25, 2020 at 9:17 | history | edited | Andrej Bauer | CC BY-SA 4.0 |
added 10 characters in body
|
| Nov 24, 2020 at 16:11 | comment | added | Andrej Bauer | @user95393: You might also be interested in the Flypitch project, a formal verification of the independence of the continuum hypothesis in the Lean theorem prover (which is based on type theory). | |
| Nov 24, 2020 at 16:04 | comment | added | Andrej Bauer | Also, my insistence of having to substantiate various claims with practical experiments is based on the fact that I have seen lots of mathematicians and logicians have fairly naive ideas about how things work or might work. It is easy to be wrong about this topic, I even doubt myself most of the time. It is definitely the case that one has to provide positive evidence about claims, and not expect the other party to provide negative evidence. | |
| Nov 24, 2020 at 16:02 | comment | added | Andrej Bauer | At least in programming (which is quite similar to formalization of mathematics in terms of large-scale organization) there are decades of experience showing that safety is better than a loaded gun pointed at your knee. Regarding formalization of set theory (large cardinals), see for instance Isabelle/ZF. One can very nicely formalize ZF in type theory: the class $V$ is a type, and then other types are things like $V \to V$, $V \times V$, $\mathrm{On}$, etc. Or you can have the type of classes if you want. (Think of the types as meta-level sorts.) | |
| Nov 24, 2020 at 14:24 | comment | added | user95393 | @AndrejBauer: It was you asking a question, I gave an answer. I have nothing to demonstrate. But can I ask you: do you think doing set theory (e.g.,large cardinals) with a type-theoretic proof assistant would be feasible? "safety is valued above the ability to shoot yourself in the foot.": I am afraid this is an unsubstantiated claim (there are opposite opinions, as hinted by my quotation above). Even if it had some merit, it would be greatly diminished in the context of a theorem prover, where you ultimately have a certification of correctness, contrary to most other programming languages. | |
| Nov 24, 2020 at 6:54 | comment | added | Andrej Bauer | @user95393: As I said, it is very easy to have ideas and it is a little harder to demonstrate them in practice. You are quite welcome to demonstrate the benefits of this imagined freedom by exhibiting the practical advantages. Mind you, you will be going not only against the received wisdom in design of proof assistants, but also in programming language design, where safety is valued above the ability to shoot yourself in the foot. | |
| Nov 23, 2020 at 18:39 | comment | added | user95393 | In other words, I don't think the main goal in choosing a foundation should be "stopping people from doing stupid things, because that would also stop them from doing clever things." (quote intended) | |
| Nov 23, 2020 at 18:33 | comment | added | user95393 | @AndrejBauer: "why bother with the set-theoretic kernel that requires a type-theoretic fence to insulate the user from the unintended permissiveness of set theory?" Because the possibility of giving up such a fence when the user wants (while still keeping it when useful) is a freedom not available under type-theoretical foundations. | |
| S Nov 21, 2020 at 12:50 | history | suggested | Erkin Alp Güney | CC BY-SA 4.0 |
grammar edit
|
| Nov 21, 2020 at 10:58 | review | Suggested edits | |||
| S Nov 21, 2020 at 12:50 | |||||
| Nov 21, 2020 at 9:04 | history | edited | Andrej Bauer | CC BY-SA 4.0 |
added 2 characters in body
|
| Nov 21, 2020 at 8:45 | comment | added | Andrej Bauer | @CrabMan: That is a standard definition of natural numbers in set theory. However, how many number theorists do you know who write $2 \in 3$ instead of $2 < 3$? | |
| Nov 21, 2020 at 8:44 | comment | added | Andrej Bauer | @TomLeinster: There is a separation of concern here. The kernel, and only the kernel, is responsible for preventing certification of invalid proofs. A bug in the elaborator might trick the user into thinking that they proved $A$ whereas the kernel received and checked $B$. So you need to trust the printing routines as well. (Mind you, everything we're saying here is a bit idealized.) | |
| Nov 21, 2020 at 8:34 | comment | added | CrabMan | The set of natural number, as defined in Hrbacek's Introduction to set theory, which has $0 = \emptyset, 1 = \{0\}, 2 = \{0, 1\}, 3 = \{0, 1, 2\}$, actually is a jaberwocky set. So the definition of jaberwocky is not so nonsensical. | |
| Nov 21, 2020 at 8:25 | history | edited | Andrej Bauer | CC BY-SA 4.0 |
added 1 character in body
|
| Nov 21, 2020 at 8:24 | comment | added | Andrej Bauer | @TomLeinster: What Mike said, and also note how you're immediately facing design choices. Do you want a map with a separate hypothesis of linearity, or an element of the $\mathrm{Hom}$-set? Yes, yes, "it doesn't matter" – but it does when you design formalized mathematics. And when you design a proof assistant you work very hard so that it wouldn't matter. | |
| Nov 20, 2020 at 22:20 | comment | added | Mike Shulman | @TomLeinster However, under that interpretation (which I would also favor), you then have to implicitly coerce your linear map to a set-function in order to write $f(x)$. (-: | |
| Nov 20, 2020 at 22:20 | vote | accept | MWB | ||
| Nov 20, 2020 at 21:40 | comment | added | Sebastian Reichelt | I can't help but plug my own proof assistant under construction at slate-prover.org, which is DTT-based but appears completely set-theoretic. Here I'm entering your "jaberwocky" example as far as the prover will let me (note how $U$ is not selectable): imgur.com/ZDYBjc7.png | |
| Nov 20, 2020 at 21:40 | comment | added | MWB |
What is Lean's F? (And does it change between versions?)
|
|
| Nov 20, 2020 at 21:20 | comment | added | Tom Leinster | This is a really fantastic answer, MathOverflow at its best. Two questions/objections, though: (1) "A bug in the kernel allows invalid proofs to be accepted, whereas a bug in any other component is just an annoyance": what about a bug in the elaborator? Couldn't that be catastrophic too? (2) I see no implicit coercion in "let $U$ and $V$ be vector spaces and $f: U \to V$ a linear map". As a category theorist, I take you at your word. $f$ is a linear map between vector spaces, and that's that. It's an arrow in $\mathbf{Vect}$. Sets simply aren't mentioned here... right? | |
| Nov 20, 2020 at 18:28 | comment | added | Mario Carneiro | @TimothyChow Metamath in particular was designed with this use case in mind; the tool reports what axioms any particular theorem depends on, and there are a lot of redundant axioms specifically so that you can prove a theorem with the minimum axiomatic strength for which it holds; since the entire library is written that way you can both find out if a given proof is in ZF-replacement, and also a nontrivial fraction of theorems are in fact in that subset. | |
| Nov 20, 2020 at 14:48 | comment | added | jmc | @AndrejBauer Ok, then we are on the same page concerning $M$ (-; It is mathematically uninteresting, but for the working mathematician (interested in proof assistants) it is quite interesting. | |
| Nov 20, 2020 at 14:44 | comment | added | Andrej Bauer | @TimothyChow: Isabelle/ZF (see also this library) is desgined in this fashion: Isabelle is a general framework based on simple type theory, in which FOL and ZF are formulated. It has been quite successful in formalization of great amounts of mathematics. I wouldn't be surprised if Isabelle can help with discovering what fragment of ZF is needed for any particular theorem. | |
| Nov 20, 2020 at 14:35 | history | edited | Andrej Bauer | CC BY-SA 4.0 |
added 27 characters in body
|
| Nov 20, 2020 at 14:35 | comment | added | Timothy Chow | @AndrejBauer : Thanks for the additional explanation. My answer to the question about the ZFC kernel is largely motivated by the reverse-mathematical concerns I alluded to. To put it another way, I'd be okay with a type-theoretic kernel as long as there is a set-theoretic layer on top of it that allows me to think about what I'm doing in set-theoretic terms (e.g., do I need powerset or replacement for this argument?). As a mathematician, I have a fairly clear mental model of how all of math is built on set theory. I don't have a clear mental model of how all math is built on type theory. | |
| Nov 20, 2020 at 14:23 | comment | added | Andrej Bauer | @jmc: I said that from a mathematical point of view $M$ is less interesting because it is more like a programming language and less like a foundational system – not because mathematicians wouldn't use it. Quite the contrary, mathematicians need $M$ to automate their work as much as possible. | |
| Nov 20, 2020 at 14:19 | comment | added | Andrej Bauer | @TimothyChow: you also ask if it's possible to tell whether a given theorem is provable in this or that fragment. Current proof assistants are not really designed to answer such questions, although perhaps with some preparation one could get useful information out of them. With my coworkers I am working on a proof assistant that does not have a fixed foundation, but rather supports user-definable foundations. There may be some way of using that sort of flexibility to verify provability in a fragment, but I don't know. | |
| Nov 20, 2020 at 14:16 | comment | added | Andrej Bauer | @TimothyChow: most elaborators do in fact implement their own brand of type theory, even when the kernel is type-theoretic. The purpose of the secondary type theory is to elaborate, not to guarantee correctness. If there is "super-kernel" on top of a ZFC-kernel, why do we need the ZFC kernel? What's the benefit of complicating the design and having to implement two kernels? | |
| Nov 20, 2020 at 13:52 | comment | added | Jason Rute | @TimothyChow When you say " tell whether a particular theorem can be proved in Zermelo set theory (ZF minus Replacement)", I assume you don't mean that exactly, because that isn't even easily possible with the logic ZFC. I think you mean something like "tell whether the axioms used in the proof are logically no stronger than ZF-Replacement", right? However, even if this is possible, it likely isn't going to be of a lot of value, since practical ITP projects (esp. in Lean) often use more axioms than strictly necessary, e.g. AC, for convenience. | |
| Nov 20, 2020 at 13:46 | comment | added | Timothy Chow | @jmc : Granted. But there's currently a lot more interest in the mathematical community in the reverse mathematics of set theory and of subsystems of second-order arithmetic, than in the reverse mathematics of type theory. One thing that has always made me vaguely uneasy about the existing type-theoretic proof assistants is that I have no clear sense of how the axiomatic strength of what I'm doing lines up against standard measures of axiomatic strength. | |
| Nov 20, 2020 at 13:39 | comment | added | jmc | @TimothyChow probably not (maybe in Mizar or Metamath), but vice versa, in a proof assistent based on ZF(C) it would be nontrivial to tell whether a particular theorem can be proved in MLTT without function extensionality. | |
| Nov 20, 2020 at 13:30 | comment | added | Timothy Chow | @AndrejBauer : To answer your final question directly and elaborate on my remark about calibrating logical strength: Is it easy in any of the current proof assistants to tell whether a particular theorem can be proved in Zermelo set theory (ZF minus Replacement)? | |
| Nov 20, 2020 at 13:25 | comment | added | jmc | Andrej, thanks a lot for this great answer! (Super minor nitpick: let's see whether the meta-language $M$ is not important for mathematicians. It might turn out that it is important that mathematicians/users can easily write short amounts of meta code that codify proof methods specific to a certain subfield of maths. Example: in my recent project with Rob Lewis formalising the ring of Witt vectors, we wrote tactics (meta code) for so-called "ghost calculations" — a common method specific to Witt vectors. This allowed us to then write 2-line proofs of many identities, mimicking the informal.) | |
| Nov 20, 2020 at 13:15 | comment | added | Timothy Chow | Very informative answer! But I don't understand the remark that "a proof assistant whose foundation $F$ is based on ZFC will accept the above definition as valid." Whether it gets accepted depends on the vernacular rather than the foundation, doesn't it? What's to stop someone from building a vernacular that is similar to type theory on top of a set-theoretic foundation? That seems to be the natural thing to do if we want to be able to calibrate logical strength in terms of set-theoretic axioms but want the advantages of type theory in the human interface. | |
| Nov 20, 2020 at 12:32 | history | edited | Andrej Bauer | CC BY-SA 4.0 |
added 223 characters in body
|
| Nov 20, 2020 at 12:21 | history | edited | Andrej Bauer | CC BY-SA 4.0 |
added 19 characters in body
|
| Nov 20, 2020 at 12:13 | history | edited | Andrej Bauer | CC BY-SA 4.0 |
added 594 characters in body
|
| Nov 20, 2020 at 12:02 | history | answered | Andrej Bauer | CC BY-SA 4.0 |
