Quantificador universal

term: Quantificador universal symbol: \forall etymology: '∀ — A invertido, de all. Gentzen, 1935.' summary: '∀ (A invertido — "all"). ∀x P(x) afirma que P(x) é verdadeiro para todo x no domínio.' relatedModules: [predicate-logic] seeAlso: [quantificador-existencial, predicado]

Símbolo

$\forall$ (lê-se para todo). Um $A$ maiúsculo de cabeça para baixo — o A de all (todos), invertido. Introduzido por Gerhard Gentzen em 1935 (Untersuchungen über das logische Schließen). A própria forma é mnemônica: o leitor reconhece o símbolo em vez de memorizá-lo.

Definição

$\forall x\, P(x)$ significa para todo $x$ no domínio, $P(x)$ é verdadeiro.

Intuição

Afirmação sobre todos os elementos. Generalização. Para refutar, basta um contraexemplo.

Registro computacional

all() em Python; o quantificador percorre o domínio e retorna False ao primeiro contraexemplo.

all(x > 0 for x in domain)   # ∀x ∈ domain: x > 0

Negação

$\neg(\forall x\, P(x)) \equiv \exists x\, \neg P(x)$.

Exemplo

$\forall x\, (x^2 \geq 0)$ — para todo número real $x$, $x^2$ é não-negativo (verdadeira).