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

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

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

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

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

Див. також

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

Посилання

• 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.