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

Матеріал з Вікіпедії — вільної енциклопедії.
Перейти до навігації Перейти до пошуку
[неперевірена версія][неперевірена версія]
Рядок 16: Рядок 16:
* 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}}
* 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), [http://link.springer.com/book/10.1007%2F978-3-319-22686-6 "Advances in Proof-Theoretic Semantics"], Trends in Logic 43, Springer, 2016.
* Thomas Piecha, Peter Schroeder-Heister (eds), [http://link.springer.com/book/10.1007%2F978-3-319-22686-6 "Advances in Proof-Theoretic Semantics"], Trends in Logic 43, Springer, 2016.

==Зовнішні посилання==
*[http://arche-wiki.st-and.ac.uk/~ahwiki/bin/view/Arche/ProofTheoreticSemantics Arché Bibliography on Proof-Theoretic Semantics.]

{{logic-stub}}


[[Категорія:Незавершені статті з логіки]]
[[Категорія:Незавершені статті з логіки]]

Версія за 20:37, 28 травня 2017

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

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

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

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

Див. також

Посилання

Зовнішні посилання