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


Introdução

editar

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

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

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
  • 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
  •  
# wff razão
1.   THEN-1*
2.   THEN-1**
3.   THEN-2***.
4.   2,3 MP.
5.   1,4 MP.

*   ,  

**   ,  

***   ,   ,  


 

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