Теоретико-доказова семантика: відмінності між версіями
| [неперевірена версія] | [неперевірена версія] |
Вилучено вміст Додано вміст
Виправлено джерел: 3; позначено як недійсні: 0.) #IABot (v2.0.8.6 |
м повідомлення про помилки вікіфікації |
||
Рядок 4:
[[Ґергард Ґенцен]] є засновником теоретичної семантики, надаючи їй офіційну основу в своєму звіті про усунення виключення для секвенційного обчислення і деякі провокаційні філософські зауваження про те, як визначити сенс логічних зв'язок у правилах їх введення в межах [[Дедукція|природної дедукції]]. З тих пір історія теоретико-семантичної теорії доказів була присвячена вивченню наслідків цих ідей.
{{Нп|Dag Prawitz|Даг Правіц}} поширив поняття Генцена на [[доказ|аналітичний доказ]], [[дедукція|природну дедукцію]] і припустив, що значення доказу в природному виведенні можна розуміти як його нормальний вигляд. Ця ідея лежить в основі [[Ізоморфізм|ізоморфізму Керрі-Говарда]] та {{Нп|Intuitionistic type theory|інтуїтивної теорії типів}}<!-- Проблема вікіфікації: Сторінка [[:en:Intuitionistic type theory]] перекладена як [[Інтуїціоністська теорія типів]], хоча хотіли [[Intuitionistic type theory]] (SashkoR0B0T)-->. Його [[інверсія|принцип інверсії]] лежить в основі більшості сучасних звітів про теоретико-семантичну теорію доказів.
[[Майкл Ентоні Ердлі Дамміт|Майкл Дамм]] представив фундаментальну ідею [[гармонія|логічної гармонії]], спираючись на пропозицію {{Нп|Nuel Belnap|Нуеля Белнапа|en|}}. Мова,яку,як розуміється, пов'язана з певними шаблонами виведення, має логічну гармонію.Якщо завжди можна відновити аналітичні докази від довільних демонстрацій, то можна показати секвенційне обчислення за допомогою теорем виключення вирізу і для природного виведення за допомогою теорем нормування. Мова, у якій відсутня логічна гармонія, буде страждати від наявності некоректних форм виведення-це, ймовірно, буде непослідовним.
| |||