Regra de inferência - Rule of inference

Na filosofia da lógica , uma regra de inferência , regra de inferência ou regra de transformação é uma forma lógica que consiste em uma função que assume premissas, analisa sua sintaxe e retorna uma conclusão (ou conclusões ). Por exemplo, a regra de inferência chamada modus ponens assume duas premissas, uma na forma "Se p, então q" e outra na forma "p", e retorna a conclusão "q". A regra é válida com respeito à semântica da lógica clássica (assim como a semântica de muitas outras lógicas não clássicas ), no sentido de que se as premissas são verdadeiras (sob uma interpretação), então a conclusão também é.

Normalmente, uma regra de inferência preserva a verdade, uma propriedade semântica. Na lógica de muitos valores , ele preserva uma designação geral. Mas a ação de uma regra de inferência é puramente sintática e não precisa preservar nenhuma propriedade semântica: qualquer função de conjuntos de fórmulas a fórmulas conta como uma regra de inferência. Normalmente, apenas as regras recursivas são importantes; ou seja, regras tais que haja um procedimento eficaz para determinar se uma dada fórmula é a conclusão de um determinado conjunto de fórmulas de acordo com a regra. Um exemplo de regra que não é eficaz nesse sentido é a regra infinitária ω .

As regras populares de inferência na lógica proposicional incluem modus ponens , modus tollens e contraposição . A lógica de predicado de primeira ordem usa regras de inferência para lidar com quantificadores lógicos .

Forma padrão

Na lógica formal (e em muitas áreas relacionadas), as regras de inferência são geralmente fornecidas na seguinte forma padrão:

  Premissa # 1
  Premissa # 2
        ...
  Premissa # n   
  Conclusão

Essa expressão afirma que, sempre que, no curso de alguma derivação lógica, as premissas dadas foram obtidas, a conclusão especificada também pode ser tomada como certa. A linguagem formal exata que é usada para descrever as premissas e as conclusões depende do contexto real das derivações. Em um caso simples, pode-se usar fórmulas lógicas, como em:

Esta é a regra do modus ponens da lógica proposicional . As regras de inferência são freqüentemente formuladas como esquemas que empregam metavariáveis . Na regra (esquema) acima, as metavariáveis ​​A e B podem ser instanciadas para qualquer elemento do universo (ou às vezes, por convenção, um subconjunto restrito, como proposições ) para formar um conjunto infinito de regras de inferência.

Um sistema de prova é formado por um conjunto de regras encadeadas para formar provas, também chamadas de derivações . Qualquer derivação tem apenas uma conclusão final, que é a afirmação provada ou derivada. Se as premissas não forem satisfeitas na derivação, então a derivação é uma prova de uma afirmação hipotética : " se as premissas são válidas, então a conclusão é válida".

Exemplo: sistemas de Hilbert para duas lógicas proposicionais

Em um sistema de Hilbert , as premissas e a conclusão das regras de inferência são simplesmente fórmulas de alguma linguagem, geralmente empregando metavariáveis. Para compactação gráfica da apresentação e para enfatizar a distinção entre axiomas e regras de inferência, esta seção usa a notação sequente ( ) em vez de uma apresentação vertical de regras. Nesta notação,

é escrito como .

A linguagem formal para a lógica proposicional clássica pode ser expressa usando apenas negação (¬), implicação (→) e símbolos proposicionais. Uma axiomatização bem conhecida, compreendendo três esquemas de axioma e uma regra de inferência ( modus ponens ), é:

(CA1) ⊢ A → (BA)
(CA2) ⊢ (A → (BC)) → ((AB) → (AC))
(CA3) ⊢ (¬A → ¬B) → (BA)
(MP) A, ABB

Pode parecer redundante ter duas noções de inferência neste caso, ⊢ e →. Na lógica proposicional clássica, eles realmente coincidem; as dedução teorema afirma que AB se e somente se ⊢ AB . Há, no entanto, uma distinção que vale a pena enfatizar mesmo neste caso: a primeira notação descreve uma dedução , que é uma atividade de passagem de sentenças para sentenças, enquanto AB é simplesmente uma fórmula feita com um conectivo lógico , implicação neste caso. Sem uma regra de inferência (como o modus ponens , neste caso), não há dedução ou inferência. Este ponto é ilustrado no diálogo de Lewis Carroll chamado " O que a tartaruga disse a Aquiles ", bem como nas tentativas posteriores de Bertrand Russell e Peter Winch para resolver o paradoxo introduzido no diálogo.

Para algumas lógicas não clássicas, o teorema da dedução não é válido. Por exemplo, a lógica de três valores de Łukasiewicz pode ser axiomatizada como:

(CA1) ⊢ A → (BA)
(LA2) ⊢ (AB) → ((BC) → (AC))
(CA3) ⊢ (¬A → ¬B) → (BA)
(LA4) ⊢ ((A → ¬A) → A) → A
(MP) A, ABB

Esta sequência difere da lógica clássica pela mudança no axioma 2 e pela adição do axioma 4. O teorema da dedução clássica não é válido para esta lógica, no entanto, uma forma modificada é válida, ou seja, AB se e somente se ⊢ A → ( AB ).

Admissibilidade e derivabilidade

Em um conjunto de regras, uma regra de inferência pode ser redundante no sentido de que é admissível ou derivável . Uma regra derivável é aquela cuja conclusão pode ser derivada de suas premissas usando as outras regras. Uma regra admissível é aquela cuja conclusão se mantém sempre que as premissas são válidas. Todas as regras deriváveis ​​são admissíveis. Para avaliar a diferença, considere o seguinte conjunto de regras para definir os números naturais (o julgamento afirma o fato de que é um número natural):

A primeira regra afirma que 0 é um número natural e a segunda afirma que s ( n ) é um número natural se n for. Neste sistema de prova, a seguinte regra, demonstrando que o segundo sucessor de um número natural também é um número natural, é derivável:

Sua derivação é a composição de dois usos da regra do sucessor acima. A seguinte regra para afirmar a existência de um predecessor para qualquer número diferente de zero é meramente admissível:

Este é um fato verdadeiro dos números naturais, como pode ser comprovado por indução . (Para provar que essa regra é admissível, assuma uma derivação da premissa e induza nela para produzir uma derivação de .) No entanto, não é derivável, porque depende da estrutura da derivação da premissa. Por causa disso, a derivabilidade é estável sob acréscimos ao sistema de prova, ao passo que a admissibilidade não é. Para ver a diferença, suponha que a seguinte regra absurda foi adicionada ao sistema de prova:

Nesse novo sistema, a regra do duplo sucessor ainda é derivável. No entanto, a regra para encontrar o antecessor não é mais admissível, porque não há como derivar . A fragilidade da admissibilidade advém da forma como é provada: uma vez que a prova pode incidir na estrutura das derivações das premissas, extensões ao sistema acrescentam novos casos a essa prova, que podem não mais valer.

As regras admissíveis podem ser consideradas teoremas de um sistema de prova. Por exemplo, em um cálculo sequente em que a eliminação do corte é válida, a regra do corte é admissível.

Veja também

Referências