In mathematical logic, a witness is a specific value t to be substituted for variable x of an existential statement of the form ∃x φ(x) such that φ(t) is true.
For example, a theory T of arithmetic is said to be inconsistent if there exists a proof in T of the formula "0=1". The formula I(T), which says that T is inconsistent, is thus an existential formula. 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 nplace relation on natural numbers, R is an nplace recursive relation, and ↔ indicates logical equivalence (if and only if):
In predicate calculus, a Henkin witness for a sentence in a theory T is a term c such that T proves φ(c) (Hinman 2005:196). The use of such witnesses is a key technique in the proof of Gödel's completeness theorem presented by Leon Henkin in 1949.
