Saltar para o conteúdo

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

Fonte: Wikiversidade



Uma outra forma de lidar sintáticamente com o CPC é axiomáticamente. 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.

* ,

** ,

*** , ,