Razoabilidade (lógica)

 Nota: Se procura conceito jurídico, veja Razoabilidade.

Na lógica matemática, razoabilidade é 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 várias variações da razoabilidade; As diferentes fórmulas de classes são estudadas e que objetos são realizadores diferentes estas várias variações.

Razoabilidade pode ser visto como a formalização da interpretação de BHK da lógica intuicionista; na razoabilidade 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 razoabilidade 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 provê.

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

Exemplo: razoabilidade por números

A versão original de Kleene de razoabilidade 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 fixada função de pares; segundo, para cada número natural n, φ_n é a função computável com index 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 o 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:

Deixe A ser a sentença da aritmética de Heyting(HA). Se HA provê 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 é prová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 provê a sentença (∃ x)A(x) então existe um n tal que HA provê A(n)
• Se HA provê uma sentença A∨B então HA provê A ou HA provê B.

Desenvolvimentos posteriores

Kreisel introduziu razoabilidade modificada, que utiliza cálculo lambida tipado como uma linguagem de realizadores. Razoabilidade 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))$.

Razoabilidade 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

Razoabilidade é um dos métodos usados na prova de mining para extrair "programas" concretos de provas matemáticas aparentemente não construtivas. Extração de programas usando razoabilidade é implementado em alguma prova adjunta tal qual Coq. Realizability is one of the methods used in proof mining to extract concrete "programs" from seemingly nonconstructive mathematical proof. Program extraction using realizability is implemented in some prova adjuntas such as 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.