定理8.4.1 　证明 只要证明 Tr(A(.)) =A以及 Tr(F)(.) = F 即可。这是一个按定义条款直接验证的证明。读者可尝试自行作出。 　　说明 　　(1) 关于线性逻辑的协调性和完备性，通常是用相对简单一些的相空间语义作出来的。证明思路与大部分的形式逻辑系统的协调性和完备性证明相类似。 　　(2) 近邻空间语义主要揭示出线性逻辑的证明自身结构的完美性：（a） 每一可证公式A的证明，是A的语义结构A* 中一个特殊的子集π* , (一个团体)。（b）一个形为AB 的公式的证明，对应于由A*到B *的一个线性映射。"线性逻辑"的名称由此而来。（c）重要之处是要证明一个公式A , 在公式A内部所含的信息资源中寻找即可，不用外部资源。这可以拿经典命题逻辑中的语义判断作一个比较, 令A是一个CNF， 含 n 个文字，（ 一个文字是一个原子命题或原子命题的否定）为了在赋值意义下证明A是永真公式，从理论上说，需要 2n 个长度为 n 的，由 {0,1} 组成的序列，而A在每一个序列上都取值 1 , 这样才得到A为永真的证明。而线性逻辑中的公式A , 它是可证的当且仅当近邻空间 A* 中存在一个团体，这个团体既是A的证明。这个性质是其他的逻辑系统所没有的。 　　(3) 证明论专家普遍认为，线性逻辑系统的证明是最类似"算法"的语义对象，将为计算机科学，特别是并行算法提供一个新的、有力的工具。