Text

E-book Advances in Proof-Theoretic Semantics

---

Penilaian

---

Both Heyting and Gentzen approached questions of meaning in relation to whatit is to prove something, but as seen from the above, their approaches were stillvery different. Gentzen was concerned with what justifies inferences and therebywith what makes something a valid form of reasoning. These concerns were absentfrom Heyting’s explanations of mathematical propositions and assertions. The con-structions that Heyting refers to in his meaning explanations, called proofs in theBHK-interpretation, are mathematical objects, naturally seen as belonging to a hier-archy of effective operations as suggested by Kreisel. They are not proofs built upfrom inferences. Nor does a proof in Heyting’s sense, the realization of an intendedconstruction, constitute a proof built up of inferences, although it does constitutewhat is required to assert the proposition in question. As was later remarked byHeyting (1958) [8], the steps taken in the realization of the intended construction, inother words, in the construction of the intended object, can be seen as correspondingto inference steps in a proof as traditionally conceived.These differences between what I am calling BHK-proofs and Gentzen proofsdo not rule out the possibility that the existence of such proofs nevertheless comesmaterially to the same. For instance, a BHK-proof of an implicationA?Bis definedas an operation that takes a BHK-proof ofAinto one ofB, and a closed Gentzen proofofA?Baffords similarly a construction that takes a Gentzen proof ofAinto oneofB; the latter holds because the validity of a closed deduction ofA?Bguaranteesa closed valid deduction in canonical form (by principle II when seen as a clause inan inductive definition) containing a valid deduction ofBfrom the assumptionA(principle I), which gives rise to a closed valid deduction ofBwhen a closed valid deduction ofAis substituted for the assumption (principle III). Such similarities maymake one expect that one can construct a BHK-proof given a Gentzen proof and viceversa.However, the ideas of Gentzen discussed above are confined to a specific formalsystem with particular elimination rules associated with reductions, while there isno comparable restriction of the effective operations that make up a BHK-proof. Itis easily seen that for each (valid) deduction in that system there is a correspondingBHK-proof (provided that there are BHK-proofs corresponding to the deductionsof atomic sentences), but the converse does not hold. For instance, there is a BHK-proof (over the set of proofs of arithmetical identities) of the conclusion obtained byan application of mathematical induction if there are BHK-proofs of the premisses,but there is no corresponding valid deduction unless we associate a reduction toapplications of mathematical induction. If Gentzen proofs are to match BHK-proofs,Gentzen’s ideas have first to be generalized, making them free from any particularformal system.

---

Ketersediaan

Informasi Detail

Judul Seri

-

No. Panggil

511.3 PE a

Penerbit

Switzerland : Springer Nature., 2016

Deskripsi Fisik

281 hlm

Bahasa

English

ISBN/ISSN

9783319226866

Klasifikasi

511.3

Tipe Isi

text

Tipe Media

computer

Tipe Pembawa

online resource

Edisi

-

Subjek

Mathematical Logic

Info Detail Spesifik

-

Pernyataan Tanggungjawab

-

Versi lain/terkait

Lampiran Berkas

Komentar

---

Anda harus masuk sebelum memberikan komentar