Em matemática , as expressões " para tudo " e " existe ", usadas para formular proposições matemáticas no cálculo de predicados , são chamadas de quantificações . Os símbolos que representam a linguagem formal são chamados de quantificadores (ou anteriormente quantificadores ).
A quantização universal ("para todos ..." ou "qualquer coisa ...") é denotada pelo símbolo ∀ (um A invertido ).
Exemplo:
∀ x P ( x )lê
"Para todos os x P ( x )"e meios
“Qualquer objeto do domínio considerado possui a propriedade P ”.A notação "∀" foi usada pela primeira vez por Gerhard Gentzen em 1933 (publicada em 1934). A palavra alemã alle que significa "todos", propõe um "símbolo ( Zeichen ) válido para todos ( für alle )" . Gentzen indica que escolheu como “símbolo para tudo” ( All-Zeichen ) o A invertido por analogia com o símbolo “∃” para o quantificador existencial que ele tira de Russell .
A quantificação existencial ("existe um ..." no sentido "existe pelo menos um ...") é anotada com o sinal ∃ (um E retornado). Mais precisamente,
∃ x P ( x )meios
existe pelo menos um x tal que P ( x ) (pelo menos um objeto do domínio considerado tem a propriedade P )Para expressar singularidade além da existência, o sinal usado é ∃! (o quantificador existencial seguido por um ponto de exclamação), mais precisamente,
∃! x P ( x )meios
existe um único x tal que P ( x ), ou então existe um e somente um x tal que P ( x ) (um objeto exatamente do domínio considerado tem a propriedade P ).Este último quantificador é definido pelo cálculo de predicados igualitários a partir dos dois quantificadores anteriores (e da igualdade), por exemplo, por
∃! x P ( x ) ≡ ∃ x [ P ( x ) e ∀ y ( P ( y ) ⇒ y = x )].
A notação ∃ foi usada pela primeira vez por Giuseppe Peano em 1897 no volume II de sua Forma Matemática com uma sintaxe diferente, o sinal sendo diretamente associado ao predicado (∃ P para nosso ∃ x P ( x )). Bertrand Russell é o primeiro a usá-lo da maneira atual, como um operador de link.
A negação de é:
Ou: .A negação de é:
, ou: na lógica clássica , mas não na lógica intuicionista .Para uma fórmula formatada com antecedência , a ordem dos quantificadores entre cada bloco de quantificadores idênticos (portanto, bloco de quantificadores existenciais ou bloco de quantificadores universais) é irrelevante, a fórmula permanece a mesma. Por outro lado, a alternância dos blocos de quantificadores existenciais ou universais dá fórmulas muito distintas, cuja complexidade lógica é observada em particular na hierarquia aritmética .
Na dedução natural , Gerhard Gentzen apresenta os dois quantificadores da seguinte forma:
Regras introdutórias | Regras de eliminação | |
---|---|---|
para tudo | . | |
isso existe |
Se pegarmos um grupo de gatos pretos, podemos dizer que qualquer gato que escolhermos desse grupo, será preto. ( )
Se em um grupo de gatos pretos houver alguns gatos brancos (ou apenas um), podemos dizer que há um (ou apenas um) gato branco neste grupo.
( )
Símbolo | Unicode | Html | Látex | |
---|---|---|---|---|
para tudo | ∀ | U + 2200 | & para todos; | \ para todos |
isso existe | ∃ | U + 2203 | &existir; | \ existe |
A exposição das regras que governam os quantificadores usuais existe e tudo o que pode ser encontrado em todos os livros de cálculo de predicados , uma bibliografia dos quais pode ser encontrada em lógica matemática .
Para uma generalização desses quantificadores, podemos nos voltar para: