Witness (mathematics)

Input value for which an existential statement of a function is true

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.

## Examples

[edit]

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 n-place relation on natural numbers, R is an (n+1)-place recursive relation, and ↔ indicates logical equivalence (if and only if):

S(x1, ..., xn) ↔ ∃y R(x1, . . ., xn, y)
"A y such that R holds of the xi may be called a 'witness' to the relation S holding of the xi (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 defined s to be (positively) recursively semidecidable, or simply semirecursive.

## Henkin witnesses

[edit]

In predicate calculus, a Henkin witness for a sentence  ∃ x φ ( x ) {\displaystyle \exists x\,\varphi (x)} 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.

## Relation to game semantics

[edit]

The notion of witness leads to the more general idea of game semantics. In the case of sentence  ∃ x φ ( x ) {\displaystyle \exists x\,\varphi (x)} the winning strategy for the verifier is to pick a witness for  φ {\displaystyle \varphi } . For more complex formulas involving universal quantifiers, the existence of a winning strategy for the verifier depends on the existence of appropriate Skolem functions. For example, if S denotes  ∀ x ∃ y φ ( x , y ) {\displaystyle \forall x\,\exists y\,\varphi (x,y)} then an equisatisfiable statement for S is  ∃ f ∀ x φ ( x , f ( x ) ) {\displaystyle \exists f\,\forall x\,\varphi (x,f(x))} . 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.

## See also

[edit]

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

## References

[edit]

* 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