Completeness Proofs for Linear Logic Based on the Proof Search Method(Preliminary Report)(Type Theory and its Applications to Computer Systems)
Mitsuhiro Okada, Kazushige Terui · Institutional Repositories DataBase (IRDB) · 1998
The proof search method is a traditionally established way to prove the completeness theorem for various logics.The purpose of this paper is to show that this method can be adapted to linear logic.First we prove the completeness theorem for a certain fragment of intuitionistic linear logic, called naive linear logic, with respect to naive phase semantics, i.e., phase semantics without any closure condition, using the proof search method in a certain labelled sequent system.Then the completeness of the (rudimentary) classical linear logic can be obtained as a direct corollary by a Kolmogorov-G\"odel style double negation interpretation.To apply the proof search method for the full system of linear logic, we generalize the notion of branch in the standard proof search method to that of OR-iree, and give a proof of the completeness theorem for intuitionistic (classical, resp.)linear logic with respect to intuitionistic (classical, resp.)phase semantics, based on a generalized form of $\mathrm{t}1_{1}\mathrm{e}$ proof search method.