Inmathematical logic, awitness is a specific valuet to be substituted for variablex of anexistential statement of the form∃xφ(x) such thatφ(t) is true.

For example, a theoryT of arithmetic is said to be inconsistent if there exists a proof inT of the formula "0 = 1". The formula I(T), which says thatT is inconsistent, is thus an existential formula. A witness for the inconsistency ofT is a particular proof of "0 = 1" inT.

Boolos, Burgess, and Jeffrey (2002:81) define the notion of a witness with the example, in whichS is ann-place relation on natural numbers,R is an(n+1)-placerecursive relation, and ↔ indicateslogical equivalence (if and only if):

S(x₁, ...,x_n) ↔ ∃yR(x₁, . . .,x_n,y)

"Ay such thatR holds of thex_i may be called a 'witness' to the relationS holding of thex_i (provided we understand that when the witness is a number rather than a person, a witness only testifies to what is true)."

In this particular example, the authors defineds to be(positively) recursively semidecidable, or simplysemirecursive.

Inpredicate calculus, aHenkin witness for a sentence${\displaystyle \mathrm{\exists }x\phi (x)}$ in a theoryT is atermc such thatT provesφ(c) (Hinman 2005:196). The use of such witnesses is a key technique in the proof ofGödel's completeness theorem presented byLeon Henkin in 1949.

The notion of witness leads to the more general idea ofgame semantics. In the case of sentence${\displaystyle \mathrm{\exists }x\phi (x)}$ the winning strategy for the verifier is to pick a witness for${\displaystyle \phi }$. For more complex formulas involvinguniversal quantifiers, the existence of a winning strategy for the verifier depends on the existence of appropriateSkolem functions. For example, ifS denotes${\displaystyle \mathrm{\forall }x\mathrm{\exists }y\phi (x,y)}$ then anequisatisfiable statement forS is${\displaystyle \mathrm{\exists }f\mathrm{\forall }x\phi (x,f(x))}$. The Skolem functionf (if it exists) actually codifies a winning strategy for the verifier ofS by returning a witness for the existential sub-formula for every choice ofx the falsifier might make.

• Certificate (complexity), an analogous concept in computational complexity theory

• George S. Boolos, John P. Burgess, and Richard C. Jeffrey, 2002,Computability and Logic: Fourth Edition, 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, pp. 159–166.
• Peter G. Hinman, 2005,Fundamentals of mathematical logic, A.K. Peters,ISBN 1-56881-262-0.
• J. Hintikka and G. Sandu, 2009, "Game-Theoretical Semantics" in Keith Allan (ed.)Concise Encyclopedia of Semantics, Elsevier,ISBN 0-08095-968-7, pp. 341–343

• Logic
• Quantifier (logic)
• Mathematical logic

• Articles with short description
• Short description is different from Wikidata