I’m looking forward to spending time today with @ohad@mathstodon.xyz, @modaltype@types.pl and other folks at the LFCS at Edinburgh, and getting to talk about some weird substructural modal logic.
Remote
Greg Restall
@consequently@hcommons.social
hometown 4.5.18+hometown-1.2.1Philosopher and logician, from Australia, now based at the University of St Andrews in Scotland.
I like thinking about—and helping other people think about—logic and philosophy and the many different ways they can inform and enhance each other.
I suppose I’m known for work on substructural logics, logical pluralism, and (more recently) what philosophers should know about proof theory, and proof theorists should know about philosophy.
0 Followers
0 Following
17 Posts
Joined November 07, 2022
Website:
Location:
Scotland, mostly, sometimes Australia, sometimes elsewhere
Pronouns:
he/him
My *next* talk in this spring/summer of research combines some longstanding interests of mine (Graham Priest’s Logic of Paradox) and more recent interests (natural deduction and the sequent calculus). I bet you didn’t think that you could creatively apply Gentzen’s thoroughly standard rules of natural deduction to give you a sound and complete calculus for Priest’s LP, but it turns out that you can.
Oh, look! In a few weeks time I’m going to be over in Edinburgh, giving a talk the LFCS. https://informatics.ed.ac.uk/lfcs/lfcs-seminar-tuesday-5th-may-greg-restall
If you’re in town on May 5 and like crazy proof theory, this could be fun. I’ll be talking about what happens when you take a hypersequent calculus for the modal logic S5, and *thoroughly* linearise it, removing all traces of contraction and weakening. The result is stranger than you might think. (Well, it was stranger than I first thought, anyway.) Along the journey we experience strange algebras, cut elimination and decidability arguments, and weird local/global perspective shifts. I learned a lot when thinking about this stuff, so hopefully the audience gets something out of it, too.
We’re at that time of the semester in Advanced Logic, where we’re checking our understanding of the key concepts we’ll rely on in our final ascent to the heights of the incompleteness theorems.
This Easter season, my church has held an art exhibition on the theme of betrayal, and a short set of reflective services on Maundy Thursday, Good Friday and Holy Saturday.
I was invited to give a short reflection at the Saturday service, and since I have a website to archive my presentations, I’ve uploaded the text of the reflection: https://consequently.org/presentation/2026/holy-saturday-reflection/
It’s neat to see that an old (fiddly, complicated) decidability argument I wrote up in the 1990s is getting some attention. Here, Raj Goré and Anthony Peigné formalise (and generalise) my decidability argument for display formulations of some substructural logics. This is interesting work, worth looking into.
https://link.springer.com/article/10.1007/s11225-026-10239-8
Replying to
@rzeta0@mathstodon.xyz Why should that explanation apply in the case of All? "All" and "Some" mean different things and have a different logic.
They are connected in that if All Fs are Gs, then it's *not* the case that Some Fs are not Gs. And conversely, if it's not the case that some Fs are not Gs, then All Fs are Gs.
If you follow that, you see that if there are no Fs, since it can't be the case that some Fs are not Gs (since there are no Fs at all), then indeed all Fs (vacuously) are Gs.
Replying to
@ohad@mathstodon.xyz @modaltype@types.pl Thanks so much for hosting me, and for the excellent and thought provoking conversations. I look forward to future cooperation.
Replying to
@RanaldClouston I have a draft, but it’s not yet for public circulation. (I’ll post it after I’ve got some more feedback.)
In the meantime, check your email.
I’m glad to be back in Glasgow today, this time to give a presentation at the Philosophy Department Senior Seminar. (Seeing the early signs of spring on the train journey from Dundee to Glasgow is an added bonus.)
https://consequently.org/presentation/2026/must-do-mdb-better-glasgow/
Replying to
The video of last Thursday’s debate on whether mathematics is invented or discovered is now available for viewing: https://www.youtube.com/watch?v=gdk4EIGMTFI
This House Believes That Maths is FAKE
Replying to
@rntz@recurse.social Yes, this presentation is very accessible! As a friend of relevant logic/types, it’s really nice to see these considerations emerge naturally in this context.
Replying to
@mevenlennonbertrand This is a really neat paper! I especially appreciated the explanation of the difference between the two different kinds of normal forms in STLC with sums. (And of course, the connections between bidirectional typing and interpolation is natural when you see it.)
Replying to
@dwarfobserver There should be a recording https://hcommons.social/@consequently/116046676806077869
I don't think it will be live streamed.