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 verdadera.
Ejemplos de
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 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 solo si):
- S ( x 1 , ..., x norte ) ↔ ∃ y R ( x 1 ,..., X norte , y )
- "Una y tal que R tiene de x i puede ser llamada un 'testigo' de la relación S que tiene de x i (siempre que entendamos que cuando el testigo es un número en lugar de una persona, un testigo solo testifica de lo que es cierto)."
En este ejemplo particular, los autores definieron s como (positivamente) recursivamente semidecidable , o simplemente semirecursivo .
Testigos de Henkin
En cálculo de predicados , un testigo de Henkin para una oraciónen 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 demostración del teorema de completitud de Gödel presentada por Leon Henkin en 1949.
Relación con la semántica del juego
La noción de testigo conduce a la idea más general de la semántica del juego . En el caso de 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 denotaentonces un enunciado equisatisfactorio 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 de la subfórmula existencial para cada elección de x que pueda hacer el falsificador.
Ver también
- Certificado (complejidad) , un concepto análogo en la teoría de la complejidad computacional
Referencias
- George S. Boolos, John P. Burgess y Richard C. Jeffrey, 2002, Computability and Logic: Fourth Edition , Cambridge University Press, ISBN 0-521-00758-5 .
- Leon Henkin, 1949, "La integridad del cálculo funcional de primer orden", Journal of Symbolic Logic v. 14 n. 3, págs. 159-166.
- Peter G. Hinman, 2005, Fundamentos de lógica matemática , AK Peters, ISBN 1-56881-262-0 .
- J. Hintikka y G. Sandu, 2009, "Semántica teórica de juegos" en Keith Allan (ed.) Concise Encyclopedia of Semantics , Elsevier, ISBN 0-08095-968-7 , págs. 341–343