Теоретико-доказова семантика: відмінності між версіями
| [неперевірена версія] | [неперевірена версія] |
вікіфікація |
Виправлено джерел: 1; позначено як недійсні: 0. #IABot (v2.0beta14) |
||
| Рядок 17: | Рядок 17: | ||
* 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.] |
* [https://web.archive.org/web/20090415110223/http://arche-wiki.st-and.ac.uk/~ahwiki/bin/view/Arche/ProofTheoreticSemantics Arché Bibliography on Proof-Theoretic Semantics.] |
||
{{Logic-stub}} |
{{Logic-stub}} |
||
Версія за 11:26, 8 травня 2019
 | Ця стаття містить правописні, лексичні, граматичні, стилістичні або інші мовні помилки, які треба виправити. (травень 2017) |
Теоретико-доказова семантика — це підхід до семантики логіки, яка намагається знайти сенс пропозицій і логічних зв'язок не в термінах інтерпретацій, як в підходах до семантики в стилі Тарського, а в ролі, яку судження або логічна зв'язність грає в системі висновку.
Ґергард Ґенцен є засновником теоретичної семантики, надаючи їй офіційну основу в своєму звіті про усунення виключення для секвенційного обчислення і деякі провокаційні філософські зауваження про те, як визначити сенс логічних зв'язок у правилах їх введення в межах природної дедукції. З тих пір історія теоретико-семантичної теорії доказів була присвячена вивченню наслідків цих ідей.
Даг Правіц[en] поширив поняття Генцена на аналітичний доказ, природну дедукцію і припустив, що значення доказу в природному виведенні можна розуміти як його нормальний вигляд. Ця ідея лежить в основі ізоморфізму Керрі-Говарда та інтуїтивної теорії типів[en]. Його принцип інверсії лежить в основі більшості сучасних звітів про теоретико-семантичну теорію доказів.
Майкл Дамм представив фундаментальну ідею логічної гармонії, спираючись на пропозицію Нуеля Белнапа[en]. Коротше кажучи, мова, яка, як розуміється, пов'язана з певними шаблонами виведення, має логічну гармонію, якщо завжди можна відновити аналітичні докази від довільних демонстрацій, то можна показати секвенційне обчислення за допомогою теорем виключення вирізу і для природного виведення за допомогою теорем нормування. Мова, у якій відсутня логічна гармонія, буде страждати від наявності некоректних форм виведення: це, ймовірно, буде непослідовним.
Див. також
Посилання
- Proof-Theoretic Semantics, at the Stanford Encyclopedia of Philosophy
- Logical Consequence, Deductive-Theoretic Conceptions, at the Internet Encyclopedia of Philosophy.
- 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), «Advances in Proof-Theoretic Semantics», Trends in Logic 43, Springer, 2016.
- Arché Bibliography on Proof-Theoretic Semantics.
|
Це незавершена стаття з логіки. Ви можете допомогти проєкту, виправивши або дописавши її. |