Proof-theoretic semantics

rdf:langString Semântica Prova-Teórica

rdf:langString 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 idéias. Dag Prawitz estendeu a noção de 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 . 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.