埃尔布朗扩展及来自图表的证明提取  

Herbrand Expansions and Extraction of Proofs from Diagrams

作　　者：马蒂亚斯·贝兹 诺伯特·普雷宁 Matthias Baaz;Norbert Preining(Institute of Discrete Mathematics and Geometry Vienna University of Technology;Mercari Inc.,Tokyo)

机构地区：[1]维也纳工业大学离散数学与几何研究所 [2]东京Mercari公司

出　　处：《逻辑学研究》2023年第3期53-88,共36页Studies in Logic

摘　　要：本文介绍射影几何中的图作为有效的证明工具。尽管图表用于支持对射影几何中证明的理解,它们本身不被视为证明。我们将表明图表可转换为无切割证明,反之亦然。这意味着,图表是种有效且完备的证明工具,然而图表可能比通常的使用切割规则的证明更复杂。作为这些分析的一个有趣结论,我们将证明,图表在逻辑意义上不是构造性的。This paper introduces diagrams in projective geometry as valid proving tools.Although diagrams are used to support the understanding of proofs in projective geometry,they are not considered as proofs themselves.We will show that diagrams can be transformed in cutfree proofs with elementary expense and vice versa.This means,that diagrams are a valid and complete proof tool,however diagrams may be nonelementarily more complex than usual proofs using lemmata(cuts).As an interesting consequence of these analyses we will demonstrate,that diagrams are not constructive in the logical sense.

关 键 词：射影几何 逻辑意义 构造性 图表 埃尔布朗 有趣 

分 类 号：B81-05[哲学宗教—逻辑学]