3 ms·

>> i found the foundations via set-theory unintuitive and a bit ackward to work with. > Type theories, especially dependent type theories a la Martin-Löf, are

>> i found the foundations via set-theory unintuitive and a bit ackward to work with. > Type theories, especially dependent type theories a la Martin-Löf, are quite natural to work with (and) are easier to implement on a computer... Whether or not type theories are "natural" is probably a matter of taste. But it's hard to argue that they are necessarily "easier to implement on a computer". Metamath is a general-purpose verifier, and its primary database (the Metamath Proof Explorer at http://us.metamath.org/mpeuni/mmset.html http://us.metamath.org/mpeuni/mmset.html ) is based on classical logic and ZFC set theory. A Metamath verifier in Mathematica is only 74 lines, while another in Python is only 350 lines. The Metamath verifier written in Rust is longer (it's written for speed), but it manages to verify about 32,000 proofs in about 0.9 seconds. It's so easy to write one that there's a long list of verifiers (see http://us.metamath.org/other.html#verifiers http://us.metamath.org/other.html#verifiers ). Metamath can handle HOL, too. I don't know of any shorter verifier that can handle the full range of mathematics. So by both code size and speed it's hard to argue that type theory is necessarily "easier" than traditional set theory on a computer. They both simply process symbols given a small set of rules. There are many possible foundations of mathematics beyond ZFC and type theory, e.g., Quine's "New Foundations" (NF) (see http://us.metamath.org/nfeuni/mmnf.html http://us.metamath.org/nfeuni/mmnf.html for a Metamath encoding of that), HOL, etc. And that's not even counting logic systems: Classical logic is the most common in mathematics (by far), but intuitionistic logic is in use (and tools like Coq are built on it), and there are many other logic systems as well (paraconsistent, minimal, etc.). That said, I believe ZFC (combined with classical logic) is by far the most commonly foundation referenced in mathematics today. Wikipedia claims: "Today, Zermelo–Fraenkel set theory, with the historically controversial axiom of choice (AC) included, is the standard form of axiomatic set theory and as such is the most common foundation of mathematics." https://en.wikipedia.org/wiki/Zermelo%E2%80%93Fraenkel_set_theory https://en.wikipedia.org/wiki/Zermelo%E2%80%93Fraenkel_set_t... That doesn't mean that other systems are "not as good" or "not mathematical" - but when people ask about mathematical foundations, ZFC is typically what people refer to first. It's probably good to at least know a little about ZFC when discussing foundations, even if you decide to do something different.

gylterud 7y ago
EDIT: It is a fair point that it is difficult to say what is easier to implement (the below expands on this). By type theory being natural I was mostly thinking of the fact that it is basically a functional programming language with a very strict compiler. Actually, Metamath is not tied to ZFC. As the name implies it is a meta-theory where you could implement a lot of different theories. That said, most Metamath developments use ZFC. I haven’t seen anyone doing type theory in Metamath, but from what I understand it may be possible. Also, this means if you are counting lines you need to include the formalisation of the logic and the axioms of ZFC inside metamath. The kernel of Coq is similarly a quite short program. Certainly there is a wealth of systems available. But the ones based on type theory, such as Coq, seem to be at least as popular as the set theory based ones (For instance the first formalised proof of the four colour theorem and Gödel’s theorems were in Coq).
- dwheeler 7y ago
  > Actually, Metamath is not tied to ZFC. As the name implies it is a meta-theory where you could implement a lot of different theories. That said, most Metamath developments use ZFC. I haven’t seen anyone doing type theory in Metamath, but from what I understand it may be possible. That's true. There's a Metamath database that encodes Higher-Order Logic (HOL) aka simple type theory: http://us.metamath.org/holuni/mmhol.html http://us.metamath.org/holuni/mmhol.html It's very bare-bones, but it shows it's possible. > Certainly there is a wealth of systems available. But the ones based on type theory, such as Coq, seem to be at least as popular as the set theory based ones... I suspect we have to ask "popular for whom?" I'd agree that type theory is at least as popular as set theory among computer tools that formalize math. But I think far more mathematicians point to ZFC, not type theory, as the foundations of mathematics. Type theory probably seems "natural" to people who are used to programming languages and compilers, and thus already have a daily familiarity with types (in the computer science sense). "It's complicated" seems like an accurate summary of affairs :-).
  - 0815test 7y ago
    > But I think far more mathematicians point to ZFC, not type theory, as the foundations of mathematics. That's true, but it's just as true that those same mathematicians only care about foundations as a proof of concept, not a practical device that you might someday want to do actual math in. ZFC is plenty good enough for the former, but you need type theories - or at least structural-set theories - to enable the latter (with the sorts of sanity checks that we've come to expect in any practical formal endeavor)!

gylterud 7y ago

EDIT: It is a fair point that it is difficult to say what is easier to implement (the below expands on this). By type theory being natural I was mostly thinking of the fact that it is basically a functional programming language with a very strict compiler. Actually, Metamath is not tied to ZFC. As the name implies it is a meta-theory where you could implement a lot of different theories. That said, most Metamath developments use ZFC. I haven’t seen anyone doing type theory in Metamath, but from what I understand it may be possible. Also, this means if you are counting lines you need to include the formalisation of the logic and the axioms of ZFC inside metamath. The kernel of Coq is similarly a quite short program. Certainly there is a wealth of systems available. But the ones based on type theory, such as Coq, seem to be at least as popular as the set theory based ones (For instance the first formalised proof of the four colour theorem and Gödel’s theorems were in Coq).

dwheeler 7y ago
> Actually, Metamath is not tied to ZFC. As the name implies it is a meta-theory where you could implement a lot of different theories. That said, most Metamath developments use ZFC. I haven’t seen anyone doing type theory in Metamath, but from what I understand it may be possible. That's true. There's a Metamath database that encodes Higher-Order Logic (HOL) aka simple type theory: http://us.metamath.org/holuni/mmhol.html http://us.metamath.org/holuni/mmhol.html It's very bare-bones, but it shows it's possible. > Certainly there is a wealth of systems available. But the ones based on type theory, such as Coq, seem to be at least as popular as the set theory based ones... I suspect we have to ask "popular for whom?" I'd agree that type theory is at least as popular as set theory among computer tools that formalize math. But I think far more mathematicians point to ZFC, not type theory, as the foundations of mathematics. Type theory probably seems "natural" to people who are used to programming languages and compilers, and thus already have a daily familiarity with types (in the computer science sense). "It's complicated" seems like an accurate summary of affairs :-).
- 0815test 7y ago
  > But I think far more mathematicians point to ZFC, not type theory, as the foundations of mathematics. That's true, but it's just as true that those same mathematicians only care about foundations as a proof of concept, not a practical device that you might someday want to do actual math in. ZFC is plenty good enough for the former, but you need type theories - or at least structural-set theories - to enable the latter (with the sorts of sanity checks that we've come to expect in any practical formal endeavor)!