Realizabilidade

Origem: Wikipédia, a enciclopédia livre.
Saltar para a navegação Saltar para a pesquisa
Ambox important.svg
Foram assinalados vários aspectos a serem melhorados nesta página ou se(c)ção:

Na lógica matemática, Realizabilidade é uma coleção de métodos na teoria da prova usado para estudar provas construtivas e extrair informações adicionais dele. [1] Fórmulas de uma teoria formal são "compreendidas" como objetos, conhecidos como "realizadores", de um jeito que conhecimento do realizador dão conhecimento sobre a verdade da fórmula. Existem diversas variantes da Realizabilidade; exatamente que classe de fórmulas é estudada e que objetos são realizadores é o que distingue essas variantes.

Realizabilidade pode ser vista como a formalização da interpretação de BHK da lógica intuicionista; na Realizabilidade a noção de prova (que é deixada indefinida na interpretação BHK) é recolocada com uma notação formal de 'realizadores'. A maioria das variações da Realizabilidade começam com o teorema de que qualquer afirmação que é provada em um sistema formal estudado é realizável. O 'realizador', de qualquer maneira, geralmente dá mais informações sobre a fórmula do que a prova formal proveria.

Além de dar uma visão sobre a demonstrabilidade intuicionista, Realizabilidade pode ser aplicada para provar a Propriedades da existência e da disjunção para teorias intuicionistas e para extrair programas de provas, como na mineração de prova. É também relacionado com a teoria de topos através da Realizabilidade de topos.

Exemplo: Realizabilidade por números[editar | editar código-fonte]

A versão original de Kleene de Realizabilidade usa números naturais como 'realizadores' para fórmulas na aritmética de Heyting. As cláusulas seguintes são usadas para definir uma relação "n 'realiza' A" entre fórmulas A na linguagem da aritmética de Heyting. Alguns pedaços da notação são requeridas: primeiro, um par ordenado (n,m) é tratado como um único número usando uma função de emparelhamento fixada; segundo, para cada número natural n, φn é a função computável com índice n.

  • Um número n realiza uma fórmula atômica s=t se e somente se s=t é verdadeiro. Assim, cada número que 'realizar' uma equação verdadeira, e nenhum número 'realizar uma equação falsa.
  • Um par(n,m) realiza uma fórmula AB se e somente se n 'realiza' A e m realiza B. Assim o 'realizador' de uma conjunção é um par de realizadores para o conjunto.
  • Um par (n,m) realiza a fórmula AB se e somente se: n é 0 ou 1; e se n é 0 então m realiza A; e se n é um então m realiza B. Assim um realizador para uma disjunção explícita escolhe uma das disjunções (com n) e provê um realizador para ele (with m).
  • Um número n realiza uma fórmula AB se e somente se todo m que realiza A, φn(m) realiza B. Assim o realizador para uma implicação é uma função computável que pega o realizador para a hipótese e produz um realizador para a conclusão.
  • Um par (n,m) realiza a fórmula (∃ x)A(x) se e somente se m é um realizador para A(n). Assim um realizador para uma fórmula existencial produz uma testemunha explícita para todo o quantificador com um realizador para a fórmula instanciada com aquela testemunha.
  • Um número n realiza a fórmula (∀ x)A(x) se e somente se, para todo m, φn(m) é definido e realiza A(m). Assim, um realizador para uma afirmação universal é uma função computável que produz, para cada m, uma testemunha para a fórmula instanciada com m.

Com esta definição, o seguinte teorema é obtido:[2]

Suponha que A seja uma sentença da aritmética de Heyting (HA). Se HA prova A, então existe um n tal que n realiza A.

Em contrapartida, existe uma fórmula tal que ela é realizada porém não é demonstrável em HA, um fato estabelecido primeiramente por Rose.[3]

Análises posteriores do método podem ser usadas para provar que HA tem a "Propriedades de existência e disjuntas":[4]

  • Se HA prova a sentença (∃ x)A(x) então existe um n tal que HA prova A(n)
  • Se HA prova uma sentença AB então HA prova A ou HA prova B.

Desenvolvimentos posteriores[editar | editar código-fonte]

Kreisel introduziu Realizabilidade modificada, que utiliza cálculo lambida tipado como uma linguagem de realizadores. Realizabilidade modificada é um jeito de mostrar que o principio de Markov não é derivável na lógica intuicionista. Ao contrário, é possível construir uma justificativa para o princípio da independência das premissas:

.

Realizabilidade relativa[5] é uma análise intuicionista recursiva de elementos enumeráveis de dados estruturados que não necessariamente são computáveis, tal qual operações computáveis em todos os números reais quando reais podem ser aproximados em sistemas computacionais digitais.

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

Realizabilidade é um dos métodos usados na mineração de prova para extrair "programas" concretos de provas matemáticas aparentemente não construtivas. Extração de programas usando Realizabilidade é implementado em alguns assistentes de prova tal como Coq.

Ver também[editar | editar código-fonte]

Referências

  1. van Oosten 2000
  2. van Oosten 2000, p. 7
  3. Rose 1953
  4. van Oosten 2000, p. 6
  5. Birkedal 2000
  • Kreisel G. (1959). "Interpretation of Analysis by Means of Constructive Functionals of Finite Types", in: Constructivity in Mathematics, edited by A. Heyting, North-Holland, pp. 101–128.
  • Kleene, S. C. (1945). «On the interpretation of intuitionistic number theory». Journal of Symbolic Logic. 10 (4): 109–124. JSTOR 2269016. doi:10.2307/2269016 
  • Kleene, S. C. (1973). "Realizability: a retrospective survey" from Mathias, A. R. D.; Hartley Rogers (1973). Cambridge Summer School in Mathematical Logic : held in Cambridge/England, August 1–21, 1971. Berlin: Springer. ISBN 3-540-05569-X  , pp. 95–112.
  • Rose, G. F. (1953). «Propositional calculus and realizability». Transactions of the American Mathematical Society. 75 (1): 1–19. JSTOR 1990776. doi:10.2307/1990776 

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

  • Realizability Collection of links to recent papers on realizability and related topics.