Exibir código-fonte para Lógica/Cálculo Quantificacional Clássico

Voltar para o Índice de [[Lógica]]

=Introdução=

:	Se você leu as partes deste wikibook que tratam da lógica aristotélica e do CPC (e você deveria ter lido o segundo antes de começar a ler este), deve ter reparado que não podemos formalizar os silogismos categóricos por meio do Cálculo Proposicional. Vejamos o seguinte silogismo em Darii:

:Toda espécie de mamífero é produtora de leite.
:Alguns animais marítimos são espécies de mamíferos.
:Logo, alguns animais marítimos são produtores de leite.

:	As duas premissas e a conclusão consistem em sentenças distintas, tornando impossível formalizar o argumento (mantendo sua validade) por meio do CPC. Para tal, faz-se necessário um sistema que não se limite às sentenças, mas também permita trabalhar os elementos que a constituem (sujeito, predicado etc.), ou seja, um cálculo de predicados de primeira ordem. E ainda, precisamos lidar com a quantificação (todos, algum(ns), nenhum). Para satisfazer essas condições, temos o Cálculo Quantificacional Clássico.
 

==Do CPC para o CQC==

:Tanto o CPC quanto o CQC são sistemas da lógica clássica, ou seja, ambos compartilham os mesmos princípios: bivalência, não-contradição, terceiro excluído e identidade.  De fato, pode-se considerar o CQC como uma extensão do CPC, ou então, o CPC como um subsistema do CQC. 
:''O que muda então de um sistema para outro?''
:Em primeiro, enquanto o CPC lida com letras sentenciais – uma letra do alfabeto romano maiúscula representa uma proposição e consiste numa fórmula atômica, enquanto uma letra do alfabeto grego minúscula representa uma fórmula qualquer – o CQC lida com constantes individuais, constantes de predicados e variáveis individuais. 
:Em segundo, no CQC aparece outro tipo de operador: os quantificadores. Estes, diferente da negação e dos conectivos, não são funções de verdade. Mesmo porque, o CPC já contém todas funções de verdade que o princípio de bivalência permite (ver: [[Lógica: Funções de verdade e os 16 possíveis conectivos no CPC|Funções de Verdade]]).

=Constantes individuais e de predicados=

:Constantes são coisas que tem sempre o mesmo valor dentro de um sistema. Por exemplo, o valor de <math>\pi \,\!</math> é sempre o mesmo, seja na fórmula do comprimento da circunferência (<math>\mathrm{C}=2\pi r \,\!</math>), seja na fórmula da área do círculo (<math>\mathrm{A}=\pi r^2 \,\!</math>), qualquer que seja o valor de <math>r\,\!</math>. No CQC teremos dois tipos de constantes: '''constantes individuais''' e '''constantes de predicado'''.
:As constantes individuais, evidentemente, são indivíduos: Aristóteles, Gödel, João, Maria, o gato do vizinho, o irmão do Pedro etc. Estes são designados por letras do alfabeto romano minúsculas: <math>a\,\!</math>, <math>b\,\!</math>, <math>c\,\!</math>, <math>d\,\!</math>, <math>e\,\!</math>... . Evitando usar as letras <math>x\,\!</math>, <math>y\,\!</math> e <math>z\,\!</math>, que são canonicamente usadas como variáveis, como será falado adiante. Também é lícito usar números juntamente com as letras. Ex: <math>m1\,\!</math> para designar “Maria Silveira” e <math>m2\,\!</math> para designar “Maria Oliveira”.
:As constantes de predicados são atributos que podem ser predicados às constantes individuais, ex: “...é filósofo”, “...é matemático”, “...está correndo”, “...é bela”,  “...matou aula hoje”, “...escreve livros” etc. Estes são designados por letras do alfabeto romano maiúsculas: <math>A\,\!</math>, <math>B\,\!</math>, <math>C\,\!</math>, <math>D\,\!</math>, <math>E\,\!</math> etc.
:Uma constante isolada não consiste numa fórmula. Afinal, “Aristóteles”, “Gödel”, “...é matemático”, “...é filósofo” e coisas do gênero não podem ser valoradas como verdadeiras ou falsas.
:Contudo, é claro que sentenças formadas por estas constantes – “Aristóteles é matemático”, “Gödel é matemático”, “Aristóteles é filósofo” e “Gödel é filósofo” – são valoráveis como verdadeiro ou falso. Ou seja, são proposições. Para representá-las, basta colocar as constantes individuais à direita das constantes de predicado (podendo estar sub-escritas ou não). Assim, se <math>g\,\!</math> significa “Gödel”, <math>a\,\!</math> significa “Aristóteles”; <math>M\,\!</math>, “...é matemático” e <math>F\,\!</math>, “é filósofo”; então <math>Mg\,\!</math> significa “Gödel é matemático”; <math>Ma\,\!</math>, “Aristóteles é matemático”; <math>Fg\,\!</math> significa “Gödel é filósofo” e <math>Fa\,\!</math>, “Aristóteles é filósofo”. Constantes individuais atribuídas a uma constante de predicado consistem numa fórmula atômica do CQC. E podemos usar todos operadores do CPC com elas. Por exemplo, usando as mesmas constantes acima, podemos construir as fórmulas:

:<math> \neg Ma</math>
:“Aristóteles não é matemático”.

:<math>Fa\land Mg </math>
:“Aristóteles é filósofo e Gödel é matemático”.

:<math> Fa\lor Ma </math>
:“Aristóteles é filósofo ou matemático”.

:<math> Fg\to Mg </math>
:“Se Gödel é filósofo, então Gödel é matemático”.

:<math> Mg\leftrightarrow Ma </math>
:“Gödel é matemático se e somente se Aristóteles é matemático”.

:Voltando a tratar de fórmulas atômicas, estas podem ter mais de uma constante individual, quando se atribui a um indivíduo uma propriedade em relação a outro indivíduo. Por exemplo, digamos que vamos formalizar a sentença “João beijou Maria”. Teremos as constantes individuais j (para João) e m (para Maria), e a constante de predicado B para “...beijou...”.  A fórmula fica então: <math>Bjm\,\!</math>.
:Poderíamos formalizar isto de outra forma, considerando a constante de predicado B como “...foi beijado(a) por...”. A fórmula fica então: <math>Bmj\,\!</math>.
:Em algumas circunstâncias, é possível sermos econômicos e poupar as fórmulas de constantes individuais. Por exemplo, digamos um sistema no qual só a Maria é beijada e tudo que Maria faz é ser beijada. Então podemos considerar a constante B como “...beijou Maria”. A sentença “João e Pedro(p) beijaram Maria” fica assim: <math> Bj\land Bp </math>.
:Por fim, é lícito usar letras sentenciais para expressar orações sem sujeito, por exemplo: <math>C\!\,</math> para “Está chovendo”. Assim podemos formalizar uma proposição como “Se está chovendo, então Maria não saiu de casa” assim: <math>C\to \neg Sm</math>. Sendo <math>S\,\!</math> a constante de predicado “...saiu de casa”.

=Variáveis individuais e Quantificadores=

:Até agora o que vimos não distingue muito o CQC do CPC. Todos os ''esquemas de fórmulas tautológicas''' no CPC tem instâncias de '''fórmulas universalmente válidas''' no CQC, por exemplo: <math>Pa\to Pa</math>, <math>\neg \left (Rb\land\neg Rb\right )</math>, <math> Fd\lor \neg Fd </math> etc. Também, os mesmos argumentos que são válidos no CPC também são válidos no CQC, por exemplo: <math>Pa\vDash Pa</math>, <math>\left \{Ab\to Cd, Ab\right \}\vdash \mathrm{Cd}</math> etc.
:Contudo, ainda não temos o suficiente para formalizar sentenças como “Alguém comeu a última fatia de bolo”. Os recursos usados para tal são o diferencial do CQC em relação ao CPC. 
:Analisemos a sentença citada acima. “Alguém” significa algum indivíduo indeterminado do sistema em questão. Digamos que o sistema seja uma família de três indivíduos: : Brian (<math>b\,\!</math>), Lisa (<math>l\,\!</math>) e Brian Júnior (<math>j\,\!</math>). Neste caso, sendo <math>C\,\!</math> a constante de predicado “... comeu a última fatia de bolo”, a sentença poderia ser formalizada assim: <math> Cb\lor Cl\lor Cj </math>.
:Contudo, a quantidade de constantes individuais pode ser tão grande que isto se tornar impraticável, por exemplo: “Alguns brasileiros cursam o Ensino Superior”. Neste caso, há milhões de constantes individuais. Poderia até ser infinita, como “alguns números naturais são pares”. E ainda há sistemas nos quais não há informação sobre o número de constantes individuais. Portanto, serão usadas variáveis para representar estes indivíduos indeterminados.
:Mas só a adição de variáveis não é suficiente. Vejamos o sistema da família de três indivíduos. Digamos que neste sistema tenhamos a seguinte sentença: “Todos estão assistindo TV”. Sendo <math>A\,\!</math> a constante de predicado “...está assistindo TV”, neste caso poderíamos fazer assim: <math> Ab\land Al\land Aj </math>. Mais uma vez, esta solução é impraticável caso haja um número muito grande ou infinito  de constantes individuais ou não haja informação sobre este número. Portanto, serão usadas variáveis nestes casos também. Assim, se faz necessário algo para diferenciar “Alguns As são Bs” de “Todo A é B”. Isto é feito com os quantificadores. Existem dois quantificadores no CQC: universal (<math>\forall </math>) e existencial (<math>\exists </math>).  Funcionam assim:

:Sendo <math>x\,\!</math> uma variável individual,
:<math>\forall x\left (Px\right )</math> significa “Para todo <math>x\,\!</math>, <math>P\,\!</math> é predicado de <math>x\,\!</math>”.
:<math>\exists x\left (Px\right )</math> significa “Existe algum <math>x\,\!</math>, tal que <math>P\,\!</math> é predicado de <math>x\,\!</math>”.
:Os quantificadores não são funções de verdade. Não é possível chegar ao valor de verdade de <math>\forall x\left (\alpha\right )</math> ou <math>\exists x\left (\alpha\right )</math> a partir do valor de <math>\alpha \,\!</math>.
: Tudo isto amplia a definição de fórmula:
:Se <math>x\,\!</math> é uma variável e <math>\alpha \,\!</math> é uma fórmula onde <math>x\,\!</math> ocorre, então <math>\forall x\left (\alpha\right )</math> e <math>\exists x\left (\alpha\right )</math> são '''fórmulas gerais'''.

==Expressão de Sentenças==
:Agora vejamos como expressar sentenças com quantificadores no sistema CQC. 
:“Toda espécie de mamífero é produtora de leite”.
:Não podemos usar o sujeito da sentença como constante individual. Afinal, não se trata de um indivíduo, mas de um conjunto de indivíduos. Precisaremos usar uma variável (<math>x\,\!</math>) e um quantificador, no caso, o universal. Vamos usar <math>M\,\!</math> para “... é espécie de mamífero” e <math>L\,\!</math> para “... é produtor de leite”. A fórmula fica:
:<math>\forall x\left (Mx\to Lx\right ) </math>
:Ou seja:  Para todo <math>x\,\!</math>, se <math>x\,\!</math> é espécie de mamífero, então <math>x\,\!</math> é produtor de leite.


:Formalizemos agora a sentença “Alguns animais marítimos são espécies de mamíferos”. Usando <math>A\,\!</math> para “...é animal marítimo”, a fórmula fica:

:<math>\exists x\left (Ax\land Mx\right )</math>
:Ou seja: Existe algum <math>x\,\!</math>, tal que <math>x\,\!</math> é animal marítimo e <math>x\,\!</math> é mamífero.


:Vejamos como formalizar uma sentença onde aparece a palavra “nenhum”, tal como “Nenhum mamífero respira debaixo d’água”.  Sendo <math>R\,\!</math> a constante de predicado “...respira debaixo d’água”, a fórmula fica:
:<math>\forall x\left (Mx\to \neg Rx\right ) </math>
:Ou seja: Para todo <math>x\,\!</math>, se <math>x\,\!</math> é mamífero, então <math>x\,\!</math> não respira debaixo d’água.
:A sentença também pode ser formalizada assim:
:<math>\neg \exists x\left (Mx\land Rx\right )</math>
:Ou seja: Não existe algum <math>x\,\!</math>, tal que <math>x\,\!</math> é mamífero e <math>x\,\!</math> respira debaixo d’água.
:<math>\forall x\left (Mx\to \neg Rx\right ) </math> é equivalente a <math>\neg \exists x\left (Mx\land Rx\right )</math>.


:Vejamos como formalizar uma sentença com variável e constante individual, como, “Se todos garotos da rua beijaram Maria, então o namorado de Maria ficará furioso”. As constantes individuais são: “Maria” (<math>m\,\!</math>) e “namorado de Maria” (<math>n\,\!</math>). As constantes de predicado são: “...é garoto da rua” (<math>G\,\!</math>), “...beijou...” (<math>B\,\!</math>) e “...ficará furioso” (<math>F\,\!</math>). A fórmula fica assim:

:<math>\forall x\left (Gx\to Bxm\right )\to Fn </math>
:Ou seja: Para todo <math>x\,\!</math>, se <math>x\,\!</math> é garoto da rua implica que <math>x\,\!</math> beijou Maria, então o namorado de Maria ficará furioso.


:Repare que <math>\forall x\left (Gx\to Bxm\right )</math> é subfórmula de <math>\forall x\left (Gx\to Bxm\right )\to Fn </math>. Ou seja, uma subfórmula pode ser geral (conter um quantificador) e nada impede de uma fórmula conter várias subfórmulas gerais. Por exemplo, acima foi dito que <math>\forall x\left (Mx\to \neg Rx\right ) </math> é equivalente a <math>\neg \exists x\left (Mx\land Rx\right )</math>. Portanto, são fórmulas válidas:

:<math>\forall x\left (Mx\to \neg Rx\right )\leftrightarrow \neg \exists x\left (Mx\land Rx\right )</math>.
:<math>\forall x\left (Mx\to \neg Rx\right )\to \neg \exists x\left (Mx\land Rx\right )</math>.
:<math>\neg \exists x\left (Mx\land Rx\right )\to \forall x\left (Mx\to \neg Rx\right )</math>.
:Veremos mais adiante como verificar se uma fórmula é válida.
:E é claro que não apenas fórmulas válidas podem ter subfórmulas gerais.


:Uma fórmula geral também pode ter mais de um quantificador. Ex:
:“Todos que são ingênuos são enganadas por alguns que não tem escrúpulos”. 
:Usando a notação: <math>I\,\!</math>: “... é ingênuo(a)”, <math>E\,\!</math>: “... é enganado(a) por...” e <math>D\,\!</math>: “... tem escrúpulos”; temos a fórmula:
:<math>\forall x\exists y\left (\left (Ix\land \neg Dy\right )\to Exy\right )   </math>
:Ou seja: Para todo <math>x\,\!</math>, existe algum <math>y\,\!</math>, tal que se <math>x\,\!</math> é ingênuo e <math>y\,\!</math> não tem escrúpulos; então <math>x\,\!</math> é enganado por <math>y\,\!</math>.


:Vejamos um exemplo que tenha dois quantificadores universais:
:“Se uma pessoa é empregada da outra, então esta é patrão dessa”.
:Usando a notação: <math>E\,\!</math>: “... é empregada de...” e <math>P\,\!</math>: “... é patrão de de...”, temos a fórmula:
:<math>\forall x\forall y\left (Exy\leftrightarrow Pyx\right )</math>
:Ou seja: Para todo <math>x\,\!</math> e para todo <math>y\,\!</math>, <math>x\,\!</math> é empregada de <math>y\,\!</math> se e somente se <math>y\,\!</math> é patrão de <math>x\,\!</math>.
:Repare que não foi inserido na fórmula a constante de predicado “...é pessoa”, pois esta fórmula (deve) estar inserida num sistema onde todas constantes individuais são pessoas. Quando mais pra frente lidarmos com formalização da aritmética, também não será preciso a constante de predicado “... é número”.


:Por fim, resta tratar da questão que surge com o uso de mais de um quantificador – e conseqüentemente mais variáveis individuais - numa fórmula. Não há limites para o número de variáveis individuais, mas canonicamente são usadas as letras {x, y, z} para representá-las. O que fazer se for necessária uma quarta, quinta ou mais variáveis? Apesar de situações como estas serem raras, qualquer letra do alfabeto romano minúscula inserida na frente de um quantificador vale como variável. Ex:
:<math>\forall x\forall y\exists z\exists w\left (\left (Mx\to \neg Ry\right )\to \left (Az\land Bw\right )\right )</math>

=Tablôs Semânticos no CQC=
:Tablôs semânticos no CQC seguem as mesmas regras que no CPC, adicionando regras para lidar com os quantificadores e as variáveis.
:Este texto partirá do princípio que já tenha sido lido o artigo: [[Lógica: Cálculo Proposicional Clássico: Tablôs semânticos]].

==Tablôs de Fórmulas==
: Recapitulemos as regras de construção de tablôs já conhecidas:

[[Imagem:Regras de construção de tablos.gif]]

:Em vista destas regras já conhecidas podemos facilmente verificar que a seguinte fórmula é válida: <math>\exists x\left (Px\land Qx\right )\to\exists x\left (Px\land Qx\right ) </math>. 
:Relembremos o procedimento de construção de tablôs:
* Supor que a fórmula seja falsa.
* Desenvolver esta suposição.
* Caso cair em contradição (a mesma fórmula receber dois valores distintos) em todos ramos do tablô, concluir que ela não pode ser falsa. O que no caso do CQC significa concluir que ela é universalmente válida.
:Façamos o tablô da fórmula em questão:
<div align="center">
:<math>\mathbf{F}\quad \exists x\left (Px\land Qx\right )\to\exists x\left (Px\land Qx\right ) </math>
:<math>\mathbf{V}\quad \exists x\left (Px\land Qx\right )</math>
:<math>\mathbf{F}\quad \exists x\left (Px\land Qx\right )</math>
:<math>\times</math>
</div>

:Muito simples! De fato, <math>\exists x\left (Px\land Qx\right )\to\exists x\left (Px\land Qx\right ) </math> consiste numa instância de tautologia, do Princípio de Identidade (<math>\alpha\to \alpha</math>). 
:Obviamente, nem todas fórmulas válidas do CQC são instâncias de tautologia. Não tardemos a tratar delas.

=====Exemplo 1=====

:Comecemos por uma fórmula simples que envolva o quantificador universal: <math>\forall x\left(Gx\right)\to Ge</math>
:Ela poderia significar algo como “Se todos [indivíduos do sistema em questão] são geômetras, então Euclides é geômetra”. O que intuitivamente parece válido e, como veremos, de fato o é.
*Primeiro passo, supor que ela seja falsa:
<div align="center">
:<math>\mathbf{F}\quad \forall x\left(Gx\right)\to Ge</math>
</div>
:Temos a falsidade de uma implicação. Então temos que supor que o antecedente seja verdadeiro e o conseqüente falso:
<div align="center">
:<math>\mathbf{F}\quad \forall x\left(Gx\right)\to Ge\quad \mathbf{ok}</math>
:<math>\mathbf{V}\quad \forall x\left(Gx\right)</math>
:<math>\mathbf{F}\quad Ge\,\!</math>
</div>

:Já estamos diante de uma novidade: a verdade de uma fórmula geral formada por um quantificador universal. Vejamos como lidar com isto. 
:<math>\forall x\left(Gx\right)</math> significa que <math>G\,\!</math> é predicado de todas constantes individuais do sistema. Assim, sendo <math>\forall x\left(Gx\right)</math> verdade no tablô, então podemos inserir nele <math>Ga\,\!</math>, <math>Gb\,\!</math>, <math>Gc\,\!</math>, <math>Gd\,\!</math>, <math>Ge\,\!</math> etc., sendo todas verdadeiras. Não precisamos ter certeza que <math>a\,\!</math>, <math>b\,\!</math>, <math>c\,\!</math>, <math>d\,\!</math> etc. realmente estão inseridas no sistema. Podemos apenas supor isto (aliás, todo tablô é uma suposição). 
:Obviamente, inserir no tablô que <math>Ga\,\!</math>, <math>Gb\,\!</math>, <math>Gc\,\!</math>, <math>Gd\,\!</math>, <math>Gf\,\!</math>, <math>Gh\,\!</math>... são verdadeiras, em nada  nos serve neste caso. Contudo, se inserirmos que <math>Ge\,\!</math> é verdadeira, o único ramo do tablô fecha e a validade de <math>\forall x\left(Gx\right)\to Ge</math> fica provada:
<div align="center">
:<math>\mathbf{F}\quad \forall x\left(Gx\right)\to Ge\quad \mathbf{ok}</math>
:<math>\mathbf{V}\quad \forall x\left(Gx\right)</math>
:<math>\mathbf{F}\quad Ge\,\!</math>
:<math>\mathbf{V}\quad Ge\,\!</math>
:<math>\times</math>
</div>


:Repare que não marcamos <math>\forall x\left(Gx\right)</math> com um “OK” como fazíamos com outras fórmulas usadas. Afinal, ainda há infinitas outras fórmulas além de <math>Ge\,\!</math> que podem ser extraídas da verdade de :<math>\forall x\left(Gx\right)</math>.

=====Exemplo 2=====
:<math>Ge\to \forall x\left(Gx\right)</math>
:Intuitivamente podemos dizer que a fórmula não é válida. Afinal, não é porque <math>G\,\!</math> é predicado de uma constante, que necessariamente <math>G\,\!</math> seja predicado de todas constantes. De qualquer forma, façamos o tablô:

<div align="center">
:<math>\mathbf{F}\quad Ge\to \forall x\left(Gx\right)</math>
:<math>\mathbf{V}\quad Ge\,\!</math>
:<math>\mathbf{F}\quad \forall x\left(Gx\right)</math>
</div>

:O que fazer com a falsidade de uma fórmula geral que contém o quantificador universal? Se é falso que <math>G\,\!</math> é predicado de todas as constantes individuais, então deve haver alguma(s) constante(s) individual(is) que, se <math>G\,\!</math> for predicado a elas, tem-se uma fórmula falsa. Mas quais? Podemos supor quaisquer constantes individuais, desde que elas ainda não tenham aparecido no ramo do tablô. Ou seja, podemos inserir no tablô a falsidade de <math>Ga\,\!</math>, <math>Gb\,\!</math>, <math>Gc\,\!</math>, <math>Gd\,\!</math> etc. Contudo, não podemos inserir a falsidade de <math>Ge\,\!</math>, pois a constante <math>e\,\!</math> já aparece no ramo. Então o tablô fica aberto e concluímos que a fórmula não é válida.

=====Exemplo 3=====
:Vejamos como fazer um tablô de uma fórmula que não contenha constantes individuais: <math>\forall x\left(Ax\to Ax\right)</math>.
<div align="center">
:<math>\mathbf{F}\quad \forall x\left(Ax\to Ax\right)</math>
</div>

:Já vimos que, dada a falsidade de uma fórmula geral que contém o quantificador universal, podemos remover o quantificador e substituir a variável por uma constante individual, desde que ela ainda não tenha aparecido no ramo do tablô. Como não há constantes individuais no tablô em questão, estamos livres para usar de qualquer constante:

<div align="center">
:<math>\mathbf{F}\quad \forall x\left(Ax\to Ax\right)\quad \mathbf{ok}</math>
:<math>\mathbf{F}\quad Af\to Af\quad \mathbf{ok}</math>
:<math>\mathbf{V}\quad Af\,\!</math>
:<math>\mathbf{F}\quad Af\,\!</math>
:<math>\times</math>
</div>

=====Exemplo 4=====
:Vejamos finalmente uma fórmula que contém o quantificador existencial: <math>Ge\to \exists x\left(Gx\right)</math> . 

<div align="center">
:<math>\mathbf{F}\quad Ge\to \exists x\left(Gx\right)\quad \mathbf{ok}</math>
:<math>\mathbf{V}\quad Ge\,\!</math>
:<math>\mathbf{F}\quad \exists x\left(Gx\right)</math>
</div>

:Como lidar com a falsidade de uma fórmula geral formada por um quantificador existencial? Vejamos... se é falso que existe alguma constante individual a qual forme uma fórmula atômica verdadeira com a constante de predicado <math>G\,\!</math>, então podemos inserir no tablô a falsidade de qualquer fórmula atômica formada por <math>G\,\!</math> (<math>Ga\,\!</math>, <math>Gb\,\!</math>, <math>Gc\,\!</math>, <math>Gd\,\!</math>, <math>Ge\,\!</math> etc.). Se inserirmos a falsidade de <math>Ge\,\!</math>, o tablô fecha e concluímos a validade da fórmula <math>Ge\to \exists x\left(Gx\right)</math> :
<div align="center">
:<math>\mathbf{F}\quad Ge\to \exists x\left(Gx\right)\quad \mathbf{ok}</math>
:<math>\mathbf{V}\quad Ge\,\!</math>
:<math>\mathbf{F}\quad \exists x\left(Gx\right)</math>
:<math>\mathbf{F}\quad Ge\,\!</math>
:<math>\times</math>
</div>

:A validade desta fórmula também é intuitivamente evidente. “Se Euclides é geômetra, então alguém é geômetra” é bastante óbvio. Vejamos agora um exemplo mais complicado.

=====Exemplo 5=====
:Anteriormente foi dito que <math>\forall x\left (Mx\to \neg Rx\right ) </math> é equivalente a <math>\neg \exists x\left (Mx\land Rx\right )</math>, ou seja, que :<math>\forall x\left (Mx\to \neg Rx\right )\leftrightarrow \neg \exists x\left (Mx\land Rx\right )</math> é válida. Façamos o tablô para verificar se isto está correto.

[[Imagem:Tablo formula quantificacional.jpg]]

:Foi feito todo ramo esquerdo do tablô e o direito até chegarmos a uma novidade: a verdade de uma fórmula geral formada por um quantificador existencial. Antes de tratar disto, vejamos o que foi feito do lado esquerdo. 
*A fórmula não continha constantes individuais, nos deixando livres para inserir qualquer constante, que no caso é <math>f\,\!</math>. 
*Não foi gratuitamente que  comecei pela falsidade de <math>\forall x\left (Mx\to \neg Rx\right ) </math>. Como vimos acima, dada a falsidade de uma fórmula geral que contém o quantificador universal, podemos remover o quantificador e substituir a variável por uma constante individual, desde que ela ainda não tenha aparecido no ramo do tablô. Se começássemos pela falsidade de <math>\exists x\left (Mx\land Rx\right )</math>, depois não poderíamos usar a mesma constante individual a fim de encontrar a contradição.
:Agora vejamos como lidar com a verdade de uma fórmula geral formada pelo quantificador existencial. Se é verdade que <math>M\,\!</math> e <math>R\,\!</math> são predicados de algumas das constantes individuais, então deve haver alguma(s) constante(s) individual(is) que, se <math>M\,\!</math> e <math>R\,\!</math> forem predicadas a elas, tem-se uma fórmula verdadeira. Mas quais? Podemos supor quaisquer constantes individuais, desde que elas ainda não tenham aparecido no ramo do tablô.
:Em vista disto, procederemos na construção do tablô da  seguinte forma: trabalhar primeiro com a verdade de <math>\exists x\left (Mx\land Rx\right )</math> e depois com a verdade de <math>\forall x\left (Mx\to \neg Rx\right ) </math>. Assim, seja qual for a constante individual que aplicarmos na primeira, poderemos aplicar na segunda.

[[Imagem:Tablo formula quantificacional2.jpg]]

=====Exemplo 6=====
Vejamos agora um tablô de uma fórmula de múltiplos quantificadores.

<div align="center">
:<math>\mathbf{F}\quad \forall x\exists y\left(Pxy\right)\to \exists y\left(Pay\right)\quad \mathbf{ok}</math>
:<math>\mathbf{V}\quad \forall x\exists y\left(Pxy\right)</math>
:<math>\mathbf{F}\quad \exists y\left(Pay\right)</math>
:<math>\mathbf{V}\quad \exists y\left(Pay\right)</math>
:<math>\times</math>
</div>

==Regras de construção de tablôs para fórmulas quantificadas==

:Sendo <math>x\,\!</math> uma variável individual, <math>\alpha\,\!</math> uma fórmula onde <math>x\,\!</math> ocorre, e <math>c\,\!</math> alguma constante que substitui <math>x\,\!</math> na fórmula <math>\alpha\,\!</math>, temos:

:<math>{\mathrm{V}\quad \forall x\left(\alpha\right)\over \mathrm{V}\quad \alpha\left [x\mathcal {n} c\right]}</math>

: Para qualquer <math>c\,\!</math>.


:<math>{\mathrm{F}\quad \forall x\left(\alpha\right)\over \mathrm{F}\quad \alpha\left [x\mathcal {n} c\right]}</math>

:Desde que <math>c\,\!</math> seja nova no ramo.


:<math>{\mathrm{V}\quad \exists x\left(\alpha\right)\over \mathrm{V}\quad \alpha\left [x\mathcal {n} c\right]}</math>

:Desde que <math>c\,\!</math> seja nova no ramo.


:<math>{\mathrm{F}\quad \exists x\left(\alpha\right)\over \mathrm{F}\quad \alpha\left [x\mathcal {n} c\right]}</math>

: Para qualquer <math>c\,\!</math>.


:Nos casos em que a constante adicionada deve ser nova no ramo, a fórmula recebe marcação pois não pode novamente ser usada.


:Um tablô que envolve fórmulas quantificadas está ''terminado'' se:

:*todos ramos do tablô fecharem (caírem em contradição). Neste caso a fórmula ou argumento é válido(a)

:Ou se:

:*Foram utilizadas todas fórmulas moleculares.
:*Todos existenciais e todos universais falsos que ocorrem em cada ramo foram utilizados.
:*Foram utilizados cada universal verdadeiro e cada existencial falso para cada constante individual do ramo.
:Se atendidas estas três condições o tablô não fechar, então a fórmula ou argumento é inválido(a).

==Tablôs de Argumentos==
: Os tablôs das fórmulas acima – fora o exemplo 5 - são bastante simples. Afinal, estavam sendo apresentadas as regras de construção de tablôs para quantificadores. Compensemos isto agora lidando com algo mais sofisticado: a formalização e construção de tablôs de argumentos da lógica aristotélica.
: Relembrando o processo de construção de tablôs de argumentos:
* Supor que o argumento seja inválido, ou seja, que a premissas podem ser verdadeiras e a conclusão falsa..
* Desenvolver esta suposição.
* Caso cair em contradição (a mesma fórmula receber dois valores distintos) em todos ramos do tablô, concluir que a conclusão não pode ser falsa enquanto as premissas são verdadeiras.

=====Exemplo 1=====

:Vejamos o silogismo categórico '''Barbara''':

:Todo A é um B.
:Todo B é um C.
:∴ Todo A é um C.

:Na linguagem simbólica do CQC, ele pode ser expresso assim:

:<math>\left\{\forall x\left(Ax\to Bx\right) , \forall x\left(Bx\to Cx\right)\right\}\vDash \forall x\left(Ax\to Cx\right)</math>

:O primeiro passo é supor que as premissas sejam verdadeiras e a conclusão seja falsa:

<div align="center">
:<math>\mathbf{V}\quad \forall x\left(Ax\to Bx\right)</math>
:<math>\mathbf{V}\quad \forall x\left(Bx\to Cx\right)</math>
:<math>\mathbf{F}\quad \forall x\left(Ax\to Cx\right)</math>
</div>

:A estratégia adotada para resolver o tablô será começar pela conclusão e depois usar as premissas. Assim, podemos inserir qualquer constante individual na conclusão, e depois remeter a esta mesma constante nas premissas.

<div align="center">
:<math>\mathbf{V}\quad \forall x\left(Ax\to Bx\right)</math>
:<math>\mathbf{V}\quad \forall x\left(Bx\to Cx\right)</math>
:<math>\mathbf{F}\quad \forall x\left(Ax\to Cx\right)\quad \mathbf{ok}</math>
:<math>\mathbf{F}\quad Al\to Cl\quad \mathbf{ok}</math>
:<math>\mathbf{V}\quad Al</math>
:<math>\mathbf{F}\quad Cl</math>
</div>

:Agora utilizaremos as premissas, aplicando a mesma constante individual <math>l\,\!</math>:

<div align="center">
[[Imagem:Tablobarbara.jpg]]</div>

=====Exemplo 2=====

:Vejamos o silogismo categórico '''Darii''':

:Todo B é um A.
:Alguns Cs são Bs.
:∴ Alguns Cs são As.

:Na linguagem simbólica do CQC, ele pode ser expresso assim:

:<math>\left\{\forall x\left(Bx\to Ax\right) , \exists x\left(Cx\land Bx\right)\right\}\vDash \exists x\left(Cx\land Ax\right)</math>

:O primeiro passo:

<div align="center">
:<math>\mathbf{V}\quad \forall x\left(Bx\to Ax\right)</math>
:<math>\mathbf{V}\quad \exists x\left(Cx\land Bx\right)</math>
:<math>\mathbf{F}\quad \exists x\left(Cx\land Ax\right)</math>
</div>

:Pelo mesmo motivo do exemplo acima, nossa estratégia começa usando a segunda premissa, na qual temos a verdade de um existencial:

<div align="center">
:<math>\mathbf{V}\quad \forall x\left(Bx\to Ax\right)</math>
:<math>\mathbf{V}\quad \exists x\left(Cx\land Bx\right)\quad \mathbf{ok}</math>
:<math>\mathbf{F}\quad \exists x\left(Cx\land Ax\right)</math>
:<math>\mathbf{V}\quad \exists x\left(Cx\land Bx\right)\quad \mathbf{ok}</math>
<math>\mathbf{V}\quad Cd\land Bd\quad \mathbf{ok}</math>
<math>\mathbf{V}\quad Cd</math>
<math>\mathbf{V}\quad Bd</math>

</div>

=Dedução Natural no CQC=

=Símbolos de identidade e funcionais <math>(CQC_f^=)</math>=

==Tablôs Semânticos para o <math>CQC_f^=</math>==

==Dedução Natural no <math>CQC_f^=</math>==

==Formalização de sistemas pelo <math>CQC_f^=</math>==
===Fomalização da Aritmética pelo <math>CQC_f^=</math>===
:'''N1''' <math> \forall x\; \left (sx\ne x\right )</math>
:'''N2''' <math> \forall x\;\forall y\; \left (sx=sy\leftrightarrow x=y\right )</math>
:'''N3''' <math> \forall x\; \left (x+0=x\right )</math>
:'''N4''' <math> \forall x\;\forall y\; \left (x+sy=s\left (x+y\right )\right )</math>
:'''N5''' <math> \forall x\; \left (x*0=0\right )</math>
:'''N6''' <math> \forall x\;\forall y\; \left (x*sy=\left (x*y\right )+x\right )</math>
:'''N7''' <math> \forall x\;\neg \left (x < \;0\right )</math>
:'''N8''' <math> \forall x\;\forall y\; \left (x< \;sy\leftrightarrow \;\left (x< \;y\lor \;x=y\right )\right )</math>
:'''N8''' <math> \forall x\;\forall y\; \left (x< \;y\lor \;x=y\lor \;y< \;x\right )</math>

{{stub}}


[[Categoria:Lógica Clássica|Cálculo Quantificacional Clássico]]