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

Матеріал з Вікіпедії — вільної енциклопедії.
Перейти до навігації Перейти до пошуку
Інтерактивний перегляд історії
[неперевірена версія][неперевірена версія]
← Попереднє редагуванняНаступне редагування →
Вилучено вміст Додано вміст
ВізуальнийВікірозмітка
Немає опису редагування
Мітки: Редагування з мобільного пристрою Редагування через мобільну версію
Немає опису редагування
Мітки: Редагування з мобільного пристрою Редагування через мобільну версію
Рядок 1: Рядок 1:
'''Теоретико-доказова семантика''' - це підхід до [[семантика логіки|семантики логіки]], яка намагається знайти сенс пропозицій і [[Логічних зв'язок|логічних зв'язок]] не в термінах [[інтерпретація|інтерпретацій]], як в підходах до семантиці в [[Тарський]], а в ролі, яку судження або логічна зв'язність грає в [[висновок|системі висновку]].
'''Теоретико-доказова семантика''' - це підхід до [[семантика логіки|семантики логіки]], яка намагається знайти сенс пропозицій і [[Логічних зв'язок|логічних зв'язок]] не в термінах [[інтерпретація|інтерпретацій]], як в підходах до семантиці в [[Тарський]], а в ролі, яку судження або логічна зв'язність грає в [[висновок|системі висновку]].


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


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


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


Посилання
Посилання

Версія за 18:21, 28 травня 2017

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

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

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

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

Посилання

Отримано з https://uk.wikipedia.org/w/index.php?title=Теоретико-доказова_семантика&oldid=20471501