Anhinga anhinga playground

I'll be placing the references to systems equipped with non-commutative conjunctions in comments to this post; mostly, this will be about generalized equalities valued in quantales.

The context here is that there is a duality between metric and logical viewpoints:

http://anhinga-anhinga.livejournal.com/70309.html

This duality comes from the fact that distance can be thought about as a degree of inequality. Whether all we have here is two notions equivalent up to a dual viewpoint, or whether there are deeper dualities lurking underneath remains open.

When people consider sets equipped with equalities valued in the algebra of open sets of a topology ("Omega-sets"), the natural metric counterpart of that is the notion of partial ultrametric valued in the algebra of closed sets of the same topology. The independently made generalizations to fuzzy equalities valued in commutative quantales and to partial metrics valued in commutative quantales also coincide up to dual viewpoint/dual notation.

There is plenty of interesting work related to fuzzy equalities valued in non-commutative quantales, the references I'll be collecting here might be helpful in doing something interesting with that on the metric side.

http://www.math.tulane.edu/~mfps/mfps26/Titles_and_Abstracts.html

В Оттаву ехать, всё таки, облом, но есть интересные доклады, особенно Эскардо..

"I'll begin by developing and applying the topological view of computation to perform seemingly impossible practical and theoretical tasks, based on some of my papers, including "Infinite sets that admit fast exhaustive search" and "Exhaustible sets in higher-type computation". For example, (1) sets that admit exhaustive search in finite time are topologically compact, [...]"

Надо будет понять, как это работает:

http://www.cs.bham.ac.uk/~mhe/

Prague, Brno, attending SumTopo 2009:

http://www.umat.feec.vutbr.cz/~kovar/webs/sumtopo/
http://atlas-conferences.com/cgi-bin/abstract/caxs-01

Limited internet connectivity during this period, but I'll try to check the comments to this post.

Let's look at the bijection mentioned in the previous post more closely. A model is "a map from the syntactic theory to a semantic space". In particular, given a Lindenbaum algebra L(T) we can build a "generic model" of T called M_T in L(T) (by mapping the propositional variables to their classes of equivalences in L(T) ).

Now, for a homomorphism f : L(T) → A, the corresponding model of the theory T in A is a map f o M_T (mapping the propositional variables to the elements of A).

Now, if we look at the post of June 9, we'll see a duality between generalized points and models. "Generic point" and "generic model" correspond to each other, and global points 1 → X correspond to standard models in the 2-valued Boolean algebra 2 = {false, true}, that is to the homomorphisms L(T) → 2.

One of the main ideas in the Vickers' text is that one can think about all kinds of spaces as spaces of models (one takes a space and starts thinking about its points as models of a logical theory of an appropriate type, usually more complex than classical propositional logic), and that in a large variety of logical situations one can take all models and form a space from them.

I've completed the first reading of Steve Vickers' rather brilliant text, "Locales and toposes as spaces", from here

http://www.cs.bham.ac.uk/~sjv/

The problem with all these categorical games is that one can understand every neat trick separately, but there are just too many of them, and it's difficult to hold the resulting picture together. So I think I'll try to write them down, one trick at a time, and this might help me.

Trick of the day: points as arrows. If a category has a terminal object 1, then (global) points of object X are (defined as) arrows 1 → X. However, in many cases there are not enough global points, so for any object A people define "points of X at stage A" as arrows A → X. In particular, the "generic point" of X is simply the identity arrow, id : X → X.

Продолжение http://anhinga-drafts.livejournal.com/4076.html (внутренний диалог):

- А что ещё "не случилось" выучить?
- А.. вот.. мо-монады..
- "Згя, батенька!". Например, if one takes a partial order and interprets it as a category, the monads are exactly the closure operations, and given a monad (a closure operation), the Eilenberg-Moore algebras of this monad are exactly the fixed points of this closure operation..
- Oops.. м-да.. знать бы это лет двадцать назад.. ну, хотя бы, десять..

Consider a set of all subsets of some set X, P(X), partially ordered by inclusion, ⊆. Consider a function "conjunction with U" from P(X) to P(X), mapping each set V to U ∩ V. The upper adjoint of this function will be a function mapping each set W to the largest set V, such that U ∩ V ⊆ W. This largest set V is (X \ U) ∪ W, which is why the upper adjoint is called "the implication from U".

A one element set X yields a familiar Boolean implication, if its subset X encodes true, and empty subset, ∅, encodes false, yielding partial order false ≤ true.

As another example, consider the set R⁺ of non-negative reals with added +∞, but with the order being the reverse of the usual: +∞ ≤' x ≤' 0. Consider a function "addition to x" mapping R⁺ to R⁺ as follows: y maps to x + y. The upper adjoint of this function will be a function mapping each z to the largest (in our reversed order, the largest is closest to zero) number y, such that x + y ≤' z.

This "largest" (closest to 0) number is z - x, when z ≤' x, and 0 otherwise. We can write this operation as mapping z to z -' x. When people want to view all this logically, they, sometimes, still call this operation "an implication from x", thinking about + as a generalized conjunction.

A remark on (monotone) Galois connections (соответствия Галуа).

Consider two partially ordered sets, (A, ≤_A), and (B, ≤_B), and two monotone functions, F : A → B, G : B → A.

F and G form a Galois connection, if for all a in A, b in B, F(a) ≤_B b ⇔ a ≤_A G(b).

In this situation, F is called the lower adjoint of G and G is called the upper adjoint of F.

Consider a Galois connection (F,G) and true statements G(b) ≤_A G(b), F(a) ≤_B F(a). Then we obtain: for all b∈B, F(G(b)) ≤_B b, and for all a∈A, a ≤_A G(F(a)).

one of these:
http://www.slimy.com/~steuard/tutorials/