Ця стаття містить правописні, лексичні, граматичні, стилістичні або інші мовні помилки, які треба виправити. (травень 2017) |
Теоретико-доказова семантика — це підхід до семантики логіки, яка намагається знайти сенс пропозицій і логічних зв'язок не в термінах інтерпретацій, як в підходах до семантики в стилі Тарського, а в ролі, яку судження або логічна зв'язність грає в системі висновку.
Ґергард Ґенцен є засновником теоретичної семантики, надаючи їй офіційну основу у своєму звіті про усунення виключення для секвенційного обчислення і деякі провокаційні філософські зауваження про те, як визначити сенс логічних зв'язок у правилах їх введення в межах природної дедукції. Відтоді історія теоретико-семантичної теорії доказів була присвячена вивченню наслідків цих ідей.
[en] поширив поняття Генцена на аналітичний доказ, природну дедукцію і припустив, що значення доказу в природному виведенні можна розуміти як його нормальний вигляд. Ця ідея лежить в основі ізоморфізму Керрі-Говарда та інтуїціоністської теорії типів. Його принцип інверсії лежить в основі більшості сучасних звітів про теоретико-семантичну теорію доказів.
Майкл Дамм представив фундаментальну ідею логічної гармонії, спираючись на пропозицію [en]. Мова, яка, як розуміється, пов'язана з певними шаблонами виведення, має логічну гармонію. Якщо завжди можна відновити аналітичні докази від довільних демонстрацій, то можна показати секвенційне обчислення за допомогою теорем виключення вирізу і для природного виведення за допомогою теорем нормування. Мова, у якій відсутня логічна гармонія, буде страждати від наявності некоректних форм виведення — це, ймовірно, буде непослідовним.
Див. також
- [en]
- [en]
Посилання
- Proof-Theoretic Semantics [ 11 березня 2017 у Wayback Machine.], at the Stanford Encyclopedia of Philosophy
- Logical Consequence, Deductive-Theoretic Conceptions [ 8 травня 2009 у Wayback Machine.], at the .
- Nissim Francez, «On a Distinction of Two Facets of Meaning and its Role in Proof-theoretic Semantics», 9, 2015. DOI:10.1007/s11787-015-0118-8
- Thomas Piecha, Peter Schroeder-Heister (eds), «Advances in Proof-Theoretic Semantics» [ 26 квітня 2017 у Wayback Machine.], Trends in Logic 43, Springer, 2016.
Це незавершена стаття з логіки. Ви можете проєкту, виправивши або дописавши її. |
Вікіпедія, Українська, Україна, книга, книги, бібліотека, стаття, читати, завантажити, безкоштовно, безкоштовно завантажити, mp3, відео, mp4, 3gp, jpg, jpeg, gif, png, малюнок, музика, пісня, фільм, книга, гра, ігри, мобільний, телефон, android, ios, apple, мобільний телефон, samsung, iphone, xiomi, xiaomi, redmi, honor, oppo, nokia, sonya, mi, ПК, web, Інтернет
Cya stattya mistit pravopisni leksichni gramatichni stilistichni abo inshi movni pomilki yaki treba vipraviti Vi mozhete dopomogti vdoskonaliti cyu stattyu pogodivshi yiyi iz chinnimi movnimi standartami traven 2017 Teoretiko dokazova semantika ce pidhid do semantiki logiki yaka namagayetsya znajti sens propozicij i logichnih zv yazok ne v terminah interpretacij yak v pidhodah do semantiki v stili Tarskogo a v roli yaku sudzhennya abo logichna zv yaznist graye v sistemi visnovku Gergard Gencen ye zasnovnikom teoretichnoyi semantiki nadayuchi yij oficijnu osnovu u svoyemu zviti pro usunennya viklyuchennya dlya sekvencijnogo obchislennya i deyaki provokacijni filosofski zauvazhennya pro te yak viznachiti sens logichnih zv yazok u pravilah yih vvedennya v mezhah prirodnoyi dedukciyi Vidtodi istoriya teoretiko semantichnoyi teoriyi dokaziv bula prisvyachena vivchennyu naslidkiv cih idej en poshiriv ponyattya Gencena na analitichnij dokaz prirodnu dedukciyu i pripustiv sho znachennya dokazu v prirodnomu vivedenni mozhna rozumiti yak jogo normalnij viglyad Cya ideya lezhit v osnovi izomorfizmu Kerri Govarda ta intuyicionistskoyi teoriyi tipiv Jogo princip inversiyi lezhit v osnovi bilshosti suchasnih zvitiv pro teoretiko semantichnu teoriyu dokaziv Majkl Damm predstaviv fundamentalnu ideyu logichnoyi garmoniyi spirayuchis na propoziciyu en Mova yaka yak rozumiyetsya pov yazana z pevnimi shablonami vivedennya maye logichnu garmoniyu Yaksho zavzhdi mozhna vidnoviti analitichni dokazi vid dovilnih demonstracij to mozhna pokazati sekvencijne obchislennya za dopomogoyu teorem viklyuchennya virizu i dlya prirodnogo vivedennya za dopomogoyu teorem normuvannya Mova u yakij vidsutnya logichna garmoniya bude strazhdati vid nayavnosti nekorektnih form vivedennya ce jmovirno bude neposlidovnim Div takozh en en PosilannyaProof Theoretic Semantics 11 bereznya 2017 u Wayback Machine at the Stanford Encyclopedia of Philosophy Logical Consequence Deductive Theoretic Conceptions 8 travnya 2009 u Wayback Machine at the Nissim Francez On a Distinction of Two Facets of Meaning and its Role in Proof theoretic Semantics 9 2015 DOI 10 1007 s11787 015 0118 8 Thomas Piecha Peter Schroeder Heister eds Advances in Proof Theoretic Semantics 26 kvitnya 2017 u Wayback Machine Trends in Logic 43 Springer 2016 Ce nezavershena stattya z logiki Vi mozhete dopomogti proyektu vipravivshi abo dopisavshi yiyi