5 ms·

It is not difficult to keep the notation sane in formalizations based on set theory. One way is to defer overloading of symbols to the presentation layer. You c

It is not difficult to keep the notation sane in formalizations based on set theory. One way is to defer overloading of symbols to the presentation layer. You can see an example of that at [1] where the + sign is used to denote the group operation, right and left shifts on sets and the natural "addition" of subsets of the group derived from the group operation. [1] http://isarmathlib.org/TopologicalGroup_ZF.html http://isarmathlib.org/TopologicalGroup_ZF.html

auggierose 7y ago
If it can be done, it needs to be done at the presentation layer, I guess so too. It has been a while since I worked with Isabelle locales. So how come that in your example "x + y" is not being confused with "A + B", although all involved entities are ZF sets? Or does A actually have a different type than x ?
- robinzfc 7y ago
  Isabelle allows the user to define symbols. So, those two operations are represented by different symbols in the source (the *.thy files) but the presentation layer renders them both as "+". You may want to look at the corresponding IsarMathLib source at [1] on GitHub. Isabelle/ZF uses only two types: set ("i") and prop("o"). [1] https://github.com/SKolodynski/IsarMathLib/blob/master/IsarMathLib/TopologicalGroup_ZF.thy https://github.com/SKolodynski/IsarMathLib/blob/master/IsarM...
  - auggierose 7y ago
    Ah, I see. So, when I type in those formulas, can I use + or do I need to type in the original symbols? Nevermind, I know the answer to that. That's why Set theory notation is a difficult problem, and you need some sort of type presentation / input layer. Some people also refer to that as a user space type system or soft types: https://www21.in.tum.de/~krauss/publication/2010-soft-types-note/ https://www21.in.tum.de/~krauss/publication/2010-soft-types-...
dwheeler 7y ago
> It is not difficult to keep the notation sane in formalizations based on set theory. Keeping notation sane is, of course, very important. I think keeping notation sane is harder than it might first appear, but it is certainly possible. One interesting trick used by Metamath's set.mm is to define variables that look similar to operators but can be defined for purposes of a particular proof (e.g., as hypotheses). For example, + underline, * underline, and so on. For an example, see theorem grpridd, "Deduce right identity from left inverse and left identity in an associative structure (such as a group)." http://us.metamath.org/mpeuni/grpridd.html http://us.metamath.org/mpeuni/grpridd.html - the hypotheses include statements about "+ underscore", and lead to a proof about + underscore.

auggierose 7y ago

If it can be done, it needs to be done at the presentation layer, I guess so too. It has been a while since I worked with Isabelle locales. So how come that in your example "x + y" is not being confused with "A + B", although all involved entities are ZF sets? Or does A actually have a different type than x ?

robinzfc 7y ago
Isabelle allows the user to define symbols. So, those two operations are represented by different symbols in the source (the *.thy files) but the presentation layer renders them both as "+". You may want to look at the corresponding IsarMathLib source at [1] on GitHub. Isabelle/ZF uses only two types: set ("i") and prop("o"). [1] https://github.com/SKolodynski/IsarMathLib/blob/master/IsarMathLib/TopologicalGroup_ZF.thy https://github.com/SKolodynski/IsarMathLib/blob/master/IsarM...
- auggierose 7y ago
  Ah, I see. So, when I type in those formulas, can I use + or do I need to type in the original symbols? Nevermind, I know the answer to that. That's why Set theory notation is a difficult problem, and you need some sort of type presentation / input layer. Some people also refer to that as a user space type system or soft types: https://www21.in.tum.de/~krauss/publication/2010-soft-types-note/ https://www21.in.tum.de/~krauss/publication/2010-soft-types-...

dwheeler 7y ago

> It is not difficult to keep the notation sane in formalizations based on set theory. Keeping notation sane is, of course, very important. I think keeping notation sane is harder than it might first appear, but it is certainly possible. One interesting trick used by Metamath's set.mm is to define variables that look similar to operators but can be defined for purposes of a particular proof (e.g., as hypotheses). For example, + underline, * underline, and so on. For an example, see theorem grpridd, "Deduce right identity from left inverse and left identity in an associative structure (such as a group)." http://us.metamath.org/mpeuni/grpridd.html http://us.metamath.org/mpeuni/grpridd.html - the hypotheses include statements about "+ underscore", and lead to a proof about + underscore.