Regra de inferência: diferenças entre revisões
Conteúdo apagado Conteúdo adicionado
Linha 33:
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 <math>n\,\,\mathsf{nat}</math> como <math>n</math> pertencendo ao conjunto dos números naturais).
<math>
\begin{matrix}
\frac{}{\mathbf{0} \,\,\mathsf{nat}} &
\frac{n \,\,\mathsf{nat}}{\mathbf{s(}n\mathbf{)} \,\,\mathsf{nat}} \\
\end{matrix}
</math>
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:
<math>
\frac{n \,\,\mathsf{nat}}{\mathbf{s(s(}n\mathbf{))} \,\,\mathsf{nat}}
</math>
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:
<math>
\frac{\mathbf{s(}n\mathbf{)} \,\,\mathsf{nat}}{n \,\,\mathsf{nat}}
</math>
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 <math>n \,\,\mathsf{nat}</math>). 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:
<math>
\frac{}{\mathbf{s(-3)} \,\,\mathsf{nat}}
</math>
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 <math>\mathbf{-3} \,\,\mathsf{nat}</math>. 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 <math> \vdash </math> "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 <math> \vdash </math> 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 <math>\vdash p</math> você pode inferir que <math>\vdash Provable(p)</math> é um enunciado que diz que se você pode provar p, então é provável que p seja provável. Isto é usado na aritmética de Peano, por exemplo.
O axioma <math>p \to Provable(p)</math> pode significar que todo enunciado verdadeiro é prová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 seqüencial e na dedução natural.
=={{Ver também}}==
| |||