Kinds of Categorical Fuzzy Sets

In the logic seminar in Stanford sometimes people are asked to present papers. That's how I ended up reading Takeuti and Titani on fuzzy sets, which turned to be very interesting.

Now I'm reading Gottwald on "Universes of Fuzzy Sets and Axiomatizations of Fuzzy Set Theory. Part II: Category Theoretic Approaches" and this is very interesting too, for the same reason.

I have known since around  1990 that I can construct a "fuzzy" version of dialectica categories.  I know that this construction gives us a symmetric monoidal closed category with products and coproducts, with a (admittedly complicated) linear exponential comonad, hence is a model of Linear Logic. I know that there are other fuzzy sets that are also models of Linear Logic. Presumably I can relate these models via functors.

 I have not managed, so far,   to discover what makes fuzzy logic such a "crowd-puller", such a strong favorite. so I have no idea if this attractiveness will hold for the linear logic models. Or not.

Reading about Univalent Foundations

Voevodsky’s proposal to the NSF and IAS(2010) consists of 13 pages. The slides from his talk in Goteborg (Sept 2011) are easier to understand. Both can be found  in the univalent foundations page.

There is also the page on Homotopy Type Theory tout court, with more information on other researchers' views. 

Homotopy Type Theory refers to a new interpretation of Martin-Löf’s system of intensional, constructive type theory into abstract homotopy theory.  Propositional equality is interpreted as homotopy and type isomorphism as homotopy equivalence. Logical constructions in type theory then correspond to homotopy-invariant constructions on spaces, while theorems and even proofs in the logical system inherit a homotopical meaning. Slides from Thierry Coquand following this kind of explanation in Oberwolfach are  linked from here.

The original work that is the basis of this stuff is the groupoid model of Martin-Loeuf's CTT by Thomas Streicher and Martin Hofmann, here.

The broad motivation behind univalent foundations is a desire to have a system in which mathematics can be formalised in a manner which is as natural as possible. Whilst it is possible to encode all of mathematics into Zermelo-Fraenkel set theory, the manner in which this is done is frequently ugly; worse, when one does so, there remain many statements of ZF which are mathematically meaningless. This problem becomes particularly pressing in attempting a computer formalisation of mathematics; in the standard foundations, to write down in full even the most basic definitions—of isomorphism between sets, or of group structure on a set—requires many pages of symbols.

Univalent foundations seeks to improve on this situation by providing a system, based on Martin-Loef’s dependent type theory, whose syntax is tightly wedded to the intended semantical interpretation in the world of everyday mathematics. In particular, it allows the direct formalisation
of the world of homotopy types; indeed, these are the basic entities dealt with.

Constructing a model of the univalent foundations in the category of simplicial sets Voevodsky shows the consistency of these foundations relative to the usual ones. But this is just a first sanity check, if the new foundations are to be used, what do we need to know about them?

Some highlights of the Voevodsky proposal (first pages only).

1. We're close to "a new era which will be characterized by the widespread use of automated tools for proof construction and verification". yeah.
2. V came up with "a new semantics for dependent type theories - the class of formal systems which are widely used in the theory of programming languages"    Cool about the new semantics. I wish the bit about 'widely used' was true.
3.  "univalent semantics" interprets types as homotopy types. "the key property of the univalent interpretation is that it satisfies the univalence axiom a new axiom which makes it possible to automatically transport constructions and proofs between types which are connected by appropriately defined weak equivalences."    ok, need definitions...
4.  The key features of  "univalent foundations":

•  axiomatization of n-categorical structure
•  language is dependent type theory
•  based on homotopy types, not sets
•  both constructive and non-constructive maths

Univalent Foundations? Go Voevodsky!

 I should be an awful lot better at explaining hard stuff than I am.  This is because before starting mathematics I had one year of journalism and half a year of law in college. Long story, don't ask.(oddly enough, this hasn't helped me much.)

But since I am not good at explanations and I would like to improve, I've decided to write down (over)simplified versions of ideas to see if "practice makes perfect". I've decided to start with Vladimir Voevodsky's programme on Univalent Foundations for Mathematics.

There is a couple of reasons for that. First it's one of the more interest-generating new ideas in Category Theory. Some of it it's just because Voevodsky is a Fields medallist and all that. Some is because category theorists have a "chip on their shoulder" as far as other branches of mathematics are concerned. Despite claims in Wikipedia (of all places) that  abstract nonsense is a term of endearment, true category theorists know that it's not. It's an insult where more established branches of mathematics want to say that what we do is just dress up old concepts in new language. But thirdly and far more importantly the reason for trying to explain (to myself) what Univalent Foundations is about is that fact that this is the first serious attempt to extract new mathematics from the Curry-Howard isomorphism.

Why does this matter, do you ask? Well, the Curry-Howard iso is something that I've been trying to explain (to myself and others) for the last twenty years and I still haven't got a good way of doing it. So I wanted to use this non-serious medium (I cannot be corrupting the youth or damaging anyone else's reputation in a blog post) to try out a few off the wall ideas.

One of the things that makes explaining other people's work hard is that your own work and ideas keep trying to introduce themselves into the explanation. One has to fight to keep them off. The case of univalent foundations is slightly easier for me, as my own work is very marginally related to them. 

More on why Infinite Possibilities was so cool..

The Infinite Possibilities Conference (IPC) is a national conference that is designed to promote, educate, encourage and support minority women interested in mathematics and statistics.

The conference is important because African-American, Hispanic/Latina, and American Indian women have been historically underrepresented in mathematics. In 2002, less than 1% of the doctoral degrees in the mathematical sciences were awarded to American women from underrepresented minority groups. Even professionals who have succeeded in completing advanced degree programs in science and engineering fields can face inequities within their professional lives with respect to advancement and salaries. 

 In 2012 IPC was called "Building Diversity in Science and Mathematics", it happened 30-31st March at the University of Maryland, Baltimore County, Baltimore, MD and I had the honor of being one of the two keynote speakers. Many of the mathematicians I met there seemed to be working with mathematical Biology,  I was the only speaker talking from a Computer Science,  programming languages perspective.

My talk was entitled ``Edwardian Proofs for Futuristic Programs" and besides the required description of my career path so far,  talked about the birth of Mathematical Logic in the early years on the 20th century and how Proof Theory, one of the main strands of Mathematical Logic got a big impulse via the advent of Computing for all, through the (still today!) poorly recognized Curry-Howard Isomorphism and its more mathematical incarnations. 

This is a difficult talk to give, even for people interested in Computer Science, let alone for a generic mathematical audience. So I reckon I need to keep working on making it more accessible. It's a tall order, as Category Theory seems to scare people off, even mathematicians. The slides are available here, if you want to have a look.

Paraty 2012

I've been invited to give a talk at
Proof Theory: Linear Logic, Ludics and Geometry of Interaction. 

yay!!!

The link is here, but I don't think there's much information there, yet.

Intuitionistic Modal Logic and Applications 2011 Nancy, France

Natasha Alechina and I organized this meeting on

Intuitionistic Modal Logics and Applications Workshop (IMLA'11)

as part of the 14th Congress of Logic, Methdology and Philosophy of Science in Nancy, France, 25 July 2011.

The webpage is in the Agents Lab in the University of Nottingham and the call for papers for the publication after the meeting is here.

 

Party at NASSLLI?