System I is a proof language for a fragment of propositional logic where isomorphic propositions, such as $A\wedge B$ and $B\wedge A$, or $A\Rightarrow(B\wedge C)$ and $(A\Rightarrow B)\wedge(A\Rightarrow C)$ are made equal. System I enjoys the strong normalisation property. This is sufficient to prove the existence of empty types, but not to prove the introduction property (every closed term in normal form is an introduction). Moreover, a severe restriction had to be made on the types of the variables in order to obtain the existence of empty types. We show here that adding $\eta$-expansion rules to System I permits to drop this restriction, and yields a strongly normalizing calculus with enjoying the introduction property.

翻译：系统I 是一个证据性语言, 用于证明存在不固定的参数逻辑的片段, 其中, 诸如 $A\wege B$ 和 $B\wege A$, 或 $A\Rightrowr (B\wege C) 和$(A\Rightrow B)\wedge (A\Rightrowr C) 等变量, 或 $A\Rightrowr (B\wedge) 和$(A\Rightrowr B)\wedge (A\Rightrowr C) 等。 系统I 拥有强大的正常化属性。 这足以证明存在空型号, 但却不能证明引入属性( 通常的每个封闭期都是导言 ) 。 此外, 为了获得空型, 必须对变量的类型做出严格的限制 。 我们在此显示, 将 $\ a$ Exacion 规则添加到系统I 允许取消这一限制, 并产生高度正常化的计算 并享受引入属性 。