Sistema dedutivo
Um sistema dedutivo (também chamado de aparato dedutivo de um sistema formal) é constituído de axiomas e regras de inferência que podem ser usadas para derivar os teoremas do sistema.
Tal sistema dedutivo tem como propósito preservar certas qualidades dedutivas nas fórmulas que são expressas no sistema. Normalmente a qualidade na qual estamos preocupados é a verdade em oposição à falsidade. No entanto, outras modalidades, tais como justificação ou crença, podem ser preservadas alternativamente.
A fim de manter sua integridade dedutiva, um aparato dedutivo deve ser definido sem referência a nenhuma interpretação pretendida da linguagem. O objetivo é garantir que cada linha de uma derivação é meramente uma consequência formal de linhas que a precedem. Não deveria haver nenhum elemento pertencente a qualquer interpretação da linguagem envolvido na natureza dedutiva do sistema.
Dedução natural
[editar | editar código-fonte]A dedução natural é um sistema dedutivo que segue uma via formal e utiliza árvores de derivação. A dedução natural é formada de várias regras formais que são utlizadas para construir uma determinada árvore de derivação (este sistema dedutivo também é conhecido como sistema N [1] na lógica proposicional, e sistema N [1] na lógica de primeira ordem).