Wednesday, April 16, 2014

Tasks of Proof Theory?


According to Buss in the Handbook of Proof Theory, the principal tasks of Proof Theory can be summarized as follows.
  • First, to formulate systems of logic and sets of axioms which are appropriate for formalizing mathematical proofs and to characterize what results of mathematics follow from certain axioms; or, in other words, to investigate the proof-theoretic strength of particular formal systems. 
  •  Second, to study the structure of formal proofs; for instance, to find normal forms for proofs and to establish syntactic facts about proofs. This is the study of proofs as objects of independent interest. 
  • Third, to study what kind of additional information can be extracted from proofs beyond the truth of the theorem being proved. In certain cases, proofs may contain computational or constructive information. 
  • Fourth, to study how best to construct formal proofs; e.g., what kinds of proofs can be efficiently generated by computers?
    Isn't this too restrictive? 


Thursday, March 27, 2014

Lead and Crime

(I have been looking for pictures of contradictions, so here is a nice one, as it's very ordinary.)

I've read this amazing article by Kevin Drum on how

America's Real Criminal Element

was lead a while back and this outlandish hypothesis has stayed with me ever since. It is surprising, the math appears solid, Drum seems to have done his homework properly.

Since a friend of a friend was discussing crime in Facebook, I pointed him to the article. He produced two skeptical links on the same subject. One by a blogger in the Discovery Magazine site and the other some off the cuff comments by Pinker. While the skeptical arguments are sensible, I think they're besides the point. As I said to Alberto, what I find most fascinating about the article is not exactly the correlation between lead levels and crime, but the following description from Drum:

Experts often suggest that crime resembles an epidemic. But what kind? Karl Smith, a professor of public economics and government at the University of North Carolina-Chapel Hill, has a good rule of thumb for categorizing epidemics: If it spreads along lines of communication, he says, the cause is information. Think Bieber Fever. If it travels along major transportation routes, the cause is microbial. Think influenza. If it spreads out like a fan, the cause is an insect. Think malaria. But if it's everywhere, all at once—as both the rise of crime in the '60s and '70s and the fall of crime in the '90s seemed to be—the cause is a molecule.

A molecule? That sounds crazy. What molecule could be responsible for a steep and sudden decline in violent crime?


Whether the molecule of lead is really responsible or not for crime rates is much less important than whether the spread of stuff can be classified as Smith does above. It even makes feel like getting to grips with the probability theory necessary to have an educated opinion. oh well, another thing for the to-do pile. 

Thursday, March 6, 2014

Wow! the book is out!

Just got email from Christi, the nice Springer person, saying the book is OUT!!!

The link for the book

Advances in Natural Deduction

A Celebration of Dag Prawitz's Work (Series Trends in Logic, Vol. 39, Edited by Pereira, Luiz Carlos, Haeusler, Edward Hermann, de Paiva, Valeria) is functional.
The price is absurd, as usual and regrettable.
But at least our small  tribute to the great logician and philosopher Dag Prawitz is on print.

Saturday, February 22, 2014

Global WordNet Conference 2014

 So I missed the chance of going to Tartu, Estonia for the Global WordNet conference, Jan 25-29, 2014. I'm told it was great!

But I did prepare slides, as sometimes it's useful to do so, before a meeting, to make sure that  all collaborators are on the same page. My slides weren't presented, Alexandre produced his own, but they represent my understanding of the work as of Jan 2014, so I reckon I should post them. If nothing else, later on I can see how wrong I was. Slides for Nominalizations and for Progress Report on OpenWN-PT.

Sunday, February 16, 2014

Subtyping, oh subtyping, where art thou?...

I don't know how come I ended up skimming the following report Extending ML F with Higher-Order Types, as System F is nowadays very far from my worries.

 But I did. and this reminded me that I really should try to get my mind clear about what the issues are and how much progress has been made  in the subject of subtyping in System F since I did some very preliminary work on it in the context of the programming language Ponder, when working as an RA in Cambridge.

The report (Subtyping in Ponder) is available from the Computer Lab in Cambridge.

This reminds me, again, of how much I owe Michael Gordon.  And it feels good to be grateful. Btw I love Mike's favicon, will try to copy it sometime...

Saturday, February 15, 2014

Angry that...

Angry that this paper The Dialectica Categories has been available from http://www.cs.bham.ac.uk/~vdp/publications/dial87.pdf  for some 20 years and people insist on not reading it, even when they want to  discuss dialectica categories.

Why??!?? ...

is it because the book is AMS? because it's not in latex?

I know the writing is not sparkling, but come on people... if you want to talk about this stuff, you've got to read it!

Disagreement is fair; criticism is hard to deal with, but unavoidable. But ignoring it completely, this is simply NOT ON.

Tuesday, February 11, 2014

Workshops I am organizing this year

Workshop on Natural Language in Computer Science, Vienna Month of Logic, Austria, July 2014.


Workshop on Logics and Ontologies for Natural Language (LogOnto) 2014, associated to FOI2014, Rio de Janeiro, Brazil LogOnto 2014 - Workshop on Logics and Ontologies for Natural Language (LogOnto) - September 22, 2014

at least I'm getting my work to converge, I think..