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

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

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

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

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