Logic

Stream: CSLib

[Thomas Waring]

Starting a channel for general discussion of logic development in cslib (hope that's appropriate).

[Thomas Waring]

My PR on natural deduction cslib#66 is finally ready for review, I refactored it significantly so that deduction trees are defined for minimal logic (which matches more nicely with computational applications), and derivability/equivalence are relative to a Theory (set of propositions), which will make a more general semantic completeness result easy, as well as letting us add intuitionistic & classical principles to the logic. Feedback appreciated!

[Chris Henson]

If this is CSLib specific conversation, it should probably be moved to that channel. Also you can link you can link to PRs like this: cslib#66

[Thomas Waring]

oops my mistake, of course — should i open a topic there? who can move it?

[Notification Bot]

This topic was moved here from #computer science > cslib: Logics by Fabrizio Montesi.

[Fabrizio Montesi]

Moved. :)

[Malvin Gattinger]

Nice! I don't have a specific comment, but wanted to ask this about "Logic in CSLib " for a while already: do we have a plan for accommodating multiple (very many?) different logics (or different proof systems for the same logic) and how they relate? So for example will we later also have natural deduction for First-Order Logic and will that formally extend the Propositional system in some way?
Or suppose :innocent: I want to do a specific modal logic, do I roll my own Proposition type for modal formulas and Derivation from scratch each time or can I somehow extend the types for the propositional system?

I think this is known as the Expression_problem and maybe my question is just whether people have thought about how to "solve" it in Lean.

[Maximiliano Onofre-Martínez]

Yes, at least for me, the ideal vision for CSLib is exactly what you describe. However, as far as I know, there's no concrete roadmap for it just yet.

[Thomas Waring]

I think that would be ideal, yes, but my two cents is that I feel there is a non-trivial tradeoff between generality in this sort of way and how closely things stick to computer science.

For example, the Formalised Formal Logic people have done a very good job of being modular — as I understand it, something like "conjunction elimination" is a typeclass on a deduction system, so results about conjunction elimination are valid for any deduction system which has it as a rule — but they (predominantly) use a Hilbert-style calculus. I started here with natural deduction because of how closely it sticks to the lambda calculus, and so it felt appropriate for inclusion specifically in a computer science library, even if it isn't the right formalism to prove things in full mathematical generality.

All that being said, some machinery along the lines of, "I want to define a type of derivations which is NJ.Derivation + some extra rules" would be great, and I am very open to reworking my PR to include it if someone knows how!

[Thomas Waring]

Also, I just added a note about a small design question to my PR cslib#66 — whether derivations should be parametric in a theory, giving them two kinds of axiom rules. I'd love some feedback here or there! (ping @Fabrizio Montesi as it's probably you who will review it)

[Malvin Gattinger]

I much agree that there is a trade-off between generality and usability of the instances of the general thing (be it formula or derivation types). And typeclasses as used in FFL can get quite far. I also think it might make sense to wait until a bunch of different logics are in cslib and how they are used by other areas before trying to find a general definition of what "a logic" is. But maybe not wait too long until all hope of unifying things is gone :wink:

[Malvin Gattinger]

Related to this, @Ramy Shahin gave a talk about a possible approach to the expression problem in Lean at TYPES2025, see paper and video. I do not want to suggest to make cslib depend on this (still quite experimental) code, but for the long term future it might be a nice inspiration.

[Thomas Waring]

Thomas Waring said:

Also, I just added a note about a small design question to my PR cslib#66

The more I think about this the less I'm satisfied with the current presentation — I've closed the PR & I'll put up a better version in pieces (sorry to anyone who spent time reviewing it, the new one should be relatively similar)

[Fabrizio Montesi]

For the record, the plan is that yes, we're very interested in finding general and reusable patterns across different logics. My plan for now is very simple: I'd like us to have at least 2 different logics and start the discussion from there. :)
I see a first likely candidate for generalisation in the concept of logical equivalence.

[Chris Henson]

This topic is relevant to lambda calculi too, but I don't have a great answer. I have plans to build something that generates lambda calculus boilerplate (similar to Austosubst2), but this is a pretty big undertaking that I don't plan to finish anytime soon, and I'm not sure that I want this to be a CSLib dependency.

[Thomas Waring]

Propositional logic definitions are now at cslib#89 (once more with feeling!) — I'll add natural deduction in a follow up, this one is short so should easy the earlier burden on reviewers

[Fabrizio Montesi]

Hi all, finally got some bandwidth for logic, so I'd like to circle back to this. :)
Let's start from cslib#89. It looks really interesting, I'm just struggling a bit to distinguish what's a formalisation choice and what's in the original presentation (like representing bot as a possible member of the atoms and the use of Theory; which I like, it's pretty clever, just want to understand a bit). @Thomas Waring could you maybe clarify and/or give a reference maybe?

[Fabrizio Montesi]

(Another reason for circling back now is that I think we've accumulated some relevant experience from other simpler parts in cslib.)

[Thomas Waring]

Great! I agree that there are a lot of non-obvious choices to be made, & I'm very open to discussion &/or reworking what I've got as we go along. Probably the reference which is closest to how I've presented it is Sørensen & Urzyczyn's lecture notes, but I don't know of anywhere doing it exactly like I have, mostly because the needs of formalisation are a bit orthogonal to the usual way we write about proof theory imo.

I'd say most of the things you mention fall under formalisation choices: I'll try to write some more clarifying documentation, but to answer the things you raise here:

• I wanted to capture minimal logic (intuitionistic without efq) because that's the one with the most obvious / direct computational content — essentially it is STLC with sums and products.
• Once you're in minimal logic, either you don't have falsum, or it behaves exactly like an atom (ie there are no rules for it), so it seemed reasonable to have it be optional for a given language of propositions. In the case that it is present, we have ⊥ = atom ⊥ definitionally, so it doesn't really add much overhead i think.
• The use of Theory is a bit less obvious. Usually on pen-and-paper you switch between minimal / intuitionistic / classical by adding and removing rules — since we don't have an easy way (cf above discussion) to do this as is stands, the best solution seemed to be to formulate the extra deduction rules as implications, and allow appealing to them as axioms.
• Another point in favour of Theory is it makes it easy to define "equivalence modulo some axioms", which is nice in itself and helps with developing semantics.

[Chris Henson]

Oh I didn't realize you were working from that, it's just a few feet away on my bookshelf. This is jumping way ahead, but if SOL is on your radar for the future, I would love to be able to formalize Wadler's The Girard-Reynolds Isomorphism. IIRC those notes do not go into the detail of the each direction of transformations between System F and second order logic. It would be a fun milestone of the library to see that our lambda calculus and logic developments line up in this way.

[Thomas Waring]

nice, that's my bad i meant to put it in the references earlier. i found that paper kind of confusing to read when i looked at it (ages ago) but the idea is definitely interesting (all the more reason to formalise!). SOL is possibly beyond my lean abilities (i've been steering clear of free/bound variables for reasons you can probably understand), but that circle of ideas is definitely in my wheelhouse — realisability / reducibility / logical relations etc

[Chris Henson]

Hmm, I see. Next on my list is to add lambda calculus in the well scoped style (the type of Terms indexed by the number of free variables) which should be easier to use than the locally nameless System F I've done so far. If I make that a sufficiently good example to work from for simple types, I think it would be not so hard to transfer over the binding aspect. (A bridge to cross when we reach it...)

[Fabrizio Montesi]

Re binding: I've been steering clear of polymorphism/variables in linear logic for exactly the same reason, would love to settle together on a 'good' way to do it in the future.

[Chris Henson]

My inclination is that well-scoped indices as I mention above are probably what we want. I have in my mind to make a Lean implementation of Autosubst that would allow you to have all the substitution/variable lemmas generated for you, but this is a big project. Maybe in the meantime I can just do simple types and polymorphism "by hand" as an example you can use.

[Fabrizio Montesi]

Thomas Waring said:

Great! I agree that there are a lot of non-obvious choices to be made, & I'm very open to discussion &/or reworking what I've got as we go along. Probably the reference which is closest to how I've presented it is Sørensen & Urzyczyn's lecture notes, but I don't know of anywhere doing it exactly like I have, mostly because the needs of formalisation are a bit orthogonal to the usual way we write about proof theory imo.

I'd say most of the things you mention fall under formalisation choices: I'll try to write some more clarifying documentation, but to answer the things you raise here:

• I wanted to capture minimal logic (intuitionistic without efq) because that's the one with the most obvious / direct computational content — essentially it is STLC with sums and products.
• Once you're in minimal logic, either you don't have falsum, or it behaves exactly like an atom (ie there are no rules for it), so it seemed reasonable to have it be optional for a given language of propositions. In the case that it is present, we have ⊥ = atom ⊥ definitionally, so it doesn't really add much overhead i think.
• The use of Theory is a bit less obvious. Usually on pen-and-paper you switch between minimal / intuitionistic / classical by adding and removing rules — since we don't have an easy way (cf above discussion) to do this as is stands, the best solution seemed to be to formulate the extra deduction rules as implications, and allow appealing to them as axioms.
• Another point in favour of Theory is it makes it easy to define "equivalence modulo some axioms", which is nice in itself and helps with developing semantics.

Thanks, that's very helpful! I'll reflect a bit on this after I'm done with my current PR to revise CLL equivalences into proof-relevant ones.

[Fabrizio Montesi]

By the way, I'm doing stuff like this an awful lot:

have : (a⫠ ::ₘ b⫠ ::ₘ {b ⊗ a}) = ((b ⊗ a) ::ₘ ({b⫠} + {a⫠})) := by grind -- whatever rewriting of the sequent in the goal I need
rw [this]
apply Proof.tensor -- whatever rule I need to apply here

Is there a more elegant way to express 'apply this rule by rewriting the goal with this, and that's fine because grind says it'? :-)

[Thomas Waring]

Fabrizio Montesi said:

Thanks, that's very helpful!

Great! I think I addressed the main choice but let me know if there's anything else I can explain further

[Thomas Waring]

Fabrizio Montesi said:

By the way, I'm doing stuff like this an awful lot:

have : (a⫠ ::ₘ b⫠ ::ₘ {b ⊗ a}) = ((b ⊗ a) ::ₘ ({b⫠} + {a⫠})) := by grind -- whatever rewriting of the sequent in the goal I need
rw [this]
apply Proof.tensor -- whatever rule I need to apply here

Is there a more elegant way to express 'apply this rule by rewriting the goal with this, and that's fine because grind says it'? :-)

Hmm you can golf slightly as

rw [show a⫠ ::ₘ b⫠ ::ₘ {b ⊗ a}) = ((b ⊗ a) ::ₘ ({b⫠} + {a⫠}) by grind]
apply Proof.tensor -- whatever rule I need to apply here

but more generally we should probably have a rule along the lines of eg docs#SimpleGraph.Walk.copy — when the type depends on data you have API to transfer elements along equalities of the index (not sure if I'm getting all the terminology right lol)

[Fabrizio Montesi]

Thanks!
Re the rule, yeah, I tried to write it, but it's not working as well as I wanted... I'll submit a PR as soon as I'm done fixing everything.

[Thomas Waring]

Okay fair enough :) honestly I have been cheating and using weakening instead of defining that API (ie making grind prove ⊆ instead of =), but that (importantly!) doesn't apply to your case...

[Chris Henson]

I am not following what you want from grind. Any chance you have a full example in a branch I could work with?

[Chris Henson]

I am guessing the problem here is that this is in the middle of a proof, rather than something terminal grind can finish?

[Fabrizio Montesi]

Chris Henson said:

I am not following what you want from grind. Any chance you have a full example in a branch I could work with?

Correct. Grind is doing wonders. It's apply that can't see that the goal is a 'simple' series of multiset rewrites away. (I'm not saying it should, it's just my problem here.)

[Chris Henson]

The general pattern I follow is trying to get everything grind needs to use at the end of a proof branch. Sometimes you can use suffices to move things around a bit, or use have to place a general theorem that grind can access. If you point out any of these in a review I'm happy to try golfing.

[Fabrizio Montesi]

I think I'm almost there. Here's my current WIP: https://github.com/leanprover/cslib/blob/new-logic/Cslib/Logics/LinearLogic/CLL/Basic.lean

Basically I've rewritten Proof to use multisets directly (that's what most people do on paper nowadays anyway, and grind now makes working with this decent enough), and adapted all proofs of equivalences to be proof-relevant (I still have two small sorrys).

Feedback/help welcome. :-)

I feel this is well-behaved/simple enough that once we're done we could make a typeclass for the \Downarrow notation and the \===\Downarrow equivalence notation (maybe it should just be \===, but for now I'm trying to be explicit where I want actual types).

[Fabrizio Montesi]

grind is having trouble doing proofs by itself, maybe I should annotate something more..

Note also I'm annotating Multiset stuff. Maybe we wanna have a Data/Multiset.lean thing where we put this kind of stuff until mathlib annotates multiset defs/theorems for grind.

[Chris Henson]

I'm seeing some errors trying to build that branch that don't look grind related? Maybe let's not provision a file for it (you convinced me of this last time I suggested something similar!), but gathering together multiset grind annotations somewhere sounds like a good idea.

[Fabrizio Montesi]

Yes look only at that file, I still gotta fix the rest. :⁠-⁠)

[Malvin Gattinger]

Two small comments: I would be happy if proof sequents in general will be Multisets (in the PDL project we used Lists but mostly just because the API was nicer, Multisets feels more like "the right thing to do", e.g. because of docs#Multiset.IsDershowitzMannaLT). Second, I was wondering about how much notation CSlib wants to use/occupy and whether that can clash with mathlib or lean core: the Proof notation ⇓ is also used in Std.Do.PostCond. Does the "scoped" mean this will not be a problem? (Hypothetically someone some day may want to write an imperative program working with Proofs :thinking: )

[Chris Henson]

Regarding notation: we have a convention (that we test for) that we do not add any declarations to a new top level namespace. This includes notation, meaning that all our notations are scoped. This isn't a guarantee of non-conflict with Mathlib/core notations, but covers a number of common unscoped notations. In your example above for instance, maybe there is still a problem of you want both scopes open. At minimum, there is a test of importing both Mathlib and CSLib.

[Fabrizio Montesi]

This is basically my concern in https://github.com/leanprover/cslib/issues/23. Suggestions/solutions are highly welcome. Notations are bound to be 'duplicated'. In this specific example, ⇓ is also a common symbol for termination in operational semantics and barbs in concurrency.

[Fabrizio Montesi]

Re the sequents: I agree multisets are now pretty nice to work with, yes. IIRC in some sequent calculi order is actually important, so there List will be the natural choice.

[Malvin Gattinger]

Right, for substructural logics the sequents should be lists. Another edge case where List works better than Multiset is when we want to build formulas based on sequents, for example taking the conjunction or disjunction of all formulas in a Multiset-sequent would be noncomputable / need choice, but with a List-sequent is easy.

[Fabrizio Montesi]

Here's my PR: https://github.com/leanprover/cslib/pull/187
Please have a look, maybe we can make grind do better. Also, where should I put the grind annotations for Multiset? Mmh..

[Chris Henson]

I don't think I've looked at these files previously. I am a bit more fundamentally concerned with the way it constructs data (non-Prop types) with tactics.

[Fabrizio Montesi]

Me too, but I couldn't figure out how to do it without tactics.. :-)
Using tactics gives a very similar approach to the one followed on paper.

[Thomas Waring]

I ran into similar issues, though possibly for NJ it's easier to avoid bc the rules are a bit more relaxed. @Chris Henson you'll know better but as I understand it some uses of tactics for data are generally okay — like refine / apply — and improve readability, but some aren't — I'm guessing steering clear of rw is a start, but is there a reference / some documentation on this issue?

[Thomas Waring]

I haven't tried hard to work this out but I think a lot of the problematic tactic use could be avoided with a functional Proof.copy API: at very least that could avoid rwing the sequent in the goal. You can see a bit of this at work in cslib#91 — I don't have a copy but I do have weakening, and often I avoid a rw by convincing lean that the sequent I prove is a subset of the sequent I want, which suffices in the non-linear setting

[Chris Henson]

Yes, rw is particularly troublesome. I'm not actually not sure of docs about this. I don't follow the last bit, can you explain what Proof.copy is?

[Thomas Waring]

Right I see. The copy idea is pretty rough, based on docs#SimpleGraph.Walk.copy — I'll write a mwe some time but the idea is roughly this: say in Fabrizio's example we want to apply Proof.tensor, but the goal is something like ⇓ a⫠ ::ₘ b⫠ ::ₘ {b ⊗ a}, whereas the conclusion of the rule we want to apply is ⇓(a ⊗ b) ::ₘ (Γ + Δ) — these are propeq but not defeq (I think), so using tactics we rw the goal to be what we want. I see now there actually is a rule doing what I want (though using tactics)

def Proof.sequent_rw (h : Γ = Δ) (p : ⇓Γ) : ⇓Δ := by rw [h] at p; exact p

The rough idea though is that we can push the use of grind etc inside the hypothesis h, so all the data is produced without tactics, and then cook up enough simp lemmas etc to make sequent_rw friendly to work with.

[Thomas Waring]

I guess whether this helps or not depends on what problems actually arise from the use of tactics for data, which was why I asked about any docs / general intuition for why we try to avoid it

[Chris Henson]

I think can rewrite that Proof.sequent_rw to not use tactics. The intuition I have for why we do this is that tactics can unpredictability cause complicated terms that are hard to work with, simp and rw especially. I seem to recall a thread talking about how even refine can cause difficulties in some cases.

[Thomas Waring]

Chris Henson said:

I think can rewrite that Proof.sequent_rw to not use tactics

right I think even h ▸ p would work? my intuition was similar (though i'd be interested to see how refine runs into trouble) — i think if we have enough API for sequent_rw that would make it easier to deal with, but the proof would be in the pudding i suppose

[Fabrizio Montesi]

You're getting where I wanted! But I didn't try enough to write a direct term.. :⁠-⁠)

(Btw I should've probably cased sequent_rw differently.)

[Chris Henson]

Thomas Waring said:

Chris Henson said:

I think can rewrite that Proof.sequent_rw to not use tactics

right I think even h ▸ p would work?

Yes, exactly. I can make a pass later today through the PR and try to make this and other changes that as much as possible use terms instead of tactics.

[Fabrizio Montesi]

I've defined eta-expansion for CLL. cslib#198

This was useful to gain experience in rewriting conclusions as needed to build proofs (see the PR). I wonder if we could use calc in a smart way in this kind of defs (without entering by).