Lógica/Cálculo Proposicional Clássico/Axiomática

Origem: Wikilivros, livros abertos por um mundo aberto.
Saltar para a navegação Saltar para a pesquisa


Introdução[editar | editar código-fonte]

Uma outra forma de lidar sintáticamente com o CPC é axiomaticamente. Como você deve saber, axiomas são proposições tomadas como verdadeiras a partir das quais os teoremas são derivados.

Funciona assim:

Seja o conjunto dos axiomas e todas suas instâncias, se , então . Ou seja, se é dedutível dos axiomas, então é teorema.

E seja um conjunto qualquer de fórmulas, se então . Ou seja, se é dedutível de um conjunto de fórmulas juntamente com os axiomas, então um raciocínio que tenha como premissas e como conclusão é válido.

A escolha adequada de axiomas e da regra de inferência primitiva confere ao sistema tanto a correção quanto a completude.

Axiomática de Frege[editar | editar código-fonte]

Gottlob Frege usava apenas a implicação e a negação como operadores primitivos, definindo as demais operações por meio destes, mas sem criar símbolos para expressá-las. Sua axiomática do CPC tem seis axiomas e uma regra de inferência.

Por questões de economia, demonstraremos algumas regras de inferência derivadas e as aplicaremos.

Nas tabelas onde as deduções são expressas, "wff" significa "well formed formula", ou seja, "fórmula bem formada".

  • Axiomas

THEN-1:
THEN-2:
THEN-3:
FRG-1:
FRG-2:
FRG-3:


  • Regra de Inferência

MP:


Regra THEN-1*:

# wff razão
1. premissa
2. THEN-1
3. MP 1,2.


Regra THEN-2*:

# wff razão
1. premissa
2. THEN-2
3. MP 1,2.


Regra THEN-3*:

# wff razão
1. premissa
2. THEN-3
3. MP 1,2.


Regra FRG-1*:

# wff razão
1. FRG-1
2. premissa
3. MP 2,1.


Regra TH1*:

# wff razão
1. premissa
2. THEN-1
3. MP 1,2
4. THEN-2
5. MP 3,4
6. premissa
7. MP 6,5.


Teorema TH1:

# wff razão
1. THEN-1
2. THEN-2
3. TH1* 1,2
4. THEN-3
5. MP 3,4.


Teorema TH2:

# wff razão
1. THEN-1
2. FRG-1
3. TH1* 1,2.


Teorema TH3:

# wff razão
1. TH 2
2. THEN-3
3. MP 1,2.


Teorema TH4:

# wff razão
1. TH3
2. FRG-1
3. MP 1,2
4. FRG-2
5. TH1* 3,4.


Teorema TH5:

# wff razão
1. FRG-1
2. THEN-3
3. MP 1,2
4. FRG-3, with A := B
5. TH1* 4,3
6. FRG-1
7. MP 5,6.


Teorema TH6:

# wff razão
1. TH4, with A := B, B := A
2. TH5, with A := B, B := A
3. FRG-1
4. MP 2,3
5. TH1* 4,1.


Teorema TH7:

# wff razão
1. FRG-3
2. FRG-2
3. TH1* 1,2.


Teorema TH8:

# wff razão
1. TH7, com A :=
2. THEN-3
3. MP 1,2.


Teorema TH9:

# wff razão
1. THEN-1, com A := B, B := .


Teorema TH10:

# wff razão
1. TH7
2. THEN-3
3. MP 1,2
4. TH5
5. TH1* 3,4.


Teorema TH11:

# wff razão
1. TH10
2. THEN-2
3. MP 1,2
4. TH5
5. TH1* 3,4.


Teorema TH12:

# wff razão
1. THEN-1
2. TH1
3. MP 1,2
4. THEN-1
5. TH1* 3,4.


Teorema TH13:

# wff razão
1. THEN-2
2. THEN-3* 1
3. TH7
4. MP 3,2.


Regra TH14*:

# wff razão
1. premissa
2. THEN-1
3. MP 1,2
4. THEN-2
5. MP 3,4
6. THEN-1
7. MP 5,6
8. THEN-2* 7
9. premissa
10. MP 9,8.


Teorema TH15:

# wff razão
1. THEN-2
2. TH12
3. TH14* 1,2
4. THEN-3* 3
5. THEN-1
6. TH1* 5,4
7. THEN-3* 6
8. TH13
9. TH1* 7,8.


Teorema TH16:

# wff razão
1. FRG-1
2. THEN-3* 1
3. FRG-3
4. TH1* 3,2
5. THEN-3* 4
6. FRG-2
7. THEN-1
8. MP 6,7
9. THEN-2
10. MP 8,9
11. TH1* 5,10.


Teorema TH17:

# wff razão
1. TH16, com B := \neg B
2. FRG-3
3. THEN-1
4. MP 2,3
5. THEN-2
6. MP 4,5
7. TH1* 6,1.


Teorema TH18:

# wff razão
1. THEN-1
2. TH16
3. TH1* 2,1
4. TH15
5. MP 3,4
6. TH17
7. TH1* 5,6
8. THEN-2
9. MP 7,8
10. FRG-1
11. TH1* 10,9
12. TH17
13. TH1* 11,12.


Teorema TH19:

# wff razão
1. TH10
2. FRG-3
3. THEN-1
4. MP 2,3
5. THEN-2
6. MP 4,5
7. FRG-1* 6
8. TH14* 1,7
9. TH18
10. FRG-1* 9
11. TH14* 8,10
12. THEN-1* 11
13. THEN-2* 12
14. THEN-2
15. TH1* 13,14
16. FRG-1
17. TH1* 16,15
18. TH16
19. TH14* 17,18
20. FRG-1
21. TH1
22. MP 20,21
23. TH1* 19,22.


Teorema TH20:

# wff razão
1. TH11
2. TH7
3. MP 2,1.


Teorema TH21:

# wff razão
1. TH2, com B := ~B
2. FRG-2
3. TH14* 1,2.

Prova de que o terceiro axioma é dedutível dos dois primeiros[editar | editar código-fonte]

O lógico e filósofo polonês Jan Łukasiewicz, famoso por seus estudos em lógicas não-clássicas, provou que o THEN-3 é dedutível do THEN-1 e do THEN-2.

  • THEN-1:
  • THEN-2:


  • Tese 1:
# wff razão
1. THEN-1*
2. THEN-2
3. MP 1,2.

*

*


  • Tese 2:
# wff razão
1. THEN-2*
2. Prop. 1
3. MP 1,2.

*

*

*


  • Tese 3:
# wff razão
1. Prop.2
2. THEN-1*
3. MP 1,2.

*

*


  • Tese 4:
# wff razão
1. THEN-2*
2. Prop.3
3. MP 1,2.

*

*

*


  • Tese 5:
# wff razão
1. THEN-1*
2. THEN-1
3. MP 1,2.

*

*


  • Tese 6:
# wff razão
1. Prop.4*
2. Prop.5**
3. MP 1,2.

*

*

**

**

**


  • Tese 7:
# wff razão
1. Prop.3*
2. Prop.6
3. MP 1,2.

*

*

*


  • THEN-3:
# wff razão
1. Prop.7*
2. THEN-2
3. MP 1,2.

*

*


Axiomática de 5 operadores[editar | editar código-fonte]

  • THEN-1:
  • THEN-2:
  • AND-1:
  • AND-2:
  • AND-3:
  • OR-1:
  • OR-2:
  • OR-3:
  • NOT-1:
  • NOT-2:
  • NOT-3:
  • IFF-1:
  • IFF-2:
  • IFF-3:


Alguns Teoremas[editar | editar código-fonte]

# wff razão
1. THEN-1*
2. THEN-1**
3. THEN-2***.
4. 2,3 MP.
5. 1,4 MP.

* ,

** ,

*** , ,


Nuvola apps edu mathematics-p.svg

Esta página é um esboço de matemática. Ampliando-a você ajudará a melhorar o Wikilivros.