Na lógica matemática, o cálculo proposicional implicacional é um fragmento do cálculo proposicional clássico (bivalente) que usa somente um conectivo, chamado de implicação ou condicional. Nas fórmulas, essa operação binária é indicada por "implica", "se ..., então ...", "
", etc.
A implicação e a completude funcional
A implicação sozinha não é funcionalmente completa porque não é possível definir todas as outras funções de verdade bivalentes a partir dela. Contudo, se houver uma proposição que sabemos ser falsa e usamos tal proposição como um conectivo 0-ário para a falsidade (bottom), então podemos definir todas as demais funções de verdade. Se P, Q e F são proposições, e sabe-se que F é falsa, então:
- ¬P é equivalente a P → F
- P ∧ Q é equivalente a (P → (Q → F)) → F
- P ∨ Q é equivalente a (P → F) → Q
- P ↔ Q é equivalente a ((P → Q) → ((Q → P) → F)) → F
Portanto, qualquer expressão lógica pode ser expressa usando-se “→” e F, sendo F uma proposição falsa.
Onde em cada caso, P, Q, R podem ser substituídos por qualquer proposição que contenha somente "→" como conectivo.
O primeiro passo é derivar o metateorema da dedução usando os axiomas 1, 2 e modus ponens. A seguir demonstraremos um teoremaesquemático (onde A e B podem ser substituídos por qualquer proposição que contenha somente "→" como conectivo):
- (A → ((B → A) → A)) → ((A → (B → A)) → (A → A)) axioma 2
- A → ((B → A) → A) axioma 1
- (A → (B → A)) → (A → A) modus ponens 2,1
- A → (B → A) axioma 1
- A → A modus ponens 4,3 QED
Procede-se a seguir como explicado no verbete teorema da dedução.
Substituição por uma proposição falsa
Se A e Z são proposições, então A → Z é equivalente a (¬A*) ∨ Z, onde A* é o resultado da substituição de todas, algumas ou nenhuma das ocorrências de Z em A por uma proposição falsa. De maneira semelhante, (A → Z) → Z é equivalente a A* ∨ Z. Então, dependendo das condições, podemos usar tais sentenças para dizer, respectivamente, que A* é falso ou que A* é verdadeiro.
Completude dos axiomas, parte 1
Veremos que os axiomas anteriores são completos no sentido de que qualquer tautologia que contém apenas 
como conectivo pode ser deduzida a partir deles. Considere uma tautologia S que contém apenas P1, P2, ..., Pn como variáveis proposicionais.
Escolha uma linha da tabela verdade para S. Ela mostra os valores de verdade (verdadeiro ou falso) assumidos por cada uma das subfórmulas de S para uma dada valoração. Por indução matemática sobre o comprimento das subfórmulas, mostraremos que a partir de proposições da forma Pk → Z (quando Pk recebe o valor falso) ou (Pk → Z) → Z (quando Pk recebe o valor verdadeiro) podemos deduzir proposições semelhantes para cada subfórmula de S. Isso requer o uso dos lemas abaixo.
Lema para uma conclusão verdadeira
Considere a subfórmula P → Q de S. Se Q recebe da valoração o valor verdadeiro, então P → Q receberá também o valor verdadeiro. Então precisamos mostrar que ((P → Q) → Z) → Z pode ser demonstrada a partir destas hipóteses sobre a valoração.
- (Q→Z)→Z 1. hipótese
- (P→Q)→Z 2. hipótese
- Q 3. hipótese
- P 4. hipótese
- Q 5. repetição do 3
- P→Q 6. dedução de 4 a 5
- Z 7. modus ponens 6,2
- Q→Z 8. dedução de 3 a 7
- Z 9. modus ponens 8,1
- ((P→Q)→Z)→Z 10. dedução de 2 a 9
- ((Q→Z)→Z)→(((P→Q)→Z)→Z) 11. dedução de 1 a 10
Lema para uma hipótese falsa
Se a valoração dá o valor falso para P, então P → Q receberá o valor verdadeiro. Então precisamos mostrar que ((P → Q) → Z) → Z pode ser demonstrado a partir destas hipóteses sobre a valoração.
- P→Z 1. hipótese
- (P→Q)→Z 2. hipótese
- Z→Q 3. hipótese
- P 4. hipótese
- Z 5. modus ponens 4,1
- Q 6. modus ponens 5,3
- P→Q 7. dedução de 4 a 6
- Z 8. modus ponens 7,2
- (Z→Q)→Z 9. dedução de 3 a 8
- ((Z→Q)→Z)→Z 10. Lei de Peirce
- Z 11. modus ponens 9,10
- ((P→Q)→Z)→Z 12. dedução de 2 a 11
- (P→Z)→((P→Q)→Z)→Z) 13. dedução de 1 a 12
Lema para uma hipótese verdadeira e uma conclusão falsa
Se P tem uma valoração verdadeira e Q tem uma valoração falsa, então P → Q terá valor falso. Então, devemos verificar que (P → Q) → Z pode ser demonstrada a partir destas hipóteses sobre a valoração.
- (P→Z)→Z 1. hipótese
- Q→Z 2. hipótese
- P→Q 3. hipótese
- P 4. hipótese
- Q 5. modus ponens 4,3
- Z 6. modus ponens 5,2
- P→Z 7. dedução de 4 a 6
- Z 8. modus ponens 7,1
- (P→Q)→Z 9. dedução de 3 a 8
- (Q→Z)→((P→Q)→Z) 10. dedução de 2 a 9
- ((P→Z)→Z)→[(Q→Z)→((P→Q)→Z)] 11. dedução de 1 a 10
Completude dos axiomas, parte 2
Na primeira parte da demonstração da completude, mostramos que (S → Z) → Z pode ser demonstrado para cada valoração da tautologia S, dadas hipóteses apropriadas sobre as variáveis proposicionais. Agora vamos combinar as valorações e eliminar estas hipóteses sobre as variáveis proposicionais.
Considere P como uma variável proposicional que ainda não foi eliminada das hipóteses. Usando o metateorema da dedução, obtemos (P → Z) → ((S → Z) → Z), e similarmente ((P → Z) → Z) → ((S → Z) → Z), ambos a partir de um conjunto de hipóteses no qual P não ocorre.
- (P→Z)→((S→Z)→Z) 1. hipótese
- ((P→Z)→Z)→((S→Z)→Z) 2. hipótese
- S→Z 3. hipótese
- P→Z 4. hipótese
- (S→Z)→Z 5. modus ponens 4,1
- Z 6. modus ponens 3,5
- (P→Z)→Z 7. dedução de 4 a 6
- (S→Z)→Z 8. modus ponens 7,2
- Z 9. modus ponens 3,8
- (S→Z)→Z 10. dedução de 3 a 9
- [((P→Z)→Z)→((S→Z)→Z)]→[(S→Z)→Z] 11. dedução de 2 a 10
- [(P→Z)→((S→Z)→Z)]→
([((P→Z)→Z)→((S→Z)→Z)]→[(S→Z)→Z]) 12. dedução de 1 a 11
Podemos então combinar pares de linhas da tabela verdade e repetir esse processo até que todas as hipóteses sobre os valores das variáveis proposicionais sejam eliminadas. O resultado será que teremos demonstrado ((S → Z) → Z), onde S é uma tautologia e Z é uma proposição qualquer. Escolhemos agora Z igual a S, donde (S → S) → S é um teorema sempre que S for uma tautologia. Mas, como foi demonstrado anteriormente, S → S. Por modus ponens, S é um teorema, para qualquer tautologia S. Portanto, o nosso conjunto de axiomas é completo.
Essa prova é construtiva. Isto é, dada uma tautologia e seguindo as instruções dadas acima, pode-se criar uma prova dela a partir dos axiomas tratados. Entretanto, o comprimento da prova aumenta de acordo com o número de variáveis proposicionais na tautologia. Portanto, não é um método prático para todas as tautologias, apenas para as mais curtas.
É interessante notar que a lei do terceiro excluído (na forma da Lei de Peirce, o axioma 3) aparece apenas uma vez na demonstração da completude (na demonstração do lema para uma hipótese falsa). Em contraste, a demonstração da completude no livro de Mendelson usa a lei do terceiro excluído em vários passos, especialmente no passo onde as linhas da tabela verdade são combinadas para eliminar a dependência das variáveis proposicionais. Mendelson usa seu terceiro axioma (¬A → ¬B) → ((¬A → B) → A) para derivar (A → B) → ((¬A → B) → B), uma formulação da lei do terceiro excluído, que é então usado para combinar as linhas da tabela de verdade.
Ver também
