Regra de inferência

Inferência é o processo pelo qual se chega a uma proposição, firmada na base de uma ou outras mais proposições aceitas como ponto de partida do processo. O Argumento é chamado de premissa e o valor de conclusão. As conclusões são deduzidas a partir das premissas. Caso o estado das premissas esteja vazio, então a conclusão é dita ser o axioma da lógica.

Uma propriedade desejável de uma regra de inferência é que esta seja efetiva, isto é, existe um procedimento efetivo para determinar se uma dada fórmula é inferível de um dado conjunto de fórmulas.

Regras de inferência têm as seguintes características:

Se a Hipótese for verdadeira, então a Conclusão é verdadeira;
Verificação de tipos é baseada em inferência. Se E1 e E2 tem certos tipos, então E3 tem um certo tipo;
Regras de inferência são uma notação compacta para comandos de implementação;
Inicia-se com um sistema simplificado de regras ao qual adiciona-se novas características gradualmente;
As premissas são regras sem hipóteses.

Uma regra de inferência não precisa preservar qualquer propriedade semântica como verdadeira, já que não existe nenhuma regra que garanta que uma caracterização lógica sintática tenha uma semântica. Uma regra pode preservar, por exemplo, a propriedade da conjunção de uma sub-fórmula da uma fórmula mais extensa do conjunto de premissas.

Note que existem diferentes sistemas de lógicas formais, cada qual com seus próprios conjuntos de fórmulas bem-formadas, regras de inferências, e algumas vezes, semânticas. Tome como exemplo as lógicas temporal, modal ou intuicionista. Na lógica de primeira ordem, é necessária uma regra de inferência adicional, conhecida como generalização.

Na lógica formal, as regras de inferência são normalmente determinadas nas seguinte forma:
premissa #1
premissa #2
...
premissa #n
____________
conclusão

Esta expressão indica, que sempre que as premissas dadas forem obtidas durante alguma derivação lógica, a conclusão especificada pode ser provada. A linguagem formal que é usada para descrever ambas premissas e conclusões depende do atual contexto das derivações. Por exemplo, pode ser usada como uma fórmula lógica, assim como em

A→B

A

∴B

ao qual é justamente a regra modus ponens da lógica proposicional. Regras de inferência são freqüentemente formuladas como regras esquematizadas pelo uso de variáveis universais. Na regra (esquemática) acima. A e B podem ser substituídas por algum elemento do universo (ou às vezes, por convenção, alguns sub-conjuntos restritos como as proposições) um conjunto infinito de regras de inferência.

Um sistema de prova é formado por um conjunto de regras, as quais podem ser interligadas para formar provas, ou derivações. Uma derivação tem apenas uma conclusão, a qual é um enunciado provado ou derivado. Se a premissa for verdadeira, então a conclusão também o será.

Admissibilidade e Derivabilidade

Em um conjunto de regras, uma regra de inferência pode ser redundante no sentido de que ela pode ser admissível ou derivável. Uma regra derivável é aquela que a conclusão pode ser derivada de suas premissas usando outras regras. Uma regra admissível é aquela que a conclusão é verdadeira sempre que as premissas também o forem. Todas as regras deriváveis são admissíveis. Para observar a diferença, considere os seguintes conjuntos de regras para definir os números naturais (tome $n\,\,{\mathsf {nat}}$ como $n$ pertencendo ao conjunto dos números naturais).

${\begin{matrix}{\frac {}{\mathbf {0} \,\,{\mathsf {nat}}}}&{\frac {n\,\,{\mathsf {nat}}}{\mathbf {s(} n\mathbf {)} \,\,{\mathsf {nat}}}}\\\end{matrix}}$

A primeira regra indica que 0 é um número natural, e o segundo indica que s(n) é um número natural se n também o for. Em um sistema de provas, a regra a seguir demonstra que o segundo sucessor de um número natural é também um número natural, é derivável:

${\frac {n\,\,{\mathsf {nat}}}{\mathbf {s(s(} n\mathbf {))} \,\,{\mathsf {nat}}}}$

Estas derivações são apenas composições de dois usos da regra de sucessão acima. A regra a seguir para a afirmação da existência de um antecessor para algum número diferente de zero é meramente admissível:

${\frac {\mathbf {s(} n\mathbf {)} \,\,{\mathsf {nat}}}{n\,\,{\mathsf {nat}}}}$

Este é um fato dos números naturais, como pode ser provado por indução (para provar que esta regra é admissível, uma delas deve assumir uma derivação da premissa, e induzir para produzir uma derivação de $n\,\,{\mathsf {nat}}$ ). Entretanto, ele não é derivável, porque ele depende de uma estrutura da derivação da premissa. Pelo fato desta derivabilidade ser estável sob adições para um sistema de provas, a admissibilidade não o é. Para ver a diferença, suponha que a seguinte regra sem sentido fosse adicionada para o sistema de provas:

${\frac {}{\mathbf {s(-3)} \,\,{\mathsf {nat}}}}$

Neste novo sistema, a regra da dupla sucessão ainda é derivável. Entretanto, a regra para achar o antecessor já não é admissível, pois não há como derivar $\mathbf {-3} \,\,{\mathsf {nat}}$ . A fragilidade da admissibilidade vem da maneira como é provada: desde que a prova possa induzir na estrutura das derivações das premissas, extensões para o sistema adicionam novos casos para esta prova, a qual pode já não ser mais válida.

Regras admissíveis podem ser pensadas como teoremas de sistemas de provas. Por exemplo, no cálculo seqüencial onde o teorema do corte é válido, a regra do corte é admissível.

Outras Considerações

Regras de inferências podem também ser indicadas desta forma: 1. algumas (talvez nenhuma) premissas. 2. o símbolo $\vdash$ "infere", "prova" ou "conclui". 3. uma conclusão.

Isto geralmente uma visão relacional (oposto de funcional) de uma regra de inferência, onde o $\vdash$ mantém uma relação de dedução entre premissas e conclusões.

Regras de inferência devem ser distinguidas de axiomas de uma teoria. Em termos de semântica, axiomas são asserções válidas. Axiomas são considerados pontos iniciais para a aplicação de regras de inferência e geração de um conjunto de conclusões. Ou em termos informais:

Regras são enunciados SOBRE o sistema, axiomas são enunciados no sistema. Por exemplo:

A regra que de $\vdash p$ você pode inferir que $\vdash$ Derivável(p) é um enunciado que diz que se você pode provar p, então é provável que p seja derivável. Isto é usado na aritmética de Peano, por exemplo.

O axioma Derivável(p) pode significar que todo enunciado verdadeiro é derivável. Isto, entretanto, não é usado na aritmética de Peano.

Regras de inferência possuem um papel vital na especificação do cálculo lógico tanto na teoria de prova quanto no cálculo sequencial e na dedução natural.

Ver também

Ligações externas