# Mean dependence

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

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*-place recursive relation, and ↔ indicates logical equivalence (if and only if):

- "
*S*(*x*_{1}, ...,*x*_{n}) ↔ ∃*y**R*(*x*_{1}, . . .,*x*_{n},*y*)

- "
- " A
*y*such that*R*holds of the*x*may be called a 'witness' to the relation_{i}*S*holding of the*x*(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, B-B-J have defined_{i}*s*to be*(positively) recursively semidecidable*, or simply*semirecursive*.

## Henkin witnesses

In predicate calculus, a **Henkin witness** for a sentence $\mathrm{\exists}x\phantom{\rule{0.167em}{0ex}}\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

The notion of witness leads to the more general idea of game semantics. In the case of sentence $\mathrm{\exists}x\phantom{\rule{0.167em}{0ex}}\varphi (x)$ the winning strategy for the verifier is to pick a witness for $\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 $\mathrm{\forall}x\mathrm{\exists}y\phantom{\rule{0.167em}{0ex}}\varphi (x,y)$ then an equisatisfiable statement for *S* is $\mathrm{\exists}f\mathrm{\forall}x\phantom{\rule{0.167em}{0ex}}\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.

## References

- 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