O que significa “provar”?
O que significa "provar"?
Estou usando os exemplos a seguir para entender os casos gerais. Não sei como articular minhas perguntas no caso geral. Eu queria saber em que níveis os seguintes são declarados, como os seguintes são formulados e quais diferenças e relações existem entre eles:
Prove uma fórmula $p$. Isso significa provar$ \vdash p$ (ou $\models p$?) e, portanto, converter a tarefa para 3 abaixo? (Posso ter perguntado isso em algum comentário, e alguém pode ter respondido que provar$p$ meios para provar $\vdash p$, mas não consigo encontrar os comentários.)
Provar se $\phi$, então $\psi$. O que significa provar:$\phi \to \psi$, $\phi \vdash \psi$, ou $\phi \models \psi$e, portanto, converter a tarefa em 1 acima ou 3 abaixo?
Provar $\phi \vdash \psi$.
Isso significa derivar $\phi \vdash \psi$, usando as regras de inferência e axiomas em um determinado sistema de prova (por exemplo, cálculo sequencial)?
Ou trata $\phi \vdash \psi$ como uma fórmula em um idioma em um nível mais alto do que o idioma que contém $\phi$ e $\psi$, e provar $\vdash (\phi \vdash \psi)$ aplicando um determinado sistema de prova (por exemplo, cálculo sequencial) a essa linguagem de nível superior?
Provar se $\phi' \vdash \psi'$, então $\phi \vdash \psi$.
Isso significa derivar $\phi \vdash \psi$, usando $\phi' \vdash \psi'$, e as regras de inferência e axiomas em um determinado sistema de prova (por exemplo, cálculo sequencial)?
Ou trata $\phi' \vdash \psi'$ e $\phi \vdash \psi$ como fórmulas em um idioma em um nível superior do que o idioma que contém $\phi$, $\psi$, $\phi'$ e $\psi'$, e provar $(\phi' \vdash \psi') \vdash (\phi \vdash \psi)$ aplicando um determinado sistema de prova (por exemplo, cálculo sequencial) a essa linguagem de nível superior?
e 6. Considere substituir $\vdash$ com $\models$ em 3 e 4
Algo relacionado: perguntei :
"Provável" ou "contestável" aplica-se apenas a fórmulas, não a "uma inferência" ou "derivação", como $∃𝑥𝑅𝑥⊢∀𝑦𝑅𝑦$? Podemos reescrever$∃𝑥𝑅𝑥⊢∀𝑦𝑅𝑦$ como uma fórmula, de modo que é (quase) derivável se e somente se a fórmula correspondente é demonstrável?
Lemontree respondeu :
"Provável" significa "derivável sem premissas", ou seja, a provabilidade é uma propriedade das fórmulas, enquanto a derivabilidade é uma propriedade das inferências em geral. O que você está procurando é provavelmente o teorema da dedução, também conhecido como teorema de importação-exportação, que afirma que$𝐴_1,…,𝐴_𝑛⊢𝐵$ se e apenas se $⊢(𝐴_1∧…∧𝐴_𝑛)→𝐵$. Assim, com$∃𝑥𝑅(𝑥)⊬∀𝑦𝑅(𝑦)$ nós temos isso $⊬∃𝑥𝑅(𝑥)→∀𝑦𝑅(𝑦)$, isto é, a fórmula $∃𝑥𝑅(𝑥)→∀𝑦𝑅(𝑦)$ não é provável.
Acho que minhas perguntas acima são uma coisa de metalinguagem , ou teoria da prova, e sei pouco sobre elas. Ao mesmo tempo, também estava me perguntando como as técnicas de prova são formuladas na lógica matemática? , que pode ser parte da teoria da prova?
Obrigado.
Respostas
“Provar” em matemática significa escrever uma prova de uma afirmação no contexto de uma teoria matemática. Uma prova será um "argumento" começando com os axiomas da teoria e resultados comprovados anteriores e concluindo com a afirmação a ser provada que usa etapas dedutivas "corretas" lógicas (isto é, um argumento válido ).
Na lógica, temos o conceito de derivação, isto é, o modelo matemático formal de uma prova no contexto de um cálculo lógico, por exemplo, dedução natural .
Os passos lógicos dedutivos são normalmente formalizados através de regras de inferência , que são os blocos básicos de construção do sistema de prova , também conhecido como: "cálculo lógico".
Tentando seguir o livro de Ebbinghaus, o símbolo $\vDash$é uma expressão de metalinguagem usada no contexto semântico com diferentes usos: flanqueada à direita por uma fórmula que abrevia “é válida” (página 35); entre o nome de um conjunto de fórmulas e uma fórmula abrevia “é uma consequência de” (página 33).
Finalmente, ladeado pelo nome de uma interpretação e de uma fórmula abrevia "é verdadeiro segundo a interpretação".
Não faz parte da linguagem formal do cálculo: é usado para expressar propriedades das fórmulas do cálculo; no contexto do cálculo proposicional , lemos a expressão "$⊨ A ∨ ¬A$“como“ fórmula ... é uma tautologia ”, ou seja, é uma fórmula válida de cálculo proposicional.
Podemos provar (na metateoria) que a fórmula $A ∨ ¬A$é uma tautologia que usa o método da tabela de verdade (esta "prova" é uma prova matemática, e não uma derivação no cálculo).
Semelhante para o símbolo $\vdash$ (ver definição página 61).
Seguindo Ebbinghaus, $\varphi \to \varphi$ é uma fórmula, ou seja, uma expressão da linguagem formal que lemos: “se $\varphi$, então $\varphi$”.
Podemos facilmente derivá-lo no sistema de prova e simbolizamos a existência de tal derivação com $\vdash \varphi \to \varphi$ que novamente não é uma fórmula da linguagem formal, mas uma expressão da meta-linguagem abreviando a afirmação: “há uma derivação de ....” e nós lemos (de acordo com a resposta ao seu post anterior): “fórmula. .. é derivável (no cálculo) ".
Infelizmente, em algumas formulações de ND e Cálculo de Sequência, o símbolo $\vdash$faz parte da linguagem formal, caso em que podemos ter problemas para usá-la também na metateoria .
Finalmente, temos que considerar o Teorema da Solidez e da Completude , um metateorema válido tanto para o cálculo proposicional quanto para o predicado (ver página 70 e página 75) que dizem em poucas palavras:
“$\vdash \text { iff } \vDash$”.
Este teorema expressa uma propriedade do cálculo e sua semântica. Provamos isso de uma forma matemática “padrão”.
Como dito acima, podemos usar a tabela verdade para provar que $A ∨ ¬A$ é uma tautologia ($⊨ A ∨ ¬A$) e, em seguida, usar Completude para provar $⊢ A ∨ ¬A$.
Desta forma, usamos um argumento (tabela verdade) para provar uma propriedade "semântica" de uma determinada fórmula e, em seguida, usamos um meta-teorema (Completude) para provar uma segunda propriedade da mesma fórmula: a existência de uma derivação na sistema de prova correspondente.
Essa é a essência dos dois símbolos onipresentes .