I’m starting a new thread because this is a reply to several different comments and because the nesting level in threaded view is getting ridiculous.
I think there is one fundamental problem that is cropping up repeatedly in several guises in this discussion, which I mentioned up here. It appears to have led me astray in a few places as well (as it’s done before in the past; argh!). Namely, in unaugmented structural set theory (including ETCS and SEAR and type theory), a structured set is not a single object in the domain of discourse. For instance, in none of these cases does the formal language allow one to talk about a group. A group in SEAR (to be specific) consists of a set and an element and a function , such that certain axioms are satisfied. By contrast, in ZF, a group can be defined to consist of an ordered triple such that , is a function , and certain other axioms are satisfied.
This is what I meant when I said here that the relation between rationals and (Dedekind) reals is extra structure on the same set of reals. The ordered field of reals consists of the set , some elements , some functions , a relation , etc. The relation is one more piece of structure on the same set , which you can use or not use as you please.
Likewise, this is what I think is going on with opposites. If I’m working with a group as above, then I can construct its opposite group to consist of the same set , the same element , and a reversed function . Now of course it makes sense to ask whether an element of and an element of are equal, since they are elements of the same set. On the other hand, if I am just given two groups and , it makes no sense to ask whether an element of is equal to an element of . So what I said here is not quite right, and I apologize: what I should have said is that it would be a type error to compare elements of (sets underlying) two different structures unless those structures are built on the same underlying set(s).
(If you’re going to object to the notion of sets being “the same,” I think the answer was provided by Toby: we mean the external judgment that two terms are syntactically equal, rather than a (disallowed) internal proposition that two terms refer to the same object.)
So I think it is misleading to speak about two different groups “having elements in common”—either we are talking about two different group structures on the same set, in which case the two have exactly the same elements by definition, or we are talking about group structures on different sets, in which case asking whether an element of one is equal to an element of the other is a type error. Therefore, I was also not quite right when I said that a structural system would not be able to construct categories having common objects: it can construct pairs of categories (such as a category and its opposite) that have the same collection of objects, but no more.
Now going back to the original subject of intersections, in a structural theory the operation of “intersection” does not apply to arbitrary pairs of sets, but rather to pairs of subsets of the same fixed ambient set. (One might argue that the intersection of a set with itself should be defined (and equal to itself), but I think this probably derives from a misconception that distinct sets in structural set theory are “disjoint,” rather than it just not being meaningful to ask whether their elements are equal.) In particular, it is not meaningful to speak of the intersection of the sets of objects of two categories.
It never really occurred to me before to consider this peculiarity (that structured sets are not single things) as a problem, since “for any group, …” can always be interpreted as shorthand for “for any set , element , and function such that <blah>, …”, and similar sorts of interpretations happen in other foundations like ZF. But I guess that this sort of implicit interpretation is part of the “compilation from high-level language to assembly language,” and what you want is a formalization of the higher-level language that (among other things) includes “a group” as a fundamental object of study.
I admit that this is definitely something I have found frustrating about existing proof assistants: they do not seem to really understand that “a group” is a thing. But somehow I never really isolated the source of my frustration before.
One way to deal with this (which I believe is adopted by many type theorists?) is to introduce one set called a “universe” whose elements are (interpreted as) sets in some way. Then a triple of sets can be modeled by an element of , and so on. But a really structural approach would insist that sets are not the elements of any set, but rather the objects of a category—so what we really need is structural category theory, which doesn’t quite exist yet. Possibly this is what Lawvere was thinking of when he said that “when one wishes to go substantially beyond [ETCS], a much more satisfactory foundation… will be provided by a theory of the category of categories”—although I’ve always felt that one should really be thinking about the 2-category of categories.
Regardless, it does seem that existing structural frameworks fall short here. Now I feel all fired up to improve them! But that’s a whole nother kettle of worms.
I’m also feeling bad about hijacking this discussion with a long branching argument about the merits of structural/categorial set theory. If people have the energy, let’s also go back to FMathL and your larger proposal and see what other constructive things we can discuss about it. As I said way back at the beginning, I am really excited about the overall idea—which is perhaps what is driving me to be overly critical of FMathL, since I would like such a system to “get it right” (and for better or for worse, I usually seem to think I know what’s “right”). But as I’ve said, I feel like I understand a little better now where you are coming from and what problems you are trying to solve.
Re: Towards a Computer-Aided System for Real Mathematics
Incredibly ambitious! I dare say even ridiculously ambitious…
Reading this reminded me of a much more modest idea. I’d love a plugin for my web browser and/or PDF previewer that can automagically follow citations like [Theorem 6.5, 17]. This would perhaps work by deciphering out what [17] is (by reading the bibliography of the same paper), extracting or locating online a copy of the paper, and searching through that for Theorem 6.5. I’d imagine the user interaction is just right-clicking on a citation, and having a pop-up box showing me the theorem statement, that I could then click on to get the statement in the original paper.
At least for papers on the arXiv, which are generated using hypertex, it shouldn’t be too hard to algorithmically locate “Theorem 6.5”.