Obra: Lógica/Cálculo Proposicional Clássico/Dedução Natural - Parte I
Matéria: Matemática
introdução até agora nós temos dois métodos que sempre determinam validade de argumentos fórmulas no cpc cálculo proposicional clássico as tabelas de verdade os tableaux semânticos claro que também podemos determinar validade de uma fórmula mostrando que esta se trata de uma instância de outra fórmula válida ou por de operadores mostrar que ela equivalente uma outra fórmula válida mas estes métodos não são aplicáveis em quaisquer circunstâncias agora aprenderemos um terceiro método que sempre determina validade de fórmulas argumentos no cpc além de consistir em um método de derivação dedução natural tomemos seguinte argumento as tabelas de verdade não parecem muito práticas neste caso afinal temos quatro fórmulas atômicas que requer uma tabela de linhas sem falar que teríamos muitas colunas também dada quantidade de sub fórmulas alternativa provar validade do argumento por tableaux contudo repare que intuitivamente este argumento não passa da simples combinação de vários argumentos válidos simples que nós já conhecemos temos modus ponens eliminação da dupla negação também sabemos que se uma fórmula verdadeira então entre uma fórmula arbitrária ao menos uma verdadeira ou seja esse argumento chamado de expansão ora seguinte argumento obviamente uma instância da expansão se sabemos de tudo isso então porque usar método de tableaux semânticos se estes nos obrigam considerar valor de proposições arbitrárias como assim como lidar com os valores de de quando sabemos que primeira equivalente justamente isto que dedução natural permite por meio de um pequeno número de regras de inferência demonstrar validade de uma infinidade de fórmulas argumentos sem necesidade de considerar os valores que cada fórmula ou subfórmula recebe ou seja não estamos mais lidando com semântica mas com sintaxe agora incrementaremos nossa notação terminologia até agora usamos martelo semântico agora usaremos martelo sintático leitura que fazemos de cada conseqüência semântica de ou implica semanticamente em conseqüência sintática de ou partir de prova se uma fórmula válida tautologia no caso do cpc um teorema dito de um sistema lógico que ele correto se ele verifica seguinte propriedade ou seja que todos os argumentos sintaticamente válidos também são semanticamente válidos dito de um sistema lógico que ele completo se ele verifica seguinte propriedade ou seja que todos os argumentos semanticamente válidos também são sintaticamente válidos cpc verifica ambas propriedades ou seja cpc verifica que obviamente isto também verificado na instância em que portanto ou seja todo teorema tautologia toda tautologia teorema regras de inferência diretas nas disciplinas matemáticas como lógica geometria aritmética etc preferível demonstrar máximo de teoremas construções válidos obviamente por meio do mínimo de conceitos primitivos axiomas regras de inferência etc na dedução natural trabalhamos apenas com regras de inferência para que correção do sistema seja verificada as regras escolhidas dev
penas com regras de inferência para que correção do sistema seja verificada as regras escolhidas devem ser reconhecidas como válidas completude um pouco mais complicada digamos que para verificar completude ideal seria ter duas regras para cada operador usado uma que insira outra que remova trabalharemos primeiramente com as regras de infererência diretas como nome sugere estas regras regulam quais fórmulas podemos inferir diretamente de outras fórmulas ficheiro regras de inferencia diretas png agora vejamos como construir uma dedução usando as regras de inferência diretas vamos provar aquele argumento da introdução primeiro passo colocar cada premissa em uma linha enumerada premissa premissa agora aplicamos as regras de inferência que julgarmos úteis para chegar ao resultado esperado para cada nova fórmula inferida inserimos uma linha enumerada indicando direita as linhas que contém as fórmulas partir das quais foi efetuada inferência assim como regra aplicada por exemplo vamos aplicar nas linhas modus ponens mp premissa premissa mp agora aplicaremos regra de dupla negação dn na linha fim de derivar então aplicaremos expansão fim de obter premissa premissa mp dn ou seja sob conjunto de premissas derivamos por meio de inferências reconhecidas como válidas portanto repare também que na linha provamos que na linha façamos mais uma derivação fim de aplicar outras regras vamos provar que premissa premissa bc mp nas linhas temos as premissas respectivamente aplicamos bi condicionais para condicionais bc na linha derivamos na linha então aplicamos separação na linha fim de derivar na linha aplicamos modus ponens nas linhas fim de derivar na linha então aplicamos conjunção nas linhas fim de derivar exercícios prove por dedução natural que resolução dos exercícios trabalhando com hipóteses você deve ter reparado que faltou uma regra para inserir negação assim como uma regra para inserir implicação da bi implicação para tal fazemos uso das regras hipotéticas ou seja regras que nos permitem trabalhar com hipóteses em dedução natural hipóteses são quaisquer fórmulas bem construídas que inserimos na derivação sem derivá las de quaisquer outras fórmulas com as regras hipotéticas nosso sistema fica completo vejamos então um esquema geral para trabalhar com as hipóteses premissa hipótese inserimos uma hipótese na linha isto nos obriga inserir uma linha vertical esta linha permanecerá aí até aplicarmos uma regra hipotética que remova até então tudo que derivarmos por meio das regras diretas estará direita da linha de hipótese premissa hipótese alguma regra hipotética também podemos levantar hipóteses dentro de hipóteses inserindo novas linhas verticais premissa hipótese hipótese alguma regra hipotética alguma regra hipotética antes de apresentarmos as regras hipotéticas lembre se de sempre respeitar as seguintes prescrições introduzir uma linha vertical para cada nova hipótese uma vez que uma linha descartada não usar mais qualquer fórmula que esteja sua direita
nova hipótese uma vez que uma linha descartada não usar mais qualquer fórmula que esteja sua direita as hipóteses devem ser descartadas na ordem inversa nas quais são levantadas uma dedução não está terminada enquanto não forem descartadas todas as hipóteses redução ao absurdo raa se partir de uma hipótese derivarmos uma contradição então descartamos hipótese introduzimos na derivação um exemplo premissa hipótese raa na linha temos como premissa na linha levantamos hipótese na linha aplicamos conjunção em obtendo contradição como partir da hipótese derivamos uma contradição descartamos deduzimos sua negação portanto regra de prova condicional rpc se ao levantarmos uma hipótese inferimos então podemos descartar hipótese inserir na derivação por exemplo premissa premissa hipótese mp mp rpc aqui temos as premissas nas linhas respectivamente na linha levantamos hipótese aplicando modus ponens nas linhas inferimos na linha aplicando modus ponens nas linhas inferimos na linha dado que apartir de inferimos descartamos hipótese inserimos na dedução portanto exercícios fazendo uso das regras hipotéticas demonstre que resolução dos exercícios