Axiomatic Thinking, Identity of Proofs and the Quest for an Intensional Proof-Theoretic Semantics

Peter Schroeder-Heister ()
Additional contact information
Peter Schroeder-Heister: University of Tübingen, Department of Computer Science

Chapter Chapter 8 in Axiomatic Thinking I, 2022, pp 145-163 from Springer

Abstract: Abstract Starting from Hilbert’s Axiomatic Thinking, the problem of identity of proofs and its significance is discussed in an elementary proof-theoretic setting. Identifying two proofs, one of which is obtained from the other one by removing redundancies, leads, when used as a universal method, to a collapse of all proofs of a provable proposition into one single proof and thus trivialises proof identity. Principles of proof-theoretic harmony with restricted means of redundancy reduction might be used instead, though this limits one to a certain format of formal systems. The discussion of proof identity suggests the claim that annotations of proofs telling the reader which rule is applied at a particular step, must be considered part of the proof itself. As a general perspective, it is advocated that the investigation of intensional aspects of proofs should be given more space in proof theory and proof-theoretic semantics.

Date: 2022
References: Add references at CitEc
Citations:

There are no downloads for this item, see the EconPapers FAQ for hints about obtaining it.

Related works:
This item may be available elsewhere in EconPapers: Search for items with the same title.

Export reference: BibTeX RIS (EndNote, ProCite, RefMan) HTML/Text

Persistent link: https://EconPapers.repec.org/RePEc:spr:sprchp:978-3-030-77657-2_8

Ordering information: This item can be ordered from
http://www.springer.com/9783030776572

DOI: 10.1007/978-3-030-77657-2_8

Access Statistics for this chapter

More chapters in Springer Books from Springer
Bibliographic data for series maintained by Sonal Shukla () and Springer Nature Abstracting and Indexing ().