Semantyka teorii dowodu

Semantyka teorii dowodu to podejście do semantyki logiki , które próbuje zlokalizować znaczenie zdań i spójników logicznych nie w kategoriach interpretacji , jak w podejściach Tarskiego do semantyki, ale w roli, jaką zdanie lub spójnik logiczny odgrywa w systemie wnioskowania .

Przegląd

Gerhard Gentzen jest twórcą semantyki opartej na teorii dowodu, dostarczając jej formalnej podstawy w swoim opisie eliminacji cięcia dla rachunku sekwensowego oraz kilku prowokacyjnych uwagach filozoficznych na temat umiejscowienia znaczenia spójników logicznych w regułach ich wprowadzania w ramach dedukcji naturalnej . Od tego czasu historia semantyki opartej na teorii dowodu była poświęcona badaniu konsekwencji tych idei.

Dag Prawitz rozszerzył Gentzenowskie pojęcie dowodu analitycznego na dedukcję naturalną i zasugerował, że wartość dowodu w dedukcji naturalnej można rozumieć jako jego normalną postać. Idea ta leży u podstaw izomorfizmu Curry’ego-Howarda i teorii typu intuicjonistycznego . Jego zasada inwersji leży u podstaw większości współczesnych opisów semantyki opartej na teorii dowodu.

Michael Dummett przedstawił bardzo podstawową ideę logicznej harmonii , opierając się na sugestii Nuela Belnapa . Krótko mówiąc, język, który jest rozumiany jako powiązany z pewnymi wzorami wnioskowania, charakteryzuje się logiczną harmonią, jeśli zawsze możliwe jest odzyskanie dowodów analitycznych z dowolnych demonstracji, jak można wykazać dla rachunku sekwencyjnego za pomocą twierdzeń o eliminacji przecięć i dla dedukcji naturalnej za pomocą twierdzeń o normalizacji. Język pozbawiony logicznej harmonii będzie cierpieć z powodu niespójnych form wnioskowania: prawdopodobnie będzie niespójny.

Zobacz też

• Wnioskująca semantyka ról
• Semantyka warunkowa prawdziwości

• Semantyka teoretyczna dowodu w Stanford Encyclopedia of Philosophy
• Konsekwencja logiczna, koncepcje dedukcyjno-teoretyczne w internetowej encyklopedii filozofii .
• Nissim Francez , „O rozróżnieniu dwóch aspektów znaczenia i jego roli w semantyce dowodowej”, Logica Universalis 9, 2015. doi : 10.1007/s11787-015-0118-8
• Thomas Piecha, Peter Schroeder-Heister (red.), „Postępy w semantyce teorii dowodu” , Trends in Logic 43, Springer, 2016.

Linki zewnętrzne

• Bibliografia Arché na temat semantyki teoretycznej dowodu.