AXIOMATIZAÇÃO

AXIOMATIZAÇÃO
Equipe: André Augusto Kaviatkovski, Daniel Elias Ferreira,

Vinicius Zaramella
Curso: Engenharia de Computação
Disciplina: Lógica para Computação
Professor: Adolfo Neto (DAINF)
Universidade Tecnológica Federal do Paraná (UTFPR) 1
Sistema Dedutivo:
• Sistemas Dedutivos são métodos utilizados na lógica e em

outras ciências para se inferir conseqüências lógicas a partir
de um conjunto de fórmulas tomadas a priori.
• Existem várias formas de se realizar inferências. Entre

esses métodos estão os Sistemas de Dedução Natural,
Métodos de Tablôs analíticos e as Axiomatizações.
• Quando um Sistema Dedutivo infere uma fórmula A de uma

teoria Γ, escreve-se Γ Ⱶ A.
• Esta expressão é chamada de sequente. Ela é constituída
do antecedente (ou hipótese) Γ e do consequente (ou
conclusão) A.
2
Axiomatização:
• O axioma era um importante elemento do método lógico
dedutivo dos gregos. Um método dedutivo baseado em
axiomas método foi utilizado na apresentação da geometria
euclidiana.Tratava-se, na época, de axiomatizar uma teoria,
a teoria geométrica.
•Posteriormente, as axiomatizações foram utilizadas em

tentativas de prover um fundamento seguro para a
matemática.
•Em lógica, porém, compreende-se axiomatização como uma

forma lógica de inferência.
•Uma axiomatização possui dois elementos distintos:

axiomas e regras de inferência.
3
Axioma:
•Um axioma é aceito como verdade e serve como ponto

inicial para dedução e inferências de outras verdades
(dependentes de teoria).
•Um axioma não é necessariamente uma verdade auto-

evidente, mas apenas uma expressão lógica formal usada
em uma dedução, visando obter resultados mais facilmente.
•Axiomatizar um sistema é mostrar que suas inferências

podem ser derivadas a partir de um pequeno e bem-definido
conjunto de sentenças.
4
Regras de inferência:
•As regras de inferência possuem como características:
I)Se a Hipótese inicial for verdadeira, então a Conclusão é

verdadeira.
II) As premissas de um sistema de inferência são regras sem

hipóteses.
III) Permitem inferir novas fórmulas a partir de formulas já

inferidas.
•No caso da axiomatização da lógica proposicional clássica

será utilizado o Modus Ponens.
5
Modus Ponens:
•A partir de A → B e A, infere-se B.
•O argumento tem duas premissas:

-A condição "se - então", nomeadamente que A implica B.
-A é verdadeiro.
•Destas duas premissas pode ser logicamente concluído que

B tem de ser também verdadeiro.
EXEMPLO:
- Se chover, então fico em casa.

- Choveu.
- Então fico em casa.
Fonte: WIKIPEDIA. Modus Ponens. Disponível em: <http://pt.wikipedia.org/wiki/Modus_ponens>. Acesso em: 21 mar. 2009.
Substituição:
•A substituição de um átomo p por uma fórmula B em uma
fórmula A é representada por A[p := B].
•A definição formal de substituição se dá por indução

estrutural sobre a fórmula A, sobre a qual se processa a
substituição, da seguinte maneira:
1.p[p := B] = B
2.q[p := B] = q, para q ≠ p.
3.(¬A) [p:=B]= ¬(A [p:=B]).
4.(A1 ο A2) [p := B] = (A1 [p := B]) ο (A2 [p := B]), para ο ∈

{∧,∨,→}
Fonte: CORRÊA DA SILVA, Flávio Soares; FINGER, Marcelo;VIEIRA DE MELO, Ana Cristina. Lógica para computação. São Paulo: Thomson, 2006. p. 35.
.
Substituição:
Exemplo:
(p → (p ∧ q))[p := (r ∨ s)]
= p[p := (r ∨ s)] → (p ∧ q)[p := (r∨ s)]
= (r ∨ s) → (p[p := (r ∨ s)] ∧ q[p := (r ∨ s)])
= (r ∨ s) → ((r ∨ s) ∧ q)
•Quando uma fórmula B é resultante da substituição de um

ou mais átomos da fórmula A, dizemos que B é uma
instância da fórmula A.
Fonte: CORRÊA DA SILVA, Flávio Soares; FINGER, Marcelo;VIEIRA DE MELO, Ana Cristina. Lógica para computação. São Paulo: Thomson, 2006. p. 35.
.
Dedução, teoremas:
• Axiomas da lógica proposicional clássica:
(→1) p → (q → p);
(→2) (p → (q → r)) → ((p → q) → (p → r));
(∧1) p → (q → (p ∧ q));
(∧2) (p ∧ q )→ p ;
(∧3) (p ∧ q )→ q ;
(∨1) p → (p ∨ q);
(∨2) q → (p ∨ q);
(∨3) (p →r) → ((q → r) → ((p ∨ q) → r));
(¬1) (p →q) → ((p → ¬q) → ¬p);
(¬2) ¬ ¬p → p . 9
Fonte: CORRÊA DA SILVA, Flávio Soares; FINGER, Marcelo;VIEIRA DE MELO, Ana Cristina. Lógica para computação. São Paulo: Thomson, 2006. p. 36 .
• Dedução: uma seqüência de fbf A1, A2 … An tal que cada

fbf na seqüência é uma instância de axioma ou pode
ser obtida das fbfs anteriores por meio das regras de
inferência.
• Teorema: uma fbf A tal que existe uma dedução A1, A2

… An = A . Neste caso escreve-se Ⱶ A .
• A axiomatização possui a propriedade da substituição

uniforme, isto é, se A é um teorema e se B é uma
instância de A, então B também é um teorema
10
Fonte: KAESTNER, Celso A. A. Disponível em: <http://www.dainf.cefetpr.br/~kaestner/Logica/SistemasDedutivos.ppt>. Acesso em: 18 mar. 2009.
• “Pode-se ainda definir o conceito de fórmula dedutível de uma teoria
(conjunto de fbf);
• Diz-se que A é dedutível a partir de uma teoria Γ se há

uma dedução, ou seja seqüência de fbf A1, A2 … An = A
tal que cada fbf na seqüência é:
1. uma fbf da teoria Γ; ou
2. uma instância de um axioma; ou
3. pode ser obtida das fórmulas anteriores por meio

das regras de inferência;”
11
Fonte: KAESTNER, Celso A. A. Disponível em: <http://www.dainf.cefetpr.br/~kaestner/Logica/SistemasDedutivos.ppt>. Acesso em: 18 mar. 2009.
Exemplo de dedução:
•Dedução do teorema I = A → A.
• (→2), onde p := A, q := A → A e r := A. Assim temos:

1.(A → ((A → A) → A)) → ((A → (A → A)) → (A → A)).
• (→1), onde p := A, q :=A → A.Obtemos assim:

2.A → ((A → A) → A).
•Aplicando Modus Ponens 1, 2, obtemos a fórmula 3:

3. ((A → (A → A)) → (A → A).
•(→1) onde p := A e q := A:
4. A → (A → A).
•Aplicando Modus Ponens 3, 4, obtemos a fórmula 5:

5. A → A.
12
Fonte: Adaptado de CORRÊA DA SILVA, Flávio Soares; FINGER, Marcelo;VIEIRA DE MELO, Ana Cristina. Lógica para computação.
São Paulo: Thomson, 2006. p. 38.
Teorema da dedução:
•O teorema da dedução diz que: Γ, A Ⱶ B se e somente se
Γ Ⱶ A → B.
•É capaz de transformar uma dedução que poderia ser
complexa em uma dedução bastante simples.
•Exemplo:
• B= (A → B) → ((C → A) → (C → B))
• A → B, C → A, C Ⱶ B. Tomamos como Hipótese as fórmulas:
1 – A →B
2 – C →A
3 – C.
•Aplicamos agora o Modus Ponens 2,3 e obtemos a fórmula:
4–A
•Por fim, aplicamos o Modus Ponens 1,4 e obtemos a
fórmula:
5–B
13
Referências:
CORRÊA DA SILVA, Flávio Soares; FINGER, Marcelo;VIEIRA

DE MELO, Ana Cristina. Lógica para computação. São Paulo:
Thomson, 2006. p. 33 – 41.
KAESTNER, Celso A. A. Disponível em:

<http://www.dainf.cefetpr.br/~kaestner/Logica/SistemasDedutivos.pp
t>. Acesso em: 18 mar. 2009.
WIKIPEDIA. AXIOMA. Disponível em:

<http://pt.wikipedia.org/wiki/Axioma>. Acesso em: 13 mar. 2009.
WIKIPEDIA. Modus Ponens. Disponível em:

<http://pt.wikipedia.org/wiki/Modus_ponens>. Acesso em: 21 mar.
2009.
14

AXIOMATIZAÇÃO

Enviado por

Direitos autorais:

Formatos disponíveis

AXIOMATIZAÇÃO

Enviado por

Dados do documento

Descrição original:

Direitos autorais

Formatos disponíveis

Compartilhar este documento

Compartilhar ou incorporar documento

Opções de compartilhamento

Você considera este documento útil?

Este conteúdo é inapropriado?

Direitos autorais:

Formatos disponíveis

AXIOMATIZAÇÃO

Enviado por

Direitos autorais:

Formatos disponíveis

AXIOMATIZAÇÃO

Equipe: André Augusto Kaviatkovski, Daniel Elias Ferreira,

• Sistemas Dedutivos são métodos utilizados na lógica e em

• Existem várias formas de se realizar inferências. Entre

• Quando um Sistema Dedutivo infere uma fórmula A de uma

•Posteriormente, as axiomatizações foram utilizadas em

•Em lógica, porém, compreende-se axiomatização como uma

•Uma axiomatização possui dois elementos distintos:

•Um axioma é aceito como verdade e serve como ponto

•Um axioma não é necessariamente uma verdade auto-

•Axiomatizar um sistema é mostrar que suas inferências

•As regras de inferência possuem como características:

I)Se a Hipótese inicial for verdadeira, então a Conclusão é

II) As premissas de um sistema de inferência são regras sem

III) Permitem inferir novas fórmulas a partir de formulas já

•No caso da axiomatização da lógica proposicional clássica

•O argumento tem duas premissas:

•Destas duas premissas pode ser logicamente concluído que

- Se chover, então fico em casa.

•A definição formal de substituição se dá por indução

3.(¬A) [p:=B]= ¬(A [p:=B]).

4.(A1 ο A2) [p := B] = (A1 [p := B]) ο (A2 [p := B]), para ο ∈

= p[p := (r ∨ s)] → (p ∧ q)[p := (r∨ s)]

= (r ∨ s) → (p[p := (r ∨ s)] ∧ q[p := (r ∨ s)])

•Quando uma fórmula B é resultante da substituição de um

(→2) (p → (q → r)) → ((p → q) → (p → r));

(∨3) (p →r) → ((q → r) → ((p ∨ q) → r));

(¬1) (p →q) → ((p → ¬q) → ¬p);

• Dedução: uma seqüência de fbf A1, A2 … An tal que cada

• Teorema: uma fbf A tal que existe uma dedução A1, A2

• A axiomatização possui a propriedade da substituição

• Diz-se que A é dedutível a partir de uma teoria Γ se há

1. uma fbf da teoria Γ; ou

2. uma instância de um axioma; ou

3. pode ser obtida das fórmulas anteriores por meio

• (→2), onde p := A, q := A → A e r := A. Assim temos:

• (→1), onde p := A, q :=A → A.Obtemos assim:

•Aplicando Modus Ponens 1, 2, obtemos a fórmula 3:

•Aplicando Modus Ponens 3, 4, obtemos a fórmula 5:

CORRÊA DA SILVA, Flávio Soares; FINGER, Marcelo;VIEIRA

KAESTNER, Celso A. A. Disponível em:

WIKIPEDIA. AXIOMA. Disponível em:

WIKIPEDIA. Modus Ponens. Disponível em:

Você também pode gostar