Відмінності між версіями «Теоретико-доказова семантика»

нема опису редагування
Мітки: Редагування з мобільного пристрою Редагування через мобільну версію
Мітки: Редагування з мобільного пристрою Редагування через мобільну версію
[[Герхард Гентца]] є засновником теоретико-теоретичної семантики, надаючи йому офіційну основу в своєму звіті про усунення [[виключення]] для [[секвенційне обчислення|секвенційного обчислення]] і деякі провокаційні філософські зауваження про те, як визначити сенс логічних зв'язок в правилах їх введення в межах [[Дедукція|природного дедукції]]. З тих пір історія теоретико-семантичної теорії доказів була присвячена вивченню наслідків цих ідей.
 
[[Даг Правітц]] поширив поняття Генцен на [[доказ|аналітичний доказ]], [[дедукція|природну дедукцію]] і припустив, що значення доказу в природному виведення можна розуміти як його нормальний вигляд. Ця ідея лежить в основі [[Ізоморфізм|ізоморфізму Керрі-Говарда]] і [[теорія типів|інтуїтивної теорії типів]]. Його [[інверсія|принцип інверсії]] лежить в основі більшості сучасних звітів про теоретико-семантику доказу.
 
[[Майкл Дамм]] представив дуже фундаментальну ідею [[логічна гармонія|логічної гармонії]], спираючись на пропозицію [[Нуель Белнап]]. Коротше кажучи, мова, яка, як розуміється, пов'язаний з певними шаблонами виведення, має логічну гармонію, якщо завжди можна відновити аналітичні докази від довільних демонстрацій, що можна показати для секвенційного обчислення за допомогою теорем виключення вирізу і Для природного виведення за допомогою теорем нормування. Мова, в якому відсутня логічна гармонія, буде страждати від наявності некогерентних форм виведення: це, ймовірно, буде непослідовним.
170

редагувань