可證性邏輯的發(fā)展史研究.pdf

1、直覺主義數(shù)學(xué)對邏輯聯(lián)接詞和量詞的解釋依賴于“構(gòu)造性”等不精確的概念，因而不是嚴(yán)格構(gòu)造性的，這不同于形式可證性概念。哥德爾想嘗試用嚴(yán)格構(gòu)造性的證明概念來代替，他希望實(shí)現(xiàn)一種放寬條件的希爾伯特綱領(lǐng)，構(gòu)造同時具有直覺主義的構(gòu)造性特征和有窮主義特點(diǎn)的形式可證性邏輯。可證性邏輯為困擾已久的自指概念提供了新的研究工具，另外，可證性研究了數(shù)學(xué)上許多重要的結(jié)論（如哥德爾第二不完全性定理）。沿著哥德爾的思想，后來的邏輯學(xué)家也作了很多相關(guān)研究，阿提莫夫的證

2、明邏輯是比較有代表性的研究成果。本文就主要對可證性邏輯發(fā)展史進(jìn)行研究，全文由四章構(gòu)成。
　　第一章：直覺主義邏輯BHK的解釋。本章首先介紹了直覺主義流派的主要思想，并將直覺主義邏輯與經(jīng)典邏輯的不同點(diǎn)進(jìn)行分析；然后描述了直覺主義命題邏輯和一階謂詞邏輯系統(tǒng)，并在此基礎(chǔ)上得出直覺主義邏輯BHK的解釋。
　　第二章：哥德爾的可證性邏輯。本章首先介紹了哥德爾的主要理論成果，以了解哥德爾可證性邏輯的歷史背景；然后具體分析哥德爾的可證性邏

3、輯系統(tǒng)，它克服了直覺主義數(shù)學(xué)的非構(gòu)造性特點(diǎn)，是介于直覺主義數(shù)學(xué)與古典數(shù)學(xué)之間的邏輯系統(tǒng)。
　　第三章：Logic of proofs?？勺C性（Provability）研究的兩個新方向：一個是由S.Artemov在1994年發(fā)起的loqic of proofs（這是受到基礎(chǔ)關(guān)系以及給直覺主義邏輯提供強(qiáng)有力的可證性語義問題的鼓舞）；另一個是graded provability algebras,旨在為可證性邏輯在主流的證明理論傳統(tǒng)中建