Realizabilidade

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. 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

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 A∧B 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 A∨B 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 A→B 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:

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.

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

• 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 A∨B então HA prova A ou HA prova B.

Desenvolvimentos posteriores

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:

$(\neg A\rightarrow \exists x\;P(x))\rightarrow \exists x\;(\neg A\rightarrow P(x))$.

Realizabilidade relativa é 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

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

• Isomorfismo de Curry-Howard

Referências

• Birkedal, Lars; Jaap van Oosten (2000). Relative and modified relative realizability. [S.l.: s.n.] 

• 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.

• van Oosten, Jaap (2000). Realizability: An Historical Essay. [S.l.: s.n.] 

• 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

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