Sistema de Hilbert

Na lógica matemática, um Sistema de Hilbert, também chamado de Cálculo de Hilbert ou de Sistema de Hilbert-Ackermann, é um tipo de sistema de dedução formal atribuído a Gottlob Frege e David Hilbert. Esses sistemas dedutivos são usualmente estudados para a Lógica de primeira ordem, mas é do interesse de outras áreas de pesquisa também. A maioria das variantes de Sistemas de Hilbert são constituídos de um balanceamento característico entre e regras de inferência. Sistemas de Hilbert podem ser caracterizados pelo grande número de axiomas lógicos e um pequeno conjunto de regras de inferência. Comparativamente, os sistemas de dedução natural incluem um grande conjunto de regras de inferência, no entanto, um pequeno número de axiomas. Os sistemas de Hilbert mais usualmente estudados contém apenas uma regra de inferência, o modus ponens, quando se trata de sistemas na lógica proposicional, ou duas regras de inferência: além do modus ponens, a generalização universal (que afirma que se pode ser derivado, então também pode ser), na lógica de primeira ordem. Sistemas de Hilbert para a lógica modal proposicional, chamados de Sistemas de Hilbert-Lewis, são geralmente axiomatizados com mais duas regras adicionais, a e a regra da . Uma característica que está presente em várias versões de sistemas de Hilbert é que o contexto não é alterado em quaisquer de suas regras de inferência, enquanto tanto o método de dedução natural quanto o cálculo de sequentes contém algumas regras que variam de acordo com o contexto. Daí, se estamos interessados apenas na derivabilidade de tautologias, sem julgamentos hipotéticos, então podemos formalizar o sistema de Hilbert de tal forma que as suas regras de inferência contém apenas julgamentos de uma forma bastante simples. O mesmo não pode ser feito com os outros dois sistemas de dedução: como contexto é alterado em algumas de suas regras de inferências, eles não podem ser formalizados de forma que julgamentos hipotéticos poderiam ser evitados - nem mesmo se quisermos usá-los apenas para provar derivabilidade de tautologias.