A question concerning E Mingle

[Gemma Robles]

Dear FOMers,

José M. Méndez and I are working on E Mingle (EM)

EM is Anderson and Belnap's logic of entailment E plus the axiom Mr

Mr: (A->B)->[(A->B)->(A->B)]

EM is included in E plus Mr'

Mr': (A->B)->[(C->D)->[(A->B)v(C->D)]]

Let us call this system EM'.

It is obvious that EM is included in EM'. On the other hand, Slaney's
program MaGIC, does not find a matrix verifying EM and falsifying Mr'.
Could anybody help us to find a proof of Mr' from EM? (Both EM and EM' are
understood as extensions of Anderson and Belnap's Hilbert-style formulation
of E.)

Gemma Robles
https://gemmarobles.github.io
-------------- next part --------------
An HTML attachment was scrubbed...
URL: </pipermail/fom/attachments/20220701/db44bf43/attachment-0001.html>