Timeline for What makes dependent type theory more suitable than set theory for proof assistants?
Current License: CC BY-SA 4.0
22 events
| when toggle format | what | by | license | comment | |
|---|---|---|---|---|---|
| Nov 29, 2020 at 20:13 | comment | added | Ulrik Buchholtz | @TimothyChow : Adding various amounts of choice, excluded middle, and impredicativity is just as easy, if not easier, in type theory as in set theory. As to type-theoretic Big Five equivalents, I'm afraid this margin is too small to really elaborate, but yes, “relatively easy” for the most part: Basic type theory is ca. ACA₀, a hierarchy of universes bumps to ATR₀, adding W-types lands you in the vicinity of Π¹₁–CA₀. It's slightly trickier to go below towards finitism and RCA₀/WKL₀, but there's work in that direction by Herbelin and Patey. I think polytime systems are also doable, but harder. | |
| Nov 29, 2020 at 16:33 | comment | added | Timothy Chow | @UlrikBuchholtz : The first topic that comes to my mind (in connection with RM based on set theory) is weakenings of the axiom of choice. Exactly how much choice (on top of ZF) is needed to prove various theorems? There is also some work on what can be accomplished without Replacement and/or Powerset, although my impression is that that's of interest to a pretty small community of researchers. But do I understand correctly that you're claiming that RM a la Simpson's SOSOA book is "relatively easy to capture" with type theory? The five big systems have natural type-theoretic equivalents? | |
| Nov 29, 2020 at 15:15 | comment | added | Ulrik Buchholtz | @TimothyChow : well, type theory incorporates finite type arithmetic as a subsystem, so that kind of higher-order RM is relatively easy to capture. And there are natural weak subsystems of type theory, as I said. I'm not so familiar with work on RM based on set theory. Could you give some pointers? I can imagine as base system something like IKP with extensions, but perhaps something else is used? | |
| Nov 29, 2020 at 15:13 | comment | added | Ulrik Buchholtz | @TimothyChow : By “abstract math” I mean stuff about “arbitrary” sets/groups/topological spaces/etc. that don't have a fixed place in the finite type hierarchy. Results about these are very awkward if not impossible to formalize in simple type theory/HOL. | |
| Nov 29, 2020 at 13:57 | comment | added | Timothy Chow | @UlrikBuchholtz : What exactly are you referring to with the phrase "abstract math"? In any case, I don't mean to say that there isn't any interesting reverse mathematics to be done in the type-theoretic world. I only mean that there's a large amount of reverse mathematics that has already been done in a set-theoretical or arithmetical setting, and one might hope that a proof assistant would be able to capture this knowledge naturally. | |
| Nov 29, 2020 at 9:56 | comment | added | Ulrik Buchholtz | A comment about reverse mathematics (RM) & Maddy's Risk Assessment and Metamathematical Corral: I think the jury is still out on this: Most work in RM uses either (classical) subsystems of 2nd order arithmetic or of HA/PAomega (arithmetic in finite types), and these systems are not suitable for abstract math. Type theory has natural weak fragments of strength HA, through predicative arithmetic, and up. And there's preliminary work also on finitistic type theories. I think formalization in something like (intuitionistic) Kripke-Platek set theory would be unwieldy by comparison. | |
| Nov 25, 2020 at 4:03 | comment | added | MWB |
@KevinBuzzard Even if I had proved 2 > 0 on the previous line, I had to prove it again on this line -- Maybe this part of Lean should have been fixed instead? I know nothing about proof assistants, but this sounds totally unreasonable.
|
|
| Nov 25, 2020 at 1:45 | comment | added | Timothy Chow | @Max : Yes. Or at least, 1/0 = 0 in Lean. | |
| Nov 25, 2020 at 0:15 | comment | added | MWB |
giving 0/0 a concrete value Does this apply to Lean though?
|
|
| Nov 24, 2020 at 19:25 | history | edited | Timothy Chow | CC BY-SA 4.0 |
Major rewrite
|
| Nov 22, 2020 at 11:49 | comment | added | მამუკა ჯიბლაძე | @RobertFurber Would not you agree that it is more difficult to make accidental mistake in a typed/oop language compared to an untyped one? For an opposite extreme - most efficient coding is doable in assembly language or even just in machine codes, but you must be a true ace flying high to locate errors in such code I guess. | |
| Nov 21, 2020 at 6:53 | comment | added | Robert Furber | There's also this article by Leslie Lamport and Larry Paulson: lamport.azurewebsites.net/pubs/lamport-types.pdf The point is that just because a programming language is typed, that doesn't mean one should make the specification language typed, and types can cause problems as well as solve them. There is some rebuttal to the "$2 \in 3$ is gibberish" argument. My own is that I have never found any difficulty in writing gibberish in any typed language, especially by accident. | |
| Nov 21, 2020 at 5:21 | history | edited | Timothy Chow | CC BY-SA 4.0 |
Added links to FOM list
|
| Nov 21, 2020 at 5:09 | history | edited | Timothy Chow | CC BY-SA 4.0 |
added 72 characters in body
|
| Nov 20, 2020 at 14:16 | comment | added | Kevin Buzzard | When I am doing counting, I like my natural numbers to start at 0 (because some sets are empty). When I am doing primes and factoring, I like them to start at 1 (otherwise I have to continually have to write "if n isn't zero then..."). My feelings about sets and types are the same -- different foundational systems make different things easier/nicer. | |
| Nov 20, 2020 at 12:04 | comment | added | Andrej Bauer | I never insisted that one way is uniformly better than the other. In any case, I explained my position more carefully in a separate answer. | |
| Nov 20, 2020 at 10:22 | comment | added | Asaf Karagila♦ | @Andrej: What if they are but also aren't (the slides raise excellent points), and insisting that one thing is better than the other in a grand, uniform way, is actively harmful to the conversation about foundations of mathematics? | |
| Nov 20, 2020 at 3:39 | comment | added | Deane Yang | Types are wonderful in both programming and mathematics. | |
| Nov 19, 2020 at 20:24 | comment | added | Andrej Bauer | What if they are also more natural for mathematicians? | |
| Nov 19, 2020 at 20:01 | comment | added | Asaf Karagila♦ | I liked the slides. The argument that type theories are more natural to programmers is something I heard before, and it had made me cry from the inside. | |
| Nov 19, 2020 at 19:20 | comment | added | Andrej Bauer | John Harrison's slides are a fine collection of suggestions, but there is a long way from having good ideas about theorem provers to implementing them and trying them out. Has Harisson worked on the ideas? | |
| Nov 19, 2020 at 18:49 | history | answered | Timothy Chow | CC BY-SA 4.0 |