Subject: Re: BV on display
Newsgroups: gmane.science.mathematics.frogs
Date: 2005-08-03 13:31:48 GMT (3 years, 48 weeks, 16 hours and 1 minute ago)
Hi Jon, >In other words, it merges branches, keeping track of which branch is on >the left and which is on the right. It turns out that this isn't >*quite* the rule we want in our DC system, for reasons that I won't go >into. Anyway, let's settle on notation. I'll use a semicolon for the >meta-level seq connective and < for the object level one. The semicolon >satisfies the obvious display postulates: > >X;Y |- Z X;Y |- Z X |- Y;Z X |- Y;Z >========= ======== ======== ======== >X |- Z;*Y Y |- *X;Z *Y;X |- Z X;*Z |- Y > > > If I understood your system correctly, I think it actually proves more formulas (or structures) than BV. For instance, consider the following proof a |- a ------- a;I |- a -------- I |- *a ; a I think the display postulates above need to be strengthened a bit, for instance, with a proviso that Y is not unit. Although I don't know how it would affect the completeness proof. Best regards, -Alwen