Teorema da Dedução - Interpretação
No livro "Um passeio pela lógica matemática" - de Robert S. Wolf, o teorema da dedução é especificado da seguinte forma:
Se T $\cup$ {P} $\vdash$ Q, então T $\vdash$ (P $\to$ Q)
Onde T é uma teoria de primeira ordem e P & Q são algumas fórmulas, na linguagem desta teoria de primeira ordem. Então, a seguinte interpretação, do teorema da dedução, é correta?
Se Q é derivável / provável de T $\cup$ {P}, então pode-se dizer que - se P é derivável de T (isto é, P é um teorema de T), então Q também é derivável de T.
Além disso, essa interpretação captura a essência do teorema da dedução?
PS: outra questão intitulada Teorema da dedução - Intuição , parece focar principalmente nos aspectos sintáticos do teorema e do cálculo de predicados em geral - ao invés de em sua semântica.
Respostas
é a seguinte interpretação, do teorema da dedução, correta?
Não. O que você escreve é
E se $T \cup \{P\} \vdash Q$, então se $T \vdash P$, então $T \vdash Q$.
Isso é o mesmo que dizer
(1) Se $T \cup \{P\} \vdash Q$, então $T \nvdash P$ ou $T \vdash Q$.
Mas isso não é equivalente a
(2) Se $T \cup \{P\} \vdash Q$, então $T \vdash P \to Q$.
Pode ser o caso de $P$ não é provável, mas $P \to Q$também não é. Então "$T \nvdash P$ ou $T \vdash Q$"segura, mas"$T \vdash P \to Q$"não. Então (1) $\not \Rightarrow$ (2)
Isso é o que se entende nos comentários por "trivialização": "se $T \vdash P$ então $T \vdash Q$"(= o que você escreveu) torna-se trivialmente verdadeiro se $T \nvdash P$, ou seja, se $P$é improvável. Mas "$T \vdash P \to Q$"(= o que afirma o teorema da dedução) não: Só porque não podemos provar $P$ não significa que podemos provar $P\to Q$- como você observou. Daí porque "$T \vdash P \to Q$"é uma afirmação mais forte de que" Se $T \vdash P$ então $T \vdash Q$"
A essência do teorema de dedução é que você pode "inverter" entre ter um teorema dependente de uma suposição aberta e provar uma afirmação condicional:
Se houver uma prova de$Q$ que ainda depende da suposição $P$, então haverá uma prova na teoria da afirmação $P \to Q$. Este é o efeito imediato da técnica de prova condicional (ver p. 14).
E para a direção oposta do teorema da dedução, se você pode provar$P \to Q$, então você será capaz de provar $Q$ sob a suposição de que $P$. Isso é uma consequência da regra de inferência do modus ponens (ver p. 13).
As duas direções combinadas, o teorema da dedução simplesmente justifica o que queremos dizer com uma prova de "$\to$"
Você está completamente certo em apontar que a noção central de um sistema formal é a de prova e não de verdade. Mas tenha em mente que normalmente estamos interessados em projetar um sistema de prova "útil" que esteja "alinhado" com a noção de verdade: uma afirmação deve ser demonstrável em uma teoria exatamente quando é verdadeira em todos os modelos da teoria . Afinal, o objetivo de um sistema de prova é ter um dispositivo mecânico para provar com rigor as afirmações que consideramos verdadeiras. Portanto, embora a noção de uma prova de$\to$ é formulado em termos de regras de inferência, a forma como essas regras são usadas reflete a tabela de verdade para $\to$: Um sistema de prova deve ser (e como para o sistema de prova apresentados no livro de Wolf, é) som wrt a semântica: O que pode ser provado é verdade (de acordo com as definições da tabela de verdade) em todas as estruturas; o sistema (espero) não prova um absurdo aleatório.