一种命题逻辑模同构的外延证明
Extensional proofs in a propositional logic modulo isomorphisms
AI总结：
本文通过向系统I添加η-展开规则，去除了变量类型限制，构造出兼具强归一化与完整引入性质的命题逻辑证明演算。
摘要：
系统I是一种针对命题逻辑片段的证明语言，在该片段中，同构的命题，例如$A\wedge B$与$B\wedge A$，或$A\Rightarrow(B\wedge C)$与$(A\Rightarrow B)\wedge(A\Rightarrow C)$，被视为相等。系统I具有强归一化性质。这足以证明空类型的存在性，但不足以证明引入性质（每个处于正规形式的闭项都是一个引入）。此外，为了获得空类型的存在性，必须对变量的类型施加严格的限制。我们在此证明，向系统I添加$η$-展开规则可以去除这一限制，并得到一个具有完整引入性质的强归一化演算。
英文摘要：
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.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
