Sistema de Hilbert – Wikipédia, a enciclopédia livre

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 axiomas lógicos 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 ${\displaystyle \vdash P(x)}$ pode ser derivado, então ${\displaystyle \vdash \forall xP(x)}$ 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 regra da necessitação e a regra da substituição uniforme.

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.

Deduções Formais[editar | editar código-fonte]

Em um sistema de dedução de Hilbert, uma dedução formal é uma seqüência finita de fórmulas em que cada fórmula é um axioma ou é obtido a partir de fórmulas anteriores por uma regra de inferência. Estas deduções formais são feitas para refletir provas em língua natural, embora em língua natural seja muito mais detalhado.

Suponha que ${\displaystyle \Gamma }$ é um conjunto de fórmulas, consideradas como hipóteses. Por exemplo, ${\displaystyle \Gamma }$ poderia ser um conjunto de axiomas para Teoria dos grupos ou Teoria dos conjuntos. A notação ${\displaystyle \Gamma \vdash \phi }$ significa que há uma dedução que termina (conclui) em ${\displaystyle \phi }$ usando como axiomas apenas axiomas lógicos e elementos de ${\displaystyle \Gamma }$. Desse modo, dizemos que ${\displaystyle \Gamma \vdash \phi }$ significa que ${\displaystyle \phi }$ pode ser provado assumindo todas as fórmulas presentes em ${\displaystyle \Gamma }$.

Sistemas de dedução de Hilbert são caracterizadas pela utilização de numerosos esquemas de axiomas lógicos. Um esquema de axiomas é um conjunto infinito de axiomas obtidos pela substituição de todas as fórmulas de alguma forma em um padrão específico. O conjunto de axiomas lógicos inclui não apenas os axiomas gerados a partir deste padrão, mas também qualquer generalização de um desses axiomas. A generalização de uma fórmula é feita prefixando nenhum ou vários quantificadores universais na fórmula. Então, temos por exemplo, que ${\displaystyle \forall y(\forall xPxy\rightarrow Pty)}$ é uma generalização da fórmula ${\displaystyle \forall xPxy\rightarrow Pty}$.

Axiomas Lógicos[editar | editar código-fonte]

Há diversas variantes de axiomatizações da lógica de predicados, uma vez que para qualquer lógica há liberdade na escolha de axiomas e regras que caracterizam esse tipo de lógica. Descrevemos aqui um sistema de Hilbert com nove axiomas e apenas a regra modus ponens, que nós chamamos de axiomatização com uma regra (do original em inglês: one-rule axiomatization) e que descreve a lógica equacional clássica. Lidamos com uma linguagem mínima para essa lógica, de forma que as fórmulas usam apenas os conectivos ${\displaystyle \neg }$ e ${\displaystyle \rightarrow }$, e apenas o quantificador universal ${\displaystyle \forall }$. Posteriormente, mostrar-se-á como o sistema pode ser estendido para incluir conectivos lógicos adicionais, tais como ${\displaystyle \vee }$ e ${\displaystyle \wedge }$, e sem aumentar a classe de fórmulas dedutíveis.

Os primeiros quatro esquemas lógicos axiomáticos permitem, em conjunto com o modus ponens, a manipulação dos conectivos lógicos:
Axioma #1: ${\displaystyle \phi \rightarrow \phi }$
Axioma #2: ${\displaystyle \phi \rightarrow (\psi \rightarrow \phi )}$
Axioma #3: ${\displaystyle (\phi \rightarrow (\psi \rightarrow \zeta ))\rightarrow ((\phi \rightarrow \psi )\rightarrow (\phi \rightarrow \zeta ))}$
Axioma #4: ${\displaystyle (\neg \phi \rightarrow \neg \psi )\rightarrow (\psi \rightarrow \phi )}$

O axioma 1 é redundante, já que é uma conclusão lógica a partir dos axiomas 2, 3 e 4 com a utilização da regra modus ponens. Esse axiomas descrevem a lógica proposicional clássica, sem o axioma 4 nós descrevemos parte da lógica intuicionista. A lógica intuicionista pode ser completamente descrita por ao contrário de adicionar o axioma 4, utilizar o ex falso quodlibet (que significa "do falso qualquer coisa", que é um axioma lógica clássica proposicional):

Axioma #4i: ${\displaystyle \neg \phi \rightarrow (\phi \rightarrow \psi )}$

Note que estes são axiomas esquemáticos, que representam um número infinito de instâncias específicas de axiomas. Por exemplo, o aximoa 1 pode representar a instância axiomática ${\displaystyle \rho \rightarrow \rho }$, da mesma forma que pode representar a instância ${\displaystyle (\rho \rightarrow \theta )\rightarrow (\rho \rightarrow \theta )}$. O ${\displaystyle \phi }$ é uma generalização onde qualquer fórmula pode ser instanciada em seu lugar. Uma variável como essa que representa um universo de fórmulas é denominada de "variável esquemática" (do inglês schematic variable).

Com a segunda regra, a de substituição uniforme, nós podemos mudar cada um desses axiomas esquemáticos em um único axioma, substituindo cada variável esquemática por alguma variável proposicional que não é mencionado em nenhum axioma para obter o que chamamos de axiomatização substitucional (do inglês: substitutional axiomatization). Ambas as formalizações tem variáveis​​, mas enquanto a axiomatização com uma regra tem variáveis ​​esquemáticas que estão fora da linguagem da lógica, a axiomatização substitucional usa variáveis ​​proposicionais que fazem o mesmo trabalho, expressando a ideia de uma variável que abrangendo o espaço de fórmulas com uma regra que usa substituição.

Regra de Substituição Uniforme: Seja ${\displaystyle \phi (\rho )}$ ser uma fórmula com uma ou mais instâncias ${\displaystyle \rho }$, e seja ${\displaystyle \psi }$ outra fórmula. Então, de ${\displaystyle \phi (\rho )}$, infira ${\displaystyle \phi (\rho )}$.

Os próximos três axiomas esquemáticos nos fornece maneiras de adicionar, manipular e remover quantificadores universais:

Axioma #5: ${\displaystyle \forall x\phi (x)\rightarrow \phi [x:=t]}$, onde t pode ser substituído por x em ${\displaystyle \phi }$
Axioma #6: ${\displaystyle \forall x(\phi \rightarrow \psi )\rightarrow (\forall x(\phi )\rightarrow \forall (\psi ))}$
Axioma #7: ${\displaystyle \phi \to \forall x\left(\phi \right)}$, onde x não é uma variável livre de ${\displaystyle \phi }$.

Essas três regras adicionais estendem o sistema proposicional para axiomatizar a lógica de predicados clássica. Da mesma forma, estas três regras do sistema para estender a lógica proposicional intuicionista(com o Axioma #3 e #4i) a lógica de predicados intuicionista.

Quantificação universal muitas vezes é dado uma axiomatização alternativa usando uma regra extra de generalização (veja a seção sobre Metateoremas), caso em que os axiomas 5 e 6 são redundantes.

Os axiomas esquemáticos finais são requeridos a trabalhar com fórmulas que envolvem o símbolo da igualdade.

Axioma #8: ${\displaystyle x=x}$ para toda variável livre x
Axioma #9: ${\displaystyle \left(x=y\right)\to \left(\phi [z:=x]\to \phi [z:=y]\right)}$

Extensões Conservativas[editar | editar código-fonte]

É comum a inclusão em um sistema de dedução de Hilbert apenas axiomas para a implicação e negação. Tendo em conta estes axiomas, é possível formar extensões conservativas (do inglês: conservative extensions) do teorema da dedução (do inglês: deduction theorem) que permitem a utilização de conectivos adicionais. Estas extensões são chamadas de conservativas porque se uma fórmula ${\displaystyle \phi }$ envolvendo novos conectivos é reescrita como uma fórmula logicamente equivalente ${\displaystyle \theta }$ envolvendo apenas negação, implicação e quantificação universal, então ${\displaystyle \phi }$ é derivável no sistema estendido, se e somente se, ${\displaystyle \theta }$ é derivável no sistema original . Quando totalmente estendido, um sistema de Hilbert vai se assemelhar de forma muito próxima a um sistema de dedução natural.

Quantificação Existencial[editar | editar código-fonte]

• Introdução

${\displaystyle \forall x(\phi \rightarrow \exists y(\phi [x:=y]))}$

• Eliminação

${\displaystyle \forall x(\phi \rightarrow \psi )\rightarrow \exists x(\phi )\rightarrow \psi }$, onde x não é uma variável livre de ${\displaystyle \psi }$

Conjunção e Disjunção[editar | editar código-fonte]

• Conjunção
  • Introdução: ${\displaystyle \alpha \rightarrow \beta \rightarrow \alpha \wedge \beta }$
  • Eliminação:
    1. À esquerda: ${\displaystyle \alpha \rightarrow \beta \rightarrow \alpha }$
    2. À direita: ${\displaystyle \alpha \wedge \beta \rightarrow \beta }$
• Disjunção
  • Introdução
    1. À esquerda:${\displaystyle \alpha \rightarrow \alpha \vee \beta }$
    2. À direita:${\displaystyle \beta \rightarrow \alpha \vee \beta }$
  • Eliminação:${\displaystyle (\alpha \rightarrow \gamma )\rightarrow (\beta \rightarrow \gamma )\rightarrow \alpha \vee \beta \rightarrow \gamma }$

Metateoremas[editar | editar código-fonte]

Devido aos sistemas de Hilbert terem muito poucas regras de dedução, é comum provar metateoremas que deduzam que regras adicionais de dedução não trazem nenhum poder de dedução adicional, i. e., são desnecessária, no sentido que uma dedução usando novas regras de dedução pode ser convertida em uma dedução usando apenas as regras originais.

Algumas formas comuns de metateoremas dessa forma são:

• O teorema da dedução (do inglês: en: deduction theorem: ${\displaystyle \Gamma ,\Phi \leftrightarrow (\Gamma \vdash \phi \rightarrow \psi )}$
• ${\displaystyle \Gamma \vdash \phi \leftrightarrow \psi }$ se e somente se ${\displaystyle \Gamma \vdash \phi \to \psi }$ e ${\displaystyle \Gamma \vdash \psi \to \phi }$.
• Contraposição: Se ${\displaystyle \Gamma ;\phi \vdash \psi }$, então ${\displaystyle \Gamma ;\lnot \psi \vdash \lnot \phi }$.
• Generalização: Se ${\displaystyle \Gamma \vdash \phi }$ e x não ocorre livremente em nenhuma fórmula de ${\displaystyle \Gamma }$, então ${\displaystyle \Gamma \vdash \forall x\phi }$.

Axiomatizações Alternativas[editar | editar código-fonte]

O axioma 3 acima é creditado a Jan Łukasiewicz.^[1] O sistema original de Gottlob Frege tinha os axiomas #2 e #3, mas quatro outros axiomoas, ao invés do axioma #4 (see Frege's propositional calculus). Bertrand Russell e Alfred North Whitehead também sugeriram um sistema com cinco axiomas proposicionais.

Outras Conexões[editar | editar código-fonte]

Os axiomas #1, #2 e #3 com as regras de dedução modus ponens (formalizando a lógica proposicional), corresponde à lógica combinatório de bases combinatórias I, K eS com o operador de aplicação. Provas no sistema de Hilbert então correspondem aos termos combinatórios em lógica combinatória. Veja também Correspondência de Curry-Howard.

Notas[editar | editar código-fonte]

Referências[editar | editar código-fonte]

• Curry, Haskell B.; Robert Feys (1958). Combinatory Logic Vol. I. 1. Amsterdam: North Holland 
• Monk, J. Donald (1976). Mathematical Logic. Col: Graduate Texts in Mathematics. Berlin, New York: Springer-Verlag. ISBN 978-0-387-90170-1. 
• Ruzsa, Imre; Máté, András (1997). Bevezetés a modern logikába (em Hungarian). Budapest: Osiris Kiadó  !CS1 manut: Língua não reconhecida (link)
• Tarski, Alfred (1990). Bizonyítás és igazság (em Hungarian). Budapest: Gondolat  !CS1 manut: Língua não reconhecida (link) É uma tradução de artigos seletos de Alfred Tarski quanto à teoria semântica da verdade(en).
• David Hilbert (1927) "The foundations of mathematics", traduzido por Stephan Bauer-Menglerberg e Dagfinn Føllesdal (pp. 464–479). em:
  • van Heijenoort, Jean. From Frege to Gödel: A Source Book in Mathematical Logic, 1879–1931. 1967, 3rd printing 1976. Cambridge MA: Harvard University Press. ISBN 0-674-32449-8 

Hilbert, em 1927, baseado numa aula/palestra sobre fundamentos em 1925 (pp. 367–392), apresenta seus 17 axiomas --axiomas da impplicação #1-4, axiomas sobre & e V #5-10, axiomas da negação #11-12, seu ε-axioma lógico #13, axiomas de igualdade #14-15, e axiomas dos números #16-17 -- além de outros elementos necessários da sua "teoria de prova" Formalista -- e.g. axiomas indutivos, axiomas recursivos, etc; ele também oferece uma defesa contra o Intuicionismo de L.E.J. Brouwer. Veja também os comentários e refutações de Hermann Weyl (pp. 480–484), o apêndice de Paul Bernay's (1927) para a aula de Hilbert (pp. 485–489) e a resposta de Luitzen Egbertus Jan Brouwer (pp. 490–495) (1927)

• Kleene, Stephen Cole. Introduction to Metamathematics. 1952, 10th impression with 1971 corrections. Amsterdam NY: North Holland Publishing Company. ISBN 0-7204-2103-9 

Veja em particular o Capítulo IV Formal System (pp. 69–85, onde Kleene apresenta subcapítulos §16 Formal symbols (Símbolos Formais), §17 Formation rules (Regras de Formação), §18 Free and bound variables (Variáveis Livres e Fechadas - incluindo substituição), §19 Transformation rules (Regras de Transformação - e.g. modus ponens) -- e dessas ele apresenta 21 "postulados" -- 18 axiomas e 3 relações de "consequências imediatas" divididas da seguinte maneira: Postulates for the propostional calculus #1-8 (Postulados para a Lógica Proposicional), Additional postulates for the predicate calculus #9-12 (Postulados Adicionais para o Cálculo de Predicados), and Additional postulates for number theory #13-21 (Postulados Adicionais para Teoria dos Números).

Ligações externas[editar | editar código-fonte]

Farmer, W. M. «Propositional logic» (pdf)  Descreve (entre outros) a parte do sistema de redução de Hilbert restrita ao cálculo proposicional.