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

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

 

 

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