Sistema Dedutivo de Dedução Natural

Sistema Dedutivo de Dedução Natural

Este sistema dedutivo é bastante natural, pois reflete o raciocínio usado nas demonstrações informais em matemática ou em qualquer outro argumento lógico informal.  

        Para cada um dos símbolos lógicos existem duas regras, uma que introdução e outra de eliminação. As regras de introdução de conectivos inferem fórmulas cujo conectivo principal é aquele (por exemplo, a regra de introdução de ∧ infere uma fórmula cujo conectivo principal é ∧), já as de eliminação de um conectivo, partem de fórmulas com aquele  conectivo.Vamos representar a regra "de α e β infira γ " por α , β

                                                                               γ

                                                                                        

Regras de inferência :

        

IP        α

        α

Introdução                                                Eliminação

I∧                                                        E∧

        α,   β _                                                         α ∧ β _        α ∧ β

        α ∧ β                                                                 α                    β

I∨                                                        E∨

            α  .                   β   .                                                [α]                [β]

        α ∨ β                 α ∨ β                                                   .                  .

                                                                          .                   .

                                                         α ∨ β _         χ                 χ

                                                                                 χ

I¬                                                        E¬1                         E¬2

         [α]                [α]                                ¬α,  α _                [¬α]

           .                  .                                     β                           .

           .                  .                                                           .

           β                ¬β _                                                           α        

                 ¬α                                                                    α

I →                                                          E→

          [α]                                                α → β,   α

            .                                                        β

            .                

             β        

         α → β

I↔                                                  E↔

         α → β,  β → α _                                α ↔ β _                α ↔ β

                α ↔ β                                 α → β                 β → α

Chamamos de hipóteses (conclusões) da regra as fórmulas que ocorrem acima (abaixo) do travessão. Em algumas regras não temos simplesmente fórmulas acima do travessão, mas derivações, por exemplo,  regras I → e I¬. Nestas regras, as fórmulas entre []’s são hipóteses usadas (localmente) naquelas  derivações e não são consideradas como hipóteses das regras. Estas hipóteses entre parênteses são ditas "descarregadas".

Assim, na representação em forma de lista, uma prova de β a partir de um conjunto de premissas  Γ é uma seqüência finita de fórmulas  ρ1, ρ2, ρ3, ... , ρm tal que ρm é β e cada i=1…m, ρi∈Γ ou é obtido pela aplicação de uma regra de inferência a ρj's com j