Dedução natural
De Wikipedia, a enciclopédia encyclopedia
Dedução natural é um dos sistemas dedutivos utilizados para construir demonstrações formais na Lógica. Foram introduzidos pela primeira vez, nos anos 30, por Gentzen. Para poder realizar uma derivação formal, é necessário formalizar a expressão que queremos demonstrar. Formalizar significa traduzir da forma linguística usual para uma notação lógica, uma forma que é entendível para qualquer um, independente da língua que fala, e que também reduz o espaço ocupado pela frase escrita, tendo em vista que podemos utilizar uma notação mais económica, a lógica.
Este artigo não cita fontes confiáveis. (Maio de 2016) |
Na notação formal utilizamos conectivos lógicos, operadores que realizam a ligação entre os átomos (os menores objetos). São eles:
- - Negação (não é um conectivo, simplesmente nega a fórmula ou átomo ligado)
- - Conjunção
- - Disjunção
- - Implicação
- - Bi-implicação
No caso da lógica clássica de primeira ordem, temos ainda os quantificadores:
- - Universal
- - Existencial
Também utilizamos alguns símbolos extras para auxiliar:
- - Derivação
- - Consequência semântica
- - Top (Verdade)
- - Bottom (Absurdo, falsidade)