Quantificação: diferenças entre revisões
Conteúdo apagado Conteúdo adicionado
Linha 27:
A [[gramática de Montague]] apresenta uma nova forma semantica para linguagens naturais. Sua proposta discute uma versão muito mais formal da linguagem natural do que o tratamento tradicional de Frege, Russell e Quine.
== Quantificadores ==
== A notação para quantificadores ==▼
Um quantificador é um símbolo lógico que faz uma verificação sobre o [[conjunto]] de [[valores]] que tornam uma ou mais [[fórmulas]] verdadeiras. Este é um conceito bastante geral. Grande parte da [[matemática]] é formada por dois quantificadores: o quantificador universal e o quantificador existencial.
Informalmente, um quantificador é uma [[expressão]] que assinala a quantidade de vezes que um [[predicado]] é satisfeito numa [[classe]] de coisas (isto é, num [[domínio]]). Em [[termos]] formais, um quantificador liga uma [[variável]], transformando uma frase aberta com ''n'' [[variáveis]] livres diferentes num outra frase com ''n''-1 [[variáveis]] livres diferentes.
▲=== A notação para quantificadores ===
O símbolo tradicional para o quantificador universal é ∀, a letra "A" invertida, que se lê como "todo" . O símbolo correspondente para o quantificador existencial é ∃ , a letra "E" rotacionada, que se lê como "existe". Dessa forma, as expressões quantificadas são construídas como segue,
:: <math> \exists{x}\, P \quad \forall{x}\, P </math>
Linha 37 ⟶ 42:
No início do século XX os documentos não usavam o símbolo ∀. A notação típica era <math> (x)P </math> para expressar "para todo <math> x </math>, <math> P </math>", e "∃<math>xP </math> " para "existe <math>x</math> tal que P". O símbolo ∃ foi inventado por Giuseppe Peano por volta de 1890. Mais tarde, em torno de 1930, Gerhard Gentzen introduziu o símbolo ∀ para representar a quantificação universal. O Begriffsschrift de [[Gottlob Frege | Frege]] usou uma notação diferente, a qual não incluía um quantificador existencial ∃<math>xP</math> era sempre representado com o seu equivalente no Begriffsschrift, ¬ ∀<math>x</math>¬<math>P</math>.
O [[quantificador universal]] "''para todo''" toma uma [[variável]] e uma [[fórmula]] e afirma que a [[fórmula]] pode assumir qualquer [[valor]] para um dado ''x''. Um exemplo típico seria uma [[sentença]] como a que seque abaixo:
Note que algumas versões da notação mencionam explicitamente o escopo da quantificação. O escopo da quantificação deve sempre ser especificado, mas para uma dada teoria da matemática, isto pode ser feito de diferentes maneiras:▼
::<math>\forall x[x \le 0 ]</math> que declara que não importa qual seja o valor de ''x'', <math> x \le 0 </math>.
O [[quantificador existencial]] "''existe''" é dual; isto é, a [[fórmula]] <math> \exists x F(x) </math> é equivalente a <math> \neg\forall x\lnot F(x)</math>.
Ele declara que existe algum ''x'' satisfazendo a [[fórmula]], como em: <math>\exists x[x>0]</math> que afirma que existe algum [[valor]] de ''x'' maior que 0.
O escopo de um quantificador é a porção de uma [[fórmula]] onde ele conecta as [[variáveis]]. Algumas versões da notação mencionam explicitamente o escopo da quantificação. Note que conexões anteriores de [[variáveis]] são sobrescritas dentro do [[escopo]] de um quantificador. No exemplo acima, o [[escopo]] dos quantificadores foi a [[fórmula]] completa, mas isso nem sempre é o caso. O próximo exemplo é um uso mais complicado de quantificadores:
::<math> \displaystyle\forall x \underbrace {[x=0 \vee \exists y \overbrace{ [x=y+1 \land (y=0 \lor \exists x \underbrace{[y=x+1]}_{\text {1} } )]}^{\text{Escopo do primeiro quantificador existencial}}]}_{\text {Escopo do quantificador universal}} </math>
1: [[Escopo]] do segundo [[quantificador existencial]]. Dentro desta área, todas as referências a ''x'' refere-se a [[variável]] ligada pelo [[quantificador existencial]]. Aqui, é impossível se referir diretamente ao ''x'' ligado a partir do [[quantificador universal]].
Observe também que se pode usar qualquer variável como uma variável quantificada no lugar de outra, sob certas condições. Até mesmo se a notação usa variáveis tipificadas, pode-se ainda usar qualquer variável daquele tipo. O valor de captura de variável é extremamente importante. Como o exemplo mostra, pode ser embaraçoso quando um quantificador sobrescreve um outro. Por não mudar o significado da sentença, a troca de [[variáveis]] ligadas por outras equivalentes, porém, mais legíveis é uma solução para o problema:▼
::<math>\forall x [x=0 \vee \exists y [x=y+1 \land (y=0 \lor \exists z [y=z+1])]] </math>
Esta [[sentença]] tanto afirma que todo o [[número]] é maior ou igual a zero, ou que existe algum [[número]] menor que ele, e que o [[número]] menor que ele é também maior que zero ou tem um [[número]] menor que ele.
▲
* Assumindo um determinado domínio a ser discutido por cada quantificação, como é feito na teoria de conjuntos de [[Zermelo-Fraenkel]].
* Fixando, logo de partida, vários domínios de discurso e requerer que cada variável tenha um domínio declarado, que é representa o ''tipo'' da variável. Isto é análogo à situação em linguagens de programação de computador estaticamente tipadas, nas quais as variáveis têm tipos declarados.
* Mencionando explicitamente a faixa de quantificação, usando talvez um símbolo para o conjunto de todos os objetos naquele domínio ou o tipo dos objetos naquele domínio.
▲Observe também que se pode usar qualquer variável como uma variável quantificada no lugar de outra, sob certas condições. Até mesmo se a notação usa variáveis tipificadas, pode-se ainda usar qualquer variável daquele tipo. O valor de captura de variável é extremamente importante.
Informalmente, os "∀<math>x</math>" ou "∃<math>x</math>" podem muito bem aparecer após <math>P(x)</math>, ou até mesmo no meio, se <math>P(x)</math> for uma expressão longa. Entretanto, de modo formal, a variável ligada antecede a expressão.
Linha 64 ⟶ 87:
* Para qualquer número natural, seu produto com 2 é igual a ele somado consigo mesmo;
Um quantificador é dito "sem uso" se a [[variável]] que ele liga não aparece em lugar algum do seu escopo, tal como
::<math> \forall x \exists y [0 \le x] </math>.
Enquanto os [[quantificadores]] "sem uso" não mudam o significado da sentença, eles são ocasionalmente úteis para encontrar uma [[fórmula]] equivalente de uma forma específica.
Enquanto universal e existencial são os quantificadores mais comuns (em particular, eles são os quantificadores que aparecem na lógica de primeira ordem), algumas lógicas utilizam outros quantificadores. O quantificador <math> \exists ! xF(x) </math>, por exemplo, que significa que existe um único x satisfazendo <math> F(x) </math> é equivalente a <math> \exists x [F(x) \land \forall y[F(y) \to x=y]] </math> .
== Semântica formal ==
Linha 111 ⟶ 139:
Advertimos o leitor de que a ''lógica'' correspondente para tal semântica é bastante complicada.
== Referências ==
*Quantifier - PlanetMath Disponível em [http://planetmath.org/encyclopedia/Quantifier.html] Acessado em: 13 de junho, 2007, 10:52:00
== {{Veja Também}} ==
*[[Quantificação existencial]]
*[[Quantificação universal]]
*[[Universo de discurso]]
*[[Lógica]]
*[[Lógica proposicional]]
*[[Lógica de primeira ordem]]
*[[Variáveis livres e ligadas]]
*[[Skolemização]]
*[[Leon Henkin]]
*[[Teoria semântica da verdade]]
*[[Teorema de Herbrand]]
=={{Links Externos}}==
| |||