Sejam φ, χ e ψ símbolos para fórmulas bem formadas. (As fbfs em si não contém nenhuma letra grega, mas somente letras romanas maiúsculas, operadores conectivos, e parênteses.) Então, os axiomas são os seguintes:
| Axiomas | ||
| Nome | Esquema Axiomático | Descrição |
| ENTÃO-1 | φ → (χ → φ) | Adiciona a hipótese χ |
| ENTÃO-2 | (φ → (χ → ψ)) → ((φ → χ) → (φ → ψ)) | Distribui a hipótese φ |
| E-1 | φ ∧ χ → φ | Eliminação da conjunção |
| E-2 | φ ∧ χ → χ | Eliminação da conjunção 2 |
| E-3 | φ → (χ → (φ ∧ χ)) | Introdução da conjunção |
| OU-1 | φ → φ ∨ χ | Introdução da disjunção 2 |
| OU-2 | χ → φ ∨ χ | Introdução da disjunção |
| OU-3 | (φ → ψ) → ((χ → ψ) → (φ ∨ χ → ψ)) | Eliminação da disjunção |
| NÃO-1 | (φ → χ) → ((φ → ¬χ) → ¬ φ) | Introdução da negação |
| NÃO-2 | φ → (¬φ → χ) | Eliminação da negação |
| NÃO-3 | φ ∨ ¬φ | Lei do terceiro excluído |
| SSE-1 | (φ ↔ χ) → (φ → χ) | Eliminação da equivalência |
| SSE-2 | (φ ↔ χ) → (χ → φ) | Eliminação da equivalência 2 |
| SSE-3 | (φ → χ) → ((χ → φ) → (φ ↔ χ)) | Introdução da equivalência |
- O axioma ENTÃO-2 pode ser considerado como sendo uma "propriedade distributiva da implicação com relação à implicação."
- Os axiomas E-1 e E-2 correspondem à "eliminação da conjunção". A relação entre E-1 e E-2 reflete a comutatividade do operador da conjunção.
- O axioma E-3 corresponde à "introdução da conjunção."
- Os axiomas OU-1 e OU-2 correspondem à "introdução da disjunção." A relação entre OU-1 e OU-2 reflete a comutatividade do operador da disjunção.
- O axioma NÃO-1 corresponde à "redução ao absurdo."
- O axioma NÃO-2 diz que "tudo pode ser deduzido a partir da contradição."
- O axioma NÃO-3 é chamado "tertium non datur" (Latin: "não há uma terceira opção") e reflete a valoração semântica da fórmula proposicional: uma fórmula pode ter um valor de verdade verdadeiro ou falso. Não há um terceiro valor de verdade, pelo menos não na lógica clássica.
Nenhum comentário:
Postar um comentário