In mathematical logic

Mathematical logic

Mathematical logic is a subfield of mathematics with close connections to foundations of mathematics, theoretical computer science and philosophical logic. The field includes both the mathematical study of logic and the applications of formal logic to other areas of mathematics...

, a witness is a specific value t to be substituted for variable x of an existential statement

Existential quantification

In predicate logic, an existential quantification is the predication of a property or relation to at least one member of the domain. It is denoted by the logical operator symbol ∃ , which is called the existential quantifier...

 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

Logical equivalence

In logic, statements p and q are logically equivalent if they have the same logical content.Syntactically, p and q are equivalent if each can be proved from the other...

 (if and only if):

" S(x₁, ..., x_n) ↔ ∃y R(x₁, . . ., x_n, y)

" A y such that R holds of the x_i may be called a 'witness' to the relation S holding of the x_i (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 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

Term (logic)

In mathematical logic, universal algebra, and rewriting systems, terms are expressions which can be obtained from constant symbols, variables and function symbols...

 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

Gödel's completeness theorem

Gödel's completeness theorem is a fundamental theorem in mathematical logic that establishes a correspondence between semantic truth and syntactic provability in first-order logic. It was first proved by Kurt Gödel in 1929....

 presented by Leon Henkin

Leon Henkin

Leon Albert Henkin was a logician at the University of California, Berkeley. He was principally known for the "Henkin's completeness proof": his version of the proof of the semantic completeness of standard systems of first-order logic.-The completeness proof:Henkin's result was not novel; it had...

in 1949.