Теоретико-доказова семантика

Ця стаття містить правописні, лексичні, граматичні, стилістичні або інші мовні помилки, які треба виправити. Ви можете допомогти вдосконалити цю статтю, погодивши її із чинними мовними стандартами. (травень 2017)

Теоретично-доказова семантика—це підхід до семантики логіки, яка намагається знайти сенс пропозицій і логічних зв'язок не в термінах інтерпретацій, як в підходах до семантики в стилі Тарського, а в ролі, яку судження або логічна зв'язність грає в системі висновку.

Засновником теоретичної семантики є Ґергард Ґенцен, який надав їй офіційну основу у своєму звіті про усунення виключення для секвенційного обчислення і деякі провокаційні філософські зауваження про те, як визначити сенс логічних зв'язок у правилах їх введення в межах природної дедукції. Відтоді історія теоретично-семантичної теорії доказів була присвячена вивченню наслідків цих ідей.

Даг Правіц^[en] поширив поняття Генцена на аналітичний доказ, природну дедукцію і припустив, що значення доказу в природному виведенні можна розуміти як його нормальний вигляд. Ця ідея лежить в основі ізоморфізму Керрі-Говарда та інтуїціоністської теорії типів. Його принцип інверсії лежить в основі більшості сучасних звітів про теоретично-семантичну теорію доказів.

Майкл Дамм представив фундаментальну ідею логічної гармонії, спираючись на пропозицію Нуеля Белнапа^[en]. Ця ідея включає в себе мову, яка пов'язана з певними шаблонами виведення, має логічну гармонію. Якщо завжди можна відновити аналітичні докази від довільних демонстрацій, то можна показати секвенційне обчислення за допомогою теорем виключення вирізу і для природного виведення за допомогою теорем нормування. Мова, у якій відсутня логічна гармонія, буде страждати від наявності некоректних форм виведення — це, ймовірно, буде непослідовним.

• Виведена семантика ролі^[en]
• Істинно-умовна семантика^[en]

• Proof-Theoretic Semantics [Архівовано 11 березня 2017 у Wayback Machine.], at the Stanford Encyclopedia of Philosophy
• Logical Consequence, Deductive-Theoretic Conceptions [Архівовано 8 травня 2009 у Wayback Machine.], at the Internet Encyclopedia of Philosophy.
• Nissim Francez, «On a Distinction of Two Facets of Meaning and its Role in Proof-theoretic Semantics», Logica Universalis 9, 2015. doi:10.1007/s11787-015-0118-8
• Thomas Piecha, Peter Schroeder-Heister (eds), «Advances in Proof-Theoretic Semantics» [Архівовано 26 квітня 2017 у Wayback Machine.], Trends in Logic 43, Springer, 2016.
• Arché Bibliography on Proof-Theoretic Semantics.

Це незавершена стаття з логіки. Ви можете допомогти проєкту, виправивши або дописавши її.