Operátor výběru

Šablona:Neověřeno Operátor výběru je v logice operátor nad formulemi zavedený Davidem Hilbertem vracející term, pro který formule platí. V logice prvního řádu například platí $\mathrm{\exists }x.P(x)\supset P(\epsilon x.P)$. Formalismus podporující operátor výběru se nazývá ε-kalkulus.

Operátor výběru lze použít k eliminaci kvantifikátorů, neboť platí $\mathrm{\exists }x.P(x)\supset P(\epsilon x.P)$ a $\mathrm{\forall }x.P(x)\supset P(\epsilon x.\mathrm{\neg }P)$. Term $\epsilon x.\mathrm{\neg }P$ ve druhé ekvivalenci reprezentuje imaginární prvek, pro který formule platí, platí-li pro celé universum. V tomto smyslu je ekvivalentní Henkinovým svědkům pro univerzální kvantifikaci: $P(\epsilon x.\mathrm{\neg }P)\supset \mathrm{\forall }x.P(x)$ Šablona:Autoritní data