Перегляд вихідного коду сторінки Теоретико-доказова семантика

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

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

{{Нп|Dag Prawitz|Даг Правітц}} поширив поняття Генцен на [[доказ|аналітичний доказ]], [[дедукція|природну дедукцію]] і припустив, що значення доказу в природному виведення можна розуміти як його нормальний вигляд. Ця ідея лежить в основі [[Ізоморфізм|ізоморфізму Керрі-Говарда]] і {{Нп|Intuitionistic type theory|інтуїтивної теорії типів}}. Його [[інверсія|принцип інверсії]] лежить в основі більшості сучасних звітів про теоретико-семантику доказу.

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

== Див. також ==
* {{Нп|Виведена семантика ролі|||Inferential role semantics}}
* {{Нп|Істинно-умовна семантика|||Truth-conditional semantics}}

==Посилання==
* [http://plato.stanford.edu/entries/proof-theoretic-semantics/ Proof-Theoretic Semantics], 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]].
* 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.