Теоретико-доказова семантика: відмінності між версіями
| [неперевірена версія] | [неперевірена версія] |
→Див. також: ВП:Стиль, виправлення шаблон:нп |
Немає опису редагування |
||
| Рядок 1: | Рядок 1: | ||
'''Теоретико-доказова семантика''' - це підхід до [[семантика логіки|семантики логіки]], яка намагається знайти сенс пропозицій і [[Семантика логіки|логічних зв'язок]] не в термінах [[інтерпретація|інтерпретацій]], як в підходах до семантики в [[Тарський|Тарськіх підходах до семантики]], а в ролі, яку судження або [[Логічний сполучник|логічна зв'язність]] грає в [[висновок|системі висновку]]. |
'''Теоретико-доказова семантика''' - це підхід до [[семантика логіки|семантики логіки]], яка намагається знайти сенс пропозицій і [[Семантика логіки|логічних зв'язок]] не в термінах [[інтерпретація|інтерпретацій]], як в підходах до семантики в [[Тарський|Тарськіх підходах до семантики]], а в ролі, яку судження або [[Логічний сполучник|логічна зв'язність]] грає в [[висновок|системі висновку]]. |
||
Герхард Гентца є засновником теоретико-теоретичної семантики, надаючи йому офіційну основу в своєму звіті про усунення [[виключення]] для [[секвенційне обчислення|секвенційного обчислення]] і деякі провокаційні філософські зауваження про те, як визначити сенс логічних зв'язок в правилах їх введення в межах [[Дедукція|природного дедукції]]. З тих пір історія теоретико-семантичної теорії доказів була присвячена вивченню наслідків цих ідей. |
{{Нп|Gerhard Gentzen|Герхард Гентца}} є засновником теоретико-теоретичної семантики, надаючи йому офіційну основу в своєму звіті про усунення [[виключення]] для [[секвенційне обчислення|секвенційного обчислення]] і деякі провокаційні філософські зауваження про те, як визначити сенс логічних зв'язок в правилах їх введення в межах [[Дедукція|природного дедукції]]. З тих пір історія теоретико-семантичної теорії доказів була присвячена вивченню наслідків цих ідей. |
||
Даг Правітц поширив поняття Генцен на [[доказ|аналітичний доказ]], [[дедукція|природну дедукцію]] і припустив, що значення доказу в природному виведення можна розуміти як його нормальний вигляд. Ця ідея лежить в основі [[Ізоморфізм|ізоморфізму Керрі-Говарда]] і [[теорія типів|інтуїтивної теорії типів]]. Його [[інверсія|принцип інверсії]] лежить в основі більшості сучасних звітів про теоретико-семантику доказу. |
{{Нп|Dag Prawitz|Даг Правітц}} поширив поняття Генцен на [[доказ|аналітичний доказ]], [[дедукція|природну дедукцію]] і припустив, що значення доказу в природному виведення можна розуміти як його нормальний вигляд. Ця ідея лежить в основі [[Ізоморфізм|ізоморфізму Керрі-Говарда]] і [[теорія типів|інтуїтивної теорії типів]]. Його [[інверсія|принцип інверсії]] лежить в основі більшості сучасних звітів про теоретико-семантику доказу. |
||
[[Майкл Ентоні Ердлі Дамміт|Майкл Дамм]] представив дуже фундаментальну ідею [[гармонія|логічної гармонії]], спираючись на пропозицію |
[[Майкл Ентоні Ердлі Дамміт|Майкл Дамм]] представив дуже фундаментальну ідею [[гармонія|логічної гармонії]], спираючись на пропозицію {{Нп|Nuel Belnap|Нуель Белнап]]. Коротше кажучи, мова, яка, як розуміється, пов'язаний з певними шаблонами виведення, має логічну гармонію, якщо завжди можна відновити аналітичні докази від довільних демонстрацій, що можна показати для секвенційного обчислення за допомогою теорем виключення вирізу і Для природного виведення за допомогою теорем нормування. Мова, в якому відсутня логічна гармонія, буде страждати від наявності некогерентних форм виведення: це, ймовірно, буде непослідовним. |
||
== Див. також == |
== Див. також == |
||
Версія за 20:30, 28 травня 2017
Теоретико-доказова семантика - це підхід до семантики логіки, яка намагається знайти сенс пропозицій і логічних зв'язок не в термінах інтерпретацій, як в підходах до семантики в Тарськіх підходах до семантики, а в ролі, яку судження або логічна зв'язність грає в системі висновку.
Герхард Гентца[en] є засновником теоретико-теоретичної семантики, надаючи йому офіційну основу в своєму звіті про усунення виключення для секвенційного обчислення і деякі провокаційні філософські зауваження про те, як визначити сенс логічних зв'язок в правилах їх введення в межах природного дедукції. З тих пір історія теоретико-семантичної теорії доказів була присвячена вивченню наслідків цих ідей.
Даг Правітц[en] поширив поняття Генцен на аналітичний доказ, природну дедукцію і припустив, що значення доказу в природному виведення можна розуміти як його нормальний вигляд. Ця ідея лежить в основі ізоморфізму Керрі-Говарда і інтуїтивної теорії типів. Його принцип інверсії лежить в основі більшості сучасних звітів про теоретико-семантику доказу.
Майкл Дамм представив дуже фундаментальну ідею логічної гармонії, спираючись на пропозицію {{Нп|Nuel Belnap|Нуель Белнап]]. Коротше кажучи, мова, яка, як розуміється, пов'язаний з певними шаблонами виведення, має логічну гармонію, якщо завжди можна відновити аналітичні докази від довільних демонстрацій, що можна показати для секвенційного обчислення за допомогою теорем виключення вирізу і Для природного виведення за допомогою теорем нормування. Мова, в якому відсутня логічна гармонія, буде страждати від наявності некогерентних форм виведення: це, ймовірно, буде непослідовним.
Див. також
Посилання
- 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.