#proof-theory — Public Fediverse posts
Live and recent posts from across the Fediverse tagged #proof-theory, aggregated by home.social.
-
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.
-
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.
-
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
-
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
-
I’m looking forward to spending time today with @ohad, @modaltype and other folks at the LFCS at Edinburgh, and getting to talk about some weird substructural modal logic.
-
I’m looking forward to spending time today with @ohad, @modaltype and other folks at the LFCS at Edinburgh, and getting to talk about some weird substructural modal logic.
-
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.
-
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.
-
Propositions As Types Analogy • 1
• https://inquiryintoinquiry.com/2013/01/29/propositions-as-types-analogy-1/One of my favorite mathematical tricks — it almost seems too tricky to be true — is the Propositions As Types Analogy. And I see hints the 2‑part analogy can be extended to a 3‑part analogy, as follows.
Proof Hint ∶ Proof ∶ Proposition
∷
Untyped Term ∶ Typed Term ∶ Typeor
Proof Hint ∶ Untyped Term
∷
Proof ∶ Typed Term
∷
Proposition ∶ TypeSee my working notes on the Propositions As Types Analogy —
• https://oeis.org/wiki/Propositions_As_Types_Analogy#Mathematics #CategoryTheory #ProofTheory #TypeTheory
#Logic #Analogy #Isomorphism #PropositionalCalculus
#CombinatorCalculus #CombinatoryLogic #LambdaCalculus
#Peirce #LogicalGraphs #GraphTheory #RelationTheory -
Propositions As Types Analogy • 1
• https://inquiryintoinquiry.com/2013/01/29/propositions-as-types-analogy-1/One of my favorite mathematical tricks — it almost seems too tricky to be true — is the Propositions As Types Analogy. And I see hints the 2‑part analogy can be extended to a 3‑part analogy, as follows.
Proof Hint ∶ Proof ∶ Proposition
∷
Untyped Term ∶ Typed Term ∶ Typeor
Proof Hint ∶ Untyped Term
∷
Proof ∶ Typed Term
∷
Proposition ∶ TypeSee my working notes on the Propositions As Types Analogy —
• https://oeis.org/wiki/Propositions_As_Types_Analogy#Mathematics #CategoryTheory #ProofTheory #TypeTheory
#Logic #Analogy #Isomorphism #PropositionalCalculus
#CombinatorCalculus #CombinatoryLogic #LambdaCalculus
#Peirce #LogicalGraphs #GraphTheory #RelationTheory -
I was recently reading Turing's essay "Intelligent Machinery" (<https://archive.org/details/turing1948>, <https://doi.org/10.1093/oso/9780198250791.003.0016>), and Turing says something very interesting:
"Recently the theorem of Gödel and related results (Gödel, Church, Turing) have shown that if one tries to use machines for such purposes as determining the truth or falsity of mathematical theorems *and one is not willing to tolerate an occasional wrong result*, then any given machine will in some cases be unable to give an answer at all."
the emphasis is mine. I didn't know about that clause, "and one is not willing to tolerate an occasional wrong result". Can any mathematician or logician here tell me where I can find more technical details about this and what it's meant by Turing? Thank you!
-
I was recently reading Turing's essay "Intelligent Machinery" (<https://archive.org/details/turing1948>, <https://doi.org/10.1093/oso/9780198250791.003.0016>), and Turing says something very interesting:
"Recently the theorem of Gödel and related results (Gödel, Church, Turing) have shown that if one tries to use machines for such purposes as determining the truth or falsity of mathematical theorems *and one is not willing to tolerate an occasional wrong result*, then any given machine will in some cases be unable to give an answer at all."
the emphasis is mine. I didn't know about that clause, "and one is not willing to tolerate an occasional wrong result". Can any mathematician or logician here tell me where I can find more technical details about this and what it's meant by Turing? Thank you!
-
Hi everyone — I’m Carlos Tomas Grahm, an independent mathematician with a background in continuum mechanics and mathematical logic.
I started in modeling under an NSF-funded Texas A&M grant, developing what’s still the most accurate carotid-artery model in the literature.
These days I’m exploring how the structure of definitions shapes proofs — from ordered vs. non-ordered reasoning to broader questions in complexity theory.
I’m here to share occasional notes (and probably too many thoughts) on proof structure, modeling, and the weirdly human process of finding rigor.
Looking forward to meeting others who love the math side of things — whether it’s theory, teaching, or applied modeling.
#Mathematics #Logic #Modeling #Complexity #ProofTheory #Mathstodon
-
Hi everyone — I’m Carlos Tomas Grahm, an independent mathematician with a background in continuum mechanics and mathematical logic.
I started in modeling under an NSF-funded Texas A&M grant, developing what’s still the most accurate carotid-artery model in the literature.
These days I’m exploring how the structure of definitions shapes proofs — from ordered vs. non-ordered reasoning to broader questions in complexity theory.
I’m here to share occasional notes (and probably too many thoughts) on proof structure, modeling, and the weirdly human process of finding rigor.
Looking forward to meeting others who love the math side of things — whether it’s theory, teaching, or applied modeling.
#Mathematics #Logic #Modeling #Complexity #ProofTheory #Mathstodon
-
Tomorrow, I get to give the last of my three talks on inferentialism. It’s time to buckle up your λs, and join in the search for some unicorns…
-
My very first package on CRAN! <https://cran.r-project.org/package=Pinference>
I hope it may be of use especially to teachers of the basics of probability and of symbolic logic and proof theory.Uncountable thanks to all R people here who kindly helped with all my problems along the way. 🙏
-
My very first package on CRAN! <https://cran.r-project.org/package=Pinference>
I hope it may be of use especially to teachers of the basics of probability and of symbolic logic and proof theory.Uncountable thanks to all R people here who kindly helped with all my problems along the way. 🙏
-
Coming up this afternoon, I’m giving the talk “Inferentialism for Everyone” for the local Arché Metaphysics and Logic crew here in St Andrews.
This talk attempts to distill material I’ve been thinking about for the last decade or so down to a concentrated but accessible form. I look forward to discovering how successful the distillation efforts are…
-
I've followed these odd reductions back to the original source, 'Ideas and Results in Proof Theory' by Prawitz (1971); see attached image. These rules are introduced alongside the more usual ones, but not really discussed later as far as I can tell, except implicitly in a section when he notes that not everyone would accept rules beyond beta reduction as capturing the notion of 'the same proof'. He asserts uniqueness of normalisation, which these rules clearly break. Despite this being a quite heavily cited paper (~1000 cites), no one seems to have explicitly noted there is anything odd here until a paper by Dyckhoff in 2014, as best as I can tell! #logic #proofTheory
-
I've followed these odd reductions back to the original source, 'Ideas and Results in Proof Theory' by Prawitz (1971); see attached image. These rules are introduced alongside the more usual ones, but not really discussed later as far as I can tell, except implicitly in a section when he notes that not everyone would accept rules beyond beta reduction as capturing the notion of 'the same proof'. He asserts uniqueness of normalisation, which these rules clearly break. Despite this being a quite heavily cited paper (~1000 cites), no one seems to have explicitly noted there is anything odd here until a paper by Dyckhoff in 2014, as best as I can tell! #logic #proofTheory
-
In this week's #blog I write briefly about a 2001 paper on designing lambda calculi for intuitionistic modal logic. https://blogs.fediscience.org/the-updated-scholar/2025/08/15/discussing-extended-curry-howard-correspondence-for-a-basic-constructive-modal-logic/ #logic #modalLogic #proofTheory #typeTheory
-
In this week's #blog I write briefly about a 2001 paper on designing lambda calculi for intuitionistic modal logic. https://blogs.fediscience.org/the-updated-scholar/2025/08/15/discussing-extended-curry-howard-correspondence-for-a-basic-constructive-modal-logic/ #logic #modalLogic #proofTheory #typeTheory
-
I am going to make an attempt to #blog a bit again, reading and writing about papers and books, old and new, that are cited by recent work in my area. This week, we look at a #proofTheory #logic textbook. https://blogs.fediscience.org/the-updated-scholar/2025/08/08/discussing-basic-proof-theory/
-
I am going to make an attempt to #blog a bit again, reading and writing about papers and books, old and new, that are cited by recent work in my area. This week, we look at a #proofTheory #logic textbook. https://blogs.fediscience.org/the-updated-scholar/2025/08/08/discussing-basic-proof-theory/
-
#proofTheory / simple #typeTheory question: I'm reading Troelstra & Schwichtenberg's 'Basic Proof Theory' and they discuss 'simplification contractions' on natural deductions, which cover cases where an auxiliary premise of an elimination rule does not use the local variable it is given.
e.g.if we have an or-elimination 'case t:A ∨ B of x₁.t₁; x₂.t₂', but xᵢ is not free in tᵢ for either i = 1 or 2, then we may reduce to tᵢ.
Is this a style of reduction that is ever seen in simple type theory or implemented in languages? What are the implications of including it? I'm not used to seeing anything (in the propositional fragment) except beta, eta, and commuting conversions.
-
#proofTheory / simple #typeTheory question: I'm reading Troelstra & Schwichtenberg's 'Basic Proof Theory' and they discuss 'simplification contractions' on natural deductions, which cover cases where an auxiliary premise of an elimination rule does not use the local variable it is given.
e.g.if we have an or-elimination 'case t:A ∨ B of x₁.t₁; x₂.t₂', but xᵢ is not free in tᵢ for either i = 1 or 2, then we may reduce to tᵢ.
Is this a style of reduction that is ever seen in simple type theory or implemented in languages? What are the implications of including it? I'm not used to seeing anything (in the propositional fragment) except beta, eta, and commuting conversions.
-
Proof theory and logic programming: Computation as proof search. ~ Dale Miller. https://www.lix.polytechnique.fr/Labo/Dale.Miller/ptlp/ptlp-2025-06-27.pdf #Logic #ProofTheory #LogicProgramming
-
Proof theory and logic programming: Computation as proof search. ~ Dale Miller. https://www.lix.polytechnique.fr/Labo/Dale.Miller/ptlp/ptlp-2025-06-27.pdf #Logic #ProofTheory #LogicProgramming
-
New: pmGenerator, since version 1.2.2, can
- compress Hilbert-style proofs via exhaustive search on user-provided proof data
- convert Fitch-style natural deduction proofs into any sufficiently explored Hilbert system#Logic #HilbertSystems #NaturalDeduction #FormalMethods #ProofTheory #Mathematics
-
I’m in Amsterdam, about to give a talk about proof theory for modal predicate logic at the ILLC, the home base of the modal industrial complex. I have no idea how this is going to go over, but it should be a fun ride, however it turns out.
-
I’m in Amsterdam, about to give a talk about proof theory for modal predicate logic at the ILLC, the home base of the modal industrial complex. I have no idea how this is going to go over, but it should be a fun ride, however it turns out.
-
This Thursday, I’ll be down in London giving a talk about defining rules for quantifiers and identity, at the PPLV group in Computer Science at UCL. If you happen to be in the area, and are interested in proof theory, semantics and hints of metaphysics, I’d love to see you there.
-
This Thursday, I’ll be down in London giving a talk about defining rules for quantifiers and identity, at the PPLV group in Computer Science at UCL. If you happen to be in the area, and are interested in proof theory, semantics and hints of metaphysics, I’d love to see you there.
-
I'm glad to have space to get to writing, and the first writing project of my sabbatical has reached first-draft stage. If you're interested in modal logic, proof theory, and the metaphysics of contingent existence, have I got the paper for you!
https://consequently.org/writing/mlce-ge2/
I've got to say, I think the hypersequent calculus in this paper is pretty neat.
-
I'm glad to have space to get to writing, and the first writing project of my sabbatical has reached first-draft stage. If you're interested in modal logic, proof theory, and the metaphysics of contingent existence, have I got the paper for you!
https://consequently.org/writing/mlce-ge2/
I've got to say, I think the hypersequent calculus in this paper is pretty neat.
-
It’s a cloudy and cold Tuesday, and I’m inside writing about refinement.
At least I *think* I understand what I’m doing a bit better than Mark S and his team of macrodata refiners do.
(That’s an inappropriate #Severance, #prooftheory #ModalLogic and #ClickyKeyboard crossover post. I’m sorry about that.)
-
(The proof with alternatives does have a bit of a round-about feel, with having to store the conclusion as an alternative twice to then retrieve both in one go. This gives you the effect of contraction in conclusion position, which is required because the natural deduction introduction rule for disjunction is additive, while the elimination rule is multiplicative. In this format, your only device for contraction in conclusion position is to hoist the conclusion into the assumption context (as an alternative, under the slash) and to then retrieve two or more copies of that assumption back as a conclusion.)
-
This morning, one of my hardworking intermediate logic students (prepping for her exam next week), came to me with a query about how to prove the constructively invalid quantifier negation inference (from ∀x(A(x)∨B(x)) to ∀xA(x)∨∃xB(x)) in natural deduction with Double Negation Elimination.
It was natural that she would struggle with this exercise, since any proof of this (in that natural deduction framework at least), requires a quite bit of fancy footwork.
After we worked through that, I wondered whether the proof is much simpler in classical natural deduction with alternatives (basically the λμ calculus). If you help yourself to the derivable (and simpler to work with) ∨E* variant rule, it turns out that the proof shrinks from 14 steps to 10, and it seems much more direct.
-
I think my paper on Dummett, proof assistants and pluralism has shaped up rather nicely, and it will be good to see it out in the Proceedings of the Aristotelian Society in a few months’ time. You can read the preprint now.
Thanks to everyone who gave me feedback on earlier drafts, and discussed these issues along the way.
There's more to be done, but I hope to have clarified some issues around how we can think about the relationship between constructive and classical reasoning, and how philosophers might engage with what is going on in the application of dependent type theory in proof assistants, programming language design, and the formalisation and mechanisation of reasoning.
-
I think my paper on Dummett, proof assistants and pluralism has shaped up rather nicely, and it will be good to see it out in the Proceedings of the Aristotelian Society in a few months’ time. You can read the preprint now.
Thanks to everyone who gave me feedback on earlier drafts, and discussed these issues along the way.
There's more to be done, but I hope to have clarified some issues around how we can think about the relationship between constructive and classical reasoning, and how philosophers might engage with what is going on in the application of dependent type theory in proof assistants, programming language design, and the formalisation and mechanisation of reasoning.
-
Another week, another research presentation. Coming up on Saturday, I’ll be hanging out in Munich, talking about free logic and rules for quantifiers. https://consequently.org/presentation/2024/defining-quantifiers-mcmp/
-
@loopspace @tao For me, the most natural approach would be in the context of formal logic. Start with the set of all proofs for a given statement (in a specified formal system, with some axioms given, for example) and then introduce some transformations that transform a proof into an equivalent one. Changing the order of the proof steps is a possible transformation, and the morst trivial one. Then these transformations define an equivalence relation, and voilà!, you have a concept for proof equivalence.
The challenges here are of course (1) to find a definition that is meaningful in the real life of mathematicians, and (2) to prove interesting things with these concepts. One would try to define invariants, for example.
I have done nothing concrete in this direction and do not know whether anyone else has, but maybe there is something.
-
@loopspace @tao For me, the most natural approach would be in the context of formal logic. Start with the set of all proofs for a given statement (in a specified formal system, with some axioms given, for example) and then introduce some transformations that transform a proof into an equivalent one. Changing the order of the proof steps is a possible transformation, and the morst trivial one. Then these transformations define an equivalence relation, and voilà!, you have a concept for proof equivalence.
The challenges here are of course (1) to find a definition that is meaningful in the real life of mathematicians, and (2) to prove interesting things with these concepts. One would try to define invariants, for example.
I have done nothing concrete in this direction and do not know whether anyone else has, but maybe there is something.
-
Next week it’s our last Arché Metaphysics and Logic seminar for the academic year, and I’m going to have a go at addressing some of the big questions in the foundations of logic, with a contemporary twist.
https://consequently.org/presentation/2024/what-do-we-mean-arche/
-
"A major function [of deductive #logic is in] assessing exactly what is involved in asserting some set of propositions. […] By omitting some premiss without which the deduction of some conclusion is not valid, it misrepresents the premiss from which this conclusion is obtained, and hence responsibility for the conclusion. To agree to accept partial responsibility as good enough here is like agreeing to say that somebody was responsible for the dinner when he peeled potatoes and the cook did the rest. The first statement cannot be accepted as an elliptical, but allowable, way of making the second statement. And similarly suppression [of some premiss] enables us to obtain as causally responsible a partially sufficient rather than a fully sufficient causal condition."
Valerie Plumwood in Australasian Journal of Logic, 2023: https://ojs.victoria.ac.nz/ajl/issue/view/894 v @rrrichardzach#Plumwood #causality #correlations #economics #reason #ProofTheory #PhilSci #truth #science #ethics #ecofeminism #freedom
-
"A major function [of deductive #logic is in] assessing exactly what is involved in asserting some set of propositions. […] By omitting some premiss without which the deduction of some conclusion is not valid, it misrepresents the premiss from which this conclusion is obtained, and hence responsibility for the conclusion. To agree to accept partial responsibility as good enough here is like agreeing to say that somebody was responsible for the dinner when he peeled potatoes and the cook did the rest. The first statement cannot be accepted as an elliptical, but allowable, way of making the second statement. And similarly suppression [of some premiss] enables us to obtain as causally responsible a partially sufficient rather than a fully sufficient causal condition."
Valerie Plumwood in Australasian Journal of Logic, 2023: https://ojs.victoria.ac.nz/ajl/issue/view/894 v @rrrichardzach#Plumwood #causality #correlations #economics #reason #ProofTheory #PhilSci #truth #science #ethics #ecofeminism #freedom
-
The Nordic Logic Summer School is now in full swing here in Reykjavík. I’ve given my first proof theory class, and Rineke Verbrugge is introducing modal logic and social cognition.
-
My anticipation is building for next week’s Nordic Logic Summer School and my class on proof theory. (The fact that I get to visit Reykjavík is to teach is a cool bonus.)
-
I’m enjoying preparing my classes for next month‘s Nordic Logic Summer School in Reykjavik.
This will be the northernmost latitude at which I’ve eliminated cuts.
-
Catching up on my #blog writing with my second post in two days! I look at how a variation on the standard notion of sequent calculus led to new insights into structural #proofTheory for intuitionistic #logic. https://blogs.fediscience.org/the-updated-scholar/2024/04/24/discussing-nested-sequents-for-intuitionistic-logics/
-
I *think* I’m ready for my talk at our two-day proof theory workshop, starting tomorrow: https://consequently.org/presentation/2024/lambda-mu-arche/ — I have a lot to pack in to 25 minutes, so the monster-sized handout contains some of the details I’ll skim over in the talk.
-
New #blog up: on an interesting textbook on #ProofTheory and #AbstractAlgebra in #logic https://blogs.fediscience.org/the-updated-scholar/2024/02/09/discussing-proof-theory-and-algebra-in-logic/
-
Here’s a draft of a paper I’ve been writing over the last few months, on and off, in between other things, on the philosophical significance of the paradoxes. It’s to appear in the Oxford Handbook of Philosophical Logic, sometime in the next year or two.
I’ve tried to be fair to accounts of the paradoxes that use the paradoxes to motivate revisions to traditional logical principles, and those accounts that keep those logical principles fixed, and use them to constrain our theories of truth, of types, of properties, of vague predicates, etc.
-
It’s been an exhausting but enjoyable day of hearing about and talking about logic. First up, at Arché we had a wonderful wide ranging talk from Sara Uckelman (@doctorlogic) (Durham), entitled “Why the History of Logic [and Philosophy!] Should Matter to Modern Logicians [and Philosophers!].”
Then, this afternoon, in the open Q&A session after my Intermediate Logic lecture, a student asked: “Greg, can you explain why the natural deduction rules for the existential quantifier, disjunction, and possibility are so strange and clunky, when compared to the universal quantifier, conjunction and necessity? I look at the truth conditions, and the ∃/∨/◇ rules look no different than the ∀/∧/□ rules. What gives?“ I *love* it when they ask questions like that.
[Edited to tag Sara!]