Mostrar código-fonte de Lógica: Cálculo Proposicional Clássico: Axiomática

{{navegação|[[Lógica: Cálculo Proposicional Clássico|Voltar para o índice de Cálculo Proposicional Clássico]]|[[Lógica: Cálculo Proposicional Clássico: Dedução Natural - Parte II|Dedução Natural - Parte II]]|[[Lógica: Cálculo Proposicional Clássico: Cálculo de Sequêntes|Cálculo de Sequêntes]]}}

==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 <math>\Delta\,\!</math> o conjunto dos axiomas e todas suas instâncias, se <math>\Delta\vdash \alpha\,\!</math>, então <math>\vdash \alpha</math>. Ou seja, se <math>\alpha\,\!</math> é dedutível dos axiomas, então <math>\alpha\,\!</math> é teorema.

E seja <math>\Gamma\,\!</math> um conjunto qualquer de fórmulas, se <math>\Delta \cup \Gamma \vdash \alpha</math> então <math>\Gamma \vdash \alpha</math>. Ou seja, se <math>\alpha\,\!</math> é dedutível de um conjunto <math>\Gamma\,\!</math> de fórmulas juntamente com os axiomas, então um raciocínio que tenha <math>\Gamma\,\!</math> como premissas e <math>\alpha\,\!</math> 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==
[[w:Gottlob 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:''	<math>A \to \left(B \to A\right)</math> <br />
''THEN-2:''	<math>\left(A \to \left(B \to C\right)\right) \to \left(\left(A \to B\right) \to \left(A \to C\right)\right)</math> <br />
''THEN-3:''	<math>\left(A \to \left(B \to C\right)\right) \to \left(B \to \left(A \to C\right)\right)</math> <br />
''FRG-1:''	<math>\left(A \to B\right) \to \left(\neg B \to \neg A\right)</math> <br />
''FRG-2:''	<math>\neg\neg A \to A\,\!</math> <br />
''FRG-3:''	<math>A \to \neg\neg A\,\!</math> 

*'''Regra de Inferência'''
''MP:''  <math>\left\{P, P\to  Q\right\} \vdash  Q</math>  

'''Regra THEN-1*:''' <math>A \vdash  \left(B\to A\right)</math>
{| border="1" cellpadding="5"
!style="background:#93D7AE;"|#
!style="background:#93D7AE;"|wff
!style="background:#93D7AE;"|razão
|-
|1. || <math>A\,\!</math> ||		premissa
|-
|2. || <math>A\to \left(B\to A\right)</math> ||		THEN-1
|-
|3. || <math>B\to A\,\!</math>	|| MP 1,2.
|}

'''Regra THEN-2*:'''  <math>A\to \left(B\to C\right) \vdash  \left(A\to B\right)\to \left(A\to C\right)</math>
{| border="1" cellpadding="5"
!style="background:#93D7AE;"|#
!style="background:#93D7AE;"|wff
!style="background:#93D7AE;"|razão
|-
|1. || <math>A\to \left(B\to C\right)</math> || premissa
|-
|2. || <math>\left(A \to  \left(B \to  C\right)\right) \to  \left(\left(A \to  B\right) \to  \left(A \to  C\right)\right)</math>	|| THEN-2
|-
|3. || <math>\left(A\to B\right)\to \left(A\to C\right)</math> || MP 1,2.
|}

'''Regra THEN-3*:''' <math>A\to \left(B\to C\right) \vdash  B\to \left(A\to C\right)</math>
{| border="1" cellpadding="5"
!style="background:#93D7AE;"|#
!style="background:#93D7AE;"|wff
!style="background:#93D7AE;"|razão
|-
|1. || <math>A\to \left(B\to C\right)</math> || premissa
|-
|2. || <math>\left(A \to  \left(B \to  C\right)\right) \to  \left(B \to  \left(A \to  C\right)\right)</math> || THEN-3
|-
|3. || <math>B\to \left(A\to C\right)</math> || MP 1,2.
|}

'''Regra FRG-1*:''' <math>A\to B \vdash  \neg B\to \neg A</math>
{| border="1" cellpadding="5"
!style="background:#93D7AE;"|#
!style="background:#93D7AE;"|wff
!style="background:#93D7AE;"|razão
|-
|1. || <math>\left(A\to B\right)\to \left(\neg B\to \neg A\right)</math> || FRG-1
|-
|2. || <math>A\to B</math> || premissa
|-
|3. || <math>\neg B\to \neg A</math> || MP 2,1.
|}

'''Regra TH1*:''' <math>A\to B, B\to C \vdash  A\to C</math>
{| border="1" cellpadding="5"
!style="background:#93D7AE;"|#
!style="background:#93D7AE;"|wff
!style="background:#93D7AE;"|razão
|-
|1. || <math>B\to C</math> || premissa
|-
|2. || <math>\left(B\to C\right)\to \left(A\to \left(B\to C\right)\right)</math> || THEN-1
|-
|3. || <math>A\to \left(B\to C\right)</math> || MP 1,2
|-
|4. || <math>\left(A\to \left(B\to C\right)\right)\to \left(\left(A\to B\right)\to \left(A\to C\right)\right)</math> || THEN-2
|-
|5. || <math>\left(A\to B\right)\to \left(A\to C\right)</math> || MP 3,4
|-
|6. || <math>A\to B</math> || premissa
|-
|7. || <math>A\to C</math> || MP 6,5.
|}

'''Teorema TH1:''' <math>\left( A\to B\right) \to \left( \left( B\to C\right) \to \left( A\to C\right) \right)</math> 
{| border="1" cellpadding="5"
!style="background:#93D7AE;"|#
!style="background:#93D7AE;"|wff
!style="background:#93D7AE;"|razão
|-
|1. || <math>\left( B\to C\right) \to \left( A\to \left( B\to C\right) \right)</math>  || THEN-1
|-
|2. || <math>\left( A\to \left( B\to C\right) \right) \to \left( \left( A\to B\right) \to \left( A\to C\right) \right)</math>  || THEN-2
|-
|3. || <math>\left( B\to C\right) \to \left( \left( A\to B\right) \to \left( A\to C\right) \right)</math>  || TH1* 1,2
|-
|4.
|<math>\left( \left( B\to C\right) \to \left( \left( A\to B\right) \to \left( A\to C\right) \right) \right) \to \left( \left( A\to B\right) \to \left( \left( B\to C\right) \to \left( A\to C\right) \right) \right)</math> 
|THEN-3
|-
|5. || <math>\left( A\to B\right) \to \left( \left( B\to C\right) \to \left( A\to C\right) \right)</math>  || MP 3,4.
|} 

'''Teorema TH2:''' <math>A\to \left( \neg A\to \neg B\right)</math> 
{| border="1" cellpadding="5"
!style="background:#93D7AE;"|#
!style="background:#93D7AE;"|wff
!style="background:#93D7AE;"|razão
|-
|1. || <math>A\to \left( B\to A\right)</math>  || THEN-1
|-
|2. || <math>\left( B\to A\right) \to \left( \neg A\to \neg B\right)</math>  || FRG-1
|-
|3. || <math>A\to \left( \neg A\to \neg B\right)</math>  || TH1* 1,2.
|}

'''Teorema TH3:''' <math>\neg A\to \left( A\to \neg B\right)</math> 
{| border="1" cellpadding="5"
!style="background:#93D7AE;"|#
!style="background:#93D7AE;"|wff
!style="background:#93D7AE;"|razão
|-
|1. || <math>A\to \left( \neg A\to \neg B\right)</math>  || TH 2
|-
|2. || <math>\left( A\to \left( \neg A\to \neg B\right) \right) \to \left( \neg A\to \left( A\to \neg B\right) \right)</math>  ||	THEN-3
|-
|3. || <math>\neg A\to \left( A\to \neg B\right)</math>  || MP 1,2.
|}

'''Teorema TH4:''' <math>\neg \left( A\to \neg B\right) \to A</math>
{| border="1" cellpadding="5"
!style="background:#93D7AE;"|#
!style="background:#93D7AE;"|wff
!style="background:#93D7AE;"|razão
|-
|1. || <math>\neg A\to \left( A\to \neg B\right)</math>  || TH3
|-
|2. || <math>\left( \neg A\to \left( A\to \neg B\right) \right) \to \left( \neg \left( A\to \neg B\right) \to \neg \neg A\right)</math>  || FRG-1
|-
|3. || <math>\neg \left( A\to \neg B\right) \to \neg \neg A</math> ||	MP 1,2
|-
|4. || <math>\neg \neg A\to A</math> || FRG-2
|-
|5. || <math>\neg \left( A\to \neg B\right) \to A</math> || TH1* 3,4.
|}

'''Teorema TH5:''' <math>\left( A\to \neg B\right) \to \left( B\to \neg A\right)</math> 
{| border="1" cellpadding="5"
!style="background:#93D7AE;"|#
!style="background:#93D7AE;"|wff
!style="background:#93D7AE;"|razão
|-
|1. || <math>\left( A\to \neg B\right) \to \left( \neg \neg B\to \neg A\right)</math>  || FRG-1
|-
|2.
|<math>\left( \left( A\to \neg B\right) \to \left( \neg \neg B\to \neg A\right) \right) \to \left( \neg \neg B\to \left( \left( A\to \neg B\right) \to \neg A\right) \right)</math> 
|THEN-3
|-
|3. || <math>\neg \neg B\to \left( \left( A\to \neg B\right) \to \neg A\right)</math>  || MP 1,2
|-
|4. || <math>B\to \neg \neg B</math> || FRG-3, with A := B
|-
|5. || <math>B\to \left( \left( A\to \neg B\right) \to \neg A\right)</math>  || TH1* 4,3
|-
|6.
|<math>\left( B\to \left( \left( A\to \neg B\right) \to \neg A\right) \right) \to \left( \left( A\to \neg B\right) \to \left( B\to \neg A\right) \right)</math> 
|FRG-1
|-
|7. || <math>\left( A\to \neg B\right) \to \left( B\to \neg A\right)</math>  || MP 5,6.
|}

'''Teorema TH6:''' <math>\neg \left( A\to \neg B\right) \to B</math>
{| border="1" cellpadding="5"
!style="background:#93D7AE;"|#
!style="background:#93D7AE;"|wff
!style="background:#93D7AE;"|razão
|-
|1. || <math>\neg \left( B\to \neg A\right) \to B</math> ||TH4, with A := B, B := A
|-
|2. || <math>\left( B\to \neg A\right) \to \left( A\to \neg B\right)</math>  || TH5, with A := B, B := A
|-
|3.
|<math>\left( \left( B\to \neg A\right) \to \left( A\to \neg B\right) \right) \to \left( \neg \left( A\to \neg B\right) \to \neg \left( B\to \neg A\right) \right)</math> 
|FRG-1
|-
|4. || <math>\neg \left( A\to \neg B\right) \to \neg \left( B\to \neg A\right)</math>  || MP 2,3
|-
|5. || <math>\neg \left( A\to \neg B\right) \to B</math> || TH1* 4,1.
|}

'''Teorema TH7:''' <math>A\to A</math>
{| border="1" cellpadding="5"
!style="background:#93D7AE;"|#
!style="background:#93D7AE;"|wff
!style="background:#93D7AE;"|razão
|-
|1. || <math>A\to \neg \neg A</math> || FRG-3
|-
|2. || <math>\neg \neg A\to A</math> || FRG-2
|-
|3. ||<math> A\to A</math> || TH1* 1,2.
|}

'''Teorema TH8:''' <math>A\to \left( \left( A\to B\right) \to B\right)</math> 
{| border="1" cellpadding="5"
!style="background:#93D7AE;"|#
!style="background:#93D7AE;"|wff
!style="background:#93D7AE;"|razão
|-
|1. || <math>\left( A\to B\right) \to \left( A\to B\right)</math>  || TH7, com A := <math>A\to B</math>
|-
|2. 
|<math>\left( \left( A\to B\right) \to \left( A\to B\right) \right) \to \left( A\to \left( \left( A\to B\right) \to B\right) \right)</math> 
|THEN-3
|-
|3. || <math>A\to \left( \left( A\to B\right) \to B\right)</math>  || MP 1,2.
|}

'''Teorema TH9:''' <math>B\to \left( \left( A\to B\right) \to B\right)</math> 
{| border="1" cellpadding="5"
!style="background:#93D7AE;"|#
!style="background:#93D7AE;"|wff
!style="background:#93D7AE;"|razão
|-
|1. || <math>B\to \left( \left( A\to B\right) \to B\right)</math>  || THEN-1, com A := B, B := <math>A\to B</math>.
|}

'''Teorema TH10:''' <math>A\to \left( B\to \neg \left( A\to \neg B\right) \right)</math> 
{| border="1" cellpadding="5"
!style="background:#93D7AE;"|#
!style="background:#93D7AE;"|wff
!style="background:#93D7AE;"|razão
|-
|1. || <math>\left( A\to \neg B\right) \to \left( A\to \neg B\right)</math>  || TH7
|-
|2.
|<math>\left( \left( A\to \neg B\right) \to \left( A\to \neg B\right) \right) \to \left( A\to \left( \left( A\to \neg B\right) \to \neg B\right)\right)</math> 
|THEN-3	
|-
|3. || <math>A\to \left( \left( A\to \neg B\right) \to \neg B\right)</math>  || MP 1,2
|-
|4. || <math>\left( \left( A\to \neg B\right) \to \neg B\right) \to \left( B\to \neg \left( A\to \neg B\right) \right)</math>  || TH5
|-
|5. || <math>A\to \left( B\to \neg \left( A\to \neg B\right) \right)</math>  || TH1* 3,4.
|}

'''Teorema TH11:''' <math>\left(A\to B\right)\to \left(\left(A\to \neg B\right)\to \neg A\right)</math>
{| border="1" cellpadding="5"
!style="background:#93D7AE;"|#
!style="background:#93D7AE;"|wff
!style="background:#93D7AE;"|razão
|-
|1. || <math>A\to \left(B\to \neg \left(A\to \neg B\right)\right)</math> ||TH10
|-
|2.
|<math>\left(A\to \left(B\to \neg \left(A\to \neg B\right)\right)\right)\to \left(\left(A\to B\right)\to \left(A\to \neg \left(A\to \neg B\right)\right)\right)</math>
|THEN-2
|-
|3. || <math>\left(A\to B\right)\to \left(A\to \neg \left(A\to \neg B\right)\right)</math> || MP 1,2
|-
|4. || <math>\left(A\to \neg \left(A\to \neg B\right)\right)\to \left(\left(A\to \neg B\right)\to \neg A\right)</math> || TH5
|-
|5. || <math>\left(A\to B\right)\to \left(\left(A\to \neg B\right)\to \neg A\right)</math> || TH1* 3,4.
|}

'''Teorema TH12:''' <math>\left(\left(A\to B\right)\to C\right)\to \left(A\to \left(B\to C\right)\right)</math>
{| border="1" cellpadding="5"
!style="background:#93D7AE;"|#
!style="background:#93D7AE;"|wff
!style="background:#93D7AE;"|razão
|-
|1. || <math>B\to \left(A\to B\right)</math> ||THEN-1
|-
|2. 
|<math>\left(B\to \left(A\to B\right)\right)\to \left(\left(\left(A\to B\right)\to C\right)\to \left(B\to C\right)\right)</math>
|TH1
|-
|3. || <math>\left(\left(A\to B\right)\to C\right)\to \left(B\to C\right)</math> || MP 1,2
|-
|4. || <math>\left(B\to C\right)\to \left(A\to \left(B\to C\right)\right)</math> || THEN-1
|-
|5. || <math>\left(\left(A\to B\right)\to C\right)\to \left(A\to \left(B\to C\right)\right)</math> || TH1* 3,4.
|}

'''Teorema TH13:''' <math>\left(B\to \left(B\to C\right)\right)\to \left(B\to C\right)</math>
{| border="1" cellpadding="5"
!style="background:#93D7AE;"|#
!style="background:#93D7AE;"|wff
!style="background:#93D7AE;"|razão
|-
|1. || <math>\left(B\to \left(B\to C\right)\right) \to  \left(\left(B\to B\right)\to \left(B\to C\right)\right)</math> || THEN-2
|-
|2. || <math>\left(B\to B\right)\to  \left( \left(B\to \left(B\to C\right)\right) \to  \left(B\to C\right)\right)</math> || THEN-3* 1
|-
|3. || <math>B\to B</math> || TH7
|-
|4. || <math>\left(B\to \left(B\to C\right)\right) \to  \left(B\to C\right)</math> || MP 3,2.
|}

'''Regra TH14*:''' <math>\left\{A\to \left(B\to P\right), P\to Q\right\} \vdash A\to \left(B\to Q\right)</math>
{| border="1" cellpadding="5"
!style="background:#93D7AE;"|#
!style="background:#93D7AE;"|wff
!style="background:#93D7AE;"|razão
|-
|1. || <math>P\to Q\,\!</math> || premissa
|-
|2. || <math>\left(P\to Q\right)\to \left(B\to \left(P\to Q\right)\right)</math> || THEN-1
|-
|3. || <math>B\to \left(P\to Q\right)</math> || MP 1,2
|-
|4. || <math>\left(B\to \left(P\to Q\right)\right)\to \left(\left(B\to P\right)\to \left(B\to Q\right)\right)</math> || THEN-2
|-
|5. || <math>\left(B\to P\right)\to \left(B\to Q\right)</math> || MP 3,4
|-
|6. 
|<math>\left(\left(B\to P\right)\to \left(B\to Q\right)\right)\to  \left(A\to \left(\left(B\to P\right)\to \left(B\to Q\right)\right)\right)</math>
|THEN-1
|-
|7. || <math>A\to \left(\left(B\to P\right)\to \left(B\to Q\right)\right)</math> || MP 5,6
|-
|8. || <math>\left(A\to \left(B\to P\right)\right)\to \left(A\to \left(B\to Q\right)\right)</math> || THEN-2* 7
|-
|9. || <math>A\to \left(B\to P\right)</math> || premissa
|-
|10. || <math>A\to \left(B\to Q\right)</math> || MP 9,8.
|}

'''Teorema TH15:''' <math>\left(\left(A\to B\right)\to \left(A\to C\right)\right)\to \left(A\to \left(B\to C\right)\right)</math>
{| border="1" cellpadding="5"
!style="background:#93D7AE;"|#
!style="background:#93D7AE;"|wff
!style="background:#93D7AE;"|razão
|-
|1.
|<math>\left(\left(A\to B\right)\to \left(A\to C\right)\right)\to \left(\left(\left(A\to B\right)\to A\right)\to \left(\left(A\to B\right)\to C\right)\right)</math>
|THEN-2
|-
|2. || <math>\left(\left(A\to B\right)\to C\right)\to \left(A\to \left(B\to C\right)\right)</math> || TH12
|-
|3.
|<math>\left(\left(A\to B\right)\to \left(A\to C\right)\right)\to \left(\left(\left(A\to B\right)\to A\right)\to \left(A\to \left(B\to C\right)\right)\right)</math>
|TH14* 1,2
|-
|4.
|<math>\left(\left(A\to B\right)\to A\right)\to  \left( \left(\left(A\to B\right) \to \left(A\to C\right)\right)\to \left(A\to \left(B\to C\right)\right)\right)</math>
|THEN-3* 3
|-
|5. || <math>A\to \left(\left(A\to B\right)\to A\right)</math> || THEN-1
|-
|6.
|<math>A\to  \left( \left(\left(A\to B\right) \to \left(A\to C\right)\right)\to \left(A\to \left(B\to C\right)\right) \right)</math>
|TH1* 5,4
|-
|7.
|<math>\left(\left(A\to B\right)\to \left(A\to C\right)\right)\to \left(A\to \left(A\to \left(B\to C\right)\right)\right)</math>
|THEN-3* 6
|-
|8. || <math>\left(A\to \left(A\to \left(B\to C\right)\right)\right)\to \left(A\to \left(B\to C\right)\right)</math> || TH13
|-
|9. || <math>\left(\left(A\to B\right)\to \left(A\to C\right)\right)\to \left(A\to \left(B\to C\right)\right)</math> || TH1* 7,8.
|}

'''Teorema TH16:''' <math>\left( \neg A\to \neg B\right) \to \left( B\to A\right)</math> 
{| border="1" cellpadding="5"
!style="background:#93D7AE;"|#
!style="background:#93D7AE;"|wff
!style="background:#93D7AE;"|razão
|-
|1. || <math>\left( \neg A\to \neg B\right) \to \left( \neg \neg B\to \neg \neg A\right)</math>  || FRG-1
|-
|2. || <math>\neg \neg B\to \left( \left( \neg A\to \neg B\right) \to \neg \neg A\right)</math>  || THEN-3* 1
|-
|3. || <math>B\to \neg \neg B</math> || FRG-3
|-
|4. || <math>B\to \left( \left( \neg A\to \neg B\right) \to \neg \neg A\right)</math>  || TH1* 3,2
|-
|5. || <math>\left( \neg A\to \neg B\right) \to \left( B\to \neg \neg A\right)</math>  || THEN-3* 4
|-
|6. || <math>\neg \neg A\to A</math> || FRG-2
|-
|7. || <math>\left( \neg \neg A\to A\right) \to \left( B\to \left( \neg \neg A\to A\right) \right)</math>  || THEN-1
|-
|8. || <math>B\to \left( \neg \neg A\to A\right)</math>  || MP 6,7
|-
|9.
|<math>\left( B\to \left( \neg \neg A\to A\right) \right) \to \left( \left( B\to \neg \neg A\right) \to \left( B\to A\right) \right)</math> 
|THEN-2
|-
|10. || <math>\left( B\to \neg \neg A\right) \to \left( B\to A\right)</math>  || MP 8,9
|-
|11. || <math>\left( \neg A\to \neg B\right) \to \left( B\to A\right)</math>  || TH1* 5,10.
|}

'''Teorema TH17:''' <math>\left( \neg A\to B\right) \to \left( \neg B\to A\right)</math> 
{| border="1" cellpadding="5"
!style="background:#93D7AE;"|#
!style="background:#93D7AE;"|wff
!style="background:#93D7AE;"|razão
|-
|1. || <math>\left( \neg A\to \neg \neg B\right) \to \left( \neg B\to A\right)</math>  || TH16, com B := \neg B
|-
|2. || <math>B\to \neg \neg B</math> || FRG-3
|-
|3. || <math>\left( B\to \neg \neg B\right) \to \left( \neg A\to \left( B\to \neg \neg B\right) \right)</math>  || THEN-1
|-
|4. || <math>\neg A\to \left( B\to \neg \neg B\right)</math>  || MP 2,3
|-
|5.
|<math>\left( \neg A\to \left( B\to \neg \neg B\right) \right) \to \left( \left( \neg A\to B\right) \to \left( \neg A\to \neg \neg B\right) \right)</math> 
|THEN-2
|-
|6. || <math>\left( \neg A\to B\right) \to \left( \neg A\to \neg \neg B\right)</math>  || MP 4,5
|-
|7. || <math>\left( \neg A\to B\right) \to \left( \neg B\to A\right)</math>  || TH1* 6,1.
|}

'''Teorema TH18:''' <math>\left( \left( A\to B\right) \to B\right) \to \left( \neg A\to B\right)</math> 
{| border="1" cellpadding="5"
!style="background:#93D7AE;"|#
!style="background:#93D7AE;"|wff
!style="background:#93D7AE;"|razão
|-
|1. || <math>\left( A\to B\right) \to \left( \neg B\to \left( A\to B\right) \right)</math>  || THEN-1
|-
|2. || <math>\left( \neg B\to \neg A\right) \to \left( A\to B\right)</math>  || TH16
|-
|3. || <math>\left( \neg B\to \neg A\right) \to \left( \neg B\to \left( A\to B\right) \right)</math>  || TH1* 2,1
|-
|4.
|<math>\left( \left( \neg B\to \neg A\right) \to \left( \neg B\to \left( A\to B\right) \right) \right) \to \left( \neg B\to \left( \neg A\to \left( A\to B\right) \right) \right)</math> 
|TH15 
|-
|5. || <math>\neg B\to \left( \neg A\to \left( A\to B\right) \right)</math>  || MP 3,4
|-
|6. || <math>\left( \neg A\to \left( A\to B\right) \right) \to \left( \neg \left( A\to B\right) \to A\right)</math>  || TH17
|-
|7. || <math>\neg B\to \left( \neg \left( A\to B\right) \to A\right)</math>  || TH1* 5,6
|-
|8.
|<math>\left( \neg B\to \left( \neg \left( A\to B\right) \to A\right) \right) \to  \left( \left( \neg B\to \neg \left( A\to B\right) \right) \to \left( \neg B\to A\right) \right)</math> 
|THEN-2
|-
|9. || <math>\left( \neg B\to \neg \left( A\to B\right) \right) \to \left( \neg B\to A\right)</math>  || MP 7,8
|-
|10. || <math>\left( \left( A\to B\right) \to B\right)  \to  \left( \neg B\to \neg \left( A\to B\right) \right)</math>  || FRG-1
|-
|11. || <math>\left( \left( A\to B\right) \to B\right) \to \left( \neg B\to A\right)</math>  || TH1* 10,9
|-
|12. || <math>\left( \neg B\to A\right) \to \left( \neg A\to B\right)</math>  || TH17
|-
|13. || <math>\left( \left( A\to B\right) \to B\right) \to \left( \neg A\to B\right)</math>  || TH1* 11,12.
|}

'''Teorema TH19:''' <math>\left( A\to C\right) \to  \left( \left( B\to C\right) \to \left( \left( \left( A\to B\right) \to B\right) \to C\right) \right)</math> 
{| border="1" cellpadding="5"
!style="background:#93D7AE;"|#
!style="background:#93D7AE;"|wff
!style="background:#93D7AE;"|razão
|-
|1. || <math>\neg A\to \left( \neg B\to \neg \left( \neg A\to \neg \neg B\right) \right)</math>  || TH10
|-
|2. || <math>B\to \neg \neg B</math> || FRG-3
|-
|3. || <math>\left( B\to \neg \neg B\right) \to \left( \neg A\to \left( B\to \neg \neg B\right) \right)</math>  || THEN-1
|-
|4. || <math>\neg A\to \left( B\to \neg \neg B\right)</math>  || MP 2,3
|-
|5.
|<math>\left( \neg A\to \left( B\to \neg \neg B\right) \right) \to \left( \left( \neg A\to B\right) \to \left( \neg A\to \neg \neg B\right) \right)</math> 
|THEN-2
|-
|6. || <math>\left( \neg A\to B\right) \to \left( \neg A\to \neg \neg B\right)</math>  || MP 4,5
|-
|7. || <math>\neg \left( \neg A\to \neg \neg B\right) \to \neg \left( \neg A\to B\right)</math>  || FRG-1* 6
|-
|8. || <math>\neg A\to \left( \neg B\to \neg \left( \neg A\to B\right) \right)</math>  || TH14* 1,7
|-
|9. || <math>\left( \left( A\to B\right) \to B\right) \to \left( \neg A\to B\right)</math>  || TH18
|-
|10. || <math>\neg \left( \neg A\to B\right) \to \neg \left( \left( A\to B\right) \to B\right)</math>  || FRG-1* 9
|-
|11. || <math>\neg A\to \left( \neg B\to \neg \left( \left( A\to B\right) \to B\right) \right)</math>  || TH14* 8,10
|-
|12.
|<math>\neg C\to \left( \neg A\to \left( \neg B\to \neg \left( \left( A\to B\right) \to B\right) \right) \right)</math> 
|THEN-1* 11
|-
|13.
|<math>\left( \neg C\to \neg A\right) \to \left( \neg C\to \left( \neg B\to \neg \left( \left( A\to B\right) \to B\right) \right) \right)</math> 
|THEN-2* 12
|-
|14.
|<math>\left( \neg C\to \left( \neg B\to \neg \left( \left( A\to B\right) \to B\right) \right) \right)  \to  \left( \left( \neg C\to \neg B\right) \to \left( \neg C\to \neg \left( \left( A\to B\right) \to B\right) \right) \right)</math> 
|THEN-2
|-
|15.
|<math>\left( \neg C\to \neg A\right) \to  \left( \left( \neg C\to \neg B\right) \to \left( \neg C\to \neg \left( \left( A\to B\right) \to B\right) \right) \right)</math> 
|TH1* 13,14
|-
|16. || <math>\left( A\to C\right) \to \left( \neg C\to \neg A\right)</math>  || FRG-1
|-
|17.
|<math>\left( A\to C\right) \to \left( \left( \to C\to \neg B\right) \to \left( \neg C\to \neg \left( \left( A\to B\right) \to B\right) \right) \right)</math> 
|TH1* 16,15
|-
|18.
|<math>\left( \neg C\to \neg \left( \left( A\to B\right) \to B\right) \right) \to \left( \left( \left( A\to B\right) \to B\right) \to C\right)</math> 
|TH16
|-
|19.
|<math>\left( A\to C\right) \to  \left( \left( \neg C\to \neg B\right) \to \left( \left( \left( A\to B\right) \to B\right) \to C\right) \right)</math> 
|TH14* 17,18
|-
|20. || <math>\left( B\to C\right) \to \left( \neg C\to \neg B\right)</math>  || FRG-1
|-
|21.
|<math>\left( \left( B\to C\right) \to \left( \neg C\to \neg B\right) \right) \to \left( \left( \left( \neg C\to \neg B\right) \to  \left( \left( \left( A\to B\right) \to B\right) \to C\right)  \right)  \to  \left(  \left( B\to C\right)  \to  \left( \left( \left( A\to B\right) \to B\right) \to C\right) \right) \right)</math> 
|TH1
|-
|22.
|<math>\left( \left( \neg C\to \neg B\right) \to  \left( \left( \left( A\to B\right) \to B\right) \to C\right)  \right)  \to  \left(  \left( B\to C\right)  \to  \left( \left( \left( A\to B\right) \to B\right) \to C\right) \right)</math> 
|MP 20,21
|-
|23.
|<math>\left( A\to C\right) \to  \left( \left( B\to C\right) \to \left( \left( \left( A\to B\right) \to B\right) \to C\right) \right)</math> 
|TH1* 19,22.
|}

'''Teorema TH20:''' <math>\left( A\to \neg A\right) \to \neg A</math>
{| border="1" cellpadding="5"
!style="background:#93D7AE;"|#
!style="background:#93D7AE;"|wff
!style="background:#93D7AE;"|razão
|-
|1. || <math>\left( A\to A\right) \to \left( \left( A\to \neg A\right) \to \neg A\right)</math>  || TH11
|-
|2. || <math>A\to A</math> || TH7
|-
|3. || <math>\left( A\to \neg A\right) \to \neg A</math> || MP 2,1.
|}

'''Teorema TH21:''' <math>A\to \left( \neg A\to B\right)</math> 
{| border="1" cellpadding="5"
!style="background:#93D7AE;"|#
!style="background:#93D7AE;"|wff
!style="background:#93D7AE;"|razão
|-
|1. || <math>A\to \left( \neg A\to \neg \neg B\right)</math>  || TH2, com B := ~B
|-
|2. || <math>\neg \neg B\to B</math> || FRG-2
|-
|3. || <math>A\to \left( \neg A\to B\right)</math>  || TH14* 1,2.
|}

===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<nowiki>: </nowiki><math>P\to \left(Q\to P\right)</math>

*;THEN-2<nowiki>: </nowiki><math>\left(P\to \left(Q\to R\right)\right)\to \left(\left(P\to Q\right)\to \left(P\to R\right)\right)</math>

*;Tese 1<nowiki>:</nowiki> <math>\left(\left(Q\to R\right)\to \left( P\to \left(Q \to R\right)\right)\right)\to \left(\left(P\to Q\right)\to \left(P\to R\right)\right)</math>
{| border="1" cellpadding="5"
!style="background:#93D7AE;"|#
!style="background:#93D7AE;"|wff
!style="background:#93D7AE;"|razão
|-
|1. || <math>\left(\left(\left(P\to \left(Q\to R\right)\right)\to \left(\left(P\to Q\right)\to \left(P\to R\right)\right)\right)\to \left(\left(Q\to R\right)\to \left(\left(P\to \left(Q\to R\right)\right)\to \left(\left(P\to Q\right)\to \left(P\to R\right)\right)\right)\right)\right)</math>   ||		THEN-1*
|-
|2. || <math>\left(P\to \left(Q\to R\right)\right)\to \left(\left(P\to Q\right)\to \left(P\to R\right)\right)</math> ||		THEN-2
|-
|3. || <math>\left(\left(Q\to R\right)\to \left( P\to \left(Q \to R\right)\right)\right)\to \left(\left(P\to Q\right)\to \left(P\to R\right)\right)</math>	|| MP 1,2.
|}

'''<nowiki>*</nowiki>''' <math>P/ \left(P\to \left(Q\to R\right)\right)\to \left(\left(P\to Q\right)\to \left(P\to R\right)\right)</math>

'''<nowiki>*</nowiki>''' <math>Q/ Q\to R</math>

*;Tese 2<nowiki>:</nowiki> <math>\left(\left(Q\to R\right)\to \left(P\to\left(Q\to R\right)\right)\right)\to \left(\left(Q\to R\right)\to \left(\left(P\to Q\right)\to \left(P\to R\right)\right)\right)</math>
{| border="1" cellpadding="5"
!style="background:#93D7AE;"|#
!style="background:#93D7AE;"|wff
!style="background:#93D7AE;"|razão
|-
|1. || <math>
\left(\left(\left(Q\to R\right)\to \left(\left(P\to \left(Q\to R\right)\right)\right)\to \left(\left(P\to Q\right)\to \left(P\to R\right)\right)\right)\right)\to \left(\left(\left(Q\to R\right)\to \left(P\to \left(Q\to R\right)\right)\right)\to \left(Q\to R\right)\to \left(\left(P\to Q\right)\to \left(P\to R\right)\right)\right)</math>  ||		THEN-2*
|-
|2. || <math>\left(\left(Q\to R\right)\to \left( P\to \left(Q \to R\right)\right)\right)\to \left(\left(P\to Q\right)\to \left(P\to R\right)\right)</math> ||		Prop. 1
|-
|3. || <math>\left(\left(Q\to R\right)\to \left(P\to\left(Q\to R\right)\right)\right)\to \left(\left(Q\to R\right)\to \left(\left(P\to Q\right)\to \left(P\to R\right)\right)\right)</math>	|| MP 1,2.
|}

<nowiki>*</nowiki><math>P/ Q\to R</math>

<nowiki>*</nowiki><math>Q/ P\to \left(Q \to R\right)</math>

<nowiki>*</nowiki><math>R/ \left(P\to Q\right)\to \left(P\to R\right)</math>

*;Tese 3<nowiki>:</nowiki> <math>\left( Q\to R\right)\to \left(\left(P\to Q\right)\to \left(P\to R\right)\right)</math>
{| border="1" cellpadding="5"
!style="background:#93D7AE;"|#
!style="background:#93D7AE;"|wff
!style="background:#93D7AE;"|razão
|-
|1. || <math>\left(\left(Q\to R\right)\to \left(P\to\left(Q\to R\right)\right)\right)\to \left(\left(Q\to R\right)\to \left(\left(P\to Q\right)\to \left(P\to R\right)\right)\right)
 </math>  ||		Prop.2
|-
|2. || <math>\left(Q\to R\right)\to \left(P\to \left(Q\to R\right)\right)</math> ||		THEN-1*
|-
|3. || <math>\left( Q\to R\right)\to \left(\left(P\to Q\right)\to \left(P\to R\right)\right)</math>|| MP 1,2.
|}

<nowiki>*</nowiki> <math>P/ Q\to R</math>

<nowiki>*</nowiki> <math>Q/ P\,\!</math>

*;Tese 4<nowiki>:</nowiki> <math>\left(\left(Q\to R\right)\to \left(P\to Q\right)\right)\to \left(\left(Q\to R\right)\to \left(P\to R\right)\right)</math>

{| border="1" cellpadding="5"
!style="background:#93D7AE;"|#
!style="background:#93D7AE;"|wff
!style="background:#93D7AE;"|razão
|-
|1. || <math>\left(\left(Q\to R\right)\to \left(\left(P\to Q\right)\to \left(P\to R\right)\right)\right)\to \left(\left(\left(Q\to R\right)\to \left(P\to Q\right)\right)\to \left(\left(Q\to R\right)\to \left(P\to R\right)\right)\right) 
 </math>  ||		THEN-2*
|-
|2. || <math>\left( Q\to R\right)\to \left(\left(P\to Q\right)\to \left(P\to R\right)\right)</math> ||		Prop.3
|-
|3. || <math>\left(\left(Q\to R\right)\to \left(P\to Q\right)\right)\to \left(\left(Q\to R\right)\to \left(P\to R\right)\right)</math>	|| MP 1,2.
|}

<nowiki>*</nowiki> <math>P/ Q\to R</math>

<nowiki>*</nowiki> <math>Q/ P\to Q</math>

<nowiki>*</nowiki> <math>R/ P\to R</math>

*;Tese 5<nowiki>:</nowiki> <math>R\to \left(P\to \left(Q\to P\right)\right)</math>
{| border="1" cellpadding="5"
!style="background:#93D7AE;"|#
!style="background:#93D7AE;"|wff
!style="background:#93D7AE;"|razão
|-
|1. || <math>\left(P\to \left(Q\to P\right)\right)\to \left(R\to \left(P\to \left(Q\to P\right)\right)\right)  
 </math>  ||		THEN-1*
|-
|2. || <math>P\to \left(Q\to P\right)</math> ||		THEN-1
|-
|3. ||  <math>R\to \left(P\to \left(Q\to P\right)\right)</math>	|| MP 1,2.
|}

<nowiki>*</nowiki> <math>P/ P\to \left(Q\to P\right)</math>

<nowiki>*</nowiki> <math>Q/ R\,\!</math>

*;Tese 6<nowiki>:</nowiki> <math>\left(\left( P\to Q\right)\to R\right)\to \left(Q\to R\right)</math>
{| border="1" cellpadding="5"
!style="background:#93D7AE;"|#
!style="background:#93D7AE;"|wff
!style="background:#93D7AE;"|razão
|-
|1. || <math>\left(\left(\left(P\to Q\right)\to R\right)\to \left(Q\to \left(P\to Q\right)\right)\right)\to \left(\left(\left(P\to Q\right)\to R\right)\to \left(Q\to R\right)\right)   
 </math>  ||		Prop.4*
|-
|2. || <math>\left(\left(P\to Q\right)\to R\right)\to \left(Q\to \left(P\to Q\right)\right)</math> ||		Prop.5**
|-
|3. ||  <math>\left(\left( P\to Q\right)\to R\right)\to \left(Q\to R\right)</math>	|| MP 1,2.
|}

<nowiki>*</nowiki> <math>Q/ P\to Q</math>

<nowiki>*</nowiki> <math>P/ Q\,\!</math>

<nowiki>*</nowiki><nowiki>*</nowiki> <math>R/ \left(P\to Q\right)\to R</math>

<nowiki>*</nowiki><nowiki>*</nowiki> <math>P/ Q\,\!</math>

<nowiki>*</nowiki><nowiki>*</nowiki> <math>Q/ P\,\!</math>

*;Tese 7<nowiki>:</nowiki> <math>\left(S\to \left(\left(P\to Q\right)\to R\right)\right)\to \left(S\to \left(Q\to R\right)\right)</math>

{| border="1" cellpadding="5"
!style="background:#93D7AE;"|#
!style="background:#93D7AE;"|wff
!style="background:#93D7AE;"|razão
|-
|1. || <math>\left(\left(\left(P\to Q\right)\to R\right)\to \left(Q\to R\right)\right)\to \left(\left(S\to \left(\left(P\to Q\right)\to R\right)\right)\to \left(S\to \left(Q\to R\right)\right)\right)    
 </math>  ||		Prop.3*
|-
|2. || <math>\left(\left( P\to Q\right)\to R\right)\to \left(Q\to R\right)</math> ||		Prop.6
|-
|3. ||  <math>\left(S\to \left(\left(P\to Q\right)\to R\right)\right)\to \left(S\to \left(Q\to R\right)\right)</math>	|| MP 1,2.
|}

<nowiki>*</nowiki> <math>Q/ \left(P\to Q\right)\to R</math>

<nowiki>*</nowiki> <math>R/ Q\to R</math>

<nowiki>*</nowiki> <math>P/ S\,\!</math>

*;THEN-3<nowiki>:</nowiki> <math>\left(P\to \left(Q\to R\right)\right)\to \left(Q\to \left(P\to R\right)\right)</math>
{| border="1" cellpadding="5"
!style="background:#93D7AE;"|#
!style="background:#93D7AE;"|wff
!style="background:#93D7AE;"|razão
|-
|1. || <math>\left(\left(P\to \left(Q\to R\right)\right)\to \left(\left(P\to Q\right)\to \left(P\to R\right)\right)\right)\to \left(\left(P\to \left(Q\to R\right)\right)\to \left(Q\to \left(P\to R\right)\right)\right)     
 </math>  ||		Prop.7*
|-
|2. || <math>\left(P\to \left(Q\to R\right)\right)\to \left(\left(P\to Q\right)\to \left(P\to R\right)\right)</math> ||		THEN-2
|-
|3. ||  <math>\left(P\to \left(Q\to R\right)\right)\to \left(Q\to \left(P\to R\right)\right)</math>	|| MP 1,2.
|}

<nowiki>*</nowiki> <math>S/ P\to \left(Q\to R\right)</math>

<nowiki>*</nowiki> <math>R/ P\to R</math>

<math>\mathfrak{Quod\ Erat\ Demonstrandum}</math>

==Axiomática de 5 operadores==

* THEN-1: <math>\varphi\to\left(\chi\to\varphi\right)</math>
* THEN-2: <math>\left(\varphi\to\left(\chi\to\psi\right)\right)\to\left(\left( \varphi\to\chi\right)\to\left(\varphi\to\psi\right)\right)</math>
* AND-1: <math>\left(\varphi\land\chi\right)\to\varphi</math>
* AND-2: <math>\left(\varphi\land\chi\right)\to\chi</math>
* AND-3: <math>\varphi\to\left(\chi\to\left(\varphi\land\chi\right)\right)</math>
* OR-1: <math>\varphi\to\left(\varphi\lor\chi\right)</math>
* OR-2: <math>\chi\to\left(\varphi\lor\chi\right)</math>
* OR-3: <math>\left(\varphi\to \psi\right)\to \left(\left(\chi\to \psi\right)\to \left(\left(\varphi\lor\chi\right)\to\psi\right)\right)</math>
* NOT-1: <math>\left(\varphi\to\chi\right)\to\left(\left(\varphi\to\neg\chi\right)\to \neg\varphi\right)</math>
* NOT-2: <math>\varphi\to\left(\neg\varphi\to\chi\right)</math>
* NOT-3: <math>\varphi \lor \neg \varphi</math>
* IFF-1: <math>\left(\varphi \leftrightarrow \chi \right)\to \left(\varphi \to \chi \right)</math>
* IFF-2: <math>\left(\varphi \leftrightarrow \chi \right)\to \left(\chi \to \varphi\right)</math>
* IFF-3: <math>\left(\varphi\to\chi\right)\to\left(\left(\chi\to \varphi\right)\to \left(\varphi\leftrightarrow \chi\right)\right)</math>

===Alguns Teoremas===

*<math>\alpha \to \alpha \,\!</math>
{| border="1" cellpadding="5"
!style="background:#93D7AE;"|#
!style="background:#93D7AE;"|wff
!style="background:#93D7AE;"|razão
|-
|1. || <math>\alpha \to \left(\alpha \to \alpha\right)</math>   ||		THEN-1*
|-
|2. || <math>\alpha \to \left(\left(\alpha \to \alpha\right) \to \alpha\right)</math> ||		THEN-1**
|-
|3. || <math>\left(\alpha \to  \left(\left(\alpha \to  \alpha\right) \to  \alpha\right)\right) \to  \left(\left(\alpha \to  \left(\alpha \to  \alpha\right)\right) \to  \left(\alpha \to  \alpha\right)\right)</math>	|| THEN-2***.
|-
|4. || <math>\left(\left(\alpha \to  \left(\alpha \to  \alpha\right)\right) \to  \left(\alpha \to  \alpha\right)\right)</math>	|| 2,3 MP.
|-
|5. || <math>\alpha \to \alpha \,\!</math>	|| 1,4 MP.
|}

<nowiki>*</nowiki> <math>\varphi / \alpha\,\!</math> , <math>\chi / \alpha\,\!</math>

<nowiki>**</nowiki> <math>\varphi / \alpha\,\!</math> , <math>\chi / \alpha \to \alpha\,\!</math>

<nowiki>***</nowiki> <math>\varphi / \alpha\,\!</math> , <math>\chi / \alpha \to \alpha\,\!</math> , <math>\psi / \alpha\,\!</math>

[[Categoria:Lógica Matemática|{{SUBPAGENAME}}]]