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