Contato

  • Jean Paulo Martins (jeanmartins utfpr edu br)
  • Sala 105, Bloco S (UTFPR - Campus Pato Branco)

Conteúdo

Introdução

Estudamos na lógica proposicional dois algoritmos principais para demonstrarmos a validade e invalidade de formas de argumentos: tabelas verdade, árvores de refutação. Deste modo, dada qualquer forma de argumento com premissas e uma conclusão

é possível na lógica proposicional determinarmos se tal forma de argumento é válida ou não é valida.

  • Uma forma de argumento é válida, se sempre que suas premissas forem verdadeiras ($\phi,\psi$) sua conclusão seja verdadeira ($\chi$)

Apesar de ineficientes em certas situações, tanto tabelas verdade quanto árvores de refutação podem, em princípio, ser utilizados para implementarmos um programa que verifique a validade de formas de argumento. Esse programa hipotético, pode tomar um tempo consideravelmente grande para chegar a uma decisão, mas ele eventualmente chegará a essa decisão, portanto diz-se que:

  • A lógica proposicional é decidível. Pois existem algoritmos que decidem se qualquer forma de argumento é válida ou não.

Na lógica de predicados, a situação é diferente. Apesar de existirem procedimentos que nos permitem verificar a validade e invalidade de alguns tipos de formas de argumentos, não existe, e não pode existir, um procedimento que verifique qualquer forma de argumento da lógica de predicados. Portanto, diz-se que:

  • A lógica de predicados é indecidível. Pois não existe algoritmo que decida a validade de qualquer forma de argumento.

Árvores de refutação

As árvores de refutação para a lógica de predicados são generalizadas pela introdução de seis novas regras, as quais tratarão fórmulas precedidas pelos quantificadores universal ou existencial. No entanto, existirão situações em que apenas as regras utilizadas na lógica proposicional serão úteis. Vejamos um exemplo:

Na primeira etapa da demonstração, apenas listamos as premissas e a negação da conclusão. Neste momento a árvore possui apenas um ramo contendo todas essas três fórmulas.

Como visto nas árvores de refutação da lógica proposicional, existem apenas duas regras para expansão da árvore: conjunção, disjunção. Qualquer outro operador lógico deve ser tratado por meio de fórmulas equivalentes que utilizem apenas conjunção e/ou disjunção.

Neste exemplo, temos uma fórmula condicional do tipo $\phi\to\psi$, representada por $\forall x Fx \to \forall x Gx$, devemos então utilizar em seu lugar uma fórmula equivalente. Como $\phi\to\psi \dashv\vdash \neg\phi\lor\psi$, podemos utilizar a equivalência.

Das três fórmulas restantes não marcadas, apenas aquela na linha 4 pode ser expandida, para tal aplicamos a regra da disjunção, a qual cria dois ramos, um para cada disjuncto.

Neste momento, encontramos uma contradição em cada um dos ramos.

As contradições fecharam todos os ramos, portanto essa é uma forma de argumento válida, significando que sempre que $\forall x Fx \to \forall x Gx$ e $\neg \forall x Gx$ forem verdadeiras, então $\neg \forall x Fx$ também será verdadeira. Esta fórmula é a versão em lógica de predicados da regra Modus Tollens.

Generalização das Árvores de Refutação

Quantificador universal ($\forall$)

Se uma fórmla $\forall x Fx$ aparece num ramo aberto da árvore de refutação, e $a$ é uma letra nominal que aparece numa fórmula desse ramo, então podemos instanciar a fórmula, obtendo: $Fa$. Diferente do que ocorreria para as demais regras, a fórmula $\forall x Fx$ não é marcada com $\checkmark$ neste caso, pois ela pode ser instanciada novamente com outras letras nominais que também apareçam no mesmo ramo. Apenas nos casos em que não existam letras nominais no ramo é que uma letra pode ser introduzida.

Demonstre a validade ou invalidade das seguintes forma de argumento.

Quantificador existencial negado ($\neg \exists$)

Se uma fórmula da forma $\neg \exists x Fx$ aparece num ramo aberto, ela deverá ser marcada e substituída por sua equivalente $\forall x\neg Fx$ no final de cada ramo aberto que a contém. $\neg \exists x Fx \dashv \vdash \forall x \neg Fx$

Demonstre a validade ou invalidade das seguintes forma de argumento.

Quantificador existencial ($\exists$)

Se uma fórmula da forma $\exists x Fx$ aparece num ramo aberto, ela deve ser marcada. Escolhemos então, uma letra nominal $a$ que ainda não apareceu no mesmo ramo e instanciamos a fórmula, como $Fa$, no final de todo ramo aberto que a contenha.

Quantificador universal negado ($\neg \forall$)

Se uma fórmula da forma $\neg \forall x Fx$ aparece num ramo aberto, ela deve ser marcada e substituída por sua equivalente $\exists x \neg Fx$.

Demonstre a validade ou invalidade das seguintes forma de argumento.