{\rtf1\mac\deff2 {\fonttbl{\f0\fswiss Chicago;}{\f2\froman New York;}{\f3\fswiss Geneva;}{\f4\fmodern Monaco;}{\f6\fdecor London;}{\f8\fdecor San Francisco;}{\f11\fnil Cairo;}{\f12\fnil Los Angeles;}{\f13\fnil Zapf Dingbats;}{\f14\fnil Bookman;} {\f16\fnil Palatino;}{\f18\fnil Zapf Chancery;}{\f20\froman Times;}{\f21\fswiss Helvetica;}{\f22\fmodern Courier;}{\f23\ftech Symbol;}{\f24\fnil Mobile;}{\f33\fnil Avant Garde;}{\f34\fnil New Century Schlbk;}{\f101\fnil Wartburg;}{\f118\fnil Warwick S;} {\f128\fnil Moscow;}{\f129\fnil Russian;}{\f135\fnil MATH-BES;}{\f140\fnil Lovell;}{\f149\fnil Detroit;}{\f171\fnil XB Futura ExtraBold;}{\f176\fnil H Futura Heavy;}{\f201\fnil ¡Math;}{\f512\fnil Alexandrie;}{\f2500\fnil Konstanz;}} {\colortbl\red0\green0\blue0;\red0\green0\blue255;\red0\green255\blue255;\red0\green255\blue0;\red255\green0\blue255;\red255\green0\blue0;\red255\green255\blue0;\red255\green255\blue255;}{\stylesheet{\sbasedon222\snext0 Normal;}}{\info{\title DOjervell.RTF}{\author Centre International de Rencontres Mathematiques}}\paperw11880\paperh16820\margl1701\margr1701\margt1417\margb1417\deftab709\widowctrl\ftnbj\makebackup \sectd \linemod0\linex0\headery1077\footery1077\cols1\colsx709\endnhere \pard\plain \qc\sl360 {\b\f16 Trakhtenbrot theorem for propositional linear logic\par \par Herman R. Jervell\par }\pard \sl360 {\f16 \par \par }\pard \sl360 {\f16 This is joint work with Staal Aanderaa. Boris Trakhtenbrot has proved the following strengthening of undecidability of derivability in predicate logic.\par }\pard \sl360 {\f16 For formulas F the following is recursively inseparable\par \tab - F is derivable\par \tab - F has a finite model as a counterexample\par \par }\pard \sl360 {\f16 We prove a Trakhenbrot theorem for propositional linear logic. For formulas\par }\pard \sl360 {\f16 \par F in propositional linear logic the following is recursively inseparable\par \tab - F is derivable\par \tab - F has a finite phase structure as a counterexample\par \par }\pard \sl360 {\f16 The interpolation theorem is true for propositional linear logic. Using the Trakhtenbrot theorem we can however prove that there is no recursive function of formulas A and B giving and interpolant C of A --> B. The theorems are true both for the intuitionistic and the classical case.\par }\pard \par }