Abstract
We first give our version of the register machines to be simulated by proofs in propositional linear logic. Then we look further into the structure of the computations and show how to extract ”finite counter models” from this structure. In that way we get a version of Trakhtenbrots theorem without going through a completeness theorem for propositional linear logic. Lastly we show that the interpolant I in propositional linear logic of a provable formula A ⊸ B cannot be totally recursive in A and B.
This is a preview of subscription content, log in via an institution to check access.
Preview
Unable to display preview. Download preview PDF.
References
E Börger. Berechenbarkeit, Komplexität, Logik. Vieweg Verlag 1985. English translation published by North-Holland.
P D Lincoln, J Mitchell, A Scedrov, N Shankar. Decision problems for propositional linear logic. In Proc. 31st Annual IEEE Symposium on Foundations of Computer Science, St Louis, Missouri, October 1990.
D Roorda Resource Logics: Proof-theoretical Investigations. Thesis. Amsterdam 1991.
A S Troelstra. Lectures on linear logic. CSLI Lecture Notes No 29. 1991
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 1993 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Aanderaa, S., Jervell, H.R. (1993). Recursive inseparability in linear logic. In: Börger, E., Jäger, G., Kleine Büning, H., Martini, S., Richter, M.M. (eds) Computer Science Logic. CSL 1992. Lecture Notes in Computer Science, vol 702. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-56992-8_2
Download citation
DOI: https://doi.org/10.1007/3-540-56992-8_2
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-56992-3
Online ISBN: 978-3-540-47890-4
eBook Packages: Springer Book Archive