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

[неперевірена версія]

Поточна версія на 05:37, 2 квітня 2022

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

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

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

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

Див. такожРедагувати

ПосиланняРедагувати

Proof-Theoretic Semantics [Архівовано 11 березня 2017 у Wayback Machine.], at the Stanford Encyclopedia of Philosophy
Logical Consequence, Deductive-Theoretic Conceptions [Архівовано 8 травня 2009 у Wayback Machine.], 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» [Архівовано 26 квітня 2017 у Wayback Machine.], Trends in Logic 43, Springer, 2016.
Arché Bibliography on Proof-Theoretic Semantics.

Це незавершена стаття з логіки.
Ви можете допомогти проєкту, виправивши або дописавши її.

@@ Рядок 1: / Рядок 1: @@
+{{Мовні помилки|дата=травень 2017}}
-'''Теоретико-доказова семантика''' - це підхід до [[семантика логіки|семантики логіки]], яка намагається знайти сенс пропозицій і [[Семантика логіки|логічних зв'язок]] не в термінах [[інтерпретація|інтерпретацій]], як в підходах до семантики в [[Тарський|Тарськіх підходах до семантики]], а в ролі, яку судження або [[Логічний сполучник|логічна зв'язність]] грає в [[висновок|системі висновку]].
+'''Теоретико-доказова семантика'''&nbsp;— це підхід до [[семантика логіки|семантики логіки]], яка намагається знайти сенс пропозицій і [[Семантика логіки|логічних зв'язок]] не в термінах [[інтерпретація|інтерпретацій]], як в підходах до семантики в стилі [[Альфред Тарський|Тарського]], а в ролі, яку судження або [[Логічний сполучник|логічна зв'язність]] грає в [[висновок|системі висновку]].
-{{Нп|Gerhard Gentzen|Герхард Гентца}} є засновником теоретико-теоретичної семантики, надаючи йому офіційну основу в своєму звіті про усунення виключення для секвенційного обчислення і деякі провокаційні філософські зауваження про те, як визначити сенс логічних зв'язок в правилах їх введення в межах [[Дедукція|природного дедукції]]. З тих пір історія теоретико-семантичної теорії доказів була присвячена вивченню наслідків цих ідей.
+[[Ґергард Ґенцен]] є засновником теоретичної семантики, надаючи їй офіційну основу в своєму звіті про усунення виключення для секвенційного обчислення і деякі провокаційні філософські зауваження про те, як визначити сенс логічних зв'язок у правилах їх введення в межах [[Дедукція|природної дедукції]]. З тих пір історія теоретико-семантичної теорії доказів була присвячена вивченню наслідків цих ідей.
-{{Нп|Dag Prawitz|Даг Правітц}} поширив поняття Генцен на [[доказ|аналітичний доказ]], [[дедукція|природну дедукцію]] і припустив, що значення доказу в природному виведення можна розуміти як його нормальний вигляд. Ця ідея лежить в основі [[Ізоморфізм|ізоморфізму Керрі-Говарда]] і інтуїтивної теорії типів. Його [[інверсія|принцип інверсії]] лежить в основі більшості сучасних звітів про теоретико-семантику доказу.
+{{Нп|Dag Prawitz|Даг Правіц}} поширив поняття Генцена на [[доказ|аналітичний доказ]], [[дедукція|природну дедукцію]] і припустив, що значення доказу в природному виведенні можна розуміти як його нормальний вигляд. Ця ідея лежить в основі [[Ізоморфізм|ізоморфізму Керрі-Говарда]] та {{Нп|Intuitionistic type theory|інтуїтивної теорії типів}}. Його [[інверсія|принцип інверсії]] лежить в основі більшості сучасних звітів про теоретико-семантичну теорію доказів.
-[[Майкл Ентоні Ердлі Дамміт|Майкл Дамм]] представив дуже фундаментальну ідею [[гармонія|логічної гармонії]], спираючись на пропозицію {{Нп|Nuel Belnap|Нуель Белнап}}. Коротше кажучи, мова, яка, як розуміється, пов'язаний з певними шаблонами виведення, має логічну гармонію, якщо завжди можна відновити аналітичні докази від довільних демонстрацій, що можна показати для секвенційного обчислення за допомогою теорем виключення вирізу і Для природного виведення за допомогою теорем нормування. Мова, в якому відсутня логічна гармонія, буде страждати від наявності некогерентних форм виведення: це, ймовірно, буде непослідовним.
+[[Майкл Ентоні Ердлі Дамміт|Майкл Дамм]] представив фундаментальну ідею [[гармонія|логічної гармонії]], спираючись на пропозицію {{Нп|Nuel Belnap|Нуеля Белнапа|en|}}. Мова,яку,як розуміється, пов'язана з певними шаблонами виведення, має логічну гармонію.Якщо завжди можна відновити аналітичні докази від довільних демонстрацій, то можна показати секвенційне обчислення за допомогою теорем виключення вирізу і для природного виведення за допомогою теорем нормування. Мова, у якій відсутня логічна гармонія, буде страждати від наявності некоректних форм виведення-це, ймовірно, буде непослідовним.
 == Див. також ==
@@ Рядок 11: / Рядок 12: @@
 * {{Нп|Істинно-умовна семантика|||Truth-conditional semantics}}
-==Посилання==
+== Посилання ==
-* [http://plato.stanford.edu/entries/proof-theoretic-semantics/ Proof-Theoretic Semantics], at the [[Stanford Encyclopedia of Philosophy]]
+* [http://plato.stanford.edu/entries/proof-theoretic-semantics/ Proof-Theoretic Semantics] {{Webarchive|url=https://web.archive.org/web/20170311085000/https://plato.stanford.edu/entries/proof-theoretic-semantics/ |date=11 березня 2017 }}, at the [[Stanford Encyclopedia of Philosophy]]
-* [http://www.iep.utm.edu/l/logcon-d.htm Logical Consequence, Deductive-Theoretic Conceptions], at the [[Internet Encyclopedia of Philosophy]].
+* [http://www.iep.utm.edu/l/logcon-d.htm Logical Consequence, Deductive-Theoretic Conceptions] {{Webarchive|url=https://web.archive.org/web/20090508160144/http://www.iep.utm.edu/l/logcon-d.htm |date=8 травня 2009 }}, 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}}
+* 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»] {{Webarchive|url=https://web.archive.org/web/20170426041859/http://link.springer.com/book/10.1007%2F978-3-319-22686-6 |date=26 квітня 2017 }}, Trends in Logic 43, Springer, 2016.
+* [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}}
+[[Категорія:Незавершені статті з логіки]]
+[[Категорія:Філософська логіка]]
+[[Категорія:Теорія доведення]]