About a year and a half ago I wrote about hypersequents, a modification of the tried and trusted sequent calculus approach to structural proof theory. In that setting, instead of working with a single sequent (a set of premises alongside a set of possible conclusions) we work with a list of sequents. In this paper, we look at another such modification, called nested sequents (sometimes, tree hypersequents) in which the conclusions can contain both formulae and further nested sequents. The aim is the same: by defining communication rules between different sequents, we can give structural proof theory to logics that do not have a reasonable proof theory via conventional sequents.
I learned modal logic from a book by Hughes and Cresswell, a pair of philosophers from my home city of Wellington, so it was interesting for me to see the very different approach taken in this week’s book, which is now the standard reference for the field ( along with the Chargrov- Zakharyaschev book of the same name). While the first sentence of Hughes and Cresswell reads “Modal logic is the logic and possibility and necessity, of ‘must be’ and ‘may be’”, the first of Blackburn et al’s three ‘slogans’ frames modal logic as a more general phenomenon, of “simple yet expressive languages for talking about relational structures”. Hence possibility and necessity, or unary modalities in general, are not privileged, with almost all results developed in terms of ‘modal similarity types’, logical operators of any given arity. Familiar box and diamond logic is but one corner of a menagerie that also includes temporal logic and propositional dynamic logic (where we have a pair of modalities for each program). The key factor that distinguishes these logics from first order logic, which after all also deals with relations on sets, is their second slogan, that modal logic “provide an internal, local perspective on relational structures”, where we can talk about the truth of propositions relative to points in the structure. This point of view includes, but is not limited to, the standard “possible worlds” view where a statement may hold at one world, but not another.
Deutschland hat in den letzten Jahren einen erheblichen Investitionsstau aufgehäuft. Schulen und Brücken, Wohnungsbau, Krankenhäuser, Bahn, Gebäudesanierung, E-Mobilität, die Digitalisierung und vieles mehr: Notwendige Investitionen… Read more: Christian Lindners investitionspolitischer Pessimismus
I choose papers for this blog by looking at the most cited papers in my Google Scholar recommendations of recent papers. This week, my algorithm has read my mind by recommending a fairly new paper that was already at the top of my list of papers to read. Its topic, as with a few papers I’ve covered over the last few weeks, is intuitionistic modal logic, which combines the logic of constructive proof with the logic of the modalities ‘necessarily’ and ‘possibly’, usually written with a box and diamond respectively.
Vermutlich reiben sich nicht wenige Leute gerade die Augen: Wie kann es sein, dass die deutsche Wirtschaft nach allgemeiner Einschätzung in einer tiefen Krise steckt,… Read more: Wirtschaftskrise und Aktienboom
The algorithm I use to choose reading for this blog, pulling the most cited papers out of my Google Scholar recommendations of new papers, sometimes pops out work close to my heart; quite a few years of my own research have been direct outshoots from this paper, following its adoption by Birkedal et al., and I have read it several times. Re-reading an oft-used paper, like re-reading a favourite book, still has the capacity to produce surprises. This time around I realised I had forgotten how inspired Nakano was by theoretical work on object oriented programming in particular (a theme returned to by one of this week’s recommended papers).
There is a mini-theme on this blog of important developments in intuitionistic modal logic, in which the modal notion of necessity (and, less often, possibility) is blended with the intuitionistic notion of constructive proofs which denies, for example, the law of the excluded middle. We’ve read through Plotkin and Stirling, Simpson, Davies and Pfenning, and, recently, Benton, Bierman and de Paiva and will now turn our attention to one of a small string of papers Gisèle Fischer Servi wrote on this subject almost fifty years ago. Incidentally, I cannot find any information online about this pioneering logician apart from a list of papers on a University of Parma website. At the time she was publishing this work it appears to have been mostly ignored, but it is regularly cited now and I would certainly be grateful to anyone who can point me to any information about her career, even if it is in Italian.
I have looked at PhD dissertations for this blog before, but never one this gargantuan; at 503 pages it weighs in at 3-4 times longer than the average thesis. The author does not quite apologise for the length, but at least acknowledges it, saying “[the] length of this thesis should by no means deter the potential reader, as it is mainly a consequence of the presence of many pictures, examples and often very detailed (albeit elementary) proofs and computations”. While I wasn’t ‘deterred’ as such, I do of course have to fit my blog reading in around my other work and life commitments and therefore have only skimmed most sections.
I first became aware of this paper from a long and fascinating blog comment thread in which mathematicians argued about the utility, or lack thereof, of homotopy type theory for homotopy theorists. Urs Schreiber, arguing for team HoTT, held up this paper an exemplar of the value of the type theoretical approach, saying “it was remarkable to see a complete homotopy theory newbie, who had the proof in HoTT, explain it to none less than Charles Rezk, who said he had tried to find it using traditional means but failed”.
I’ve written before about the Coq Proof Assistant . Since then, after years of bravely ignoring the sniggers its French name produced among English speakers, the developers have decided to remain it Rocq in honour of Rocquencourt, the French town in which much of the development took place. The good news for the authors of this week’s book, should they ever decide to produce a new edition, is that Rocq’Art is an even better name.
This is a sequel to a paper by Moggi that I discussed some time ago. That paper discussed side effects, which are, roughly speaking, anything interesting that a program does other than map inputs deterministically to outputs, such as failure to terminate with a value, taking in user input, or producing output before the computation ends. Moggi noted that these effects can often be described by a particular category theoretic structure, that of a strong monad, which allows us to distinguish between ‘values of type A’ and ‘possibly effectful computations that may produce values of type A’; the latter is usually written TA. Crucially, Moggi defined a ‘computational lambda calculus’ in which T is a type former. The intention was to define a metalanguage for denotational semantics, but in fact the calculus had most impact on the practice of functional programming, with monads becoming a crucial part of the toolkit for handling effects in languages such as Haskell.
I have written before about 2-category theory, where we have objects, arrows between objects, and arrows (sometimes called 2-cells) between those arrows. The canonical example are collections of categories, which have layers of categories; functors; and natural transformations. ∞-categories generalise this to an infinite stack of layers of n-cells. An (∞,1)-category is a special case in which every n-cell after level 1 is an equivalence. This puts us into the realm of homotopy theory, where we have paths, paths between paths, and so on ad infinitum. This paper looks at such categories which are additionally (higher) toposes.
I was pleased to see this book bubbling up through my recommendations, as I once saw a keynote talk by Hiroakira Ono at a logic conference in my former home city of Wellington and it was one of the most cogent and exciting logic talks I’ve ever enjoyed. Ono’s textbook is split into two parts, which can for the most part be read separately: one on sequent calculus and one on abstract algebra for logic.
In the world of interactive theorem provers two systems stand out for their maturity and wide adoption. One is Rocq, until recently known as Coq, about which I have written previously; Isabelle/HOL, the topic of this week’s reading, is the other. Rocq is one of a number of systems (for example, Lean) based on Martin-Löf’s dependent type theory, whereas Isabelle/HOL is one of a number of systems based on the alternative foundation of higher order logic (HOL). These are not the only two options – Mizar, which is older still, takes another route – but I think it is fair to call them the most prominent.
This short but fun little paper discusses how we can combine two different logics – classical and intuitionistic – into one. Classical logic is the logic of Boole where every proposition has a definite value of True or False and negation simply inverts the value, so that ‘p or not p’ holds for any proposition p. Intuitionistic logic can be motivated in a few different ways: first, as a logic of proof, rather than truth, where negation means proved false, so that ‘p or not p’ fails for propositions not (yet) proved true or false. Second, and most relevant to this paper, in the semantics of Kripke we regard our logic as operating over a set of ‘possible worlds’, with a relation moving from one world to another as we learn new propositions, but where propositions are never forgotten on these moves. In this setting ‘not p’ is defined to hold at a world only if p fails at the world we are currently at and all possible future worlds. Again ‘p or not p’ fails, because although p might not hold at our current world, it might hold at some future world.
Domains are certain forms of ordered sets used to address problems in the denotational semantics (mathematical interpretation) of programming languages. The area was invented by Dana Scott in a series of papers starting in 1969, building on earlier work by many others that used lattices. This book (which admittedly, I did not have time to read in full detail this week) does not examine the applications of domains, but rather is a handbook on their mathematics. Indeed, at a point where computing applications are discussed, the authors apologise for “deviat[ing] from our general philosophy [to] spend some time on examples”! This is therefore possibly not the best book to start with this topic – suggested references are included in the text – but rather should be considering a book for ‘working computer scientists’ to look up results in, or fill in gaps in their knowledge with.
Welcome to the new version of my blog The Updated Scholar, previously hosted by blogspot. This blog exists mostly for me, and perhaps also as… Read more: Welcome to The Updated Scholar!
Krisen und soziale Verantwortung „Die Frage, ob der für (…) Ballastexistenzen notwendige Aufwand nach allen Richtungen hin gerechtfertigt sei, war in den verflossenen Zeiten des… Read more: Friedrich Nietzsche als ökonomischer Ratgeber?
It was an autumn night in 2013. Most people were on holiday because of the Eid of Sacrifice. I was in Genç, a war-torn municipality… Read more: War, peace, and the autumn
Die Verteidigungsausgaben Deutschlands sind seit langem ein politisches Top-Thema, vor allem seit dem Ukrainekrieg und ganz aktuell seit dem Überfall der Hamas auf Israel. 100… Read more: Die deutschen Verteidigungsausgaben
I am a postdoctoral researcher at the College of Mexico (Colmex). I usually work on the legitimation and delegitimation of state-sponsored violence, dehumanization, racism, authoritarianism,… Read more: Hello everyone!
So, goodbye scienceblogs.de, welcome to blogs.fediscience.org! Ever since the “Konradin Mediengruppe”, the publisher behind the German blog platform scienceblogs.de, announced that it would cease operating… Read more: Welcome to the new home of “rupture de caténaire”