Herbrand Expansions and Extraction of Proofs from Diagrams

Studies in Logic, Vol. 16, No. 3 (2023): 53–88   PII: 1674­3202(2023)­03­0053­36

Matthias Baaz      Norbert Preining

Abstract. 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 cut­free proofs with elementary expense and vice versa. This means, that diagrams are a valid and complete proof tool, however diagrams may be non­elementarily 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.