Change search

Cite
Citation style
• apa
• ieee
• modern-language-association-8th-edition
• vancouver
• Other style
More styles
Language
• de-DE
• en-GB
• en-US
• fi-FI
• nn-NO
• nn-NB
• sv-SE
• Other locale
More languages
Output format
• html
• text
• asciidoc
• rtf
Identity of proofs
Stockholm University, Faculty of Humanities, Department of Philosophy.
2001 (English)Doctoral thesis, monograph (Other academic)
Abstract [en]

In the early seventies it was conjectured that a certain mathematically well-defined equivalence relation (bh-equivalence) on proofs in natural deduction captures the informal notion of identity of proofs. The conjecture can be divided into two parts, a soundness part and a completeness part. The soundness part is that bh-equivalent proofs are identical. The completeness part is that identical proofs are bh-equivalent. It is argued that soundness can not be mathematically proved. It must be taken for granted or rejected. Completeness, on the other hand, can not be taken for granted. It must be proved or disproved, although the question is not a mathematically precise question.

The main result of this thesis is that the completeness part of the conjecture is true for the system of minimal implicational logic, provided that soundness can be taken for granted. The result is obtained by first proving that the notion of bh-equivalence is Post-complete. Roughly, if bh-equivalence is extended by a new schematic rule for identifying proofs, then all proofs of the same theorem are identical. In other words, there is only one schematic extension of bh-equivalence, the trivial equivalence relation that identifies all proofs of a theorem. It is then argued that the identity relation on proofs is non-trivial, i.e. that there are non-identical proofs. This proves the completeness part of the conjecture.

The thesis also contains a new proof (for the above system) of so-called confluence and a conjecture characterizing bh-equivalence in a new way.

Place, publisher, year, edition, pages
Stockholm: Almqvist & Wiksell International , 2001. , p. 85
Series
Stockholm studies in philosophy, ISSN 0491-0877 ; 22
Humanities
Research subject
Theoretical Philosophy
Identifiers
ISBN: 9122019405 (print)OAI: oai:DiVA.org:su-81497DiVA, id: diva2:562109
Public defence
2001-10-20, 10:00
Opponent
Available from: 2012-10-23 Created: 2012-10-23 Last updated: 2017-09-27Bibliographically approved

Open Access in DiVA

No full text in DiVA

PDF (Not accessible to users outside Sweden)
By organisation
Department of Philosophy
Humanities

isbn
urn-nbn

Altmetric score

isbn
urn-nbn
Total: 655 hits

Cite
Citation style
• apa
• ieee
• modern-language-association-8th-edition
• vancouver
• Other style
More styles
Language
• de-DE
• en-GB
• en-US
• fi-FI
• nn-NO
• nn-NB
• sv-SE
• Other locale
More languages
Output format
• html
• text
• asciidoc
• rtf