Trakhtenbrot theorem for propositional linear logic

Herman R. Jervell

This is joint work with Staal Aanderaa. Boris Trakhtenbrot has proved the following strengthening of undecidability of derivability in predicate logic.
For formulas F the following is recursively inseparable
	- F is derivable
	- F has a finite model as a counterexample

We prove a Trakhenbrot theorem for propositional linear logic. For formulas

F in propositional linear logic the following is recursively inseparable
	- F is derivable
	- F has a finite phase structure as a counterexample

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.