World Logic Day 2024 in Tallinn

On Monday, 15 January 2024,  colleagues in Tallinn organised the Estonian event contributing to the World Logic Day 2024.  Apart from showcasing some of the exciting logic-related work that is going on in Estonia, the event featured the following three, one-hour-long invited talks:

• Jan von Plato (U. of Helsinki), "Kurt Gödel's life and work in the light of his shorthand notebooks,"
• Valentin Goranko (Stockholm U.), "Logics for strategic reasoning of socially interacting rational agents," and 
• Margus Veanes (Microsoft Research), "The impact of logic in formal methods at Microsoft."

Jan von Plato's talk reported on some of the work his research group has done in the context of the ERC Advanced Grant GODELIANA, which is devoted to the study of the thousands of pages that Kurt Gödel wrote in a German shorthand that very few people in the world can decipher today. In his talk, Jan von Plato told the audience how the study of Gödel's notes reveals how Gödel became a logician and how he developed the ideas in his seminal and celebrated published output. Moreover, apparently Gödel left behind a book-length collection of finished, unpublished new results largely on set theory and intuitionistic logic. Overall, that amounted to about 2,500 pages of publishable results in a variety of fields that Gödel told to nobody and part of which was published by others later on! 

The part of those notebooks devoted to results on the foundations of mathematics is described in the recently-published book "Kurt Gödel: Results on Foundations", edited by Maria Hämeen-Anttila and Jan von Plato.   Overall, this was fascinating account of the thus-far-below-water iceberg of Kurt Gödel's scientific work. 

In his talk, Valentin Goranko offered an overview of some work on the use of formal logics to reason about collections of agents that act "rationally" to achieve individual and/or collective goals. His talk was based on a recent survey paper of his, to which I refer interested readers for information on that line of research. Here, I will limit myself to saying that the logics for strategic reasoning presented in Goranko's talk allow one to express properties such as 

"The coalition of agents A has a joint action to ensure satisfaction of its coalitional goal G in every outcome state that may result from that joint action." 

 

"For every joint action of the coalition A that ensures satisfaction of its goal G(A), there is a joint action of the coalition B that ensures satisfaction of its goal G(B)." 

Margus Veanes delivered a "tool-oriented" talk, in the sense that he surveyed a wealth of tools for computer-aided verification and validation developed at Microsoft Research that have their roots in a variety of logic-based formal methods. His talk clearly indicated the practical impact that logic has had on software development at Microsoft and elsewhere. 

I thank our Estonian colleagues for organising such an interesting event and for streaming it online.

Disclaimer: I hope that I have not misrepresented anything in the text above and encourage you to check the speakers' work to be sure. If you attended the event and would like to share your opinions on it, please do so by posting a comment!