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?

  • 4
    I don't understand what you're asking. What is $L$? What is $\cap^L$? What kind of lattices are you talking about?2011-07-07
  • 1
    @Qiaochu Yuan♦: $L$ is a symbol denoting some lattice (for example, the lattice of filters on a set), $\cap^L$ is meet operation on this lattice. I am talking about all kinds of lattices.2011-07-07
  • 0
    So your language has $\cap$ function, and $\cap^L$ is the interpretation in the lattice $L$? Just write it without $L$, and make a claim "If $L$ is a model for the theory 'there are infinite elements in the universe' then $L$ models $\cap^L$ is this and that", or something like that.2011-07-07
  • 0
    @Asaf Karagila: It seems you haven't understood me. I have several lattices: $L$, $M$, $N$. I wish to write $\cap^X$ without $X$ where $X$ ranges over $L$, $M$, $N$. Or what do you mean?2011-07-07
  • 2
    Can't you vary the symbols a bit? With three lattices, $\cap$, $\wedge$ and $\sqcap$ should be okay. Beyond that, there's $\Cap$, $\curlywedge$... [Symbols.pdf](http://ftp.snt.utwente.nl/pub/software/tex/info/symbols/comprehensive/symbols-a4.pdf) can help out here! If that's too noisy, why not say 'let $\cap = \cap^{L \times M}$'? AFAIK there's no fixed meta-operator set for doing stuff like that, but why not define your own? Final suggestion: [TeX SE](http://tex.stackexchange.com) :)2011-07-07
  • 1
    Perhaps its worth mentioning that join and meet in lattices are usually denoted by $\vee$ and $\wedge$. However, I am not sure what to do with your problem - I think that in moth texts this does not happen, since it is clear from the context, which lattice you take; see e.g the defininion of lattice homomorphism in this book http://books.google.com/books?id=6XJX5-zCoIQC&pg=PA30&dq=lattice+theory+foundations&hl=en&ei=2gcWTpzjFYT1-gbmqeki&sa=X&oi=book_result&ct=result&resnum=1&ved=0CCgQ6AEwAA Perhaps if you can think of some theorem that relates more than 2 lattices and find it in some book.2011-07-07
  • 0
    @Martin Sleziak: "clear from the context" is informal. I want to be close to a formal notion.2011-07-07
  • 0
    @porton: Mizar is nearly a programming language, and a pretty functional one at that, as all proof systems are. If you look at Haskell, the idiom 'let = in ' is *very* well established. Mathematicians do this as well: "In this chapter, $G$ is a finite solvable group...". If you delimit the scope of your local symbol definitions well, no one will be confused.2011-07-07
  • 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).