On Mon, May 20, 2019 at 9:19 PM Mario Carneiro <[email protected]> wrote:
> * 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. > Actually, I think the <-> symbol I used in the axiomatization in the last post is better understood as an exponential, |- ( ( A <-> B ) <-> ! ( ( A -o B ) & ( B -o A ) ) ), which is the same regardless of whether you use additive or multiplicative conjunction. That's because the way I am using it is for ( ph <-> ps ) to mean "ph and ps are interchangeable in all contexts" which requires the ability to use this fact as many times as you want. Recall that |- ph implies |- ! ph, and all the rules I gave for <-> involved it being the root symbol, something outright provable, and so |- ( ( A -o B ) & ( B -o A ) ) and |- ( ( A -o B ) (x) ( B -o A ) ) and |- ! ( ( A -o B ) & ( B -o A ) ) are all interchangeable. But the rule I gave for deducing <-> is wrong, or at least insufficiently powerful: $e |- ( ~ ph \/ ps ) $e |- ( ~ ps \/ ph ) $a |- ( ph <-> ps ) $. This can only be used to deduce <-> at the head, while what is needed is a characterization, i.e. a way to prove |- ( ( ph <-> ps ) <-> ... ) . But perhaps the most straightforward solution is to just say so, i.e.: $a |- ( ( ph <-> ps ) <-> ! ( ( ph -o ps ) & ( ps -o ph ) ) ) $. This leaves room for the double-lolly operation ( ph o-o ps ) <-> ( ( ph -o ps ) & ( ps -o ph ) ) to be a distinct symbol. By the way, I found a program called llprover online for proving LL theorems; it uses the ascii notations "/\" with "\/" par "+" plus "*" times, which mostly matches my earlier advice of combining familiar symbols where possible and reasonable symbols for the rest. The par symbol is just ridiculous. -- 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/CAFXXJSupkMX6kfvx6RBFtC%2Bm%2ByJo0OpEKrzu09H1oxP5HA89%3Dg%40mail.gmail.com.
