To install click the Add extension button. That's it.

The source code for the WIKI 2 extension is being checked by specialists of the Mozilla Foundation, Google, and Apple. You could also do it yourself at any point in time.

Kelly Slayton
Congratulations on this excellent venture… what a great idea!
Alexander Grigorievskiy
I use WIKI 2 every day and almost forgot how the original Wikipedia looks like.
Live Statistics
English Articles
Improved in 24 Hours
Added in 24 Hours
Show all languages
What we do. Every page goes through several hundred of perfecting techniques; in live mode. Quite the same Wikipedia. Just better.

Witness (mathematics)

From Wikipedia, the free encyclopedia

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 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

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.

Relation to game semantics

The notion of witness leads to the more general idea of game semantics. In the case of sentence the winning strategy for the verifier is to pick a witness for . 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 then an equisatisfiable statement for S is . 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


  • 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
This page was last edited on 25 May 2021, at 06:32
Basis of this page is in Wikipedia. Text is available under the CC BY-SA 3.0 Unported License. Non-text media are available under their specified licenses. Wikipedia® is a registered trademark of the Wikimedia Foundation, Inc. WIKI 2 is an independent company and has no affiliation with Wikimedia Foundation.