Realizabilidade

Realizabilidade é um método semântico na lógica e na ciência da computação que associa a cada enunciado um realizador, isto é, um objeto computacional concreto capaz de demonstrar a sua verdade. Em lógica intuicionista e matemática construtiva, um enunciado é considerado verdadeiro na medida em que existe um realizador que o verifica, tornando explícita a conteúdo computacional da prova. O conceito foi introduzido por Stephen Kleene na década de 1940 como interpretação construtiva da aritmética intuicionista, associando fórmulas a funções recursivas. ao longo do tempo a realizabilidade expandiu-se para interpretações de lógicas mais amplas e para fundamentos da computação, incluindo realizabilidade para-topos e realizabilidade clássica.

Em termos técnicos, para uma proposição P com quantificações, o realizador é um objeto que, de forma prática, fornece evidência computável de P. Em lógica proposicional: P∧Q é realizado por um par que realiza P e Q; P∨Q por um indicador de escolha entre as partes realizadas; P→Q por um método que transforma qualquer realizador de P em um realizador de Q; ∃x P(x) por uma evidência que inclui um witness e um realizador de P(witness); ∀x P(x) por uma função computável que, dado x, retorna um realizador de P(x). Em realizabilidade clássica, abordagens como a de Krivine estendem o framework para interpretar raciocínio não construtivo usando técnicas como continuations.

Variantes importantes incluem a realizabilidade de Kleene, a realizabilidade modificada de Kreisel e desenvolvimentos em realizabilidade para-topos. Aplicações comuns situam-se na extração de programas a partir de provas, na teoria de normalização e na semântica de sistemas de tipos, além de oferecerem ferramentas para a interpretação computacional de teoremas na lógica construtiva e na matemática.