定义8.4.7 　　假定├( =├ A1, A2,…, An) 是一个串形，对每一个中的公式 Aj, Aj* 是已经指派了 的近邻空间。串形├对应的近邻空间 (├ )* 定义为 　　（1）│(├ )*│ =│ A1*│×│ A2*│×…│ An*│ 　　（2）x1x2…xn︶y1y2…yn当且仅当j, xjyj。 　　注意到近邻空间 (├ )* 就是近邻空间A1*￡A2*￡…￡An* 。 　　现在给出演算系统中的任一证明在近邻空间中的解释：若π是一个证明过程，（ 从公理串形开始）它的结论是├ 。（通常对仅含一个公式的情形感兴趣。）π* 将是(├)*中的一个团体。 　　首先请注意公理本身是自己的证明。 定义8.4.8 　　（1） 恒等公理 ├ A, A┴ 对应于集合 { xx ; x∈│ A*│} 　　（2） cut 规则 令π是 ├, A 的证明，λ是 ├△,A的证明，通过 cut 规则，我们得到的串形是├,△。这形成├,△的证明ρ 。记住π*，λ*分别是 (├,A)*, (├△,A)*的团体，ρ *应是 (├,△)* 的团体，ρ *定义为：{ββ';z (βz∈π*∧zβ'∈ λ*)} , 这里β,β'分别是（├）*及 (├ △)* 的元素。 　　（3） 交换规则 若π是 ├的一个证明，'是中成员的位置交换结果。由此产生的├' 的证明ρ对应的团体ρ*= {δ(β) ;δ是该位置交换，β∈π*} 。 　　简单验证 （1）,（2）,（3） 中的集合ρ* 都是对应的近邻空间的团体。只要证明ρ*中的元素两两都有近邻关系。情形 1) ：注意到任给两个元素串 xx 及 yy , 根据定义, 若x 与 y 在A* 中不是近邻的，则它们一定在 (A┴)*中是近邻的，所以ρ*在A*￡ (A┴)* 是一个团体。情形 (2) 任给两个串形ββ',αα'∈ρ*, 若它们使用的联结元素z是不同的，假定是z1,z2, 则z1,z2 在其中一个情形A*或者(A┴)*必定是不近邻的，因而或者β与α近邻，或者β'与α'近邻，从而ββ'与αα'近邻。若 z1=z2, 由归纳假设，βz1与β'z1是近邻的，由此可推出β与β'是近邻的，从而ββ'与αα'是近邻的。 情形 (3) 容易。 　　用一个稍微复杂的归纳证明，可以知道，实际上，在情形 （2） 中的 z , 如果β及β'确定了， z 是唯一的。注意到在最基本的情形, 即 （1） 中，ρ*的元素都具 xx 的形式。这就决定了z的唯一性。 定义8.4.9 　　对于所有其他的规则，给出以该规则为"最后使用了的规则"的证明ρ*的近邻语义，同样ρ*必定是一个团体。 　　（1） 公理 ├ 1 解释为特殊的近邻空间 1 的团体 {0}。（ 0 是唯一的那个元素）。 　　（2） 公理 ├,T 解释为空间（├ , T ）*的空团体。 　　（3） false 规则 令π是 ├的证明，r 是 ├, ┴ 的以该规则结尾的证明，则定义ρ*= {β0;β∈π*} 。 　　（4） par 规则π是 ├, A, B 的证明，ρ是 ├ G, A￡ B 的证明，则ρ*= {β(y,z) ;βyz∈π* }。 　　（5） times 规则π是 ├, A ,λ是 ├, B 的证明，ρ是 ├, A B 的证明，则ρ*= {βy,z)α;βy∈π*, zα∈λ* }。 　　（6） lest plus 规则 令π是 ├, A的证明，ρ是 ├, A B 的证明，则ρ*= {β(y,0) ;βy∈π*} 　　（7） right plus 规则 令π是 ├, B 的证明，ρ是 ├, A B 的证明, 则ρ*= {β(y,1);βy∈π*}. 　　（8） with 规则π是 ├, A , λ是├, B 的证明，ρ是├, A& B 的证明, 则ρ*= {β(y,0) ;βy∈π*}∪{β(y,1);βy∈λ*}. 　　读者可尝试验证每一条款中定义的ρ*都是相应近邻空间的团体。 定义8.4.10 　　令 X , Y 是近邻空间，由 X到 Y 的映射 F 是线性的，如果 　　（1） 若 a X则 F (a) Y . 　　（2） 若∪bj = a X 则 F (a) =∪F (bj). 　　（3） 若 a∪b X, 则 F (a∩b) = F (a)∩F(b).