En lógica matemática , un testigo es un valor específico t que debe sustituirse 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 la 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 lo 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 el 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 demuestra φ ( c ) (Hinman 2005:196). El uso de tales testigos es una técnica clave en la prueba 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 la semántica de juegos . En el caso de la oración, 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 equisatisfacible para S es . La función de Skolem f (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 falsador podría hacer.
