Timeline for Can the Multiplicative Fragment of Linear Logic be shown to be non-truth-functional?
Current License: CC BY-SA 2.5
4 events
| when toggle format | what | by | license | comment | |
|---|---|---|---|---|---|
| Oct 8, 2010 at 18:14 | vote | accept | Z.L. Fraser | ||
| Oct 8, 2010 at 18:04 | comment | added | Z.L. Fraser | I was running out of space, and left the last sentence unclear: I mean that the problem is that there always tend to be "too many" separately provable formulae grouped together on a given line in the sequent proof, no matter how you try and break them up using the tensor rule. But that's the multiplicatives for you: they don't let you throw anything away, and so a multiplicative sequent can be unprovable because it's "choked" with separately provable formulae. | |
| Oct 8, 2010 at 18:01 | comment | added | Z.L. Fraser | Thanks, Todd. This is what several hours tinkering around with attempted sequent proofs led me to expect, but the explanation in terms of proof nets makes it clearer why the existence of such formulae are unlikely. That "any proof of A [par] B cannot make any use of the proofs of A and B" is the key obstacle. The tactic that suggests itself is to have A or B throw some [tensor]s into the mix, so that the formulae in the context can be regrouped when the [tensor] rule is employed. But if A and B are to both be provable, there always seems to be "too many provables" in any rearrangement. | |
| Oct 8, 2010 at 11:47 | history | answered | Todd Trimble | CC BY-SA 2.5 |