On Mon, May 20, 2019 at 8:57 PM Corbin Simpson <[email protected]> wrote:
> I had some other thoughts that I forgot to include: > > * Based on a technique I believe I learned from > https://blog.plover.com/math/24-puzzle-2.html , it would seem at least > plausible that I could syntactically encode associative-and-commutative > structures as bags of some sort. I'm not sure if this is a worthwhile > avenue of exploration, but I know at least one popular parenthesis-based > language family, Lisp, does this for some associative operations. > You can't really represent bags in metamath in any way that differs meaningfully from just having a binary operator with explicit association. You would still need a way to construct lists of things, and that list-making constructor could be used in various ways to get different trees, and you need to manipulate the expression to move the constructors around, and then you are back to associativity. Technically, what I just said is not true, because metamath is actually based on expressions as strings, and it can match expressions with different associations at different times for interesting effect. I strongly recommend against using this feature; it's easy to shoot yourself in the foot if you manipulate expressions that do not have a well defined syntax tree. > * I wonder whether double-lollipop should be an additive or multiplicative > conjunction. > Wikipedia says additive. I think that's right, because otherwise you wouldn't get modus ponens: From |- ( ( A -o B ) (x) ( B -o A ) ) and |- A you can't conclude |- B unless you have a way to get rid of the function going the other way. > On Monday, May 20, 2019 at 12:02:23 PM UTC-7, fl wrote: >> >> It doesn't seem they have a decent set of axioms. You won't go very far. >> > > Totally understandable. Would there be a better set of axioms for doing > this work? I don't know much about linear logic, and it seems like every > author has a different presentation. Also, of course, if there's a > preferred set of axioms that were waiting for some planned work along these > same lines, then I'd prefer to go with what everybody else wants to do. > I said this in the other post, but what I think FL means is that you don't have the axioms needed to do any set theory, only propositional logic. This is useful for studying the logic itself but not its applications. That said, you seem to be fine with adding extra axioms as needed so I would expect when you get there you will find the appropriate axioms to use, so there's not really any fundamental barrier to going farther with this. > How far should I expect to get? Is there some ceiling that you're > anticipating? I'm hoping that, after I finish adding axioms and proving a > base and doing some sanity checks, I'll be able to reach anything in > set.mm. In particular, I've convinced myself of ~ ax-1 but with lollipops > on a whiteboard, and I think (but am not sure) that ~ ax-2 is also valid in > linear logic. It is hopefully a matter of typing, proving, and trying to > remember the difference between the four connectives. > * ax-1 is not provable in LL. It's dropping the resource "ps" which is not allowed. The linear analogue of ax-1 is ( ph -o ( ? ps -o ph ) ). * ax-2 is also not provable. The resource "ph" is duplicated in this one. Possible analogues include $p |- ( ( ph -o ( ps -o ch ) ) -o ( ( th -o ps ) -o ( ( ph & th ) -o ch ) ) ) $. $p |- ( ( ! ph -o ( ps -o ch ) ) -o ( ( ! ph -o ps ) -o ( ! ph -o ch ) ) ) $. * ax-3 is provable. I'll leave that as an exercise for you. (BTW are you aware contrapos has a typo? It's an instance of identity.) * ax-mp is provable, I think you have this already. More generally, I would not recommend following the beginning of set.mm, the order of things is all wrong for this context. But the area where you have to start thinking more carefully is what to do with ax-4 on. What is the linear analogue of ( A. x ph -> ph )? What is A. x ph anyway? Simple type theory nicely interprets LL but the analogue for forall is dependent type theory and here the theory (of linear DTT) is notoriously subtle. I've only glanced at your reference but Mike Shulman is a big type theorist so he's probably worked this all out. Mario -- You received this message because you are subscribed to the Google Groups "Metamath" group. To unsubscribe from this group and stop receiving emails from it, send an email to [email protected]. To view this discussion on the web visit https://groups.google.com/d/msgid/metamath/CAFXXJSuGG%2BbvQmXtPwiRwBMaEc8FSZeSGYyN1_82dFF68qZ-xw%40mail.gmail.com.
