Lógica Matemática & Computacional

Pela professora Daniele Nantes

Índice

  1. Introdução
    1. Paradoxo de Russel
  2. Lógica Proposicional
    1. Alfabeto da Lógica
    2. Dedução natural
      1. Notação
      2. Regras
        1. Regras para conjunção
        2. Regras para negação
        3. Regras para implicação
        4. Regras para disjunção
    3. Propriedades
      1. Propriedades da negação
      2. Propriedades da implicação
    4. Lógicas Intuicionista e Clássica
      1. Propriedades diversas
    5. Semântica da Lógica Proposicional
      1. Propriedades semânticas
      2. Semântica da implicação
        1. Examplos da Álgebra
        2. Causalidade
      3. Contradição
      4. Relação entre proposições semânticas
        1. Tautologia e contradição
        2. Tautologia e satisfatibilidade
        3. Implicação semântca e implicação sintática
        4. Equivalência semântica e "se, e somente se"
        5. Equivalência e implicações semânticas
        6. Transitividade de \(= \parallel = \)
        7. Satisfatibilidade
      5. Teorema da dedução, versão semântica
        1. Corolários
    6. Princípio da indução
      1. Indução natural
      2. Indução estrutural
    7. Correção e completude
      1. Correção da lógica proposicional
      2. Corretude da lógica proposicional
    8. Fórmulas Equivalentes
      1. Equivalências importantes
      2. Formas normais conjuntivas e disjuntivas
        1. Método da tabela verdade
      3. Resolução
      4. Cláusulas
      5. Procedimento de Davis-Putnam
        1. Correção e completudo do DPP
        2. Compacidade da lógica proposicional
        3. Caso geral de correção e completude da resolução
      6. Cláusulas de Horn
      7. Cláusulas de grafos
      8. Teorema de Tseitin
  3. Lógica de Predicados

Introdução

Paradoxo de Russel

Considere o conjunto de todos os conjuntos que não são membros de si mesmos:

` Q := \{ P | P !in Q \} ` ` :. A in Q => A !in Q `

Este paradoxo levou Russel a começar a desenvolver a lógica prosicional a fim de explicar a matemática.

Lógica Proposicional

O objetivo da lógica e da Matemática é modelar situações ou problemas de forma que seja possível raciocinar sobre eles formalmente. A fim de fazer argumentos formais, vamos desenvolver uma lógica simbólica a partir da qual podemos expressar sentenças declarativas (ou proposições) e mostrar suas estruturas lógicas. Para isso, vamos definir a linguagem da lógica.

Alfabeto de Lógica

O alfabeto da lógica é constituído por:

As fórmulas da lógica proposicional são constituídas indutivamente a partir dos símbolos do alfabeto conforme as regras a seguir:

Os conectivos lógicos satisfazem a seguinte ordem:

  1. `not`
  2. `^^ > vv`
  3. `=> > <=>`

Convenciona-se que a implicação é associativa à direita.

Seja `H` uma fórmula da lógica proposicional (LP). Então:

Dedução natural

Considere o seguinte argumento:

  1. Se o trem chegar tarde e não existirem taxis na estação, então Carlos está atrasado para a reunião.
  2. Carlos não está atrasado para a reunião.
  3. O trem chegou tarde.

Dela conclui-se que havia taxis na estação. Podemos modelar a situação da seguinte forma:

`P := ` "O trem chegar tarde"

`Q := ` "Existem taxis na estação"

`R := ` "Carlos está atrasado para reunião"

  1. `P ^^ not Q => R`
  2. `not R`
  3. `P`
  4. `Q`

Vamos ter um conjunto de regras de prova que permitirão inferir derivar, concluir fórmulas a partir de outras fórmulas. Aplicando estas regras sucessivamente, podemos inferir uma conclusão a partir de um conjunto de premissas, que são proposições inciais que servem de base oara uma argumentação ou para um raciocínio.

Notação

Suponha que tenhamos um conjunto `\{ phi_i \}_(i=1)^(n)` de proposições (as nossas premissas) e uma fórmula `psi` que será a nossa conclusão (ou sequente).

`\{ phi_i \}_(i=1)^(n) |-- psi`

Suas premissas provam a conclusão. Um sequente é válido se existe uma prova para ele.

Regras

Regras para conjunção

Exemplo: prove que `P ^^ Q, R |-- Q ^^ R`

\( \cfrac {\cfrac {P \wedge Q} {Q} \ R } {Q \wedge R} \)

Exercício: `(P ^^ Q) ^^ R, S ^^ T |-- Q ^^ S`

Regras para negação

Exercício: `P, not not (Q ^^ R) |-- not not P ^^ R`

Regras para implicação

Regras para disjunção

Fórmulas lógicas `phi` com sequentes `|-- phi` são chamados Teoremas.

Propriedades

A conjunção e a disjunção são distributivas:

`(P vv Q) vv R |-- P vv (Q vv R)` e vice-versa

`P ^^ (Q vv R) |-- (P ^^ Q) vv (P ^^ R)` e vice-versa

Propriedades da negação

Elas involvem a noção de alguma contradição, que são expressões da forma `phi ^^ not phi`, onde `hi` é uma fórmula qualquer.

Exercícios:

Propridades da implicação

A regra "Inclusão da Implicação" pode ser aplicada sem descarregar nenhuma hipótese: quando se sabe que `psi` é verdadeiro, `phi => psi AA phi` e `not phi => psi AA phi`

`([R]^U \ \ Q)/(R => Q)`

`:. Q |-- R => R AA R`

Observe que a "Inclusão da Implicação" sem descarregamento de premissas pode ser substituído por uma derivação com descarregamento.

Convenção para descarregamento de hipótese temporária: a aplicação de regras com suposições temporárias podem descarregar nenhuma ou várias ocorrências de determinada fórmula.

Exemplo: `|-- phi => ((phi vv psi) ^^ (phi vv lambda))` é um descarregamento completo.

A negação de uma fórmula `phi`, dada por `not phi` pode ser representada por `not phi := phi => _|_`.

Lógicas Intuicionista e Clássica

A lógica intuicionista (LI) é composta das regras

Ela é base da matemática construtiva, que não admite a lei do meio excluído (`psi vv not psi`). Em LI, esta lei vale se, e somente se, (see) há uma prova para `psi` ou `not psi`, enquanto que, na lógica clássica (LC), `psi vv not psi` é um axioma. Portanto, `LI sube LC`.

Para alcançarmos a lógica proposional clássica, adicionaremos uma das seguintes regras:

Exercícios:

Propriedades diversas

Podemos transformar uma prova de

`phi_1, phi_2, ..., phi_n |-- psi`

em uma prova de

`|-- phi_1 => (phi_2 => (... => (phi_n => psi)))`


Em qualquer estágio de prova, é permitido fazer uma suposição temporária desde que ela seja descarregada.

Premissas podem ser utilizadas repetidamente (quantas vezes forem necessárias).

Sejam `phi,psi` fórmulas da LP. Dizemos que elas são equivalentes se os sequentes `phi |-- psi` e `psi |-- phi` são válidos. Denota-se por \( \phi \dashv \vdash \psi \).

Exercícios:

Semântica da Lógica Proposicional

A interpretação ou a semântica dis elementos sintáticos da linguagem da lógica proposicional é determinada por uma função `fr I` denominada "interpretação", que associa a cada fórmula da LPum valor verdadeiro (`TT`) ou falso (`_|_`)

`fr(I): LP -> \{ TT,_|_ \}`

`varphi |-> fr(I)(varphi) = TT,_|_`

onde o domínio LP é o conjunto de todas as fórmulas da lógica prosicional.

As regras da interpretação semântica são dadas pelas tabela-verdade.

`P` `Q` `P ^^ Q` `P vv Q` `P => Q` `P <=> Q`
`TT` `TT` `TT` `TT` `TT` `TT`
`TT` `_|_` `_|_` `TT` `_|_` `_|_`
`_|_` `TT` `_|_` `TT` `TT` `_|_`
`_|_` `_|_` `_|_` `_|_` `TT` `TT`

Propriedades Semânticas

Sejam `H,G, \{ H_i \}_(i=1)^(n)` fórmulas da LP. As propriedades semânticas são definidas por:

Semântica da Implicação

NÃO NECESSARIAMENTE UMA IMPLICAÇÃO POSSUI UMA RELAÇÃO DE CAUSA E EFEITO!

Na lógica, a fórmula `H => G` representa uma implicação material, em que não há necessariamente uma conexão causal entre `H` e `G`. O objetivo é dizer que, quando `H` é verdade e `fr(I)(H) = TT`, então `G` é verdade, i.e. `fr(I)(G) = TT`. Quando falamos da interpretação de `P => Q`, tratamos da fórmula como um todo.

Se `fr(I)(P) = _|_`, então `fr(I)(P => Q) != TT AA Q`. Informalmente, justifica-se que, a partir de uma afirmação falsa, pode-se concluir qualquer tipo de declaração.

Exemplos

Exemplo de Bertrand Russel

Se `2+2=5`, então minha namorada é o Papa.
  1. Suponha que `2+2=5`.
  2. É fácil que, se este for o caso, então `2=1`.
  3. Minha namorada e o Papa são 2 indivíduos. Como `2=1`, então minha namorada e o Papa são o mesmo indivíduo.

Exemplo da Álgebra

`P := \{ x in RR | x < 10 \}`

`Q := \{ x in RR | x^2 < 100 \}`

` x = 5 :. fr(I)(P) = TT ; fr(I)(Q) = TT :. fr(I)(P => Q) = TT `

` x = -20 :. fr(I)(P) = TT ; fr(I)(Q) = _|_ :. fr(I)(P => Q) = _|_ `

Causalidade

Conforme a tabela-verdade da implicação `P => Q`, se `fr(I)(Q) = TT`, então `fr(I)(P => Q) = TT AA P`. Logo, `P` e `Q` são independentes.

O conjunto `beta = \{ H_n \}_(n=1)^(oo)` é satisfatível see `EE fr(I) | \{ fr(I)(H_n) \}_(n=1)^(oo) -= TT`. Nesse caso, dizemos que `fr(I)` satisfaz `beta`. Denota-se `fr(I)(beta) = TT`.

Seja `S = \{\}`. Convenciona-se que `fr(I)(\{\}) = TT AA fr(I)`.

O conjunto `beta = \{ H_n \}_(n=1)^(oo)` implica semanticamente uma fórmula `H` quando existe uma interpretação `fr(I)` tal que, se `fr(I)(beta) = TT`, então `fr(I)(H) = TT`. Nesse caso, `H` é consequeência semântica de `beta`. Denota-se `B |== H`. No caso em que `beta` não implica semanticamente `H`, temos \( \beta \nvDash H \)

Exercícios

Contradição

A fórmula `P ^^ not P` está relacionada com o princípio da não-contradição da lógica clássica (LC): dada uma proposição e a sua negação, pelo menos uma delas é falsa.

Relações entre proposições semânticas

Tautologia e contradição

`H` é uma tautologia see `not H` é contraditória.

`not H` não é satisfatível see `not H` é contraditória.

Tautologia e satisfatibilidade

Dada uma fórmula `H`, se `H` é tautologia, então `H` é satisfatível.

Implicação semântica e implicação sintática

`H |== G <=> fr(I)(H => G) AA fr(I)`.

Equivalência semântica e "se, e somente se"

Dadas as fórmulas `H, G`, `H` equivale semanticamente `G` see `H <=> G` é tautologia.

Equivalência e implicações semânticas

Dadas as fórmulas `H` e `G`, \( H = \parallel = G \) `<=> (H |== G ^^ G |== H)`.

Transitividade de \(= \parallel = \)

Dadas as fórmulas `E`, `G` e `H`, se \(E = \parallel = G\) e \(G = \parallel = H\), então \( E = \parallel = H \).

Satisfatibilidade

Seja `\{ H_i \}_(i=1)^(n)` um conjunto de fórmulas. `\{ H_i \}_(i=1)^(n)` é satisfatível see `^^^_(i=1)^(n) H_i` é satisfatível.

Teorema da dedução, versão semântica

Considere `beta` um conjunto de fórmulas; e `A, B` duas fórmulas da LP.

`beta cup \{ A \} |== B <=> beta |== A -> B`

Corolários

Princípio da Indução

Indução Natural

Permite provar que todo número natural satistaz certa propriedade. Suponha que saibamos os seguintes fatos sobre uma propriedade `P`:

Indução estrutural

Na Matemática e na Computação, é necessário realizar indução sobre estruturas mais elaboradas do que os números naturais. Aqui realizaremos indução nos comprimentos das fórmulas da LP.

Seja `B(E)` uma afirmação sobre uma fórmula proposicional `E`. Se a base e o passo de indução indicados a seguir são verdadeiros, então concluímos que `B(E)` é verdadeiro para qualquer fórmula proposicional `E`. Assim, o algoritmo é:

  1. Base indutiva: `B(P)` é válido para qualquer fórmula atômica `P`.
  2. Passo indutivo: Sejam `H, G` duas fórmulas proposicionais. Se `B(G)` e `B(H)` são verdadeiras então `B(not G), B(H ^^ G), B(H vv G), B(H => G), B(H <=> G)` são verdadeiras.

Exercício: Seja `E` uma fórmula proposional. Considere `gamma (E)` o número de conectivos lógicos; e `pi (E)`, o número de parênteses. Então `gamma(E) = 1/2 pi(E)`.

Vamos mostrar utilizando indução estrutural que a estrutura de árvores de derivação corresponde à estrutura de fórmulas bem formadas.

Indutivamente, uma fórmula `phi` bem-formada é associada a uma árvore `T_(phi)` da seguinte forma:

Correção e Completude

Correção da Lógica Proposicional

As regras de dedução natural permitem uma argumentação rigorosa, pela qual chegamos a uma conclusão `varphi` assumindo outras proposições `\{ psi_i \}_(i=1)^(n)`. Neste caso, temos que o sequente `psi_1, ..., psi_n |-- varphi` é válido. Vamos mostrar que esssas regras são corretas no sentido que "sequentes válidos" preserva, a verdade calculada pela tabela-verdade semântica.

Exercícios:

Completude da Lógica Proposicional

Sejam `\{ psi_i \}_(i=1)^(n)` fórmulas proposicionais. `psi_1, ..., psi_n |-- varphi` é válida see `psi_1, ..., psi_n |== varphi` acontece.

Se `\{ psi_i \}_(i=1)^(n) |-- varphi` é válida, existe uma prova de `varphi` a partir de `\{ psi_i \}_(i=1)^(n)`. A demonstração deste teorema será por indução no comprimento da prova do sequente `psi_1, ..., psi_n |-- varphi`.

A saber, o cumprimento de uma prova é a quantidade de linhas que esta prova possui.

Hipótese da indução: suponha qie p resultado seja válido para toda prova de tamanho `k`.

Fórmulas equivalentes

Dadas as fórmulas proposicionais `H` e `G`. já sabemos que \(H = \parallel = G\) denota que `H` e `G` são equivalentes, isto é, `fr(I)(H) = fr(I)(G) AA fr I`.

Similarmente, \( H \dashv \vdash G \) significa que `H` e `G` são sintaticamente equivalentes, isto é, tanto `H |-- G` como `G |-- H` são válidos.

Pelo da teorema da correção e completude, temos que `H |== G` é o mesmo que `H |-- G` para as regras da dedução natural da lógica clássica. Então, a partir de agora dizemos que `H` e `G` são equivalentes e denotaremos por `H -= G` quando \(H = \parallel = G\) e \( H \dashv \vdash G \).

A equivalência entre fórmulas pode ser verificada utilizando tabela-verdade ou árvores de prova.

`TT -= P => P`

`_|_ -= not (P => P)`

`P vv Q -= not P => Q`

`P ^^ Q -= not (P => not Q)`

`P <=> Q -= not ((P ==> Q) ==> (not Q ==> P))`

Equivalências Importantes

Formas normais conjuntivas e disjuntivas

Já sabemos que `^^` e `vv` são associativos. É comum escrever uma sequência de conjunções ou disjunções sem utilizar parênteses:

`(A ^^ (B ^^ (C ^^ D))) -= A ^^ B ^^ C ^^ D`

`(A vv (B vv (C vv D))) -= A vv B vv C vv D`

Qualquer fórmula proposicional `H` pode ser transformada em uma fórmula normal disjuntiva, isto é, `H` é equivalente a uma disjunção de fórmulas, cada uma sendo uma conjunção.

`H -= vvv_(i=1)^(n in NN) H_i`

`H_i := ^^^_(j=1)^(m in NN) H_(i_j)`

Similarmente, temos formas normais conjuntivas: `H` é equivalente a uma conjunção de fórmulas, cada uma endo uma disjunção de fórmulas atômicas ou suas negações.

`H -= ^^^_(i=1)^(n in NN) H_i`

`H_i := vvv_(j=1)^(m in NN) H_(i_j)`

Método da tabela-verdade

Observe a seguinte fórmula:

`H := (P ^^ Q) vv not P`

Façamos a tabela verdade de H:

`P` `Q` `(P ^^ Q) vv not P` FN`vv` FN`^^`
0 0 1 `not P ^^ not Q`
0 1 1 `not P ^^ Q`
1 0 0 `not P vv Q`
1 1 1 `P ^^ Q`

`=> FN vv = (not P ^^ not Q) vv (not P ^^ Q) vv (P ^^ Q)`

`FN ^^ = not P vv Q`

Resolução

Resolução é uma regra de inferência utilizada para mostrar que um conjunto de fórmulas proposicionais da forma `vvv_(i=1)^(n) hat(P_i)` não é satisfatível. Aqui, `hat(P_i) = \{ P_i, not P_i \}`, onde `P_i` é uma fórmula atômica.

O sequente `phi_1, ..., phi_n |-- phi` é válido see o conjunto `\{ phi1, ..., phi_n, not phi \}` não é satisfatível.

Vimos que `F_1, F_2, ..., F_n |-- phi` é válido see `(^^^_(i=1)^(n) F_i) ^^ not phi` não é satisfatível. Vamos colocar cada `F_i` e `not phi` na forma conjuntiva:

`F_i := G_(i_1) ^^ G_(i_2) ^^ ... ^^ G_(i_(k_i))`

`not phi := G_1 ^^ G_2 ^^ ... ^^ G_m`

Além disso, cada `G_(i_j)` e `G_e` são da forma `hat(P_1) vv hat(P_2) vv ... vv hat(P_r)`. Assim, dizer que um argumento/sequente é válido é o mesmo que dizer um certo conjunto de disjunções de fórmulas atômicas e fórmulas atômicas negadas não é satisfatível.

Exercício: Determine a validade do sequente:

`P => Q, not P => R, Q vv R => S |-- S`

Cláusulas

Uma fórmula atômica `P`, bem como sua fórmula atômica negada `not P`, é chamada de literal.

Conjuntos finitos de literais `\{ L_i \}_(i=1)^(K)` são chamadas de cláusulas.

Uma cláusula `\{ L_i \}_(i=1)^(K)` é satisfatível sse a fórmula proposicional `vvv_(i=1)^(K) L_i` é satisfatível.

Uma cláusula vazia `\{\}` não é satisfatível.

Um conjunto de cláusulas `fr C` é satisfatível se existe uma interpretação `fr I` que satisfaz cada cláusula de `fr C`.

Se `L` é um literal, então o complemento `bar(L)` é definido por:

`bar(P) := not P`

`bar(not P) := P`

Um literal é positivo see for uma fórmula atômica e é negativo caso contrário.

Resolução é a regra

\( \frac{C \cup \{ L \} \ D \cup \{\bar{L}\}}{C \cup D} \)

onde `C` e `D` são cláusulas; e `L` é um literal. Dizemos que estamos "resolvendo" as cláusulas sobre `L`, e a cláusula `C uu D` é chamada resolvente. Uma derivação (por resolução) é uma sequência de cláusulas tais que cada uma está em `C` ou vem de cláusulas anteriores.

A resolução preserva a satisfatibilidade. Isto é, se um conjunto de cláusulas `C` é satisfeito or uma interpretação `fr I`, então qualquer resolvente ou um par de cláusulas de `C` também é satisfeito por `fr I`.

O algoritmo de resolução é correto e completo.

Não é correto aplicar resolução a mais de uma fórmula atômica.

Procedimento de Davis-Putnam (DPP)

Dado um conjunto de não-vazio finito de cláusulas `C` nas fórmulas atômicas `\{ P_i \}_(i=1)^(n)`, o procedimento DPP repete os seguintes passos até que não restem mais fórmulas atômicas:

  1. Elimine as fórmulas atômicas que contenham tanto o literal `L` quanto `bar L`;
  2. Escolha uma fórmula atômica `P` que aparece em uma das cláusulas;
  3. Adicione todos os resolventes possíveis usando resolução sobre `P` no conjunto de cláusulas;
  4. Elimine todas as cláusulas que contenham `P` ou `not P`.

Exemplo: `C = \{ \{ P, Q \}, \{ not P, R \}, \{ not P \} \}`

`( \{ P, Q \}\ \{ not P \} )/(\{ Q \})`

`( \{ P, Q \}\ \{ not P, R \} )/(\{ Q, R \})`

`C = \{ \{ Q \}, \{ R \} \}`

`=> \{ \}` sem cláusulas

` .: C` é satisfatível. `square`

Se o algoritmo retornar um conjunto sem cláusulas, então o conjunto `C` é satisfatível. Se, em algum passo, tem-se uma cláusula vazia, então o conjunto `C` não é satisfatível.

Exercício: Aplique DPP em `C := \{ \{not P, Q\}, \{not Q, R, S\}, \{ P \}, \{R\}, \{not S\} \}`

Correção e completudo do DPP

Seja `S` um conjunto finito de cláusulas. Então `S` não é satisfatível sse a saída do DPP é "cláusula vazia".

Compacidade da lógica proposicional

Seja `S` um conjunto de fórmulas prposicionais. Todo conjunto finito `S_0 in S` é satisfatível sse `S` é satisfatível.

Caso geral de correção e completude da resolução

Um conjunto de não-vazio de cláusulas `S` é não-satisfatível sse existe uma derivação de uma cláusula vazia de `S` utilizando resolução.

Cláusulas de Horn

Uma clásula de Horn é uma cláusula com, no máximo, um literal positivo.

As clásulas `\{not Q, not R, not S, not T\}` e `\{not P, Q, not R\}` são cláusulas de Horn.

Um resolvente de duas cláusulas de Horn é sempre uma cláusula de Horn.

Para saber mais, procure saber sobre o trabalho de David McCallister em lógica em sistemas de segurança.

Uma cláusula unitária é uma cláusula do tipo `\{L\}` com um único literal.

Resolução unitária refere-se a derivações de resolução nas quais pelo menos uma das cláusulas utilizadas em cada passo é uma cláusula unitária.

A resolução unitária é correta e completa para cláusulas de Horn.

Cláusulas de grafos

Dado um grafo `G` finito, um conjunto de vértices `V` e um conjunto de arestas `E`, vamos rotular cada vértice `cc v` com 0 ou 1. Este número é a chamada "carga" do vértice `cc v`. A carga total é:

`(sum_(cc v in V) fr(C)(cc v)) mod 2`

Vamos rotular cada aresta com uma fórmula atômica, de forma que arestas diferentes são rotuladas com fórmulas atômicas diferentes. Temos então um grafo rotulado `hat G`

Para cada vértice `cc v` de `G`, seja `var(cc v)` o conjunto de variáveis proposicionais nas arestas ligadas a `cc v` Para cada vértice `cc v`, construímos o conjunto de cláusulas `cls(cc v)` da seguinte forma:

`c in cls(cc v) <=>`

O conjunto de cláusulas associadas ao grafo `hat G` é dado por

`cls(hat G) := uuu_(cc v in V) cls(cc v)`

Teorema de Tseitin

`cls(hat G)` é satisfatível sse a carga total é 0.

Lógica de Predicados

Cris Silva Jr.

Mais informações...

Você pode me achar no LinkedIn ou no GitHub.

GE/CS$ d- s:- a- C++ UL++$ W++ w++ M++ PS+ PE !tv b+ DI+ D+ G e>+++++ R* h++ r* y?