Operátor výběru

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í \exists x.P(x) \supset P(\varepsilon 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í \exists x. P(x) \supset P(\varepsilon x. +moreP) a \forall x. P(x) \supset P(\varepsilon x. \neg P). Term \varepsilon x. \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(\varepsilon x. \neg P) \supset \forall x. P(x).

Kategorie:Logika