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₁, ..., x_n) ↔ ∃y R(x₁, . . ., 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 ${\displaystyle \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 ${\displaystyle \exists x\,\phi (x)}$ a estratégia vencedora para o verificador é escolher uma testemunha para ${\displaystyle \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 ${\displaystyle \forall x\exists y\,\phi (x,y)}$ então uma sentença equissatisfatível para S é ${\displaystyle \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.

Referências

• George S. Boolos, John P. Burgess, Richard C. Jeffrey, 2002, Computability e Lógica: Quarta Edição, Cambridge University Press, ISBN 0-521-00758-5.
• Leon Henkin, 1949, "The completeness of the first-order functional calculus", Journal of Symbolic Logic v. 14 n. 3, pg. 159–166.
• Pedro G. Hinman, 2005, Fundamentals of mathematical logic, A. K. Peters, ISBN 1-56881-262-0.
• J. Hintikka e G. Sandu, 2009, "Game-Theoretical Semantics" in Keith Allan (ed.) Concise Encyclopedia of Semantics, Elsevier, ISBN 0-08095-968-7, pg. 341–343