Considere esta questão resolvida. Não vou escolher a melhor resposta, pois todas elas contribuíram para minha compreensão do tópico.
Não tenho certeza do benefício que temos ao definir formalmente a semântica da lógica de predicados. Mas vejo valor em ter um cálculo formal de prova. O que quero dizer é que não precisaríamos de semântica formal para justificar as regras de inferência do cálculo da prova.
Poderíamos definir um cálculo que imite as "leis do pensamento", isto é, as regras de inferência que foram usadas pelos matemáticos por centenas de anos para provar seus teoremas. Esse cálculo já existe: dedução natural. Em seguida, definiríamos esse cálculo como sólido e completo.
Isso pode ser justificado ao se perceber que a semântica formal da lógica de predicados é apenas um modelo. A adequação do modelo só pode ser justificada intuitivamente. Assim, mostrar que a dedução natural é sólida e completa com referência à semântica formal não torna a dedução natural mais "verdadeira". Seria tão bom se justificássemos diretamente as regras da dedução natural intuitivamente. O desvio usando a semântica formal não nos dá nada.
Então, tendo definido a dedução natural como sólida e completa, poderíamos mostrar a solidez e a integridade de outros cálculos, mostrando que as provas que produzem podem ser traduzidas em dedução natural e vice-versa.
Minhas reflexões acima estão corretas? Por que é importante provar a solidez e a integridade dos cálculos de prova por referência à semântica formal?
Respostas:
Um comentário menor e uma resposta mais séria.
Primeiro, não faz sentido declarar um sistema de dedução natural completo por decreto. A dedução natural é interessante precisamente porque possui uma noção interna natural de consistência e / ou integridade - ou seja, eliminação de cortes. Este é um teorema fantástico, e a IMO justifica totalmente as tentativas de fornecer uma semântica puramente teórica de prova (e pela correspondência CH, também justifica o uso de métodos operacionais na semântica da linguagem de programação). Mas isso é interessante precisamente porque oferece uma noção mais refinada de acertar a lógica do que a consistência. Seguir o caminho teórico da prova significa que você terá que trabalhar mais, mas, em troca, obtém resultados mais fortes.
No entanto, acontece que às vezes a lógica per seassume um papel secundário. Podemos começar com uma (família de) modelos e depois procurar maneiras de falar sintaticamente sobre eles, usando uma lógica. A solidez e integridade de uma lógica em relação a uma família de modelos indica que a lógica realmente captura tudo o que é interessante e verdadeiro que você pode dizer sobre a classe de modelos. Um exemplo concreto de quando os modelos são mais interessantes do que as teorias lógicas ocorre na análise de programas e na verificação de modelos. Lá, o usual é fazer com que seu modelo seja a execução de um programa e a lógica como um fragmento da lógica temporal. As proposições que você pode dizer nessas linguagens não são (deliberadamente) terrivelmente empolgantes - por exemplo, desreferências de ponteiros nulos nunca ocorrem - mas é o fato de que se aplica às execuções reais do programa que lhe interessa.
fonte
Vou adicionar outra perspectiva para aumentar as respostas acima. Primeiro, essas reflexões valem a pena, e muitas pessoas tiveram idéias semelhantes. Na filosofia, isso às vezes é chamado de "semântica teórica da prova", apelando ao trabalho de Nuel Belnap, Dag Prawitz, Michael Dummett e outros nos anos 60 e 70, que recorrem ao trabalho de Gentzen sobre dedução natural. Per Martin-Löf e Jean-Yves Girard também parecem propor variantes dessa posição em seus escritos. E falando muito amplamente, em linguagens de programação, essa é a "abordagem sintática para digitar a solidez".
O fato é que, mesmo que você aceite que as regras da lógica não precisam de uma interpretação semântica separada, não é muito interessante / útil dizer que elas são auto-justificadas e deixam assim. A questão é o que uma semântica formal realiza e se é possível obter o mesmo com menos desvios. No entanto, o projeto de unificar a teoria do modelo com a teoria da prova analítica é importante, mas ainda não está resolvido, sendo perseguido ativamente em muitas frentes diferentes, incluindo lógica categórica, semântica de jogos e os "lúdicos" de Girard. Por exemplo, para além do que Charles mencionado, outro benefício qualitativa de ter modelos é a capacidade de fornecer concretas contra-exemplos a nãoTeoremas, e a questão é como entender isso em uma abordagem "direta". Para uma resposta inspirada no lúdico, consulte "Sobre o significado da completude lógica", de Michele Basaldella e Kazushige Terui.
fonte
Uma semântica formal fornece um significado direto dos termos no cálculo, independentemente das regras de prova sintática para manipulá-los. Sem uma semântica formal, como você pode afirmar se as regras de dedução estão corretas (solidez) ou se você possui o suficiente delas (perfeição)?
Existem "leis do pensamento" propostas antes da dedução natural. Os silogismos de Aristóteles eram uma dessas coleções. Se tivéssemos definido que eles eram sólidos e completos, talvez ainda os estivéssemos usando hoje, em vez de desenvolver técnicas lógicas mais avançadas. O ponto é que, se os silogismos capturam completamente as leis do pensamento, por que precisaríamos criar mais lógicas. E se eles fossem de fato inconsistentes? Ter uma semântica junto com o cálculo formal da prova e as provas de integridade e integridade que as conectam fornece um bastão de medição para julgar o valor de um sistema de raciocínio desse tipo. Não ficaria mais isolado.
Outro motivo para ter uma semântica formal é que existem mais lógicas do que o cálculo predicado. Muitas dessas lógicas são projetadas para raciocinar sobre um tipo específico de sistema. (Estou pensando em lógica modal). Aqui a classe de sistemas é conhecida e a lógica vem depois (embora, historicamente, isso também não seja verdade). Novamente, a solidez nos diz se os axiomas da lógica capturam corretamente o "comportamento" do sistema, e a integridade nos diz se temos axiomas suficientes. Sem uma semântica, como saberíamos se as regras de dedução são suficientes e não absurdas?
Um exemplo de lógica que foi definida puramente sintaticamente e ainda está em andamento o trabalho para fornecer uma semântica formal é a lógica BAN para raciocinar sobre protocolos criptográficos. As regras de inferência lógica parecem razoáveis; então, por que fornecer uma semântica formal? Infelizmente, a lógica do BAN pode ser usada para provar que um protocolo está correto, mas podem existir ataques a esses protocolos. As regras de dedução estão, portanto , erradas , pelo menos no que diz respeito à semântica esperada.
fonte
Concordo com a supercooldave, mas há outra razão mais pragmática para desejar mais do que um conjunto ou outro de regras de inferência que caracterizam uma lógica: um determinado conjunto de regras de inferência tende a não ser bom para responder ao tipo de problemas enfrentados ao colocar a lógica usar.
Se você tem uma lógica especificada por uma lista de axiomas e duas regras como um sistema de Hilbert, geralmente será um trabalho difícil descobrir como provar um determinado teorema no sistema e, sem uma visão teórica, você não vai ser capaz de provar que uma determinada proposição não pode ser comprovada no sistema. Os modelos tradicionais são bons para provar propriedades que se aplicam a toda a lógica por indução.
Quatro tipos de ferramentas são úteis para resolver problemas que a maioria dos lógicos deseja resolver, organizados do menos para o mais semântico:
Como a supercooldave mencionou a lógica intuicionista: sem a regra do meio excluído, a teoria dos modelos se torna muito mais complicada e as teorias analíticas da prova se tornam mais importantes, geralmente a semântica da escolha. Técnicas algébricas, como a teoria das categorias, tornam-se preferidas por abstrair da complexidade sintática.
fonte