Axioma lógico

O método axiomático torna possível definir o conjunto de leis lógicas de primeira ordem a partir de axiomas lógicos e regras de dedução de tal forma que todas as leis lógicas sejam um axioma ou uma fórmula derivada dos axiomas com um número finito de regras de dedução.

Esta apresentação, puramente sintática, equivale à apresentação semântica da teoria dos modelos , que permite definir uma lei lógica como uma fórmula verdadeira em todos os mundos possíveis. Essa equivalência é o assunto de um teorema da completude .

Os axiomas lógicos de Principia Mathematica

As leis lógicas são obtidas dentro do sistema de Whitehead e Russell (1910) a partir de seis esquemas de axiomas e duas regras de dedução, a regra de desprendimento e a regra de generalização.

Diagramas de axioma

Esses esquemas de axiomas são os seguintes. p, q e r podem ser substituídos por quaisquer fórmulas (com ou sem variáveis livres) do cálculo de predicados de primeira ordem.

if (p ou p) então p: ${\ displaystyle (P \ lor P) \ Rightarrow P}$

se p então (p ou q): ${\ displaystyle P \ Rightarrow (P \ lor Q)}$

if (p ou q) then (q ou p): ${\ displaystyle (P \ lor Q) \ Rightarrow (Q \ lor P)}$

if (if p then q) then (if (p or r) then (q or r)): ${\ displaystyle (P \ Rightarrow Q) \ Rightarrow ((P \ lor R) \ Rightarrow (Q \ lor R))}$

if (todo x é tal que p) então p ': ${\ displaystyle (\ forall x, p (x)) \ Rightarrow p '}$

onde p 'é obtido de p substituindo uma variável não ligada y em p para todas as ocorrências livres de x em p.

if (todo x é tal que (p ou q)) então (p ou todo x é tal que q): ${\ displaystyle (\ forall x, (p \ lor q (x))) \ Rightarrow (p \ lor (\ forall x, q (x)))}$

onde p é uma fórmula que não contém x como uma variável livre

As duas regras de dedução

A regra de desprendimento ou modus ponens diz que das duas premissas pe (se p então q) podemos deduzir q.

A regra de generalização diz que a partir da premissa única p podemos deduzir (todo x é tal que p)

Equivalência com dedução natural

Podemos provar que todas as verdades hipotéticas, no sentido de dedução natural, são axiomas obtidos a partir desses diagramas ou consequências que podem ser deduzidas em um número finito de etapas a partir desses axiomas, com as duas regras de dedução.

Todas as provas que podem ser formalizadas na dedução natural podem ser formalizadas no cálculo lógico (primeira ordem) de Whitehead e Russell e vice-versa.

Completude do sistema

Gödel provou um teorema da completude que afirma que esses seis esquemas de axiomas e essas duas regras de dedução são suficientes para obter todas as leis lógicas.