Prova formal - Formal proof
Em lógica e matemática , uma prova formal ou derivação é uma sequência finita de sentenças (chamadas de fórmulas bem formadas no caso de uma linguagem formal ), cada uma das quais é um axioma , uma suposição ou segue das sentenças anteriores na sequência por uma regra de inferência . Difere de um argumento de linguagem natural por ser rigoroso, inequívoco e verificável mecanicamente. Se o conjunto de suposições estiver vazio, a última frase em uma prova formal é chamada de teorema do sistema formal . A noção de teorema não é, em geral , eficaz ; portanto, pode não haver método pelo qual possamos sempre encontrar uma prova de uma dada sentença ou determinar que ela não existe. Os conceitos de prova ao estilo de Fitch , cálculo sequencial e dedução natural são generalizações do conceito de prova.
O teorema é uma consequência sintática de todas as fórmulas bem formadas que o precedem na prova. Para que uma fórmula bem formada seja qualificada como parte de uma prova, ela deve ser o resultado da aplicação de uma regra do aparato dedutivo (de algum sistema formal) às fórmulas anteriores bem formadas na sequência de prova.
As provas formais muitas vezes são construídas com a ajuda de computadores em prova interativa de teoremas (por exemplo, através do uso de verificador de prova e provador de teorema automatizado ). Significativamente, essas provas podem ser verificadas automaticamente , também por computador. Verificar provas formais é geralmente simples, enquanto o problema de encontrar provas (prova automatizada de teoremas ) é geralmente computacionalmente intratável e / ou apenas semi-decidível , dependendo do sistema formal em uso.
Fundo
Linguagem formal
Uma linguagem formal é um conjunto de sequências finitas de símbolos . Tal linguagem pode ser definida sem referência a quaisquer significados de qualquer uma de suas expressões; pode existir antes que qualquer interpretação seja atribuída a ele - isto é, antes que tenha qualquer significado. As provas formais são expressas em algumas linguagens formais.
Gramática formal
Uma gramática formal (também chamada de regras de formação ) é uma descrição precisa das fórmulas bem formadas de uma linguagem formal. É sinônimo de conjunto de cordas sobre o alfabeto da linguagem formal que constituem fórmulas bem formadas. No entanto, não descreve sua semântica (ou seja, o que significam).
Sistemas formais
Um sistema formal (também chamado de cálculo lógico ou sistema lógico ) consiste em uma linguagem formal junto com um aparato dedutivo (também chamado de sistema dedutivo ). O aparato dedutivo pode consistir em um conjunto de regras de transformação (também chamadas de regras de inferência ) ou um conjunto de axiomas , ou ter ambos. Um sistema formal é usado para derivar uma expressão de uma ou mais outras expressões.
Interpretações
Uma interpretação de um sistema formal é a atribuição de significados aos símbolos e valores de verdade às sentenças de um sistema formal. O estudo das interpretações é chamado de semântica formal . Dar uma interpretação é sinônimo de construir um modelo .
Veja também
- Sistema axiomático
- Verificação formal
- Prova matemática
- Assistente de prova
- Cálculo de prova
- Teoria da Prova
- Prova (verdade)
Referências
links externos
- "Uma edição especial sobre a prova formal" . Avisos da American Mathematical Society . Dezembro de 2008.
- 2πix.com: Lógica Parte de uma série de artigos que cobrem matemática e lógica.
- Arquivo de Provas Formais
- Home Page da Mizar