証人（数学）

数理論理学において、証人とは、 ∃ x φ ( x )という形式の存在命題の変数xに代入される特定の値tであり、 φ ( t )が真となるようなものである。

例えば、算術理論Tは、 T において「0 = 1」という式を証明するものが存在する場合、矛盾していると言われます。Tが矛盾していることを示す 式I( T )は、存在式です。Tの矛盾の証拠は、Tにおける「0 = 1」の具体的な証明です。  

Boolos、Burgess、およびJeffrey（2002:81）は、Sが自然数上のn-位置関係、 Rが(n+1) -位置の再帰関係、↔が論理的同値性（かつその場合に限る）を示す例を用いて、証人の概念を定義している。

S ( x ₁ , ..., x _n ) ↔ ∃ y R ( x ₁ , . . ., x _n , y )

「関係Rがx _iについて成り立つようなyは、関係Sがx _iについて成り立つことの『証人』と呼ばれることがある（ただし、証人が人ではなく数である場合、証人は真実であることのみを証言するということを理解しておく必要がある）。」

この例では、著者らはs を（正の）再帰的に半決定可能、または単に半再帰的であると定義した。

述語論理において、文のヘンキン証人${\displaystyle \exists x\,\varphi (x)}$理論において、Tはφ ( c )を証明する項cである(Hinman 2005:196)。このような証拠を用いることは、1949 年にレオン・ヘンキンが提示したゲーデルの完全性定理の証明における重要な手法である。

証人の概念は、より一般的なゲーム意味論の概念につながる。文の場合${\displaystyle \exists x\,\varphi (x)}$検証者にとっての勝利戦略は、${\displaystyle \varphi }$全称量化子を含むより複雑な式の場合、検証者にとっての勝利戦略の存在は、適切なスコレム関数の存在に依存します。たとえば、Sが${\displaystyle \forall x\,\exists y\,\varphi (x,y)}$Sの等充足可能な文は次のようになります。${\displaystyle \exists f\,\forall x\,\varphi (x,f(x))}$スコレム関数f (存在する場合) は、実際にはSの検証者にとっての勝利戦略をコード化しており、偽造者が行う可能性のあるxのすべての選択に対して存在部分式の証拠を返します。

• 証明書（複雑性）は、計算複雑性理論における類似の概念である。
• 証人設定

• George S. Boolos、John P. Burgess、Richard C. Jeffrey、2002年、『計算可能性と論理学：第4版』、ケンブリッジ大学出版局、ISBN 0-521-00758-5。
• レオン・ヘンキン、1949年、「一階関数計算の完全性」、Journal of Symbolic Logic v. 14 n. 3、pp.  159 – 166。
• ピーター・G・ヒンマン、2005年、『数理論理学の基礎』、AKピーターズ、ISBN 1-56881-262-0。
• J. Hintikkaおよび G. Sandu、2009、「ゲーム理論的意味論」、Keith Allan 編『意味論簡潔百科事典』、Elsevier、ISBN 0-08095-968-7 、 341 ～ 343ページ