Dedução Natural: Lógica Proposicional e de Predicadosdanielc/logicamat/lec05-prop-pred-nat… · Predicados Alfio Martini Faculdade de Informática - PUCRS Lógica para

ObjetivosO Conceito de Calculo

Calculo de Deducao NaturalTeoremas

Substituicao em FormulasRegras dos Quantificadores

Regras para IgualdadeConsistencia e Completude

Deducao Natural: Logica Proposicional e dePredicados

Alfio Martini

Faculdade de Informatica - PUCRS

Logica para Computacao

Alfio Martini Deducao Natural: Logica Proposicional e de Predicados





Outline

1 Objetivos

2 O Conceito de Calculo

3 Calculo de Deducao NaturalRegras ComputacionaisDeducoes com Regras ComputacionaisRegras EstruturaisDeducoes com Regras Estruturais

4 Teoremas

5 Substituicao em Formulas

6 Regras dos Quantificadores

7 Regras para Igualdade

8 Consistencia e Completude






Objetivos

Pontos Importantes

Entender os conceitos de calculo, teorema, demonstracao ederivabilidade.

Aprender a utilizar o calculo de deducao natural.

Compreender os conceitos de consistencia e completude docalculo de de deducao natural.

Analisar questoes de computabilidade associadas ao calculo.






Conceito de Calculo

Definition

Calculo Seja S0 um conjunto de objetos sintaticos. Um calculo(ou sistema axiomatico) sobre SO e um par K = (A,R), onde:

A e um conjunto finito de esquemas de axiomas, que saoconjunto decidıveis de SO. Os elementos de um esquema deaxioma sao chamados de axiomas.

R e um conjunto finito de regras de inferencia, que saosubconjuntos decidıveis de SOn × SO, n ≥ 1.






Exemplos de Axiomas

Logica Proposicional

Para SO = PΣ(X ), um esquema de axioma possıvel seria:

{A ∨ ¬A|A ∈ PΣ(X )}

Um axioma deste esquema poderia ser, por exemplo:

(p ∧ q) ∨ ¬(p ∧ q)






Notacao para Regras de Inferencia


Uma regra de inferencia R = 〈〈s1, . . . , sn〉, s〉 ∈ SOn × SOnormalmente e apresentada da forma:

s1, . . . , snR

s

s1, . . . , sn sao chamadas de premissas, e s de conclusao daregra.






Exemplos de Regras de Inferencia


Com SO = PΣ(X ), um exemplo de regra seria:

A ⇒ B,B ⇒ CR

A ⇒ C

A propriedade decidıvel e que esta regra vale para todoA,B,C ∈ PΣ(X ).






Conceito de Prova

Definition

Prova Uma prova em uma calculo K e uma sequencia finita (deformulas ) A1,A2, . . . ,An tal que para todo i , 1 ≤ i ≤ n:

1 Ai e um axioma do calculo, ou

2 Ai e uma consequencia imediata de formulas precedentes,atraves da aplicacao de regras de inferencia do calculo.






Teorema e Deducao

Definition

Uma formula A e um teorema em K se existir uma prova deA. Escreve-se como `K A.

Seja Γ = A1, . . . ,An uma sequencia de formulas. Umadeducao a partir de Γ e uma sequencia finita de formulasA1,A2, . . . ,An tal que:

1 Ai e um axioma.2 Ai ∈ Γ.3 Ai e obtida de formulas anteriores, pela aplicacao das regras

de inferencia do calculo.






Sistemas de Consequencia

Definition

Consequencia e Relacao de Consequencia

A e uma consequencia sintatica ou dedutıvel ou derivavel deΓ se A e uma formula que figura em uma deducao a partir deΓ. Essa consequencia e escrita como Γ `K A.

Uma relacao binaria de consequencia R e tal que o primeirocomponente e um conjunto de formulas e o segundo e umaformula que pode ser derivavel do conjunto de formulas.

Todo calculo K gera uma relacao de consequenciaCnK ⊆ ℘(SO)× SO tal que 〈Γ,A〉 ∈ CnK se e somente seΓ `K A.






Exemplos de Calculos

Tipos de Calculos

Calculo de Hilbert

Calculo de Sequentes

Calculo de Deducao Natural

Calculo de Tableaux

Calculo de Resolucao (Programacao em Logica)






Regras ComputacionaisDeducoes com Regras ComputacionaisRegras EstruturaisDeducoes com Regras Estruturais

Calculo de Deducao Natural

Caracterısticas

Nao possui axiomas.

Regras de Inferencia divididas em duas classes:1 Regras Computacionais2 Regras Estruturais

Regras Computacionais sao utilizas para as inferencias dentrode uma certa subprova.

Regras Estruturais sao usadas para estabelecer as diversassubprovas que constituem uma prova.

Cada operador possui uma regra de eliminacao e outra deintroducao.







Regras Computacionais

A,A ⇒ B⇒ E

B

A ∧ B∧E

A

A ∧ B∧E

B

A,B∧I

A ∧ B

A,¬A¬E

⊥

⊥⊥E

A

A∨I

A ∨ B

A∨I

B ∨ A







Deducao da conjectura A ∧ (B ∧ C ) ` (A ∧ B) ∧ C

1 A ∧ (B ∧ C ) Pr...............

n (A ∧ B) ∧ C

A ∧ (B ∧ C ) Pr

A ∧E(1)

B ∧ C ∧E(1)

B ∧E(3)

C ∧E(3)

A ∧ B ∧I(2, 4)

(A ∧ B) ∧ C ∧I(6, 5)







Deducao da conjectura A ` D ∨ ((B ∨ A) ∨ C )

1 A Pr......

n D ∨ ((B ∨ A) ∨ C )

A Pr

B ∨ A ∨I(1)

(B ∨ A) ∨ C ∨I(2)

D ∨ ((B ∨ A) ∨ C ) ∨I(3)







Deducao de p ∧ (q ∧ r), r ⇒ s, s ∨ t ⇒ d ` d ∧ r

1 p ∧ (q ∧ r) Pr

r ⇒ s Pr

s ∨ t ⇒ d Pr...............

n d ∧ r

p ∧ (q ∧ r) Pr

r ⇒ s Pr

s ∨ t ⇒ d Pr

q ∧ r ∧E(1)

r ∧E(4)

s ⇒E(5, 2)

s ∨ t ∨I(6)

d ⇒E(7, 3)

d ∧ r ∧I(8, 5)







Deducao de p ∨ s ⇒ t, d ∧ s,¬t ` (t ∧ q) ∧ r

1 p ∨ s ⇒ t Pr

2 d ∧ s Pr

3 ¬t Pr............

n (t ∧ q) ∧ r

p ∨ s ⇒ t Pr

d ∧ s Pr

¬t Pr

s ∧E(2)

p ∨ s ∨I(4)

t ⇒E(1, 5)

⊥ ¬E(6, 3)

(t ∧ q) ∧ r ⊥E(7)







Regras Estruturais - Introducao da → e Eliminacao do ∨

A hip...

B

A ⇒ B ⇒I

A ∨ B

A hip...

C

B hip...

C

C ∨E

As caixas representam subprovas dentro da prova principal.

O termo hip significa hipotese, e pode ser visto como uma premissaadicional que so pode ser utilizada dentro da caixa onde ela eutilizada.







Regras Estruturais

Introducao do ¬ e Contra-Classica

A hip...

⊥

¬A ¬I

¬A hip...

⊥

A CClass

O termo CClass denota a expressao Contra Classica.

Esta regra e tambem conhecida pela expressao Reducao aoAbsurdo.







Deducao da Conjectura p ⇒ (q ⇒ r) ` p ∧ q ⇒ r

1 p ⇒ (q ⇒ r) Pr

p ∧ q hip.........

r

n p ∧ q ⇒ r ⇒I

p ⇒ (q ⇒ r) Pr

p ∧ q hip

p ∧E(2)

q → r ⇒E(3, 1)

q ∧E(2)

r ⇒E(5, 4)

p ∧ q ⇒ r ⇒I(2− 6)







Deducao da Conjectura p ∧ q ⇒ r ` p ⇒ (q ⇒ r)

1 p ∧ q ⇒ r Pr

p hip

q hip...

r

q ⇒ r ⇒I

n p ⇒ (q ⇒ r) ⇒I

p ∧ q ⇒ r Pr

p hip

q hip

p ∧ q ∧I(2, 3)

r ⇒E(4, 1)

q ⇒ r ⇒I(3− 5)

p ⇒ (q ⇒ r) ⇒I(2− 6)







Projeto de prova para (p ∨ q) ∨ r ` p ∨ (q ∨ r)

1. (p ∨ q) ∨ r Pr

p ∨ q hip

q hip

p ∨ (q ∨ r)

p hip

p ∨ (q ∨ r)

p ∨ (q ∨ r) ∨E

r hip

p ∨ (q ∨ r)

n. p ∨ (q ∨ r) ∨E







Deducao da conjectura (p ∨ q) ∨ r ` p ∨ (q ∨ r)

(p ∨ q) ∨ r Pr

p ∨ q hip

q hip

q ∨ r ∨I(3)

p ∨ (q ∨ r) ∨I(4)

p hip

p ∨ (q ∨ r) ∨I(3)

p ∨ (q ∨ r) ∨E(2, 3− 5, 3− 4)

r hip

q ∨ r ∨I(2)

p ∨ (q ∨ r) ∨I(3)

p ∨ (q ∨ r) ∨E(1, 2− 6, 2− 4)







Projeto de prova para (p ∧ q) ∨ (p ∧ r) ` p ∧ (q ∨ r)

1. (p ∧ q) ∨ (p ∧ r) Pr

p ∧ q hip

p ∧ (q ∨ r)

p ∧ r hip

p ∧ (q ∨ r)

n. p ∧ (q ∨ r) ∨E







Prova da Conjectura (p ∧ q) ∨ (p ∧ r) ` p ∧ (q ∨ r)

(p ∧ q) ∨ (p ∧ r) Pr

p ∧ q hip

p ∧E(2)

q ∧E(2)

q ∨ r ∨I(4)

p ∧ (q ∨ r) ∧I(3, 5)

p ∧ r hip

p ∧E(2)

r ∧E(2)

q ∨ r ∨I(4)

p ∧ (q ∨ r) ∧I(3, 5)

p ∧ (q ∨ r) ∨E(1, 2− 6, 2− 6)






Teoremas e Regras Derivadas

O Calculo de Deducao Natural pode ser estendido com novasregras atraves da nocao de teorema.

A ideia e de que qualquer demonstracao A1, . . . ,An `DN Bpode ser utilizada com uma nova regra de inferencia daseguinte forma:

A1, . . . ,AnTeorema

B






Exemplo de Teorema

Por exemplo, uma demonstracao A ⇒ B `DN ¬A ∨ B justificaa introducao de uma nova regra:

A ⇒ BTeorema

¬A ∨ B

A introducao de teoremas nao torna o calculo mais expressivo,mas facilita enormemente a sua utilizacao.

A ideia e similar a utilizacao de bibliotecas em umadeterminada linguagem de programacao.






Teoremas Importantes

Teoremas

A ⇒ B,¬BMT

¬A

Ahip

A

A ∨ B,¬ASD

B

A ∨ B,A ⇒ C1,B ⇒ C2DC

C1 ∨ C2

A1 ⇒ A2,A2 ⇒ A3SH

A1 ⇒ A3

A ⇒ BTeorema

¬B ⇒ ¬A






Escopo de Variaveis

Definition

Variaveis Livres e Ligadas

Seja A uma formula na logica de Predicados. Uma ocorrenciade x em A e livre se ela e um nodo folha na arvore sintaticade A tal que nao existe nem um caminho para cima, a partirdo nodo x para um nodo ∀x ou ∃x .

Do contrario, a ocorrencia de x e dita ligada.






Variaveis Livres e Ligadas

Exemplo

Na formula ∀x .(P(x) ⇒ ∃x .Q(x)) a primeira ocorrencia de xesta ligada ao quanticador ∀x , enquanto que a segunda estaligada a ∃x .

Na formula ∀x .(P(x) ∧ Q(x)) ⇒ (¬P(x) ∨ Q(y)), as duasprimeiras ocorrencias de x estao ligadas a ∀x , enquanto que aterceira esta livre. A ocorrencia da variavel y e livre.






Conceito de Substituicao

Definition

Seja x uma variavel, t um termo e A uma formula com a possivelocorrencia da variavel x . Entao, a expressao

A[x/t]

denota a substituicao de todas as ocorrencias livres de x por t naformula A.






Propriedades da Substituicao

Theorem

[x/t] distribui sobre os operadores logicos:

(¬A)[x/t] = ¬A[x/t](A ∧ B)[x/t] = A[x/t] ∧ B[x/t](A ∨ B)[x/t] = A[x/t] ∨ B[x/t](A ⇒ B)[x/t] = A[x/t] ⇒ B[x/t](A ⇔ B)[x/t] = A[x/t] ⇔ B[x/t]

Se x , y , x0, y0 sao varıaveis diferentes, entao temos que

A[x0/x ][y0/y ] = A[y0/y ][x0/x ].






Propriedades da Substituicao

Theorem

Se x 6= y entao [x/t] distribui sobre ∀y e ∃y.

(∀y .A)[x/t] = ∀y .(A[x/t])(∃y .A)[x/t] = ∃y .(A[x/t])

Se x nao esta livre em A, entao A[x/t] = A.

(∀x .A)[x/t] = ∀x .A(∃x .A)[x/t] = ∃x .A






Exemplos de Substituicoes

Exemplos

Seja A = P(x , y) ∨ ∃y .Q(x , y).

A[x/a] = P(a, y) ∨ ∃y .Q(a, y)A[x/y ] = P(y , y) ∨ ∃y .Q(y , y)A[x/f (x , y , z)] = P(f (x , y , z), y) ∨ ∃y .Q(f (x , y , z), y)A[x/a][y/b] = P(a, b) ∨ ∃y .Q(a, y)






Introducao e Eliminacao de Quantificadores

Regras Computacionais

∀x .A∀E

A[x/t]

A[x/t]∃I

∃x .A






Introducao e Eliminacao de Quantificadores

Regras Estruturais

c hip...

A[x/c]

∀x .A ∀I

∃x .A

c ,A[x/c] hip...

B

B ∃E

c deve ser uma constante nova na prova!

c nao deve ocorrer em B!






Regras para a Igualdade

Regras de Deducao

= It = t

t1 = t2,A[x/t1]= E

A[x/t2]

t1 = t2= S

t2 = t1

t1 = t2, t2 = t3= T

t1 = t3

S denota simetria – E denota equality.

T denota transitividade – I denota identidade.






Theorem

Consistencia O calculo de deducao natural e consistente (sound)no sentido de que

A1, . . . ,An `DN B implica A1, . . . ,An |= B






Interpretacao

Se A e uma deducao (derivavel) das premissas Γ, entao Atambem e uma consequencia semantica dessas mesmaspremissas.

Se Γ = ∅, entao temos que se A e um teorema entao A e umatautologia.

Isso deve-se ao fato de as regras do calculo serem projetadaspara preservar a verdade de suas premissas.






Completude do Calculo de Deducao Natural

Theorem

Completude O calculo de deducao natural e completo no sentidode que

A1, . . . ,An |= B implica A1, . . . ,An `DN B

Interpretacao

Se A e uma consequencia semantica das premissas Γ, entao Atambem derivavel dessas mesmas premissas.

Se Γ = ∅, entao temos que se A e um tautologia entao A euma teorema.






Consistencia e Completude - Resumo

Pontos Principais

A completude do calculo e importante, pois se uma lei evalida (de acordo com a semantica do calculo), entao tambemencontraremos uma forma sintatica de demonstra-la.

Como o calculo e consiste e completo temos queΓ `DN B sse Γ |= B.

Entretanto, como os dois procedimentos sao equivalentes,temos a liberdade de escolha para decidir se B e umaconsequencia (sintatica ou semantica) de Γ.

Se Γ |= B ou Γ `DN B, dizemos que B e uma consequencialogica de Γ.






Questoes sobre Computabilidade

Pontos Principais

Ambos metodos sao intrataveis computacionalmente, uma vezque o primeiro exige uma procura de uma prova (programacaoem logica) e o segundo tem custo exponencial com relacao aonumero de variaveis preseentes nas formulas.

Dizemos que um problema e decidıvel quando podemosescrever um programa C ou Java (maquina de Turing) queresolve o problema (retorna sim ou nao).

O problema de consequencia logica e decidıvel para ofragmento proposicional, mas e indecidıvel para a logica depredicados.


Documents

Dedução Natural: Lógica Proposicional e de Predicadosdanielc/logica__mat__/lec05-prop-pred-nat… · Predicados Alfio Martini Faculdade de Informática - PUCRS Lógica para

Dedução Natural: Lógica Proposicional e de Predicadosdanielc/logicamat/lec05-prop-pred-nat… · Predicados Alfio Martini Faculdade de Informática - PUCRS Lógica para