1.5. Dedução Natural
A dedução natural deriva uma proposição a partir de suposições por regras que espelham o modo como matemáticos argumentam. Dag Prawitz deu ao sistema o seu estudo teórico-demonstrativo.D. Prawitz, Natural Deduction: A Proof-Theoretical Study, Almqvist & Wiksell, Stockholm, 1965. Cada regra tem zero ou mais premissas acima de uma linha horizontal e uma conclusão abaixo dela, e lê-se como segue. Dadas derivações das premissas, a linha licencia a conclusão.
Uma derivação apoia-se em suposições. Algumas regras descartam uma suposição, então uma proposição suposta no topo de uma subderivação deixa de contar como suposição aberta assim que a regra dispara. Marcamos uma suposição descartada com colchetes, como [P], e escrevemos um ⋮ vertical para a derivação interveniente. Uma proposição provada sem suposições abertas é um teorema.
Cada conectivo vem com regras de introdução, que provam uma proposição daquela forma, e regras de eliminação, que usam uma proposição daquela forma. Essa disciplina de introdução e eliminação é exatamente a estrutura que as táticas de Lean seguem na próxima seção.
1.5.1. Implicação
Para introduzir P → Q, suponha P, derive Q e descarte a suposição. Para eliminá-la, aplique uma implicação a uma prova do seu antecedente, a regra de modus ponens.
[P]
⋮
Q P → Q P
─────── →I ───────────── →E
P → Q Q
1.5.2. Conjunção
Para introduzir P ∧ Q, prove as duas partes. A eliminação projeta qualquer uma delas.
P Q P ∧ Q P ∧ Q ─────── ∧I ─────── ∧E₁ ─────── ∧E₂ P ∧ Q P Q
1.5.3. Disjunção
Para introduzir P ∨ Q, prove um disjunto. Para eliminá-la, prove uma conclusão comum R a partir de cada disjunto por vez, descartando o disjunto suposto em cada ramo.
P Q [P] [Q]
─────── ∨I₁ ─────── ∨I₂ P ∨ Q ⋮ ⋮
P ∨ Q P ∨ Q R R
────────────────────────── ∨E
R
1.5.4. Negação e Falsidade
A constante ⊥ é o absurdo, a proposição sem regra de introdução. A negação abrevia ¬P como P → ⊥, então as regras da negação são as regras da implicação lidas em ⊥. Para introduzir ¬P, suponha P, derive ⊥ e descarte a suposição. Para eliminá-la, uma prova de P e uma prova de ¬P juntas produzem ⊥. A partir de ⊥, a eliminação prova qualquer proposição C, o princípio ex falso quodlibet.
[P]
⋮
⊥ P ¬P ⊥
─────── ¬I ───────── ¬E ───── ⊥E
¬P ⊥ C
1.5.5. Regras Construtivas e Clássicas
As regras acima são construtivas, então uma derivação de uma disjunção exibe qual disjunto vale e uma derivação de um existencial exibe uma testemunha. Elas não provam a lei do terceiro excluído P ∨ ¬P nem reduzem uma dupla negação ¬¬P a P. A dedução natural clássica acrescenta mais uma regra, equivalentemente o terceiro excluído ou a reductio ad absurdum, que descarta a suposição ¬P ao derivar ⊥.
[¬P]
⋮
⊥
───────── RAA ─────────── EM
P P ∨ ¬P
A lei de De Morgan ¬(P ∧ Q) ≡ ¬P ∨ ¬Q e a lei de Peirce dependem dessa regra, como as provas em Lean abaixo tornam precisas.
1.5.6. Exemplos
As derivações abaixo provam teoremas proposicionais com as regras acima. Um numeral marca cada suposição descartada junto com a regra que a descarta, e cada árvore lê-se das folhas até a raiz.
Exemplo 1. A implicação é reflexiva.
[P]¹ ────── →I,¹ P → P
Exemplo 2. Uma conjunção implica cada uma das suas partes.
[P ∧ Q]¹
────────── ∧E₁
P
──────────── →I,¹
P ∧ Q → P
Exemplo 3. Um disjunto implica a disjunção.
[P]¹
──────── ∨I₁
P ∨ Q
──────────── →I,¹
P → P ∨ Q
Exemplo 4. Qualquer coisa decorre do absurdo, o princípio ex falso quodlibet.
[⊥]¹
────── ⊥E
P
──────── →I,¹
⊥ → P
Exemplo 5. Modus ponens, empacotado como uma única implicação.
[(P→Q)∧P]¹ [(P→Q)∧P]¹
───────────── ∧E₁ ───────────── ∧E₂
P → Q P
───────────────────────────── →E
Q
─────────────────────────────────── →I,¹
(P → Q) ∧ P → Q
Exemplo 6. A disjunção comuta.
[P]² [Q]²
[P ∨ Q]¹ ─────── ∨I₂ ─────── ∨I₁
Q ∨ P Q ∨ P
────────────────────────────────────── ∨E,²
Q ∨ P
─────────────────────── →I,¹
P ∨ Q → Q ∨ P
Exemplo 7. Introdução da dupla negação.
[¬P]² [P]¹
────────────── ¬E
⊥
────────── ¬I,²
¬¬P
────────────── →I,¹
P → ¬¬P
Exemplo 8. Contraposição.
[P→Q]¹ [P]³
[¬Q]² ─────────────── →E
Q
────────────────────── ¬E
⊥
──────────── ¬I,³
¬P
───────────────── →I,²
¬Q → ¬P
──────────────────────────── →I,¹
(P → Q) → (¬Q → ¬P)
Exemplo 9. Eliminação da dupla negação, que requer a regra clássica.
[¬P]² [¬¬P]¹
──────────────── ¬E
⊥
─────────── RAA,²
P
─────────────── →I,¹
¬¬P → P
Exemplo 10. O currying transforma uma hipótese conjuntiva em implicações aninhadas.
[P]² [Q]³
[P∧Q→R]¹ ──────────── ∧I
P ∧ Q
────────────────────────── →E
R
─────────── →I,³
Q → R
───────────────── →I,²
P → (Q → R)
───────────────────────────────── →I,¹
(P ∧ Q → R) → (P → (Q → R))