5 ms·

I can’t read things like this without bringing up Leslie Lamport, the creator of TLA+. His position is that all you need for understanding computation is “regul

I can’t read things like this without bringing up Leslie Lamport, the creator of TLA+. His position is that all you need for understanding computation is “regular” mathematics, i.e. set theory and predicate logic. With just this level of math, we have been able to specify, prove, and model-check sequential and distributed computations. For several decades. I was briefly interested in type theory, dependent types, etc., but have yet to have the payoff from the investment into it. Whereas investing in set theory and predicate logic has had immediate benefits to my day job. Can someone explain what type theory gets us that we don’t already have with set theory? Also, please have a read on one of Lamport’s most clear arguments on the subject: https://lamport.azurewebsites.net/pubs/teaching-concurrency.pdf https://lamport.azurewebsites.net/pubs/teaching-concurrency.....

exdsq 6y ago
Lamport is giving a talk at my workplace on Monday about 21st century proofs, happy to add this question to the Q&A and let you know his answer, I’m interested in this too.
GregarianChild 6y ago
The issue is automation: At this point (Feb 2021), the support in interactive theorem provers is just much better for type-theory based mathematics in contrast to set-theory based maths. Whether that is due to technical advantages of type-theory over set theory, or a historical accident, reflecting the much larger amount of attention on type-theory as basis for interactive provers, is a subject of much controversy. Let me cite a leading light in the formalisation of mathematics [1]: "I would guess that the amount of effort and funding going into type theory exceeds the amount that went into set theory by an order of magnitude if not two [...] I am certain that we would now have highly usable and flexible proof assistants based on some form of axiomatic set theory if this objective had enjoyed half the effort that has gone into type theory-based systems in the past 25 years." Paper [2] has brought renewed attention to set-theory as a basis for automating mathematics. [1] https://cs.nyu.edu/pipermail/fom/2018-June/021032.html https://cs.nyu.edu/pipermail/fom/2018-June/021032.html [2] https://arxiv.org/abs/1707.04757 https://arxiv.org/abs/1707.04757
- amw-zero 6y ago
  That’s a very insightful reply. I hadn’t thought about the fact that the number of working computer scientists today probably does dwarf the number of mathematicians around when ZFC was a current topic.
zozbot234 6y ago
Type theoretical and categorical foundations can be understood as a kind of 'structural' set theory. Structural set theory is a formalization of (naïve) set theory which stays quite a bit closer to commonly-understood mathematical semantics, avoiding a lot of unwanted 'baggage' that is introduced by 'material' set theories such as ZF(C).
- GregarianChild 6y ago
  This 'baggage' are statements like sqrt(17) ∈ log(.) (where (log(.) is the logarithm function) which are syntactically valid and have a truth value, which depends on the exact nature of how you code up various mathematical things in ZF(C). Your cannot form such propositions in type-theory. The downside of type-theory is that it seems difficult to have simple inclusions like: Naturals ⊆ Integers ⊆ Rational ⊆ Reals and that certain natural operations (like quotients) seemingly are labourious in type-theory.
  - zozbot234 6y ago
    These inclusions are anything but "simple", even in material set theory. Consider the real numbers; in common formalizations, a "real number" is an equivalence class of infinite sequences of rational numbers. You can't understand the 'inclusion' of rationals in reals as material (set theoretical) inclusion; you need an adapter/wrapper function. Type theory works the same way. Quotients are not "natural" from a constructive POV, and that's ultimately where the difficulties you're referencing come from. If you're OK with being non-constructive, quotients can be formalized ad hoc. (One of the positive side effects of homotopy-theoretical foundations is that they might help clarify what exactly is going on when one reasons on quotients.)
    - GregarianChild 6y ago
      In ZFC, you define reals as you sketch, and then specify rationals, integers etc as specific subsets, then you get inclusions, which mainstream mathematics uses without worries. And yes, mainstream mathematics is non-constructive (as is Isabelle/HOL). (I don't want to have a contentious discussion about FOMs, or which prover is best, just trying to sketch the trade-offs, and historical background.)
philzook 6y ago
"Set theory" can mean different things. The looser interpretation of set theory is just using the intuitive notion of sets to model things. I think basically everyone is for that and learning these topics is definitely the lower hanging fruit. The usual formal interpretation of what Set Theory is Zermelo Fraenkel set theory, which is roughly first order logic with some axiom schema about how sets behave https://en.wikipedia.org/wiki/Zermelo%E2%80%93Fraenkel_set_theory https://en.wikipedia.org/wiki/Zermelo%E2%80%93Fraenkel_set_t.... I would be somewhat skeptical that this notion of set theory is all that practically useful to use, although people have managed (metamath). In my opinion, first order logic is great in simplicity a degree of automatability, but clunky and awkward in terms of expressivity. Usually the awkwardness of expressing yourself outpaces the automation, and at that point there may be such a mess that it would be terrible to do it manually Type theory and dependent types are different formalizations of intuitive set theory. In a sense, types are kind of sets. From a pure english perspective, the words are close to synonyms and in practice the analogy is pretty close. 3 being of type Int is intuitively like saying 3 is in the set of ints. Type theory seems to me to lead to a cleaner system of syntactic formal reasoning, which sounds esoteric except that syntactic reasoning is what computers have to do since we can't convince them with English paragraphs. And perhaps we don't want to, since English is ambiguous. I think the success Lamport alludes to is even though he bases the TLA+ system on ZFC in some sense, users stick to the fragment of very intuitive notions of set where perhaps your foundations don't matter so much and all should basically agree. This may be more of a pedagogical emphasis than a true difference in systems, since almost everyone interested in dependent types finds the parts that go off into the stratosphere the most interesting.
- carapace 6y ago
  Hey, BTW, your combination of Otten's sequent prover with TeX output is awesome! I think you're really on to something there. https://www.philipzucker.com/javascript-automated-proving/ https://www.philipzucker.com/javascript-automated-proving/
  - philzook 6y ago
    Thanks!

exdsq 6y ago

Lamport is giving a talk at my workplace on Monday about 21st century proofs, happy to add this question to the Q&A and let you know his answer, I’m interested in this too.

GregarianChild 6y ago

The issue is automation: At this point (Feb 2021), the support in interactive theorem provers is just much better for type-theory based mathematics in contrast to set-theory based maths. Whether that is due to technical advantages of type-theory over set theory, or a historical accident, reflecting the much larger amount of attention on type-theory as basis for interactive provers, is a subject of much controversy. Let me cite a leading light in the formalisation of mathematics [1]: "I would guess that the amount of effort and funding going into type theory exceeds the amount that went into set theory by an order of magnitude if not two [...] I am certain that we would now have highly usable and flexible proof assistants based on some form of axiomatic set theory if this objective had enjoyed half the effort that has gone into type theory-based systems in the past 25 years." Paper [2] has brought renewed attention to set-theory as a basis for automating mathematics. [1] https://cs.nyu.edu/pipermail/fom/2018-June/021032.html https://cs.nyu.edu/pipermail/fom/2018-June/021032.html [2] https://arxiv.org/abs/1707.04757 https://arxiv.org/abs/1707.04757

amw-zero 6y ago
That’s a very insightful reply. I hadn’t thought about the fact that the number of working computer scientists today probably does dwarf the number of mathematicians around when ZFC was a current topic.

zozbot234 6y ago

Type theoretical and categorical foundations can be understood as a kind of 'structural' set theory. Structural set theory is a formalization of (naïve) set theory which stays quite a bit closer to commonly-understood mathematical semantics, avoiding a lot of unwanted 'baggage' that is introduced by 'material' set theories such as ZF(C).

GregarianChild 6y ago
This 'baggage' are statements like sqrt(17) ∈ log(.) (where (log(.) is the logarithm function) which are syntactically valid and have a truth value, which depends on the exact nature of how you code up various mathematical things in ZF(C). Your cannot form such propositions in type-theory. The downside of type-theory is that it seems difficult to have simple inclusions like: Naturals ⊆ Integers ⊆ Rational ⊆ Reals and that certain natural operations (like quotients) seemingly are labourious in type-theory.
- zozbot234 6y ago
  These inclusions are anything but "simple", even in material set theory. Consider the real numbers; in common formalizations, a "real number" is an equivalence class of infinite sequences of rational numbers. You can't understand the 'inclusion' of rationals in reals as material (set theoretical) inclusion; you need an adapter/wrapper function. Type theory works the same way. Quotients are not "natural" from a constructive POV, and that's ultimately where the difficulties you're referencing come from. If you're OK with being non-constructive, quotients can be formalized ad hoc. (One of the positive side effects of homotopy-theoretical foundations is that they might help clarify what exactly is going on when one reasons on quotients.)
  - GregarianChild 6y ago
    In ZFC, you define reals as you sketch, and then specify rationals, integers etc as specific subsets, then you get inclusions, which mainstream mathematics uses without worries. And yes, mainstream mathematics is non-constructive (as is Isabelle/HOL). (I don't want to have a contentious discussion about FOMs, or which prover is best, just trying to sketch the trade-offs, and historical background.)

philzook 6y ago

"Set theory" can mean different things. The looser interpretation of set theory is just using the intuitive notion of sets to model things. I think basically everyone is for that and learning these topics is definitely the lower hanging fruit. The usual formal interpretation of what Set Theory is Zermelo Fraenkel set theory, which is roughly first order logic with some axiom schema about how sets behave https://en.wikipedia.org/wiki/Zermelo%E2%80%93Fraenkel_set_theory https://en.wikipedia.org/wiki/Zermelo%E2%80%93Fraenkel_set_t.... I would be somewhat skeptical that this notion of set theory is all that practically useful to use, although people have managed (metamath). In my opinion, first order logic is great in simplicity a degree of automatability, but clunky and awkward in terms of expressivity. Usually the awkwardness of expressing yourself outpaces the automation, and at that point there may be such a mess that it would be terrible to do it manually Type theory and dependent types are different formalizations of intuitive set theory. In a sense, types are kind of sets. From a pure english perspective, the words are close to synonyms and in practice the analogy is pretty close. 3 being of type Int is intuitively like saying 3 is in the set of ints. Type theory seems to me to lead to a cleaner system of syntactic formal reasoning, which sounds esoteric except that syntactic reasoning is what computers have to do since we can't convince them with English paragraphs. And perhaps we don't want to, since English is ambiguous. I think the success Lamport alludes to is even though he bases the TLA+ system on ZFC in some sense, users stick to the fragment of very intuitive notions of set where perhaps your foundations don't matter so much and all should basically agree. This may be more of a pedagogical emphasis than a true difference in systems, since almost everyone interested in dependent types finds the parts that go off into the stratosphere the most interesting.

carapace 6y ago
Hey, BTW, your combination of Otten's sequent prover with TeX output is awesome! I think you're really on to something there. https://www.philipzucker.com/javascript-automated-proving/ https://www.philipzucker.com/javascript-automated-proving/
- philzook 6y ago
  Thanks!