Dedução nat

I – Dedução Natural
Existem muitos métodos que servem de procedimentos de dedução (provas, derivação, demonstração). A escolha de um desses métodos deve ter em conta diversas características como por exemplo a simplicidade de execução. O método mais usado pelos lógicos desde a criação da lógica formal, e por um longo período de tempo foi o método axiomático. Talvez se possa justificar esta situação pelo facto de que muitos dos lógicos e matemáticos até 1931 trabalhavam no projeto proposto por David Hilbert, que pretendia provar que a matemática podia reduzir-se a um conjunto finito, completo e consistente, de axiomas. Com isto, o desenvolvimento de outros métodos de dedução não estava na agenda dos lógicos desse período.
Contudo, algumas descobertas fizeram com que o projeto de Hilbert deixasse de ser imprescindível. Algumas dessas descobertas devem-se a Kurt Godel, com os seus teoremas de incompletude provou que uma teoria axiomática recursivamente enumerável não pode ser completa e consistente ao mesmo tempo.
Em 1934, surgiram as primeiras grandes mudanças no uso dos métodos de dedução pelos lógicos. Podemos referir o sistema de Dedução Natural que foi introduzido por Gentzen (1935) na mesma tese em que introduziu o cálculo sequencial de primeira ordem, uma das ferramentas lógicas mais usadas em trabalhos técnicos avançados. Em Basic Proof Theory, podemos ler que a motivação de Gentzen, segundo o próprio, para definir a dedução natural foi “a criação de um raciocínio tão semelhante quanto possível do raciocínio tão semelhante quanto possível do raciocínio tão semelhante possível do raciocínio real”. “to set up a formula system which comes as close as possible to actual