Martin-Löf için bir teklif kanıtı neyin nesi?

Martin-Löf'in felsefi mantık çalışmalarındaki bir önermenin kanıtı kavramı, kavramsal olarak gerçeğin nosyonundan önce - cf " Bir önermenin Gerçeği, bir kararın kanıtı, kanıtın geçerliliği "(s.414). Ancak, bildiğim kadarıyla, hiçbir zaman açık bir felsefi açıklama yapmamıştı.

Peki Martin-Löf için bir teklifin kanıtı nedir? Genel olarak, soruyu şu şekilde belirleyebiliriz:

  • Martin-Löf için bir tür terim nedir?

(Curry-Howard veya önerilerin yazışmaları gibi).

3
$ A $ teklifinin bir kanıtı, bu karar hakkındaki bilgi olan "$ A $ true" kararının bir kanıtıdır.
katma yazar binco, kaynak
Bu makaleye bir göz atın pps .univ-paris-diderot.fr/~ saurin/Enseignement/LMFI/articles & zwnj;/& hellip; . İspatın bu felsefi tanımının döngüselliğe yol açtığını ve yapıcı olmadığını (aslında sezgisel bile değil) söylemesine de değinmeliyim, ancak teori iyi işliyor (sadece felsefi temeller teoriye uygun değil)
katma yazar binco, kaynak
Bu, şu an için kırık değil: andrew.cmu.edu /user/ulrikb/80-518-818/MartinLof83.pdf . Dokümanın sayfa 9-10'a bakın (ve makalenin değil). Özel ilgi, "Bir yargıyı kanıtlayan bir kanıttır", "kanıtlamak = bilmek, anlamak, kavramak veya görmek."
katma yazar binco, kaynak
Yuvarlaklık hakkında, bu benim bir türetme değil (benim bir arkadaşım bunu önce elde etti ve bu arada yayınlanmadı). Daha fazla zamana sahip olduğumda yazabilirim, ama özünde böyle bir nesne hakkındaki bilgiyle bir nesnenin tanımlanmasıyla ilgili. Sezginin başarısızlığı ile ilgili olarak, $ \ neg \ neg A $ 'nın bazı bireylerin bakış açısından $ A $ kanıtı olduğunu ve bu nedenle de $ A $' lık bir kanıt olduğunu iddia edebiliriz. Sorun şu ki, bu kavramların anlamı ne olursa olsun, inşa etmek için tam olarak aynı şey değildir.
katma yazar binco, kaynak
Daha genel olarak, tüm bu problemlerin gerçekliğin ve geliştirilebilirliğin tanımlanmasından kaynaklandığı söylenebilir (örneğin ilk Gödel eksiklik teoremi ile karşılaştırılabilir).
katma yazar binco, kaynak
@ user40276 Bunu nasıl sonuçlandırabilirsin? 'A'nın doğruluğu' kanıtının (ya da kanıtının) bir önermenin bir kanıtı olduğunu görebiliyorum.
katma yazar Stephen Gaunt, kaynak
@ user40276 Üzgünüz, bağlantı bozuk. <�İ> Mantıksal sabitlerin anlamları ve mantıksal yasaların gerekçeleri üzerine mi demek istiyorsun? Eğer öyleyse, buna nispeten aşinayım. Peki, aklınızdaki pasajların tam olarak nerede olduğunu belirtebilir misiniz? Bu tartışmalı ama ilginç sonucun nasıl çekildiğini duymak isterim, eğer daha spesifik olabilirse (ve zaman geçirebilseydi).
katma yazar Stephen Gaunt, kaynak

1 cevap

Martin-Löf'in bu konuyla ilgili kısa bir makalesi var.

Kant and Contemporary Epistemology, Volume 54 of the series The University of Western Ontario Series in Philosophy of Science pp 87-99. Analytic and Synthetic Judgements in Type Theory, Per Martin-Löf

İddia ediyor

Dolayısıyla, yargının olağan biçimi, A, doğrudur, gerçekte varoluşçu yargı biçiminin özel bir örneğidir.

He relies thus on the intuitionist explanation of truth, [...], defined as existence of a proof, or construction, of the proposition.

Ve orada, sentetik yargılama biçimlerinin varoluşçu yargı biçimleri olduğunu söylüyor.

Metni kopyalayıp yapıştıramayacağımızdan, size alakalı sayfaların resmini vereceğim.

Analytic and Synthetic Judgements in Type Theory, Per Martin-Löf

Türleri olmayan bir başka makale ise Michael Dummett 1998'in C ve K İlkeleri Üzerindeki Gerçek ve Bilmeye Uygunluk Yargılar, önermeler, gerçekler ve kanıtlar arasında açıkça ayrım yapar.

tüm bu makaleler

https://github.com/michaelt/michaelt.github. io/ağaç/ana/martin-lof

2
katma
Teşekkürler. İlk makaleye aşinayım ve bu gerçek Martin-Löf'in başarılabilirliği ile tanımlanıyor. Yine de ilgilendiğim şey, bir yargı değil - tam olarak bir "teklifin kanıtı" nın onun için ne olduğunu bilmek. Bunun için bir fikrin var mı?
katma yazar Stephen Gaunt, kaynak