Path: utzoo!utgpu!news-server.csri.toronto.edu!rpi!zaphod.mps.ohio-state.edu!sol.ctr.columbia.edu!emory!gatech!bloom-beacon!eru!hagbard!sunic!ugle.unit.no!nuug!ulrik!eric From: eric@uio.no (Eric Monteiro) Newsgroups: comp.theory Subject: (linear logic) oops -- the latex ! Message-ID: Date: 21 May 91 05:15:53 GMT Sender: news@ulrik.uio.no (Mr News) Distribution: sci.logic Organization: University of Oslo, Norway Lines: 595 Nntp-Posting-Host: solveig.nr.no sorry, I forgot the latex-code for the paper on linear logic advertised in a previous mail. - eric \documentstyle[{A4}]{article}% \renewcommand{\today}{May 13, 1991} %\renewcommand{\baselinestretch}{1.96} \newcommand{\MEG}{Morten Elvang-G\o ransson\thanks{Department of Computer Science, The Technical University of Denmark. Visitor at Department of Informatics, University of Oslo ({\sf elvang@ifi.uio.no}).}} \newcommand{\AW}{Arild Waaler\thanks{Department of Linguistics and Philosophy, University of Oslo ({\sf arild@ulrik.uio.no}).}} \newcommand{\HRJ}{Herman Ruge Jervell\thanks{Department of Linguistics and Philosophy, University of Oslo ({\sf herman@ulrik.uio.no}).}} \newcommand{\EM}{Eric Monteiro\thanks{Norwegian Computing Center (\sf Eric.Monteiro@nr.no).}} % USED FOR TYPESETTING RULES % \Rule{name}{hyp}{conc} % \RuleN{hyp}{conc} - NO NAME % \RuleC{name}{hyp}{conc}{sidecondition} - CONDITION \newcommand{\Rule}[3]{\begin{quote}$\PSL{#1}{#2}{#3}$\end{quote}} \newcommand{\RuleN}[2]{\begin{quote}$\PS{#1}{#2}$\end{quote}} \newcommand{\RuleC}[4]{\begin{quote}$\PSL{#1}{#2}{#3}\ANNOT{#4}$\end{quote}} % USED FOR TYPESETTING PROOFS IN MATH-ENVIRONMENT % \PS{HYP}{CONC} `PS' for `proof step'. % \PA{ONLY ONE} `PA' for `proof array'. % \PAW{ONLY ONE} `PAC' for `proof array WITHOUT [?]'. % \PSR{Right annotation}{HYP}{CONC} % \PSL{Left annotation}{HYP}{CONC} % \PPS,\PPSR,\PPSL ARE SIMILAR MACROS, BUT WITH `DOUBLE LINES' % \ANNOT{annotation} - not supposed to be applied directly % \SP - space between hypotheses in proofs. \newcommand{\PS}[2]{\begin{array}[b]{c}#1\\ \hline #2\end{array}} \newcommand{\PA}[1]{\begin{array}[b]{c}#1\end{array}} \newcommand{\PAW}[1]{\begin{array}{c}#1\end{array}} \newcommand{\PPS}[2]{\begin{array}[b]{c}#1\\ \hline\hline #2\end{array}} \newcommand{\PSR}[3]{\begin{array}[b]{c}#2\\ \hline #3\end{array}\ANNOT{#1}} \newcommand{\PPSR}[3]{\begin{array}[b]{c}#2\\ \hline\hline#3\end{array}\ANNOT{#1}} \newcommand{\PSL}[3]{\ANNOT{#1}\begin{array}[b]{c}#2\\ \hline #3\end{array}} \newcommand{\PPSL}[3]{\ANNOT{#1}\begin{array}[b]{c}#2\\ \hline\hline#3\end{array}} \newcommand{\ANNOT}[1]{\mbox{$\ {}^{^{\mbox{\rm \footnotesize#1}}}$}} \newcommand{\SP}{\makebox[.5cm]{\ }} % ENVIRONMENTS %EXAMPLE \newtheorem{examP}{Example} \newenvironment{example}% {\begin{examP} \rm }% {\rm \mbox{$\Box$}\end{examP}}% %PROOF - NUMBERED INDEPENDENTLY \newtheorem{ppp}[examP]{Proof} \newenvironment{proof}% {\begin{ppp} \rm }% {\rm \mbox{$\Box$}\end{ppp}}% %PROOF - NUMBERED AS LAST THEOREM, LEMMA, COROLLARY, ETC. \newtheorem{PRooF}[examP]{Proof of} \newenvironment{Proof}% {\addtocounter{examP}{-1}\begin{PRooF} \rm }% {\rm \mbox{$\Box$}\end{PRooF}}% % DEFINITION ETC. \newtheorem{definition}[examP]{Definition} \newtheorem{lemma}[examP]{Lemma} \newtheorem{invariant}[examP]{Invariant} \newtheorem{theorem}[examP]{Theorem} \newtheorem{corollary}[examP]{Corollary} \newtheorem{axiom}[examP]{Axiom} % META-LOGIC SYMBOLS \newcommand{\EX}[2]{\mbox{$\exists #1\cdot#2$}} \newcommand{\ALL}[2]{\mbox{$\forall #1\cdot#2$}} \newcommand{\Not}{\mbox{$\neg$}} \newcommand{\And}{\mbox{$\wedge$}} \newcommand{\Or}{\mbox{$\vee$}} \newcommand{\Implies}{\mbox{$\Rightarrow$}} \newcommand{\Iff}{\mbox{$\Leftrightarrow$}} \newcommand{\Def}{\mbox{$\Leftrightarrow_{\mbox{\rm\tiny DEF}}$}} \newcommand{\Defeq}{\mbox{$=_{\mbox{\rm\tiny DEF}}$}} \newcommand{\False}{\mbox{{\sf false}}} \newcommand{\True}{\mbox{{\sf true}}} % LINEAR LOGIC SYMBOLS \newcommand{\TP}{\mbox{$\otimes$}} \newcommand{\TS}{\mbox{$+$}} \newcommand{\MTRUE}{\mbox{{\bf 1}}} \newcommand{\MFALSE}{\mbox{$\bot$}} \newcommand{\DP}{\mbox{$\times$}} \newcommand{\DS}{\mbox{$\oplus$}} \newcommand{\ATRUE}{\mbox{$\top$}} \newcommand{\AFALSE}{\mbox{{\bf 0}}} \newcommand{\WHYNOT}{\mbox{{\bf ?}}} \newcommand{\WHY}[1]{\WHYNOT#1} \newcommand{\OFCOURSE}{\mbox{{\bf !}}} \newcommand{\OFC}[1]{\OFCOURSE#1} % NEGATION \newcommand{\N}[1]{\mbox{$#1^{\bot}$}} % INDEXED ATOMIC FORMULA \GIA{atom}{holes}{indexlist} \newcommand{\IA}[3]{\mbox{${#1}{}^{^{#2}}\hspace{-.1cm}\langle#3\rangle$}} % INDEXED FORMULA \IF{formula}{holes} \newcommand{\IF}[2]{\mbox{${}^{#2}(#1)$}} % SEQUENT SYMBOLS \newcommand{\G}{\mbox{$\Gamma$}} \newcommand{\D}{\mbox{$\Delta$}} % PI for proofs PII Arilds strange symbol \newcommand{\PI}{\mbox{\normalsize$\pi$}} \newcommand{\PII}[1]{\mbox{${}^{\mbox{\normalsize $\pi_{#1}$}}\stackrel{\mbox{\normalsize .}}{:}$}} % LINKS \newcommand{\LI}[2]{\mbox{$(#1,\{#2\})$}} % general link \newcommand{\LP}[1]{\mbox{$(#1)$}} % partial link % PROOFS FOR SOME SEQUENT \newcommand{\PROOF}[1]{\mbox{$\Pi(#1)$}} % WIRINGS FOR SOME SEQUENT \newcommand{\WIR}[1]{\mbox{$\Omega(#1)$}} % ORDERING ON WIRINGS \newcommand{\ORDER}{\mbox{$\sqsubseteq$}} % USED TO INDEX GIRARDS ORIGINAL PROOF RULES \newcommand{\GIRARD}{\mbox{$_{\mbox{\rm\tiny GIRARD}}$}} % USED TO INDEX OUR PROOF RULES \newcommand{\PLL}{\mbox{$_{\mbox{\rm\tiny PLL}}$}} % vertical ldots \newcommand{\VDOTS}{\mbox{$\stackrel{\mbox{\normalsize .}}{:}$}} % linksymbol for wiring schemes \newcommand{\LINK}{\mbox{$\bullet$}} \newcommand{\ANTILINK}{\mbox{$\circ$}} % Join on wirings \newcommand{\WJ}{\mbox{$\sqcup$}} % Meet on wirings \newcommand{\WM}{\mbox{$\sqcap$}} % To join wirings in the CD? rule instantiations must be cancelled. % \CAN{set of indexed atoms}{index} \newcommand{\CAN}[2]{\mbox{$#1\backslash\hspace{-.1cm}{}^{#2}$}} \newcommand{\ATOMS}[1]{\mbox{{\sf atoms}$(#1)$}} % kind of an indexed atom \newcommand{\KIND}[1]{\mbox{{\sf kind}$(#1)$}} % lock and redundancy \newcommand{\LOCK}[1]{\mbox{{\sf lock}$(#1)$}} \newcommand{\RED}[1]{\mbox{{\sf red}$(#1)$}} % related atomic occurrences \newcommand{\REL}[1]{\mbox{{\sf rel}$(#1)$}} % analysis finished \newcommand{\OK}{\mbox{$\surd$}} % related atomic occurrences \newcommand{\INH}[2]{\mbox{$\downarrow_{#1}\hspace{-.1cm}(#2)$}} \newcommand{\SYN}[2]{\mbox{$\uparrow_{#1}\hspace{-.1cm}(#2)$}} %%%%%%%%%%%%%%%%%%% % MODIFICATION OF thebibliography FROM article.sty \newcounter{ENUMI} \def\BIB#1{\list {[\arabic{enumi}]}{\settowidth\labelwidth{[#1]}\leftmargin\labelwidth \advance\leftmargin\labelsep \setcounter{ENUMI}{\value{enumi}} \usecounter{enumi}\addtocounter{enumi}{\value{ENUMI}}} \def\newblock{\hskip .11em plus .33em minus .07em} \sloppy\clubpenalty4000\widowpenalty4000 \sfcode`\.=1000\relax} \let\endBIB=\endlist %%%%%%%%%%%%%%%%%%%%%% \begin{document} \title{Propositional linear logic : wiring semantics } \author{\normalsize\MEG\and\normalsize\HRJ\and\normalsize\EM\and\normalsize\AW} \date{University of Oslo, \today} \maketitle \begin{center} {\small - - - \ S U B M I T T E D \ T O \ I N F O R M A T I O N \ P R O C E S S I N G \ L E T T E R S \ - - - } \end{center} {\bf Keywords : theory of computation, semantics of proofs, concurrency} \subsubsection*{Introduction} We present a system, PLL, for (classical) propositional linear logic. PLL is rule equivalent with the original propositional linear logic given by Girard~\cite{GIRARD}. As a prerequisite for the definition of wiring semantics a technique for uniquely indexing formulas, sequents, and proofs are developed. Then wiring semantics is defined and a completeness result established. The completeness result shows a close correspondence between proofs and wirings. In future research we will investigate how wirings can be applied, but we find the wiring semantics interesting in it self, thus this paper. \subsubsection*{PLL}\label{SEC:PLL} \G,\D,\ldots\ are sequents, $A,B,\ldots$ are well-formed formulas, $a,b,\ldots$ are atoms (or propositions) and $\N{a},\N{b},\ldots$ are their duals. An atom and its dual are both literals. The class of well-formed formulas is generated as usual. When a context of a rule is written as ``\WHY{\G},\D'' it means that there are no occurrences of formulas with ``\WHYNOT'' as their main symbol in ``\D'', and that all formulas in ``\WHY{\G}'' have ``\WHYNOT'' as their main symbol. The negation symbol \N{(.)} is a meta symbol defined through De Morgan equalities (in the obvious way). We write the connectives $\TP, \TS$ (multiplicative), $\DP, \DS$ (additive) and $\WHYNOT, \OFCOURSE$ (exponential). The formulas in a sequent may be permuted (exchanged) freely. \[ \PSL{Ax}{}{a,\N{a}} \ \ \ \ \ \ \ \PSL{\TP} {\G_{1},\WHY\D,A \SP \G_{2},\WHY{\D},B} {\G_{1},\G_{2},\WHY{\D},A\TP B}\ \ \ \ \ \ \ \PSL{\TS} {\G,A,B} {\G,A\TS B} \ \ \ \ \ \ \ \] \[ \PSL{\DP} {\G,A\SP \G,B} {\G,A\DP B} \ \ \ \ \ \ \ \PSL{\DS $i$} {\G,A_{i}} {\G,A_{1}\DS A_{2} } \ \ \ \ \ \ \ %\] % % %\[ \PSL{\OFCOURSE} {\WHY{\G}, A} {\WHY{\G}, \OFC{A}}\ \ \ \ \ \ \ \PSL{W\WHYNOT} {\G} {\G, \WHY{A}} \ \ \ \ \ \ \ \PSL{CD\WHYNOT} {\G, A, \WHY{A}} {\G, \WHY{A}} \] This system is rule equivalent with~\cite{GIRARD} and for both systems cut elimination and interpolation theorems can be proved. The systems are equally expressive, but PLL seems to offer better control over the copying of formulas, c.f.\ the CD\WHYNOT\ rule. As usual the system PLL defines the $\vdash$ relation and \PROOF{\G} denotes the class of all proofs for the sequent \G. (The logic constants and the CUT rule heve been left out here but cause no difficulty for the wiring semantics.) \subsubsection*{Indexed formulas, sequents, and proofs} We define a technique for indexing each occurrence of a literal in a formula, sequent, or proof in a unique way, such that each occurrence is given a unique name (i.e.\ index). This is needed to define the wiring semantics. Indexed literals are of the form: $\IA{a_{k}}{n}{\phi}, \IA{\N{a_{l}}}{m}{\psi}, \ldots$, where $k,l,\ldots$ are the main indexes, $m,n,\ldots$ are the `numbers of holes', and $\phi,\psi,\ldots $ are the instantiation lists, i.e.\ lists of numbers. In adding new items to an instantiation list we shall use `.' as the append operator. ${\sf last}(\phi)$ is the last item added to $\phi$ (and $0$ if $\phi$ is empty). When an indexed literal has the form \IA{a_{\alpha}}{0}{} we write it simply as $a_{\alpha}$. An indexed literal \IA{a_{\alpha}}{i}{\phi} is said to have the kind $a$, and $\KIND{\IA{a_{\alpha}}{i}{\phi}}\ \Defeq\ a$. The indexed form $\IF{A}{0}$ of a formula $A$ is found by applying the following rules : \[ \begin{array}{ll} \IF{\WHY{A}}{n} \mapsto \WHY{\IF{A}{n+1}} & \ \ \ \ \ \ \ \IF{\OFC{A}}{n} \mapsto \OFC{\IF{A}{n}} \\ \IF{A*B}{n} \mapsto \IF{A}{n}*\IF{B}{n} & \ \ \ \ \ \ \ \IF{a}{n} \mapsto \IA{a_{k}}{n}{} \end{array} \] where $*\in\{\TP,\TS,\DP,\DS\}$ and $k$ is a new unique index. A sequent is indexed by indexing each of its formulas in turn. \ATOMS{\G} is the set of all indexed literals in the sequent \G. A proof is indexed by first indexing the sequent in the root and then successively indexing each node in the proof tree from the root and up. Each CD\WHYNOT\ node in the proof tree is indexed in the following way by replacing applications of CD\WHYNOT\ with the rule for indexed proofs: \Rule{CD\WHYNOT I} {\G, A[\alpha], \WHY{A}} {\G, \WHY{A}} $\alpha$ is a unique index for different applications of the rule. No other rules introduces new indexed formulas. In applications of the CD\WHYNOT I rule, indexed formulas are instantiated in the following way: \[ \begin{array}{ll} (\WHY{A})[\alpha] \mapsto \WHY{(A[\alpha])} & \ \ \ \ \ \ \ (\OFC{A})[\alpha] \mapsto \OFC{(A[\alpha])} \\ (A*B)[\alpha] \mapsto (A[\alpha])*(B[\alpha]) & \ \ \ \ \ \ \ (\IA{a_{k}}{n}{\phi})[\alpha] \mapsto \IA{a_{k}}{n-1}{\phi.\alpha},\ \ n>0 \end{array} \] We have the following five invariants on indexed proofs: (i) literals of the same kind in any sequent in an indexed proof are uniquely indexed; (ii) there is at most one occurrence of a formula \WHY{A} with the same index on its literals in an indexed sequent; (iii) in the root sequent all instantiation lists of atoms are empty; (iv) in the Ax-leafs the `number of holes' are 0 for all atoms; (v) if \IA{a_{\alpha}}{n}{} occurs in the root sequent of an indexed proof, then for each occurrence of \IA{a_{\alpha}}{i}{\phi} in the proof it holds that $i+\mbox{\sf length}(\phi)=n$. In the sequel we understand that all literals occurring in formulas, sequents, and proofs are indexed. \subsubsection*{Wiring semantics}\label{SEC:WIRSEM} We show that PLL is sound and complete with respect to wiring semantics. Wiring semantics for instance identifies unessential differences (i.e. permutations) among proof objects and can be applied to guide the search for proofs. A link is a pair $(a,s)$ such that $a$ is an atom and $s$ is a set of atoms dual to $a$. In its most general form, a link has the form $\LI{a}{b,c,\ldots}$ where $a,b,c,\ldots$ are atoms and $\KIND{a}$ is the dual of each of $\KIND{b},\KIND{c},\ldots$. If the set is empty, then $(a,\emptyset)$ is called a partial link, sometimes written as $(a)$. \begin{definition}[Wiring for a sequent]\label{DEF:WIRING} Let \G\ be a sequent. A wiring $\omega$ for \G\ is a finite set of links $(a,s)$, $a\in\ATOMS{\G}$, $s\subseteq\ATOMS{\G}$, such that for each $a\in\ATOMS{\G}$ there is exactly one link $(a,s)\in\omega$, and for $(a,s),(\N{a},t)\in \omega$: If $\N{a}\in s$, then also $a\in t$. \end{definition} \noindent \WIR{\G} denotes the set of all wirings for the sequent \G. Essentially a wiring is just a symmetric relation between indexed literals. \WIR{\G} can be assigned a partial order to become a complete finite lattice, but pursuing this will bring us off the track. We now give a recursive definition of $\omega(\PI)$ as $\omega(\PI)\Defeq\INH{r}{.}$ relative to the rules of PLL. For this definition we need the `generalized join' and `cancellation' operations defined below. Let $\omega_{1},\omega_{2}\in\WIR{\G}$. Define the generalized join, $\omega_{1} \WJ \omega_{2}$, to be \[ \omega_{1}\WJ\omega_{2}\ \Defeq\ \begin{array}[t]{l} \{ (a, s\cup t)| (a,s)\in\omega_{1}, (a,t)\in\omega_{2}\}\ \cup\\ \{ (a, s)\in\omega_{1}|(a,t)\not\in\omega_{2}\}\ \cup\\ \{ (a, t)\in\omega_{2}| (a,s)\not\in\omega_{1}\} \end{array}\] Let $\alpha$ be the index in an application of a CD\WHYNOT I rule and let $s\subseteq\ATOMS{\G,A[\alpha],\WHY{A}}$. The cancellation operation \CAN{s}{\alpha} (`cancel the $\alpha$-instantiation in $s$') is defined as follows \[ \CAN{s}{\alpha}\ \Defeq\ \{ \IA{b_{\beta}}{i+1}{\phi}\ |\ \IA{b_{\beta}}{i}{\phi.\alpha}\in s \}\ \cup\ \{ \IA{b_{\beta}}{i}{\phi}\in s\ |\ \mbox{\sf last}(\phi)\neq\alpha \} \] Let $\pi_{1}$ and $\pi_{2}$ denote the left and right branches of the proof tree, respectively (if there is only one branch, we take it to be the `left'). \[ \begin{array}{l} \INH{Ax}{}\ \Defeq\ \{\LI{\IA{a_{i}}{0}{\phi}}{\IA{\N{a_{j}}}{0}{\psi}}, \\ \INH{\TP}{\omega(\PI_{1}),\omega(\PI_{2})}\ \Defeq\ \omega(\PI_{1})\ \WJ\ \omega(\PI_{2}) \\ \INH{CD\WHYNOT}{\omega(\PI_{1})}\ \Defeq\ \ \{\ (\IA{a_{\beta}}{i}{\phi},\CAN{s}{\alpha}\cup\CAN{t}{\alpha}) \ |\ (\IA{a_{\beta}}{i}{\phi},s),(\IA{a_{\beta}}{i-1}{\phi.\alpha},t) \in\omega(\PI_{1})\ \}\ \cup \\ \SP\SP\SP\{\ (\IA{a_{\beta}}{i}{\phi},\CAN{s}{\alpha}) \ | \ (\IA{a_{\beta}}{i}{\phi},s)\in\omega(\PI_{1}),\ (\IA{a_{\beta}}{i-1}{\phi.\alpha},t)\not\in\omega(\PI_{1}),\ \mbox{\sf last}(\phi)\neq\alpha\ \} \\ \INH{\TS}{\omega(\PI_{1})}\ \Defeq\ \omega(\PI_{1}) \\ \INH{\DS}{\omega(\PI_{1})}\ \Defeq\ \omega(\PI_{1})\ \cup\ \{ \LP{\IA{c_{\alpha}}{i}{\phi}}\in\ATOMS{A_{2}}\} \\ \INH{\DP}{\omega(\PI_{1}),\omega(\PI_{2})}\ \Defeq\ \omega(\PI_{1})\ \WJ\ \omega(\PI_{2}) \\ \INH{\OFCOURSE}{\omega(\PI_{1})}\ \Defeq\ \omega(\pi_{1}) \\ \INH{W\WHYNOT}{\omega(\PI_{1})}\ \Defeq\ \omega(\PI_{1})\ \cup\ \{ \LP{\IA{a_{\alpha}}{i}{\phi}}\in\ATOMS{\WHY{A}}\} \end{array} \] $\omega(\pi)$ is called the characteristic wiring for $\pi$. It is easily verified that the characteristic wiring is unique for any proof $\pi$. \begin{definition}[Wiring model for a sequent]\label{DEF:MODELS}\ Let $\omega\in\WIR{\G}$. $\omega$ models \G\ (written $\omega \models \G$) if and only if (at least) one of the following cases hold: If \G\ has the form \begin{itemize} \item \it $a,\N{a}$ (Ax), then $ \{\LI{a}{\N{a}},\LI{\N{a}}{a}\}\models a,\N{a}$ \item $\G_{1},\G_{2},\WHY{\D},A\TP B$ (\TP), then $\omega\models \G_{1},\G_{2},\WHY{\D},A\TP B$ if there exists $\omega_{1}$ and $\omega_{2}$ such that $\omega=\INH{\TP}{\omega_{1},\omega_{2}}$ and %% \[ $ \omega_{1}\models \G_{1},\WHY{\D},A\ \ \ \ \ \mbox{\rm and}\ \ \ \ \ \omega_{2}\models \G_{2},\WHY{\D},B. $ %%\] \item $\G_{1},\WHY{A}$ (CD\WHYNOT), then %%\[ $ \omega\models \G_{1},A,\WHY{A} $ %%\] if there exists $\omega_{1}$ such that $\omega=\INH{CD\WHYNOT}{\omega_{1}}$ and %%\[ $ \omega_{1}\models \G_{1},\WHY{A}. $ %%\] \item Cases for \TS,\DP,\DS,\OFCOURSE,W\WHYNOT\ are similar. \end{itemize} \end{definition} \begin{theorem}[Soundness]\label{THEO:SOUND} $ \pi\vdash\G\ \Implies\ \omega(\pi)\models\G. $ \end{theorem} \begin{Proof} The proof is by induction over $\G$. Base case is for (Ax), and follows from the properties of $\vdash$ and $\models$: \[ \left(\PAW {\ \\ \hline a,\N{a}}\right) \vdash a,\N{a} \ \ \ \ \ \Implies\ \ \ \ \ \{\LI{a}{\N{a}},\LI{\N{a}}{a}\}\models a,\N{a}\ \ \ \ \ \] The induction hypothesis is (S) $\pi\vdash\G\ \Implies\ \omega(\pi)\models\G$. The induction step involves one case for each possible active formula of \G. We show the proof just for the case (\TP): Assume that $\PI\vdash\G_{1},\G_{2},\WHY{\D},A\TP B$. Then by the definition of `$\vdash$' we have $\PI_{1}\vdash\G_{1},\WHY{\D},A$ and $\PI_{2}\vdash\G_{2},\WHY{\D},B$. By (S) this gives $\omega(\PI_{1})\models\G_{1},\WHY{\D},A$ and $\omega(\PI_{2})\models\G_{2},\WHY{\D},B$. Thus $\INH{\TP}{\omega(\PI_{1}),\omega(\PI_{2})}\models \G$ by the definition of `$\models$'. All other cases are similar. \end{Proof} \begin{theorem}[Completeness] $ \omega\models\G\ \Implies\ \EX{\PI \in \PROOF{\G} }{ \PI \vdash \G }. $ \end{theorem} \begin{Proof} The proof is by induction over $\G$. The base case is similar to the one in the proof of soundness~(\ref{THEO:SOUND}). The induction hypothesis is (C) $\omega\models\G\ \Implies\ \EX{\PI \in \PROOF{\G}}{\PI \vdash \G}$. As in the proof of soundness there is one case for each possible `active' formula in \G. We just show the case for (CD\WHYNOT): Assume that $\omega\models\G_{1},\WHY{A}$. Then by the definition of `$\models$' we have $\omega_{1}\models\G_{1},A,\WHY{A}$. By (C) this gives that there exists $\PI_{1}\vdash\G_{1},A,\WHY{A}$ and thus \[ \left(\PAW {\PII{1}\\ \G_{1},A,\WHY{A} \\ \hline \G_{1},\WHY{A} }\right) \vdash \G. \] All other cases are similar. \end{Proof} \subsubsection*{Future work: applications of wiring semantics}\label{SEC:FUTURE} Currently we are investigating proof theoretical aspects of propositional linear logic, and as part hereof the invariance of wirings under permutation of rules. For instance we have established, that if $\pi_{1} \vdash \G$ and $\pi_{2} \vdash \G$ and if $\pi_{1}$ is a permutation of $\pi_{2}$ then $\omega(\pi_{1}) = \omega(\pi_{2})$. From a proof theoretical point of view this result is interesting since it suggests a close relationship to the proof nets defined by Girard~\cite{GIRARD}. We also consider automated proof search, and apply wirings to prune the search space: criterias for cutting branches in the search space can be defined by using wirings. Based on wirings modes of `lock' and `redundancy' in a sequent can be characterized. For instance the sequent $\G,a\TP\N{a}$ contains a lock if $a$ and \N{a} is connected and the sequent $a,\N{a},b$ contains redundancy for all possible wirings because there is no way to get rid of the literal $b$. A necessary condition for a sequent to be provable is that it is free for both lock and redundancy. As a consequence of the undecidability~\cite{LMSS} of propositional linear logic we will not be able to find a sufficient condition for provability. The interesting thing to investigate is how effective proof search can become in the light of the results reported in~\cite{LMSS}. Another thing will be to compare wiring semantics with already known semantics. The wiring semantics is a very weak and simple semantics which might be able to reflect hitherto undiscovered features of propositional linear logic. In particular we see a strong connection between propositional linear logic as a calculus of `resources' and wiring semantics. \subsubsection*{References} \begin{BIB}{WW} \bibitem{GIRARD} Jean-Yves Girard. {\em Linear Logic}. Theoretical Computer Science 50 (1987) pp.\ 1-102. \bibitem{LMSS} Patrick Lincoln, John Mitchell, Andre Scedrov, Natarajan Shankar. {\em Decision problems for propositional linear logic}. Proc.\ 31st annual IEEE symposium on foundations of computer science, St.\ Louis, Missouri, October, 1990. \end{BIB} \end{document}