Hacker News new | past | comments | ask | show | jobs | submit login

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

> 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 - the hypotheses include statements about "+ underscore", and lead to a proof about + underscore.

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 ?

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/IsarM...

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-...

Guidelines | FAQ | Support | API | Security | Lists | Bookmarklet | Legal | Apply to YC | Contact