Sistemas Dedutivos

Um sistema dedutivo é uma tripla (linguagem, axiomas, regras de inferência). Γ ⊢ φ significa que existe uma derivação finita de φ a partir de Γ: cada linha é premissa, instância de axioma, ou conclusão de uma regra.

Derivações, solidez e completude deste tópico — e compacidade, decidibilidade e lógicas não clássicas nos seguintes — partem dessa tripla e da relação ⊢.

As páginas se agrupam em quatro blocos. O primeiro define quando uma sequência de fórmulas conta como prova.

O segundo testa ⊢ e ⊨: conferir a derivação linha a linha, ou procurar um contra-modelo.

O terceiro escreve a prova: por esquemas e modus ponens; por introdução e eliminação com hipóteses descarregadas; ou por sequentes Γ ⇒ Δ.

O quarto compara ⊢ com ⊨ nos dois sentidos: indução na derivação; construção de Henkin.

Sistemas de Hilbert constrói P→P com os esquemas 1 e 2 e dois modus ponens, sem descarregar hipótese. Dedução Natural assume P, copia a hipótese e descarrega para P→P.

De A→B e ¬B inferir ¬A, ou de A∨B e ¬A inferir B, está em Dedução Natural. Introduzir o conectivo à esquerda ou à direita do sequente Γ ⇒ Δ está em Cálculo dos Sequentes.

Decidir Γ ⊨ φ pela tabela de valorações está em Consequência. Concluir Γ ⊢ φ a partir da ausência de contra-modelo está em Completude.

Solidez lê a derivação e conclui Γ ⊨ φ; acrescentar o axioma P(c) deixa o sistema consistente e não sólido. Completude garante Γ ⊢ φ a partir de Γ ⊨ φ e, em primeira ordem, esboça testemunhas de Henkin.