Lista de sistemas dedutivos

Este artigo contém uma lista de exemplos de Sistemas de dedução ao estilo de Hilbert da lógica proposicional.

Sistemas de cálculo proposicional clássico

Cálculo proposicional clássico é o padrão da lógica proposicional. Sua semântica é bivalente e sua principal propriedade é que é sintaticamente completo, dizendo de outra maneira, não há um novo axioma que não seja consequência dos axiomas já existentes e podem ser adicionados sem fazer a lógica inconsistente. Muitos sistemas axiomáticos diferentes, porém equivalente a outros tem sido formulados. Eles diferem na escolha dos conectivos básicos utilizados, que em todos os casos têm de ser funcionalmente completos (i.e. aptos para expressar por composição todas n-árias tabelas verdade), e na escolha completa e exata de axiomas sobre a base de conectivos escolhida.

Implicação e negação

As formulações aqui usam a implicação e a negação $\{\to ,\neg \}$ como o conjunto funcionalmente completo de conectivos básicos. Todo sistema dedutivo requer pelo menos uma regra não nula de inferência. O cálculo proposicional clássico normalmente utiliza a regra de modus ponens:

$A,A\to B\vdash B.$

Esta regra esta inclusa em todos os sistemas abaixo, salvo indicação contrária.

Sistema axiomático de Frege:

$A\to (B\to A)$

$(A\to (B\to C))\to ((A\to B)\to (A\to C))$

$(A\to B)\to (\neg B\to \neg A)$

$\neg \neg A\to A$

$A\to \neg \neg A$

Sistema axiomático de Hilbert:

$A\to (B\to A)$

$(A\to (B\to C))\to (B\to (A\to C))$

$(B\to C)\to ((A\to B)\to (A\to C))$

$A\to (\neg A\to B)$

$(A\to B)\to ((\neg A\to B)\to B)$

Sistema axiomático de Łukasiewicz:

• Primeiro:

$(A\to B)\to ((B\to C)\to (A\to C))$

$(\neg A\to A)\to A$

$A\to (\neg A\to B)$

• Segundo:

$((A\to B)\to C)\to (\neg A\to C)$

$((A\to B)\to C)\to (B\to C)$

$(\neg A\to C)\to ((B\to C)\to ((A\to B)\to C))$

• Terceiro:

$A\to (B\to A)$

$(A\to (B\to C))\to ((A\to B)\to (A\to C))$

$(\neg A\to \neg B)\to (B\to A)$

• Quarto:

$(A\to B)\to ((B\to C)\to (A\to C))$

$A\to (\neg A\to B)$

$(\neg A\to B)\to ((B\to A)\to A)$

Sistema axiomático de Łukasiewicz e Tarski:

$[(A\to (B\to A))\to ([(\neg C\to (D\to \neg E))\to [(C\to (D\to F))\to ((E\to D)\to (E\to F))]]\to G)]\to (H\to G)$

Sistema axiomático de Meredith:

$((((A\to B)\to (\neg C\to \neg D))\to C)\to E)\to ((E\to A)\to (D\to A))$

Sistema axiomático de Mendelson:

$A\to (B\to A)$

$(A\to (B\to C))\to ((A\to B)\to (A\to C))$

$(\neg A\to \neg B)\to ((\neg A\to B)\to A)$

Sistema axiomático de Russell:

$A\to (B\to A)$

$(A\to B)\to ((B\to C)\to (A\to C))$

$(A\to (B\to C))\to (B\to (A\to C))$

$\neg \neg A\to A$

$(A\to \neg A)\to \neg A$

$(A\to \neg B)\to (B\to \neg A)$

Sistema axiomático de Sobociński:

• Primeiro:

$(A\to B)\to (\neg B\to (A\to C))$

$A\to (B\to (C\to A))$

$(\neg A\to B)\to ((A\to B)\to B)$

• Segundo:

$\neg A\to (A\to B)$

$A\to (B\to (C\to A))$

$(\neg A\to C)\to ((B\to C)\to ((A\to B)\to C))$

Implicação e falsum

Ao invés da negação, a lógica clássica também pode ser formulada usando o conjunto funcionalmente completo $\{\to ,\bot \}$ de conectivos.

Sistema axiomático de Tarski–Bernays–Wajsberg:

$(A\to B)\to ((B\to C)\to (A\to C))$

$A\to (B\to A)$

$((A\to B)\to A)\to A$

$\bot \to A$

Sistema axiomático de Church:

$A\to (B\to A)$

$(A\to (B\to C))\to ((A\to B)\to (A\to C))$

$((A\to \bot )\to \bot )\to A$

Sistema axiomático de Meredith:

• Primeiro:

$((((A\to B)\to (C\to \bot ))\to D)\to E)\to ((E\to A)\to (C\to A))$

• Segundo:

$((A\to B)\to ((\bot \to C)\to D))\to ((D\to A)\to (E\to (F\to A)))$

Negação e disjunção

Ao invés da implicação, a lógica clássica também pode ser formulada usando o conjunto funcionalmente completo $\{\neg ,\lor \}$ de conectivos. Estas formulações usam as seguintes regras de inferência;

$A,\neg A\lor B\vdash B.$

Sistema axiomático de Russell–Bernays:

$\neg (\neg B\lor C)\lor (\neg (A\lor B)\lor (A\lor C))$

$\neg (A\lor B)\lor (B\lor A)$

$\neg A\lor (B\lor A)$

$\neg (A\lor A)\lor A$

Sistema axiomático de Meredith:

• Primeiro:

$\neg (\neg (\neg A\lor B)\lor (C\lor (D\lor E)))\lor (\neg (\neg D\lor A)\lor (C\lor (E\lor A)))$

• Segundo:

$\neg (\neg (\neg A\lor B)\lor (C\lor (D\lor E)))\lor (\neg (\neg E\lor D)\lor (C\lor (A\lor D)))$

• Terceiro:

$\neg (\neg (\neg A\lor B)\lor (C\lor (D\lor E)))\lor (\neg (\neg C\lor A)\lor (E\lor (D\lor A)))$

Dualmente, a lógica proposicional pode ser definida usando apenas conjunção e negação.

Conectivo de Sheffer

Pela razão de o conectivo de Sheffer (também conhecido como operador NAND) ser funcionalmente completo, ele pode ser usado para criar qualquer formulação do cálculo proposicional. As formulações NAND usam uma regra de inferência chamada modus ponens de Nicod:

$A,A\mid (B\mid C)\vdash C.$

Sistema axiomático de Nicod:

$(A\mid (B\mid C))\mid [(E\mid (E\mid E))\mid ((D\mid B)\mid [(A\mid D)\mid (A\mid D)])]$

Sistema axiomático de Łukasiewicz:

• Primeiro:

$(A\mid (B\mid C))\mid [(D\mid (D\mid D))\mid ((D\mid B)\mid [(A\mid D)\mid (A\mid D)])]$

• Segundo:

$(A\mid (B\mid C))\mid [(A\mid (C\mid A))\mid ((D\mid B)\mid [(A\mid D)\mid (A\mid D)])]$

Sistema axiomático de Wajsberg:

$(A\mid (B\mid C))\mid [((D\mid C)\mid [(A\mid D)\mid (A\mid D)])\mid (A\mid (A\mid B))]$

Sistema axiomático de Argonne:

• Primeiro:

$(A\mid (B\mid C))\mid [(A\mid (B\mid C))\mid ((D\mid C)\mid [(C\mid D)\mid (A\mid D)])]$

• Segundo:

$(A\mid (B\mid C))\mid [([(B\mid D)\mid (A\mid D)]\mid (D\mid B))\mid ((C\mid B)\mid A)]$

Uma análise computadorizada por Argonne tem revelado > 60 sistemas de um único axioma que podem ser usados para formular cálculos proposicionais com NAND .

Cálculo proposicional implicacional

O cálculo proposicional implicacional é o fragmento do cálculo proposicional clássico que somente admite o conectivo de implicação. Ele não é funcionalmente completo (pela razão de que ele carece da capacidade de expressar uma falsidade e negação) mas é, entretanto, sintaticamente completo. Os cálculos implicacionais abaixo usam modus ponens como uma regra de inferência.

Sistema axiomático de Bernays–Tarski:

$A\to (B\to A)$

$(A\to B)\to ((B\to C)\to (A\to C))$

$((A\to B)\to A)\to A$

Sistema axiomático de Łukasiewicz e Tarski:

• Primeiro:

$[(A\to (B\to A))\to [([((C\to D)\to E)\to F]\to [(D\to F)\to (C\to F)])\to G]]\to G$

• Segundo:

$[(A\to B)\to ((C\to D)\to E)]\to ([F\to ((C\to D)\to E)]\to [(A\to F)\to (D\to E)])$

• Terceiro:

$((A\to B)\to (C\to D))\to (E\to ((D\to A)\to (C\to A)))$

• Quarto:

$((A\to B)\to (C\to D))\to ((D\to A)\to (E\to (C\to A)))$

Sistema axiomático de Łukasiewicz:

$((A\to B)\to C)\to ((C\to A)\to (D\to A))$

Lógica intuicionística e intermediária

A lógica intuicionística é um subsistema da lógica clássica. Ela é comumente formulada com $\{\to ,\land ,\lor ,\bot \}$ como o conjunto de conectivos básicos (funcionalmente completo). A lógica intuicionista não é sintaticamente completa já que ela carece da lei do terceiro excluído A∨¬A ou lei de Peirce ((A→B)→A)→A que pode ser adicionado, fazendo a lógica inconsistente. Ela adere modus ponens como regra de inferência, e os seguintes axiomas:

$A\to (B\to A)$

$(A\to (B\to C))\to ((A\to B)\to (A\to C))$

$(A\land B)\to A$

$(A\land B)\to B$

$A\to (B\to (A\land B))$

$A\to (A\lor B)$

$B\to (A\lor B)$

$(A\to C)\to ((B\to C)\to ((A\lor B)\to C))$

$\bot \to A$

Alternativamente, a lógica intuicionista pode ser axiomatizada usando$\{\to ,\land ,\lor ,\neg \}$ como o conjunto básico de conectivos, substituindo o último axioma com

$(A\to \neg A)\to \neg A$

$\neg A\to (A\to B)$

As lógicas intermediárias estão entre a intuicionista e clássica. Aqui estão algumas lógicas intermediárias:

• Lógica de Jankov (KC, em inglês Jankov Logic) é uma extensão da logica intuicionista is que pode ser axiomatizada pelo sistema axiomático intuicionista mais o axioma

$\neg A\lor \neg \neg A.$

• Lógica de Gödel–Dummett (LC, em inglês Gödel–Dummett Logic) pode ser axiomatizada sobre a lógica intuicionística pela adição do axioma

$(A\to B)\lor (B\to A).$

Cálculo implicacional positivo

O cálculo implicacional positivo é o fragmento implicacional da lógica intuicionista. Os cálculos abaixo usam modus ponens como uma regra de inferência.

Sistema axiomático de Łukasiewicz:

$A\to (B\to A)$

$(A\to (B\to C))\to ((A\to B)\to (A\to C))$

Sistema axiomático de Meredith:

• Primeiro:

$E\to ((A\to B)\to (((D\to A)\to (B\to C))\to (A\to C)))$

• Segundo:

$A\to (B\to A)$

$(A\to B)\to ((A\to (B\to C))\to (A\to C))$

• Terceiro:

$((A\to B)\to C)\to (D\to ((B\to (C\to E))\to (B\to E)))$

Sistema axiomático de Hilbert:

• Primeiro:

$(A\to (A\to B))\to (A\to B)$

$(B\to C)\to ((A\to B)\to (A\to C))$

$(A\to (B\to C))\to (B\to (A\to C))$

$A\to (B\to A)$

• Segundo:

$(A\to (A\to B))\to (A\to B)$

$(A\to B)\to ((B\to C)\to (A\to C))$

$A\to (B\to A)$

• Terceiro:

$A\to A$

$(A\to B)\to ((B\to C)\to (A\to C))$

$(B\to C)\to ((A\to B)\to (A\to C))$

$(A\to (A\to B))\to (A\to B)$

Cálculo proposicional positivo

O cálculo proposicional positivo é o fragmento da lógica intuicionística que usa apenas os conectivos $\{\to ,\land ,\lor \}$ (não é funcionalmente completo). Ele pode ser axiomatizado por qualquer um dos cálculos mencionados acima; para o cálculo implicacional positivo é necessário adicionar os axiomas

$(A\land B)\to A$

$(A\land B)\to B$

$A\to (B\to (A\land B))$

$A\to (A\lor B)$

$B\to (A\lor B)$

$(A\to C)\to ((B\to C)\to ((A\lor B)\to C))$

Opcionalmente, nós podemos também incluir o conectivo $\leftrightarrow$ e os axiomas

$(A\leftrightarrow B)\to (A\to B)$

$(A\leftrightarrow B)\to (B\to A)$

$(A\to B)\to ((B\to A)\to (A\leftrightarrow B))$

A lógica minimal de Johansson pode ser axiomatizada por qualquer dos sistemas axiomáticos para o cálculo proposicional positivo e expandindo sua linguagem com o conectivo nulo $\bot$, sem adicionar esquemas axiomáticos. Alternativamente, ele pode também ser axiomatizado sob a linguagem $\{\to ,\land ,\lor ,\neg \}$ pela expansão do cálculo proposicional positivo com o axioma

$(A\to \neg B)\to (B\to \neg A)$

ou com o par de axiomas

$(A\to B)\to (\neg B\to \neg A)$

$A\to \neg \neg A$

A lógica intuicionística sob a linguagem com negação pode ser axiomatizada sobre o cálculo positivo pelo par de axiomas

$(A\to \neg B)\to (B\to \neg A)$

$\neg A\to (A\to B)$

ou pelo par

$(A\to \neg A)\to \neg A$

$\neg A\to (A\to B)$

A lógica clássica sob a linguagem $\{\to ,\land ,\lor ,\neg \}$ pode ser otido através do cálculo proposicional positivo adicionando o axioma

$(\neg A\to \neg B)\to (B\to A)$

ou o par de axiomas

$(A\to \neg B)\to (B\to \neg A)$

$\neg \neg A\to A$

O cálculo Fitch leva qualquer dos sistemas axiomáticos para o cálculo proposicional positivo e adiciona os axiomas 

$\neg A\to (A\to B)$

$A\leftrightarrow \neg \neg A$

$\neg (A\lor B)\leftrightarrow (\neg A\land \neg B)$

$\neg (A\land B)\leftrightarrow (\neg A\lor \neg B)$

Note que o primeiro e terceiro axiomas também são válidos na lógica intuicionística.

Cálculo de equivalência

Cálculo de equivalência é um subsistema do cálculo proposicional clássico que somente permite o (funcionalmente incompleto) conectivo de equivalência, aqui denotado como $\equiv$. A regra de inferência usada nestes sistemas é a seguinte:

$A,A\equiv B\vdash B$

Sistema axiomático de Iséki:

$((A\equiv C)\equiv (B\equiv A))\equiv (C\equiv B)$

$(A\equiv (B\equiv C))\equiv ((A\equiv B)\equiv C)$

Sistema axiomático de Iséki–Arai:

$A\equiv A$

$(A\equiv B)\equiv (B\equiv A)$

$(A\equiv B)\equiv ((B\equiv C)\equiv (A\equiv C))$

Sistema axiomático de Arai:

• Primeiro:

$(A\equiv (B\equiv C))\equiv ((A\equiv B)\equiv C)$

$((A\equiv C)\equiv (B\equiv A))\equiv (C\equiv B)$

• Segundo:

$(A\equiv B)\equiv (B\equiv A)$

$((A\equiv C)\equiv (B\equiv A))\equiv (C\equiv B)$

Sistema axiomático de Łukasiewicz:

• Primeiro:

$(A\equiv B)\equiv ((C\equiv B)\equiv (A\equiv C))$

• Segundo:

$(A\equiv B)\equiv ((A\equiv C)\equiv (C\equiv B))$

• Terceiro:

$(A\equiv B)\equiv ((C\equiv A)\equiv (B\equiv C))$

Sistema axiomático de Meredith:

• Primeiro:

$((A\equiv B)\equiv C)\equiv (B\equiv (C\equiv A))$

• Segundo:

$A\equiv ((B\equiv (A\equiv C))\equiv (C\equiv B))$

• Terceiro:

$(A\equiv (B\equiv C))\equiv (C\equiv (A\equiv B))$

• Quarto:

$(A\equiv B)\equiv (C\equiv ((B\equiv C)\equiv A))$

• Quinto:

$(A\equiv B)\equiv (C\equiv ((C\equiv B)\equiv A))$

• Sexto:

$((A\equiv (B\equiv C))\equiv C)\equiv (B\equiv A)$

• Sétimo:

$((A\equiv (B\equiv C))\equiv B)\equiv (C\equiv A)$

Sistema axiomático de Kalman:

$A\equiv ((B\equiv (C\equiv A))\equiv (C\equiv B))$

Sistema axiomático de Winker:

• Primeiro:

$A\equiv ((B\equiv C)\equiv ((A\equiv C)\equiv B))$

• Segundo:

$A\equiv ((B\equiv C)\equiv ((C\equiv A)\equiv B))$

Sistema axiomático XCB:

$A\equiv (((A\equiv B)\equiv (C\equiv B))\equiv C)$