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