En lógica matemática , un testigo es un valor específico t que se sustituye por la variable x de un enunciado existencial de la forma ∃ x φ ( x ) tal que φ ( t ) es verdadero.
Por ejemplo, se dice que una teoría T de aritmética es inconsistente si existe una prueba en T de la fórmula "0 = 1". La fórmula I( T ), que dice que T es inconsistente, es, por tanto, una fórmula existencial. Un testigo de la inconsistencia de T es una prueba particular de "0 = 1" en T.
Boolos, Burgess y Jeffrey (2002:81) definen la noción de testigo con el ejemplo, en el que S es una relación de n lugares en números naturales, R es una relación recursiva de (n+1) lugares y ↔ indica equivalencia lógica (si y sólo si):
En este ejemplo particular, los autores definieron s como (positivamente) recursivamente semidecidible o simplemente semirecursivo .
En cálculo de predicados , un testigo de Henkin para una oración en una teoría T es un término c tal que T prueba φ ( c ) (Hinman 2005:196). El uso de tales testigos es una técnica clave en la demostración del teorema de completitud de Gödel presentado por Leon Henkin en 1949.
La noción de testigo conduce a la idea más general de semántica de juegos . En el caso de la sentencia, la estrategia ganadora para el verificador es elegir un testigo para . Para fórmulas más complejas que involucran cuantificadores universales , la existencia de una estrategia ganadora para el verificador depende de la existencia de funciones de Skolem apropiadas . Por ejemplo, si S denota entonces un enunciado equisatisfactorio para S es . La función f de Skolem (si existe) en realidad codifica una estrategia ganadora para el verificador de S al devolver un testigo para la subfórmula existencial para cada elección de x que el falsificador pueda hacer.
