Rente und Arbeit Unsere Gesellschaft wird nicht umsonst als „Leistungsgesellschaft“ bezeichnet. Historisch hebt das damit verbundene Denken die bürgerliche Gesellschaft, in der Erwerbseinkommen über die … Read more
Der argentinische Präsident Javier Milei ist für libertäre Geister eine Art Messias. Milei will den Staat weitgehend abschaffen, zumindest da, wo er ihn für überflüssig … Read more
Der sozialpolitische Wind weht in Deutschland wieder kälter. Das Werben um die knappen Beschäftigten mit attraktiven Arbeitsbedingungen wird zunehmend durch andere Stimmen abgelöst, die meinen, … Read more
As announced every account that was not already following someone on threads.net has now had a domain block added for that instance. This makes interaction … Read more
Background Meta’s Threads platform has joined the fediverse a few months ago. In the absence of an explicit federation policy, FediScience has been treating Threads … Read more
Modal logics of necessity and possibility do not always obviously admit an acceptable notion of structural proof theory. Yet such systems can be invaluable for both work inside the logic (proof search) and work about a logic (metatheory). This paper looks at a general framework for defining sequent calculi for a wide range of classical modal logics. The technology for this is labelled sequent calculi, in which Kripke’s possible worlds semantics is internalised into the syntax, with assumptions and conclusions specifically labelled by which world they hold at. The relationships between worlds are then explicitly encoded in judgements, so for example wRx means that from a world w, the world x is possible.
Ludwig Erhard wird der Spruch „Wirtschaftspolitik ist zu 50 % Psychologie“ zugeschrieben. Die übrigen 70 % sind vermutlich Rechenfehler und auch der psychologische Teil ist … Read more
Heyting-Brouwer logic (more commonly known now as bi-intuitionistic logic) has fascinated me since I first learned of it. The idea is beguilingly simple: extend intuitionistic logic with a new connective that makes it completely symmetrical. The ‘symmetry’ I am thinking of (perhaps better called ‘duality’, but not quite the same thing as De Morgan duality) is already exhibited by most of the propositional connectives: truth, which is entailed by everything, is dual to falsity, which entails everything; conjunction, which is a sort of greatest lower bound, is dual to disjunction, which is a least upper bound. But implication (and hence negation, which is definable via implication and false) has no dual in this way. What happens if we ‘fix’ this?
This paper is an influential landmark in the development of what is now usually called guarded recursion, following a trail that roughly goes from Nakano’s introduction of the approximation modality, to this paper, to a Dreyer, Ahmed, and Birkedal paper that I haven’t yet read for this blog but will probably eventually get to, to the ‘synthetic guarded domain theory’ paper that crystalised the field and opened the way for more advanced work on applications and type theory. The goal of all these papers was to solve problems in computer science by using a modality that allows one to express that data may be generated over time, and hence prevent unreasonable circularities (data now that depends on data I will only get later) and permit self-reference that would otherwise be impossible to model. In particular, this paper introduced the symbol ▷ and name later for the modality. Despite its influence, re-reading the paper now has revealed to me that it quite seriously diverges from both Nakano’s ideas and all work I am aware of that builds on those ideas, in a way that does not seem to have been clear to the authors at the time.
I’ve written before about Coq, recently renamed to Rocq, a proof assistant based on Martin-Löf’s dependent type theory. This paper, along with various sequels written in the six years since the project was first announced, aims to mechanise the syntax and semantics of Rocq, in Rocq.
Deutschlands Wirtschaft, die in den letzten Jahren von billiger Energie aus Russland, der Erschließung des chinesischen Marktes, von Lohnzurückhaltung und vom Sparen bei öffentlichen Investitionen … Read more
I’ve been meaning to get more familiar with this dissertation for a while (reading it thoroughly would take longer than the week I try to take for my blog posts), after its ideas were used in a paper I discussed last year. This thesis presents a new technique, synthetic Tait computability, for proving the ‘syntactic’ properties of canonicity and normalisation in type systems, with the previously unproven normalisation result for cubical type theory as its highlight.
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.
Man hört es immer wieder: Unser Gesundheitswesen sei teuer, aber ineffektiv. Wie ein Mantra findet sich diese Verbindung in Begründungen dafür, dass sich im deutschen … Read more
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
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
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 have been meaning to discuss an academic trend in the social sciences for quite some time: ‘academic extractivism’. The main feature of this practice … Read more
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”.
Vor ein paar Tagen hatte ich nebenan bei Scienceblogs Karl Lauterbachs Eröffnungsrede zum Kongress Armut und Gesundheit kommentiert. Unter anderem hatte er dabei auch gesagt, … Read more
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.
Im Jahr 2021 wurden dem Statistischen Bundesamt zufolge in Deutschland 474,1 Mrd. Euro. für Gesundheit ausgegeben, etwa 5.700 Euro pro Kopf. Gut die Hälfte davon, … Read more
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
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
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
Earlier this year, I have been to my first Open Science retreat ever. It was nice to meet all these open-minded new people. Especially after … Read more
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
Verwaltungsausgaben als Streitpunkt Die gesetzlichen und privaten Krankenkassen erbringen Dienstleistungen in einem Umfang von mehr als 300 Mrd. Euro jährlich, die von den Versicherten, den … Read more
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