Дәлелдеме теориялық семантика: мағынаны дәлелдеу жүйесінде табу
Proof-theoretic semantics
Дәлелдік семантика: логикалық байланыстар мен ұсыныстар мағынасын интерпретация емес, дәлелдеу жүйесіндегі ролі арқылы қарастырады. Герхард Гентцен – негізін қалаушы.
Ағылшыншамен салыстырыңыз: абзацты басыңыз — түпнұсқа терезеде ашылады. Абзац астындағы EN түймесі оны мәтін ішінде көрсетеді.
Кіріспе
Дәлелдік теориялық семантика – логиканың семантикасына қатысты әдіс, ол пікірлер мен логикалық байланыстардың мағынасын интерпретациялар арқылы емес, Тарскидің семантикалық көзқарасындай, бірақ олардың қорытынды шығару жүйесінде атқаратын рөлі арқылы анықтауға тырысады.
Proof theoretic semantics is an approach to the semantics of logic that attempts to locate the meaning of propositions and logical connectives not in terms of interpretations, as in Tarskian approaches to semantics, but in the role that the proposition or logical connective plays within a system of inference.
Шолу
Герхард Гентцен – дәлелдемелік теориялық семантиканың негізін қалаушы, ол оның тізбекті есептеу үшін кесіндіні жою туралы есебінде және табиғи дедукция шеңберіндегі логикалық байланыстардың мағынасын олардың енгізу ережелерінде табу туралы ескертулері арқылы оған формальды негіз салды. Одан бері дәлелдемелік теориялық семантиканың тарихы осы идеялардың салдарына зерттеу жүргізуге арналды. Даг Правиц Гентценнің аналитикалық дәлелдеме туралы ұғымын табиғи дедукцияға кеңейтті және табиғи дедукциядағы дәлелдеменің құндылығы оның нормалды түрі ретінде түсіндірілуі мүмкін екенін ұсынды. Осы идея Curry-Howard изоморфизмінің және интуиционистік типтер теориясының негізінде жатыр. Оның инверсия принципі қазіргі заманғы дәлелдемелік теориялық семантиканың көптеген есептерінің негізі болып табылады. Майкл Даммет Нюэль Белнаптың ұсынысына сүйене отырып, логикалық үйлесімділіктің өте маңызды идеясын енгізді. Қысқасы, егер белгілі бір қорытынды үлгілерімен байланысты деп есептелетін тіл кез келген дәлелдемелерден аналитикалық дәлелдемелерді қайта құруға мүмкіндік берсе, онда ол логикалық үйлесімділікке ие болады, бұл тізбекті есептеу үшін кесіндіні жою теоремалары және табиғи дедукция үшін нормалау теоремалары арқылы көрсетілуі мүмкін. Логикалық үйлесімділігі жоқ тіл, үйлесімсіз қорытынды формаларының болуынан зардап шегеді: ол ықтимал түрде дәйекті емес болады.
Gerhard Gentzen is the founder of proof theoretic semantics, providing the formal basis for it in his account of cut elimination for the sequent calculus, and some provocative philosophical remarks about locating the meaning of logical connectives in their introduction rules within natural deduction. The history of proof theoretic semantics since then has been devoted to exploring the consequences of these ideas. Dag Prawitz extended Gentzen's notion of analytic proof to natural deduction, and suggested that the value of a proof in natural deduction may be understood as its normal form. This idea lies at the basis of the Curry–Howard isomorphism, and of intuitionistic type theory. His inversion principle lies at the heart of most modern accounts of proof theoretic semantics. Michael Dummett introduced the very fundamental idea of logical harmony, building on a suggestion of Nuel Belnap. In brief, a language, which is understood to be associated with certain patterns of inference, has logical harmony if it is always possible to recover analytic proofs from arbitrary demonstrations, as can be shown for the sequent calculus by means of cut elimination theorems and for natural deduction by means of normalisation theorems. A language that lacks logical harmony will suffer from the existence of incoherent forms of inference: it will likely be inconsistent.