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

Origem: Wikilivros, livros abertos por um mundo aberto.

Índice 1 Introdução 2 Axiomática de Frege 2.1 Prova de que o terceiro axioma é dedutível dos dois primeiros 3 Axiomática de 5 operadores 3.1 Alguns Teoremas

[editar] Introdução

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.

[editar] Axiomática de Frege

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.

[editar] Prova de que o terceiro axioma é dedutível dos dois primeiros

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.

*

*

[editar] Axiomática de 5 operadores

• 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:

[editar] Alguns Teoremas

• 

#	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.