Implementation of linear logic

[Ishan Murphy]

Hello,

As an excercise in both linear logic and writing Metamath databases, I am making a formalization of linear logic in Metamath The .mm file is here: https://github.com/ishanpm/metamathlinear/blob/master/linear.mm. The axiomatization I am using is based on Axioms and Models of Linear Logic by Wim H. Hesselink: https://www.rug.nl/research/portal/files/3359896/1990FormAspCompHesselink2.pdf. I know I'm not the only person doing something like this, but I wanted some feedback on what I have so far.

I am still trying to decide on good conventions for the names and order of the proofs. Do you have any advice for me regarding this? The naming is currently somewhat inconsistent since I am trying several things at once.

[Jim Kingdon]

Nice. I don't know linear logic well enough to have a lot of reactions, but I have a soft spot for obscure logics even if I keep coming back to "conventional" intuitionistic propositional logic.

[Ishan Murphy]

I'm working on this database using mmj2, but it keeps spitting out error messages when starting. These do not prevent the program from working, but they're kind of annoying. Could anyone help me get rid of them?

The first error is this:

E-TR-0102 The input library has no trivial implication rule for wli implication operator (main assertion lmp).

It seems that it doesn't like the fact that the modus ponens like rule for linear implication is not primitive. Similar error messages are printed for the linear biconditional and logical implication. How do I silence these?

The second error:

E-UT-1504 Error in callback TRANSFORMATION_SET_UP:

Error in macro transformations:

TypeError: null has no such function "getSeq" in transformations.js at line number 96

It appears that a macro script is referencing the mathboxes in set.mm, a section which is not present in my database. Is there a quick fix for this, or should I just manually edit the script to add a nullity check?

Thank you for any help.

[Mario Carneiro]

On Thu, Sep 26, 2019 at 12:41 AM Ishan Murphy <ish...@gmail.com> wrote:

I'm working on this database using mmj2, but it keeps spitting out error messages when starting. These do not prevent the program from working, but they're kind of annoying. Could anyone help me get rid of them?

The first error is this:

E-TR-0102 The input library has no trivial implication rule for wli implication operator (main assertion lmp).

It seems that it doesn't like the fact that the modus ponens like rule for linear implication is not primitive. Similar error messages are printed for the linear biconditional and logical implication. How do I silence these?

I think this is a bug, it should have rejected the rule if it didn't match the expected form, but the easy solution is to turn off AutoTransformations using

ProofAsstUseAutotransformations,no,no,no

The second error:

E-UT-1504 Error in callback TRANSFORMATION_SET_UP:

Error in macro transformations:

TypeError: null has no such function "getSeq" in transformations.js at line number 96

It appears that a macro script is referencing the mathboxes in set.mm, a section which is not present in my database. Is there a quick fix for this, or should I just manually edit the script to add a nullity check?

The entire file transformations.js contains set.mm specific theorem names. You can get a newer version of transformations.js (which has already fixed the "getSeq" null error in the master branch version) from https://github.com/digama0/mmj2/blob/master/mmj2jar/macros/transformations.js , or you can disable it entirely by commenting out line 95 of init.js. (These modifications only require that you restart mmj2.)

If you encounter any other errors, you might try updating mmj2; a new version was released a few days ago and incorporates a bunch of minor bug fixes like this.

Mario

[Ishan Murphy]

The errors from transforms.js are fixed in the newest version of mmj2, but the "trivial implication rule" errors are still sounding. I peeked into the source where this message is generated, and it looks like it wants a rule of the form B => A -> B. I'm happy to add such a theorem for the logical implication, but the linear implication cannot accommodate this due to being, y'know, linear and all.