Apostila Dedução Natural - MATC93

Prévia do material em texto

Deduc¸a˜o Natural
Universidade Federal da Bahia
MATA47 - Prof. Paul Regnier - 11 de agosto de 2016
A deduc¸a˜o natural e´ um sistema formal que permite escrever demostrac¸a˜o de resultados
usando regras de infereˆncia associadas aos conectivos da linguagem da lo´gica proposicional e da
lo´gica de primeira ordem. Ao contra´rio dos sistemas axioma´ticos, a deduc¸a˜o natural tem mais
semelhanc¸as com os racioc´ınios usuais utilizado para escrever provas informais em Matema´tica.
Portanto, este sistema formal e´ mais adequado para a formalizac¸a˜o das provas do domı´nio das
Matema´ticas.
Definic¸a˜o 1 (Conectivo principal). O conectivo (ou operador) principal de uma fo´rmula e´
definido por:
ˆ Se A e´ atoˆmica, enta˜o A na˜o tem conectivo principal;
ˆ Se A = ¬B, enta˜o ¬ e´ o operador principal de A;
ˆ Se A = B ⊕C onde ⊕ ∈ {∨,∧,→}, enta˜o ⊕ e´ o operador principal de A.
1 Deduc¸a˜o natural com Sequente
Apresentamos primeiro a notac¸a˜o da deduc¸a˜o natural com sequente. Nesta notac¸a˜o, o conjunto
das hipo´teses, chamado de contexto, necessa´rio para aplicar uma regra de infereˆncia aparece
explicitamente. A aplicac¸a˜o de certas regras modifica o contexto. Outras o deixam invariante.
Como o contexto e´ reescrito a cada linha da prova, as mudanc¸as no conjunto de hipo´teses
ao longo da prova aparece claramente. Desta forma, o conjunto das hipo´teses “correntes”,
dispon´ıveis a cada etapa da demonstrac¸a˜o para aplicac¸a˜o de uma regra de infereˆncia, aparece
explicitamente.
Definic¸a˜o 2 (Sequente). Um sequente e´ uma tupla denotada Γ ⊢ A na qual:
ˆ Γ e´ um conjunto finito de fo´rmulas que representa as hipo´teses que podem ser utilizadas
na demonstrac¸a˜o (para demostrar A).
ˆ A e´ uma fo´rmula que representa o resultado a ser demonstrado.
Γ e´ chamado de contexto do sequente A de conclusa˜o do sequente.
Regras sem Conectivos
Axioma: axΓ,A ⊢ A Enfraquecimento: Γ ⊢ A enfΓ,B ⊢ A
O axioma estabelece que se A e´ hipo´tese, enta˜o A pode ser demostrada. Ou seja, se A enta˜o
A. A regra de enfraquecimento afirma que se um resultado e´ derivado de um contexto, enta˜o
este mesmo resultado pode ser derivado de um contexto maior. Ou seja, o aumento do nu´mero
de hipo´teses na˜o pode invalidar uma prova.
Regras de Infereˆncia dos Conectivos
Para cada conectivo, existem duas regras:
ˆ Uma regra de introduc¸a˜o do conectivo, a qual permite provar uma fo´rmula tendo este
conectivo como conectivo principal da fo´rmula;
ˆ Uma regra de eliminac¸a˜o do conectivo, a qual permite utilizar uma fo´rmula tendo este
conectivo como conectivo principal.
Regra de introduc¸a˜o da implicac¸a˜o
Γ,A ⊢ B →i
Γ ⊢ A→ B
De baixo para cima, esta regra significa que para mostrar A → B, basta supor A (ou seja,
adicionar A as hipo´teses) e demostrar B.
Segue treˆs exemplos simples de utilizac¸a˜o desta regra:
ax
A,¬A ⊢ A →i
A ⊢ ¬A→ A →i⊢ A→ (¬A→ A)
ax
A,¬A ⊢ A →i¬A ⊢ A→ A →i⊢ ¬A→ (A→ A)
ax
A ⊢ A
enf
A,B ⊢ A →i
A ⊢ B → A
Observe como esta regra modifica o contexto, fazendo uso de uma hipo´tese para a inserir
na conclusa˜o, e provar assim uma fo´rmula de conectivo principal →.
Regra de eliminac¸a˜o da implicac¸a˜o
Γ ⊢ A→ B Γ ⊢ A →e
Γ ⊢ B
De baixo para cima: para demonstrar B, desde que temos um teorema afirmando A → B
(ou uma prova de A→ B), e´ suficiente provar A. Esta regra, conhecida como Modus Ponens, e´
comum ao sistema axioma´tico. Ela na˜o altera o contexto e permite provar a conclusa˜o, usando
uma fo´rmula com conectivo principal →.
Regra de introduc¸a˜o da conjunc¸a˜o
Γ ⊢ A Γ ⊢ B ∧i
Γ ⊢ A ∧B
De baixo para cima, para mostrar A ∧B, e´ suficiente mostrar A e mostrar B.
Regra de eliminac¸a˜o da conjunc¸a˜o
Γ ⊢ A ∧B ∧ee
Γ ⊢ A Γ ⊢ A ∧B ∧deΓ ⊢ B
De cima para baixo: De A ∧ B, pode se deduzir A (eliminac¸a˜o a esquerda) quanto B
(eliminac¸a˜o a direita).
2
Regra de introduc¸a˜o da disjunc¸a˜o
Γ ⊢ A ∨riΓ ⊢ A ∨B Γ ⊢ B ∨liΓ ⊢ A ∨B
De baixo para cima: para demonstrar A ∨B, e´ suficiente demostrar A ou demostrar B.
Regra de eliminac¸a˜o da disjunc¸a˜o
Γ ⊢ A ∨B Γ,A ⊢ C Γ,B ⊢ C ∨e
Γ ⊢ C
De baixo para cima: para demostrar C, tendo uma prova de A ∨B, e´ suficiente demostrar
C, por um lado, supondo A e, por outro lado, supondo B. Isto e´ um racioc´ınio por casos. Por
exemplo, tendo uma propriedade sobre um inteiro n, podera´ se distinguir os casos n par ou n
ı´mpar.
Regra de introduc¸a˜o da negac¸a˜o
Γ,A ⊢ – ¬i
Γ ⊢ ¬A
De baixo para cima: para demostrar ¬A, suponha-se A e deduz-se o absurdo.
Regra de eliminac¸a˜o da negac¸a˜o (Absurdo cla´ssico)
Γ,¬A ⊢ – ¬e
Γ ⊢ A
Esta regra (tambe´m denominada de “absurdo cla´ssico”) corresponde ao racioc´ınio por con-
tradic¸a˜o ou pelo absurdo. Para demostrar A, suponha-se ¬A e deduz-se o absurdo. Esta regra
pode se aplicar a qualquer momento, pois e´ sempre poss´ıvel supor ¬A e buscar uma contradic¸a˜o.
Regra de introduc¸a˜o do absurdo
Γ ⊢ A Γ ⊢ ¬A –i
Γ ⊢ –
Se demostramos A e ¬A, enta˜o demostramos o absurdo.
Regra de eliminac¸a˜o do absurdo
Γ ⊢ – –e
Γ ⊢ A
De cima para baixo: do absurdo, tudo se deduz. Se conseguimos demonstrar o absurdo,
enta˜o podemos demonstrar qualquer coisa.
3
Lema 1. ¬A↔ (A→ –)
ax¬A,A ⊢ A ax¬A,A ⊢ ¬A ¬e¬A,A ⊢ – →i¬A ⊢ A→ – →i⊢ ¬A→ (A→ –)
ax
A→ –,A ⊢ A axA→ –,A ⊢ A→ – →e
A→ –,A ⊢ – ¬i
A→ – ⊢ ¬A →i⊢ (A→ –)→ ¬A ∧i⊢ (A→ –)↔ ¬A
2 Deduc¸a˜o natural sem Sequente
Apresentamos agora uma notac¸a˜o mais leve, sem sequente. Esta notac¸a˜o e´ equivalente a an-
terior, pore´m o conjunto das hipo´teses e´ escrito apenas uma vez e as regras de infereˆncias sa˜o
aplicadas fazendo refereˆncia, quando necessa´rio, as hipo´teses utilizadas. Uma derivac¸a˜o de A
sob as hipo´teses A1,A2,⋯,An sera´ representada por:
A1 ⋯ An
...
A
Uma derivac¸a˜o e´ uma a´rvore finita, onde cada no´ e´ rotulado por uma fo´rmula. A a´rvore e´
constru´ıda saindo das folhas (no´s iniciais, em cima da a´rvore) dos ramos e descendo para a raiz
(no´ terminal), a fo´rmula a ser derivada.
Regras sem Conectivos
Os no´s iniciais sa˜o derivados do axioma que e´ interpretado aqui da seguinte forma: a fo´rmula
A pode ser derivada da hipo´tese A, o que e´ escrito simplesmente A.
A regra de enfraquecimento permite inserir hipo´teses quando for necessa´rio.
Axioma:
A
ax
A
Enfraquecimento:
...
A B
enf
A
Regras de Infereˆncia dos Conectivos
Regra de eliminac¸a˜o da implicac¸a˜o
...
A→ B ...A →e
B
Esta regra significa que podemos derivar B a partir das derivac¸o˜es de A→ B e A (regra do
Modus Ponens). O contexto (conjunto de hipo´teses) do consequente (B) sa˜o as mesmas que as
hipo´teses das derivac¸o˜es iniciais (A→ B e A). Na aplicac¸a˜o desta regra, o contexto na˜o muda.
Portanto, na˜o e´ preciso referenciar explicitamente as hipo´teses utilizadas.
4
Regra de introduc¸a˜o da implicac¸a˜o [A]
...
B →i
A→ B
Esta regra significa que podemos derivar A→ B, desde que temos uma derivac¸a˜o da fo´rmula
B sob a hipo´tese A. Ao aplicar esta regra, o contexto do consequente (A→ B) e´ alterado. Ele
conte´m todas as hipo´teses das derivac¸a˜o inicial de B menos todas as ocorreˆncias da hipo´tese
A. Neste caso, diga-se que a hipo´tese A foi descarregada. Formalmente, troca-se todas as
ocorreˆncias de A por [A]. Depois desta derivac¸a˜o, a hipo´tese A torna-se parte da conclusa˜o e
na˜o pode ser mais utilizada no resto da demonstrac¸a˜o.
As hipo´teses se dividem portanto em duas partes:
ˆ as hipo´teses principais: sa˜o conservadas ate´ o fim da derivac¸a˜o;
ˆ as hipo´tese auxiliares: sa˜o utilizadas para construir certas derivac¸o˜es e descarregas de
acordo.
Em deduc¸a˜o natural, uma derivac¸a˜o do consequente A sob as hipo´teses Γ e´ uma a´rvore cuja
conclusa˜o (raiz) e´ A e cujas hipo´teses principais esta˜o todas em Γ.
O conjunto das regras lo´gicas de infereˆncia e´ dado na Figura 1.
5
...
A
ax
A
...
A B
enfA
...
A→ B ...A →e
B
[A]
...
B →i
A→ B
...
A
...
B ∧i
A ∧B
...
A ∧B ∧re
A
...
A ∧B ∧le
B
...
A ∨riA ∨B
...
B ∨liA ∨B
...
A ∨B
[A]
...
C
[B]
...
C ∨e
C
[A]
...– ¬i¬A
[¬A]
...– ¬e
A
...
A
...¬A –i–
...– –e
A
Figura 1: Regras de introduc¸a˜o e eliminac¸a˜o dos conectivos em deduc¸a˜o natural.
Lema 2 (Idem lema 1.). ¬A↔ (A→ –)[A](1) [¬A](2) –i– →(1)iA→ – →(2)i¬A→ (A→ –)
[A→ –](3) [A](4) →e– ¬(4)i¬A →(3)i(A→ –)→ ¬A ∧i(A→ –)↔ ¬A
Para efeito de comparac¸a˜o, segue a prova com a notac¸a˜o de sequente:
ax¬A,A ⊢ A ax¬A,A ⊢ ¬A ¬e¬A,A ⊢ – →i¬A ⊢ A→ – →i⊢ ¬A→ (A→ –)
ax
A→ –,A ⊢ A axA→ –,A ⊢ A→ – →e
A→ –,A ⊢ – ¬i
A→ – ⊢ ¬A →i⊢ (A→ –)→ ¬A ∧i⊢ (A→ –)↔ ¬A
6
Lema 3. ⊢ ¬(A ∨B)↔ (¬A ∧ ¬B)
Prova do →:
[¬(A ∨B)](3) [A](1) ∨liA ∨B –i– ¬(1)i¬A
[¬(A ∨B)](3) [B](2) ∨riA ∨B –i– –(2)i¬B ∧i¬A ∧ ¬B →(3)i¬(A ∨B)→ (¬A ∧ ¬B)
Prova do ←:
[A ∨B](3) [A](1)
[¬A ∧ ¬B](4) ∧re¬A –i– [B](2)
[¬A ∧ ¬B](4) ∧le¬B –i– ∨(1,2)e– ¬(3)i¬(A ∨B) →(4)i(¬A ∧ ¬B)→ ¬(A ∨B)
Lema 4. ⊢ A→ ¬¬A [A](1) [¬A](2) –i– ¬(2)i¬¬A →(1)iA→ ¬¬A
Lema 5. ⊢ A ∨ ¬A [A](1) ∨i
A ∨ ¬A [¬(A ∨ ¬A)](2) –i– ¬(1)i¬A ∨i
A ∨ ¬A [¬(A ∨ ¬A)](2) –i– ¬(2)e
A ∨ ¬A
7