证明的一般性及其Brauerian表示
Generality of Proofs and its Brauerian Representation
摘要：
一个推导的一般性是一个关于变量在其前提和结论中出现的集合的等价关系，使得同一变量的两次出现在这个关系中当且仅当它们在推导的每一次一般化中都必须保持同一变量的出现。所讨论的变量是命题的或其他类型的。本文在范畴证明论的背景下，考察了两个具有相同前提和结论的导子表示相同证明的猜想当且仅当它们具有相同的一般性。为了这个目的，一般性被定义在一个范畴内，这个范畴的箭头是有限序数上的等价关系，在这个范畴中，合成是相当复杂的。几个例子给出了演绎系统的推导覆盖片段的逻辑，与相关映入范畴的等价关系的一般性。这个范畴同构地表示在其箭头是有限序数之间的二元关系的范畴中，其中复合是关系的通常的简单复合。这个表示与Richard Brauer的一个经典表示结果有关。
英文摘要：
The generality of a derivation is an equivalence relation on the set of occurrences of variables in its premises and conclusion such that two occurrences of the same variable are in this relation iff they must remain occurrences of the same variable in every generalization of the derivation. The variables in question are propositional or of another type. This paper examines in the setting of categorial proof theory the conjecture that two derivations with the same premises and conclusions stand for the same proof iff they have the same generality. For that purpose generality is defined within a category whose arrows are equivalence relations on finite ordinals, where composition is rather complicated. Several examples are given of deductive systems of derivations covering fragments of logic, with the associated map into the category of equivalence relations of generality. This category is isomorphically represented in the category whose arrows are binary relations between finite ordinals, where composition is the usual simple composition of relations. This representation is related to a classical representation result of Richard Brauer.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
