170
редагувань
[неперевірена версія] | [неперевірена версія] |
(→Див. також: ВП:Стиль, виправлення шаблон:нп) |
Немає опису редагування |
||
'''Теоретико-доказова семантика''' - це підхід до [[семантика логіки|семантики логіки]], яка намагається знайти сенс пропозицій і [[Семантика логіки|логічних зв'язок]] не в термінах [[інтерпретація|інтерпретацій]], як в підходах до семантики в [[Тарський|Тарськіх підходах до семантики]], а в ролі, яку судження або [[Логічний сполучник|логічна зв'язність]] грає в [[висновок|системі висновку]].
{{Нп|Gerhard Gentzen|Герхард Гентца}} є засновником теоретико-теоретичної семантики, надаючи йому офіційну основу в своєму звіті про усунення [[виключення]] для [[секвенційне обчислення|секвенційного обчислення]] і деякі провокаційні філософські зауваження про те, як визначити сенс логічних зв'язок в правилах їх введення в межах [[Дедукція|природного дедукції]]. З тих пір історія теоретико-семантичної теорії доказів була присвячена вивченню наслідків цих ідей.
{{Нп|Dag Prawitz|Даг Правітц}} поширив поняття Генцен на [[доказ|аналітичний доказ]], [[дедукція|природну дедукцію]] і припустив, що значення доказу в природному виведення можна розуміти як його нормальний вигляд. Ця ідея лежить в основі [[Ізоморфізм|ізоморфізму Керрі-Говарда]] і [[теорія типів|інтуїтивної теорії типів]]. Його [[інверсія|принцип інверсії]] лежить в основі більшості сучасних звітів про теоретико-семантику доказу.
[[Майкл Ентоні Ердлі Дамміт|Майкл Дамм]] представив дуже фундаментальну ідею [[гармонія|логічної гармонії]], спираючись на пропозицію
== Див. також ==
|
редагувань