Доказательно-теоретическая семантика: от Генцена до современности.
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.
Обзор
Герхард Гентцен является основоположником доказательно-теоретической семантики, предоставив ей формальную базу в своей работе по устранению отсечений для секвенциального исчисления, а также выдвинув ряд провокационных философских замечаний о локализации значения логических связок в правилах их введения в рамках натуральной дедукции. История доказательно-теоретической семантики с тех пор была посвящена исследованию последствий этих идей. Даг Правиц расширил понятие Гентцена об аналитическом доказательстве до натуральной дедукции и предположил, что ценность доказательства в натуральной дедукции можно понимать как его нормальную форму. Эта идея лежит в основе изоморфизма Карри — Ховарда и интуиционистской теории типов. Его принцип инверсии лежит в основе большинства современных подходов к доказательно-теоретической семантике. Майкл Даммет ввел фундаментальную идею логической гармонии, опираясь на предложение Нуэля Белнапа. Вкратце, язык, который понимается как связанный с определенными схемами вывода, обладает логической гармонией, если всегда возможно восстановить аналитические доказательства из произвольных демонстраций, что можно показать для секвенциального исчисления посредством теорем об устранении отсечений, а для натуральной дедукции — посредством теорем о нормализации. Язык, лишенный логической гармонии, будет страдать от существования некогерентных форм вывода: он, скорее всего, окажется непоследовательным.
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.