Testemunha (lógica matemática)

Origem: Wikipédia, a enciclopédia livre.
Saltar para a navegação Saltar para a pesquisa

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[editar | editar código-fonte]

Por exemplo, uma teoria T de 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 é um n-lugar da relação em números naturais, R é um n-lugar relação recursiva, e ↔ indica equivalência lógica (se, e somente se):

"S(x1, ..., xn) ↔ ∃y R(x1, . . ., xn, y)
"Um y tal que R contém o xi pode ser chamado de uma 'testemunha' para a relação S em xi (desde que entenda que quando a testemunha é um número em vez de uma pessoa, uma testemunha apenas testifica 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[editar | editar código-fonte]

Em cálculo de predicado, uma testemunha de Henkin dada uma sentença  em uma teoria T é um termo de 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 o jogo da semântica[editar | editar código-fonte]

A noção de testemunha leva a mais uma ideia geral do jogo da semântica. No caso de sentença a estratégia vencedora para o verificador é escolher uma testemunha . Para fórmulas mais complexas, envolvendo quantificadores universal, a existência de uma estratégia vencedora para o verificador depende da existência de adequadas funções Skolem. Por exemplo, se S denota por  , em seguida, uma instrução equisível para S é . O Skolem da função 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 pode fazer um falsificador.

Veja também[editar | editar código-fonte]

Referências[editar | editar código-fonte]

  • 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