Add formalization of substructural logics in src by mlebar-UC · Pull Request #2825 · agda/agda-stdlib

mlebar-UC · 2025-09-04T21:56:19Z

I've added a formalization of several substructural logics in the src folder, based on chapter 2 of Greg Restall's "An Introduction to Substructural Logics". This is work I did as part of a master's research project. My hope is that the work I've done here can be a useful resource for anyone wanting to study logics in Agda. Please let me know if there any changes I can make to help this fit the Agda standard library.

jamesmckinna · 2025-09-07T15:28:30Z

Zeroth thought: this looks really nice!

First thought: we might need to scratch out heads a while about opening up/committing the Logic.* namespace to this?

Second thought: could this be refactored to prune out a lot of the DRY repetition of eg the initial parameter telescopes of (most) of the definitions?

Either, by reifying them as a record, eg RawLogic on the model of Algebra.Bundles.Raw...?
Or, by making them top-level parameters of each (sub-)module?

Third thought: everything is tied to 'Logic over Set, ie at Level zero, rather than making it Level-polymorphic. Presumably (?) it would be straightforward to generalise everything, albeit a lot of tedious editing to do so...

Fourth thought: On the model of the various README modules which document/show exemplary usage, are there good such 'example' files which you could add to this development (esp. wrt the slightly 'occult' use of language such as Struct to embed propositions as ... wff-like things; readers unfamiliar with Restall's book, or general approach, might find this hard going at first?)

Fifth, nitpicky, thought: the fat semicolon is... annoying cf. #2303

JacquesCarette · 2025-09-07T15:33:47Z

I've got a detailed review incoming. Agree with thoughts 0-4.

MatthewDaggitt · 2025-09-08T01:01:51Z

At the risk of being a dissenting opinion, is this something that might be better as a standalone library? My initial reaction is that this feels very similar to https://github.com/agda/agda-stdlib/blob/master/src/Data/Fin/Substitution.agda and its child modules which I think we agreed at some point probably shouldn't live in the standard library?

JacquesCarette · 2025-09-06T13:43:08Z

CHANGELOG/mlebar-UC.md

@@ -0,0 +1 @@
+* Added a folder "Logic" in src. This provides a formalization of several substructural logics based on chapter 2 of Greg Restall's "An Introduction to Substructural Logics". My hope is that this can provide a useful framework for anyone wanting to study a variety of logics in Agda. This was a master's research project done under Professor Stuart Kurtz, and I'm really happy with my work here - I would love to contribute to the standard library, and I am happy to make any appropriate modification to help with that.


We try not to have long lines - can you please cut these down to ~80 characters wide?

JacquesCarette · 2025-09-06T13:45:37Z

src/Logic/Connectives/And-Logic.agda

+open import Logic.Logic
+
+record And-Logic
+  {Lang : Set} {Struct : Set} (S : Lang → Struct)


It would probably make sense to bundle all these things up in a record?

Certainly it would make sense to explain (in the CHANGELOG? A README?) what the overall design is.

JacquesCarette · 2025-09-06T13:46:33Z

src/Logic/Connectives/And-Logic.agda

+  (_⨾_ : Struct → Struct → Struct)
+  (_⇒_ _∧_ : Lang → Lang → Lang) : Set where
+  field
+    is-logic : Logic S _⊢_ C⟨_⟩ _⨾_  _⇒_


Shouldn't this field be a parameter? You're building And-logic on top of implicational logic, right?

JacquesCarette · 2025-09-06T13:48:07Z

src/Logic/Connectives/And-Logic.agda

+      X ⊢ B →
+      -------------------
+      X ⊢ (A ∧ B)
+    and-elimination-1 :


I think left and right would make more sense than -1 and -2. I know you're following Restall, but he chose bad names, we don't have to follow suit!

JacquesCarette · 2025-09-06T13:48:48Z

src/Logic/Connectives/And-Logic.agda

+      X ⊢ B
+
+if-and-distrib :
+  ∀ (Lang : Set) (Struct : Set)


This repetition of arguments screams for having module _ ... encapsulating that.

JacquesCarette · 2025-09-08T01:30:54Z

src/Logic/Logics/J-Logic.agda

+open import Logic.Logics.BCK-Logic
+open import Logic.Structural-Rules.W-Logic
+
+record J-Logic


If you're going to call it J, you need to explain why!

JacquesCarette · 2025-09-08T01:31:30Z

src/Logic/Logics/L-Logic.agda

+open import Logic.Connectives.Backif-Logic
+open import Logic.Connectives.Fusion-Logic
+
+record L-Logic


Lambek instead of L, unless there is precedent?

JacquesCarette · 2025-09-08T01:32:44Z

src/Logic/Logics/Or-Comma-Logic.agda

+
+    is-comma-logic : Comma-Logic S _⊢_ C⟨_⟩ _⨾_ _/_ _⇒_
+
+    comma-product-context-l :


surely a better name can be found?

JacquesCarette · 2025-09-08T01:34:58Z

src/Logic/Structural-Rules/B'-logic.agda

+
+open import Logic.Logic
+
+record B'-Logic


Is this a standard name for this logic? reference?

JacquesCarette · 2025-09-08T01:35:39Z

src/Logic/Structural-Rules/B^c-logic.agda

+  field
+    is-logic : Logic S _⊢_ C⟨_⟩ _⨾_ _⇒_
+
+    converse-assoc :


sym-assoc ?

JacquesCarette · 2025-09-08T01:43:16Z

At the risk of being a dissenting opinion, is this something that might be better as a standalone library?

I certainly agree that the bar for introducing logics into stdlib ought to be high. But my work on MathScheme strongly hints that 'logics' are both quite algebraic and 'fit' quite well in a setting like stdlib if done well and in a certain style.

jamesmckinna · 2025-09-08T07:10:58Z

Re: @MatthewDaggitt on Data.Fin.Substitution
The full discussion is on the PR which refactored that to move the untyped lambda calculus example to README, but I didn't think our intention had been to remove it entirely...

So, to the 'dissenting' view, I agree to the extent that I wouldn't be happy to give top-level Logic. over to this, but as Logic.Substructural... sure, why not?

I'd be interested to see @JacquesCarette develop his argument from MathScheme. 'Algebra of logic' seems a very respectable kind of addition... not least given my own interests towards developing (universes for) proof-theoretic constructions such as those of Harrop and successors, towards internalising certain kinds of proof procedures around classical logic/Decidable propositions.

mlebar-UC · 2025-09-08T19:46:14Z

Thanks everyone for the detailed feedback. Jacques, I especially appreciate you taking the time to go through my code in such detail. I'll take some time to modify with these comments in mind and resubmit.

MatthewDaggitt · 2025-09-09T03:58:32Z

I certainly agree that the bar for introducing logics into stdlib ought to be high. But my work on MathScheme strongly hints that 'logics' are both quite algebraic and 'fit' quite well in a setting like stdlib if done well and in a certain style.

'Algebra of logic' seems a very respectable kind of addition...

Okay, that's fine! Just wanted to raise it as a possibility, if you're both happy with the addition, let's go for it.

mlebar-UC · 2025-11-11T04:31:29Z

Hey all, just wanted to say this is still on my to do list, but the quarter has gotten away from me a bit! I'm hoping to get back to it soon.

Add formalization of substructural logics in src

bf20aed

JacquesCarette requested changes Sep 8, 2025

View reviewed changes

		@@ -0,0 +1 @@
		* Added a folder "Logic" in src. This provides a formalization of several substructural logics based on chapter 2 of Greg Restall's "An Introduction to Substructural Logics". My hope is that this can provide a useful framework for anyone wanting to study a variety of logics in Agda. This was a master's research project done under Professor Stuart Kurtz, and I'm really happy with my work here - I would love to contribute to the standard library, and I am happy to make any appropriate modification to help with that.


		is-comma-logic : Comma-Logic S _⊢_ C⟨_⟩ _⨾_ _/_ _⇒_

		comma-product-context-l :

Conversation

mlebar-UC commented Sep 4, 2025

Uh oh!

jamesmckinna commented Sep 7, 2025 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

JacquesCarette commented Sep 7, 2025

Uh oh!

MatthewDaggitt commented Sep 8, 2025

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

JacquesCarette commented Sep 8, 2025

Uh oh!

jamesmckinna commented Sep 8, 2025

Uh oh!

mlebar-UC commented Sep 8, 2025

Uh oh!

MatthewDaggitt commented Sep 9, 2025

Uh oh!

mlebar-UC commented Nov 11, 2025

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

4 participants

jamesmckinna commented Sep 7, 2025 •

edited

Loading