Semântica Prova-Teórica
Semântica prova-teórica é uma abordagem para a semântica da lógica que tenta localizar o significado de proposições e conectivos lógicos não em termos de interpretações, como em abordagens tarskianas para semântica, mas no papel que a proposição ou os conectivos lógicos têm dentro do sistema de inferências.
Gerhard Gentzen é o criador da semântica prova-teórica, fornecendo sua base formal na sua abordagem à eliminação por corte para o cálculo de sequentes, e algumas observações filosóficas provocativas sobre como localizar o significado de conectivos lógicos em suas regras de introdução dentro de dedução natural. A história dos teóricos da semântica prova-teórica desde então tem se dedicado a explorar as conseqüências dessas ideias.
Dag Prawitz estendeu a noção de prova analítica de Gentzen para a dedução natural, e sugeriu que o valor de uma prova na dedução natural pode ser entendido como a sua forma normal. Esta ideia é a base do isomorfismo de Curry-Howard, e da teoria intuicionistica de tipos. Seu princípio de inversão está no cerne da maioria das abordagens modernas à semântica prova-teórica.
Michael Dummett introduziu a ideia muito fundamental da harmonia lógica, montada a partir de uma sugestão de Nuel Belnap. Resumidamente, uma linguagem, que é entendida como sendo associada com certos padrões de inferência, tem harmonia lógica se é sempre possível recuperar provas analíticas de demonstrações arbitrárias, como pode ser mostrado para o cálculo sequente por meio dos teoremas de eliminação do corte, e para dedução natural por meio de teoremas de normalização. Uma linguagem que carece de harmonia lógica irá sofrer com a existência de formas incoerentes de inferência: ela provavelmente vai ser inconsistente.
Referencias editar
- Proof-Theoretic Semantics, at the Stanford Encyclopedia of Philosophy
- Logical Consequence, Deductive-Theoretic Conceptions, at the Internet Encyclopedia of Philosophy.
- Nissim Francez, "On a Distinction of Two Facets of Meaning and its Role in Proof-theoretic Semantics", Logica Universalis 9, 2015. doi:10.1007/s11787-015-0118-8
- Thomas Piecha, Peter Schroeder-Heister (eds), "Advances in Proof-Theoretic Semantics", Trends in Logic 43, Springer, 2016.
Ver também editar
- Inferential role semantics
- Truth-conditional semantics