agda
Add formalization of substructural logics in src
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.
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, egRawLogicon the model ofAlgebra.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
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?
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.
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.
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.
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.
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.