1.4.1. Exemplos🔗

Cada equivalência abaixo é verificada por uma tabela-verdade. Duas proposições são equivalentes quando as suas colunas finais coincidem em toda linha, e uma tautologia tem uma coluna verdadeira em toda linha.

Exemplo 1. A dupla negação devolve a proposição original, verificada na Tabela 1.4.3.

Tabela 1.4.3. Tabela-verdade de ¬¬P ≡ P.

Exemplo 2. O terceiro excluído P ∨ ¬P é uma tautologia, verificada na Tabela 1.4.4.

Tabela 1.4.4. Tabela-verdade de P ∨ ¬P.

Exemplo 3. A não contradição ¬(P ∧ ¬P) é uma tautologia, verificada na Tabela 1.4.5.

Tabela 1.4.5. Tabela-verdade de ¬(P ∧ ¬P).

Exemplo 4. A primeira lei de De Morgan, verificada na Tabela 1.4.6.

Tabela 1.4.6. Tabela-verdade de ¬(P ∧ Q) ≡ ¬P ∨ ¬Q.

Exemplo 5. A disjunção comuta, verificada na Tabela 1.4.7.

Tabela 1.4.7. Tabela-verdade de P ∨ Q ≡ Q ∨ P.

Exemplo 6. A disjunção é idempotente, verificada na Tabela 1.4.8.

Tabela 1.4.8. Tabela-verdade de P ∨ P ≡ P.

Exemplo 7. A contrapositiva, verificada na Tabela 1.4.9.

Tabela 1.4.9. Tabela-verdade de P → Q ≡ ¬Q → ¬P.

Exemplo 8. A implicação material, verificada na Tabela 1.4.10.

Tabela 1.4.10. Tabela-verdade de P → Q ≡ ¬P ∨ Q.

Exemplo 9. O bicondicional é a conjunção das suas duas implicações, verificada na Tabela 1.4.11.

Tabela 1.4.11. Tabela-verdade de P ↔ Q ≡ (P → Q) ∧ (Q → P).

Exemplo 10. A negação de uma implicação, verificada na Tabela 1.4.12.

Tabela 1.4.12. Tabela-verdade de ¬(P → Q) ≡ P ∧ ¬Q.

1.4.2. Cálculos Lógicos🔗

Tabelas-verdade decidem qualquer questão proposicional, mas o seu tamanho cresce exponencialmente no número de variáveis, e elas não se estendem aos quantificadores da Aula 2. Um cálculo responde às mesmas questões por derivação, e não por computação.

Um cálculo fixa um conjunto de axiomas, que são proposições tomadas como dadas, e um conjunto de regras de inferência, cada uma das quais produz uma proposição a partir de proposições já derivadas. Uma derivação é uma sequência finita de aplicações de regras, e uma proposição que encerra uma derivação é um teorema do cálculo. Valorações não participam disso. Uma derivação reescreve símbolos apenas segundo as regras, e é isso que permite a uma máquina verificá-la.

Duas propriedades ligam um cálculo à semântica das seções anteriores. Um cálculo é correto quando todo teorema é uma tautologia, e completo quando toda tautologia é um teorema. Post provou as duas para o cálculo proposicional em 1921, no artigo que também introduziu o método das tabelas-verdade.E. L. Post, Introduction to a General Theory of Elementary Propositions, American Journal of Mathematics 43, 1921, pp. 163–185.

A lógica proposicional admite vários cálculos, e eles diferem na forma das suas regras, não nos teoremas que provam.

Um cálculo axiomático, no estilo de Hilbert e Ackermann,D. Hilbert e W. Ackermann, Grundzüge der theoretischen Logik, Julius Springer, Berlim, 1928. tem muitos axiomas e uma regra. O sistema de Łukasiewicz e Tarski precisa de três esquemas de axioma sobre → e ¬, com o modus ponens como única regra.J. Łukasiewicz e A. Tarski, Untersuchungen über den Aussagenkalkül, Comptes Rendus des Séances de la Société des Sciences et des Lettres de Varsovie, Classe III, 23, 1930, pp. 30–50.

  A → (B → A)
  (A → (B → C)) → ((A → B) → (A → C))
  (¬A → ¬B) → (B → A)

Cada esquema representa toda proposição da sua forma, então P → (Q → P) e (P ∧ Q) → (R → (P ∧ Q)) são instâncias do primeiro. Derivar um teorema tão simples quanto P → P leva cinco passos aqui, e encontrar os passos é uma arte.

A resolução vai ao outro extremo, com uma única regra sobre proposições escritas como cláusulas, e é com ela que provadores automáticos buscam.J. A. Robinson, A Machine-Oriented Logic Based on the Resolution Principle, Journal of the ACM 12(1), 1965, pp. 23–41.

A dedução natural fica entre os dois. Ela não tem axiomas e tem duas regras para cada conectivo, uma que introduz o conectivo e outra que o elimina, e as suas derivações podem repousar sobre suposições que uma regra posterior descarta. Gentzen a projetou para seguir os passos que um matemático de fato dá.G. Gentzen, Untersuchungen über das logische Schließen. I, Mathematische Zeitschrift 39, 1935, pp. 176–210. O cálculo de sequentes, do mesmo artigo, carrega as suposições explicitamente à esquerda do símbolo ⊢ e serve a argumentos de teoria da prova.

1.4.3. O Cálculo desta Disciplina🔗

Esta disciplina usa dedução natural. As suas regras de introdução e eliminação são as que as táticas de Lean implementam, e um termo de prova em Lean corresponde a uma das suas derivações. A próxima seção apresenta as regras, e o restante da aula desenvolve as provas correspondentes em Lean.