For example, a theory T of arithmetic is said to be inconsistent if there exists a proof in T of the formula "0 = 1".
A witness for the inconsistency of T is a particular proof of "0 = 1" in T. Boolos, Burgess, and Jeffrey (2002:81) define the notion of a witness with the example, in which S is an n-place relation on natural numbers, R is an (n+1)-place recursive relation, and ↔ indicates logical equivalence (if and only if): In this particular example, the authors defined s to be (positively) recursively semidecidable, or simply semirecursive.
The use of such witnesses is a key technique in the proof of Gödel's completeness theorem presented by Leon Henkin in 1949.
The notion of witness leads to the more general idea of game semantics.
For more complex formulas involving universal quantifiers, the existence of a winning strategy for the verifier depends on the existence of appropriate Skolem functions.
The Skolem function f (if it exists) actually codifies a winning strategy for the verifier of S by returning a witness for the existential sub-formula for every choice of x the falsifier might make.