Timeline for Can the Multiplicative Fragment of Linear Logic be shown to be non-truth-functional?
Current License: CC BY-SA 2.5
13 events
| when toggle format | what | by | license | comment | |
|---|---|---|---|---|---|
| Apr 1, 2015 at 15:47 | answer | added | Robin Houston | timeline score: 3 | |
| Oct 9, 2010 at 22:40 | comment | added | Z.L. Fraser | Thanks for pointing this out, Noam. Maybe I was over-hasty in using the expression "non-truth-functional". I'll take a look at Girard's paper, I think I have it kicking around somewhere. | |
| Oct 9, 2010 at 22:37 | history | edited | Z.L. Fraser | CC BY-SA 2.5 |
changed title
|
| Oct 9, 2010 at 8:30 | comment | added | Noam Zeilberger | then phase semantics satisfies your requirements for being truth-functional, except that not every provable formula is necessarily assigned the same value. See Theorem 2 of Girard's "Linear Logic: Its Syntax and Semantics": an arbitrary linear logic formula is provable iff its interpretation in any phase space $(M,\bot)$ (where $M$ is a commutative monoid, $\bot$ an arbitrary subset of $M$) contains the neutral element. | |
| Oct 8, 2010 at 18:14 | vote | accept | Z.L. Fraser | ||
| Oct 8, 2010 at 18:13 | comment | added | Z.L. Fraser | PS: "uniquely determined by" here means "is a function of", so that ƒ(A # B) is a function of <ƒ(A), ƒ(B)>. (Which amounts to saying that IF ƒ(A1 # B1) ≠ ƒ(A2 # B2) THEN either ƒ(A1) ≠ ƒ(A2) or ƒ(B1) ≠ ƒ(B2).) | |
| Oct 8, 2010 at 18:09 | comment | added | Z.L. Fraser | Hi Neel, By "truth-functional", I mean "can be furnished with truth tables". More strictly, logic L is truth-functional iff there exists a truth-value assignment ƒ from the atoms of L into set E, such that (1) ƒ sends A to a privileged value, call it e, iff A is provable, (2) ƒ(A # B) is uniquely determined by the values of ƒ(A) and ƒ(B), for every connective # in L. Does this conform with the usual meaning of "truth-functional"? Thanks, Luke | |
| Oct 8, 2010 at 17:54 | history | edited | Z.L. Fraser | CC BY-SA 2.5 |
Forgive me for undoing the last edit. The previous changes made my "par" symbols (which should read like upside down ampersands) illegible.
|
| Oct 8, 2010 at 11:47 | answer | added | Todd Trimble | timeline score: 2 | |
| Oct 8, 2010 at 8:27 | comment | added | Neel Krishnaswami | I'm not sure what you mean by "truth-functional". Girard's phase semantics gives a sound and complete model-theoretic interpretation of the connectives of classical linear lgoic, but perhaps you want something more stringent than that? | |
| Oct 8, 2010 at 8:23 | history | edited | Neel Krishnaswami | CC BY-SA 2.5 |
improved formatting somewhat
|
| Oct 7, 2010 at 22:26 | history | edited | Z.L. Fraser | CC BY-SA 2.5 |
deleted 67 characters in body
|
| Oct 7, 2010 at 22:20 | history | asked | Z.L. Fraser | CC BY-SA 2.5 |