Testemunha (matemática)
# Testemunha (matemática)

Em lógica matemática, uma testemunha é um determinado valor de t para ser substituído pela variável x de uma afirmação existencial da forma ∃x φ(x) tal que φ(t) é verdadeira.

## Exemplos

Por exemplo, uma teoria T da aritmética é dita ser inconsistente se existe uma prova em T da fórmula "0=1". A fórmula I(T), que diz que T é inconsistente, é, assim, uma fórmula existencial. Uma testemunha para a inconsistência de T, em especial, é uma prova de "0 = 1" em T.
Boolos, Burgess e Jeffrey (2002:81) define a noção de testemunhas com o exemplo, em que S é uma relação n-ária sobre os números naturais, R é uma relação recursiva n-ária, e ↔ indica equivalência lógica (se, e somente se):
       "S(x$_1$, ..., x$_n$) ↔ ∃y R(x$_1$, . . ., x$_n$, y)
    "Um y tal que R vale para o x$_i$ pode ser chamado de uma 'testemunha' para a relação S em x$_i$ (desde que se entenda que quando a testemunha é um número em vez de uma pessoa, uma testemunha apenas confirma o que é verdadeiro)." Neste exemplo em particular, B-B-J definiu s para ser (de forma positiva) e recursivamente semidecidível ou simplesmente semirecursiva.

## Testemunhas de Henkin

No cálculo de predicados, uma testemunha de Henkin dada uma sentença $\exists x\,\phi (x)$ em uma teoria T é um termo c tal que T prova que φ(c) (Hinman 2005:196). O uso de tais testemunhas é uma técnica chave na prova de Gödel do teorema da completude apresentado por Leon Henkin , em 1949.

## Relação com semântica baseada em jogos

A noção de testemunha leva a mais uma ideia geral da semântica baseada em jogos. No caso da sentença $\exists x\,\phi (x)$ a estratégia vencedora para o verificador é escolher uma testemunha para $\phi$. Para fórmulas mais complexas, envolvendo quantificadores universais, a existência de uma estratégia vencedora para o verificador depende da existência de adequadas funções de Skolem. Por exemplo, se S denota $\forall x\exists y\,\phi (x,y)$ então uma sentença equissatisfatível para S é $\exists f\forall x\,\phi (x,f(x))$. A função de Skolem f (se existir), na verdade, codifica uma estratégia vencedora para o verificador de S, retornando uma testemunha existencial, a sub-fórmula para cada escolha de x que um falsificador possa vir a fazer.

## Veja também

* Certificado (complexidade), um conceito análogo na teoria da complexidade computacional.