Is Category Theory Constructive?

When it rains in Rio, it rains...

Pretty picture of lightening in Rio, from the much abused Niteroi...

Unrelated to the rain, recently I have been sending friends the following article of Colin McLarty

Two Constructivist Aspects of CategoryTheory

after an original suggestion of Wes Phoa. Very interesting and very relevant, as I need to write a historical account of  Categorical Logic and don't know where to start.
Later...

(Belated) Happy New Year!

We had a great time in Berlin, where the fireworks were spectacular. Very different from the ones in Rio in the beautiful picture, from Guido in Facebook.

In Rio they're big business organized by the City or the big hotels, who knows... while in Berlin, we saw families and groups of retirees putting out an incredible show that lasted more than 45 min with extremely impressive effects. But anyway the reason for the post is to add somewhere our new papers on OpenWordNet-PT for the Global WordNet Conference. One is progress report  and the other, the work with Livy Real on the integration of the nominalizations/deverbals into the OpenWN-PT.

Variable Set Theory?

Mike Barr posted in the cats mailing list the following:
Around 1986, Colin McLarty, Charles Wells, and I noticed that Scientific American had recently published a few articles on subjects mathematical
and decided to try to write one on variable set theory, AKA topos theory.
Unfortunately, that particular window at Sci Am quickly closed.  Our article was turned down and we forgot about it.  More recently, I decided it might be interesting, or at least amusing to throw it open to the
categorical community.  The result can be found at
ftp://ftp.math.mcgill.ca/barr/pdffiles/vst.pdf

(the picture is apparently Grothendieck lifting Michael Atiyah, from facebook, so who knows if it's real...)


Further news: Since the ftp site in Montreal is having some issues at the moment, Mike Barr was kind enough to send us a copy of the paper, which I'm posting here. Thanks Mike!

Set Theory for the Masses

So I've posted something about the two currents in Set Theory trying to add more axioms to solve the Continuum Hypothesis and the guys had more than a hundred comments on the post, so they are even starting to write a new paper on the subject, yay!

In some ways this is all I have always advocated for: maths needs to be done collectively, social networks can have an effective role in creating new knowledge by putting people in contact with others, etc..

But the Facebook post is not ideal: you cannot write maths properly, you cannot comment where you want, and let's face it, I cannot cope with the speed that they're producing ideas/thesis/hypotheses and demolitions. Maybe this is because I'm not a set-theorist, maybe it's because my full time job is not as a mathematician, maybe is just because I'm getting old. Who knows?
Anyways in an attempt to parse their conversation and get my own ideas straightened I've created another blog http://settheory4themasses.blogspot.com/2013/12/all-you-didnt-want-to-know-about-set.html

Long Mathematical Proofs?...

There is a Wikipedia page for them...

List of long proofs

Wish someone would organize a sensible collection of of Large Theories Common Sense problems, a bit like the TPTP collection. Also need to check out the Intuitionistic Logic benchmarks, the ILTP Library.

8th Workshop on Logical and Semantic Frameworks, with Applications (LSFA 2013)

The Workshop on Logical and Semantic Frameworks is a series of conferences in Brazil that I like to support.

As I read in their 'about us' page:

"LSFA is a series of Meetings on Logical and Semantic Frameworks with Applications. Logical and semantic frameworks are formal languages used to represent logics, languages and systems. These frameworks provide mathematical foundations for formal specification of systems and programming languages, supporting tool development and reasoning. The objective of this series is to put together theoreticians and practitioners to promote new techniques and results, from the theoretical side, and feedback on the implementation and use of such techniques and results, from the practical side."

It could've been be a bit less underspecified, methinks.

I have never been invited speaker or even invited for their programme committee, which is a surprise, as it is exactly my kind of work.
and many of the organizers are my long-standing friends...

But still I think the idea is a good one, so once again I "paid to work", instead of being paid to do it.
hmm, this is not strictly true, as I guess this is what the Brazilian CAPES funding agency  gave me a "Ciencia Sem Fronteiras" award for.
Vagaries of the Brazilian funding system and its implementation, perhaps.

I  talked about work that I did with mathematicians Charles Morgan and Samuel Gomes da Silva on Natural Numbers Objects in Dialectica Categories.

This is very interesting stuff, and the guys promised that they're writing up a more mathematical version of our content.
From my part I'd like to do the other two bits of work that we thought we would do; applications of the Dialectica construction
1. to cardinalities of the continuum and
2. to the 'laxification' of topological spaces.

Yep, I definitely need to write some of this work up and I need to put up, somewhere, all the dozens of other talks I've given that I have not written up. yet.
I guess discarded slides might end up being the notebooks of the scholars of the future.

Ilha Grande and All That....

Over the summer I went to this most wonderful place in Brazil, Ilha Grande. The meeting was called

Ilha Grande 2013: II Workshop on Logic and Semantics

and I talked about versions of constructive modal logics. The slides are here and the discussion was pretty good.