论文标题
命题逻辑模量同构中的扩展证明
Extensional proofs in a propositional logic modulo isomorphisms
论文作者
论文摘要
系统I是命题逻辑片段的一种证明语言，同构命题，例如$ a \ wedge b $和$ b \ wedge a $，或$ a \ rightarrow（b \ wedge c）$ and $（a \ rightarrow b）\ wedge（a \ rightarrow c）$相等。系统我喜欢强大的归一化属性。这足以证明存在空类型的存在，但不能证明引言属性（以正常形式的每个闭合术语都是简介）。此外，必须对变量的类型进行严格的限制，以获得空类型的存在。我们在这里表明，在系统中添加$η$ - expansion规则可以放弃此限制，并产生享有完整介绍属性的强烈正常化的微积分。
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 normalization 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 $η$-expansion rules to System I permits to drop this restriction, and yields a strongly normalizing calculus which enjoys the full introduction property.
