Loading AI tools
Da Wikipédia, a enciclopédia livre
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.
![]() | Foram assinalados vários problemas nesta página ou se(c)ção:
|
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.
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.
Com esta definição, o seguinte teorema é obtido:[2]
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]
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.
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.
Seamless Wikipedia browsing. On steroids.
Every time you click a link to Wikipedia, Wiktionary or Wikiquote in your browser's search results, it will show the modern Wikiwand interface.
Wikiwand extension is a five stars, simple, with minimum permission required to keep your browsing private, safe and transparent.