1
$\begingroup$

My long standing question:

How to eliminate writing $\cap^L$ instead of plain $\cap$ when we deal with more than one lattice? (and likewise with other (finite and infinite) structures) It is especially boring when $L$ is more than one math symbol but a more complex expression.

Can we do something like disjoint union of all lattices? It seems this problem is somehow solved in Mizar, but I don't know Mizar (despite of the fact that I'm familiar with Isabelle/ISAR). BTW, can you provide me with a readable introduction into Mizar's type system?

  • 0
    In Introduction to lattices and order By B. A. Davey, Hilary A. Priestley on [p.146](http://books.google.com/books?id=vVVTxeuiyvQC&pg=PA146) they have the same problem. (They're using two lattices $P$ and $P_c$.) They use $\bigwedge\limits_P$ and $\bigwedge_{P_c}$.2011-11-25

3 Answers 3

1

If you have a language $\mathcal L$ with a binary relation $R$ and function $f(x,y)$, you can write formulae such as $\forall x\exists y(R(f(x,y),x)\iff R(y,x))$.

When interpreting the language in a certain structure $M$ we use $R^M$ to denote the relation and $f^M$ to denote the function.

This is just an example. Suppose your language has $\cup$ and $\cap$ for functions. If you have a lattice $L$ and you want to say that this is the lattice in which you interpret your functions in you can write $\cap^L$ and $\cup^L$.

If you want to write a general statement which holds for a lattice with certain properties, you can write a sentence $\varphi$. If $L$ is a lattice in which the statement is true, then you can write $L\models\varphi$, or "$\varphi$ holds in $L$", that is to say that taking your world to be $L$ with the functions $\cap^L$ and $\cup^L$ the sentence is true.

Suppose you want to write a theorem for lattices with a certain property then you can say: "If $L$ is a lattice with such and such properties, then $\varphi$ holds in $L$".

I suppose that this is what you ultimately want to do.

1

I assume you're identifying the elements of different lattices (with incompatible operations), and/or have multiple lattices with overlapping carrier sets?

Because if not, I don't see what the problem is — if it's clear which lattice each element belongs to, then it's clear which lattice operations apply to them, even if you use the same symbols for all lattices. After all, algebraists love to reuse the symbols $+$ and $\cdot$ for completely different operations in all sorts of algebraic structures all the time, even when working with several of them at the same time.

If you do need to disambiguate between several lattice operations that could apply to the same elements (or to elements denoted with the same symbols) where the appropriate operation is not clear from context, may I second yatima2975's suggestion to use $\wedge$, $\cap$, $\sqcap$ and so on. Or just stick to your $\cap^L$ notation if that works better for you; you can always define shorthand names for your lattices if their "full" names are too unwieldy to use as superscripts.

  • 0
    I have overlapping lattices and so I need to disambiguate between several lattice operations that could apply to the same elements.2011-07-08
1

I am not sure this is quite what you were asking for but the fact that you noted theorem provers suggested you might find it interesting.

In Coq this notion of a "canonical" use of a symbol or name can be solved by type classes, something which has been done in the math-classes project.

Basically one declares a type class for a name, bind a notation to this name and make any structure using the name/notation depend on an instance of type class (rather than "directly" on the underlying object implementing it).

For more information on this approach you might want to check out this paper on the math-classes project.

Note though that their use of type classes goes a lot deeper than just notational convenience (probably just the first couple of pages are relevant to the current question).