Witness (mathematics)
   HOME

TheInfoList



OR:

In
mathematical logic Mathematical logic is the study of formal logic within mathematics. Major subareas include model theory, proof theory, set theory, and recursion theory. Research in mathematical logic commonly addresses the mathematical properties of formal ...
, 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+1)''-place
recursive relation In mathematics, a recurrence relation is an equation according to which the nth term of a sequence of numbers is equal to some combination of the previous terms. Often, only k previous terms of the sequence appear in the equation, for a paramete ...
, and ↔ indicates
logical equivalence In logic and mathematics, statements p and q are said to be logically equivalent if they have the same truth value in every model. The logical equivalence of p and q is sometimes expressed as p \equiv q, p :: q, \textsfpq, or p \iff q, depending o ...
(if and only if): :: ''S''(''x''1, ..., ''x''''n'') ↔ ∃''y'' ''R''(''x''1, . . ., ''x''''n'', ''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 Predicate or predication may refer to: * Predicate (grammar), in linguistics * Predication (philosophy) * several closely related uses in mathematics and formal logic: **Predicate (mathematical logic) **Propositional function ** Finitary relation, ...
, a Henkin witness for a sentence \exists x\, \varphi(x) in a theory ''T'' is a
term Term may refer to: * Terminology, or term, a noun or compound word used in a specific context, in particular: **Technical term, part of the specialized vocabulary of a particular field, specifically: ***Scientific terminology, terms used by scient ...
''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 is a fundamental theorem in mathematical logic that establishes a correspondence between semantic truth and syntactic provability in first-order logic. The completeness theorem applies to any first-order theory: ...
presented by
Leon Henkin Leon Albert Henkin (April 19, 1921, Brooklyn, New York - November 1, 2006, Oakland, California) was an American logician, whose works played a strong role in the development of logic, particularly in the theory of types. He was an active scholar ...
in 1949.


Relation to game semantics

The notion of witness leads to the more general idea of
game semantics Game semantics (german: dialogische Logik, translated as ''dialogical logic'') is an approach to Formal semantics (logic), formal semantics that grounds the concepts of truth or Validity (logic), validity on game theory, game-theoretic concepts, su ...
. In the case of sentence \exists x\, \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 function In mathematical logic, a formula of first-order logic is in Skolem normal form if it is in prenex normal form with only universal first-order quantifiers. Every first-order formula may be converted into Skolem normal form while not changing its ...
s. For example, if ''S'' denotes \forall x \, \exists y\, \varphi(x,y) then an
equisatisfiable In Mathematical logic (a subtopic within the field of formal logic), two formulae are equisatisfiable if the first formula is satisfiable whenever the second is and vice versa; in other words, either both formulae are satisfiable or both are not. E ...
statement for ''S'' is \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

*
Certificate (complexity) In computational complexity theory, a certificate (also called a witness) is a string that certifies the answer to a computation, or certifies the membership of some string in a language. A certificate is often thought of as a solution path within a ...
, an analogous concept in computational complexity theory


References

*George S. Boolos, John P. Burgess, and Richard C. Jeffrey, 2002, ''Computability and Logic: Fourth Edition'', Cambridge University Press, . * 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, . * 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 Logic Quantifier (logic) Mathematical logic