summaryrefslogtreecommitdiff
path: root/support/w2latex/EXEMPLES/DOjervell.rtf
blob: f312339650696d54a3d7d708c3656694fee0382f (plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
{\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 
}