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