Lógica Proposicional - Introdução

Regra da Premissa

Podemos, no decorrer da prova (e em qualquer altura desta), introduzir fbfs correspondentes a premissas. A introdução de uma premissa tem sempre um aspeto deste género:

Regra da Repetição

Regra que afirma que qualquer fbf pode ser repetida dentro de uma prova - ou seja, se já existe uma fbf numa linha anterior da prova, podemos reescrevê-la na linha atual, justificando com a regra da repetição. É identificada por $Rep, n$, onde $n$ representa a linha onde a fbf em questão foi inicialmente introduzida. A regra da repetição tem sempre um aspeto deste género:

Introdução da Conjunção

Diz-nos como introduzir (ou como construir) uma fbf cujo símbolo lógico principal é uma conjunção - aqui, uma conjunção de fbfs. Abreviada por $I\wedge, (n, m)$, onde $n$ e $m$ representam, respetivamente, as linhas onde as primeira e segunda fbfs foram introduzidas.

É importante reter que as fbfs têm de ter sido introduzidas por ordem, caso contrário não podemos aplicar diretamente a regra, tendo de usar a regra da repetição. Há professores que são particularmente rígidos com esta formalidade (apesar de não haver qualquer "impacto" no quão correta a prova está), pelo que em contexto de avaliação será importante ter este aspeto em conta.

A introdução da conjunção deverá, então, ter um aspeto deste género:

Eliminação da Conjunção

Diz-nos que, de uma fbf cujo símbolo principal é uma conjunção, podemos derivar tanto a fbf da "esquerda" como a da "direita" - se temos uma conjunção com valor lógico verdadeiro, então todos os seus membros terão de o partilhar também. Abreviada por $E\wedge, n$, onde $n$ representa a linha onde a fbf em causa foi introduzida.

A eliminação da conjunção tem sempre um aspeto deste género:

ou

Regra da Hipótese

Os sistemas de dedução natural usam o conceito de prova hipotética - uma prova iniciada com a introdução de uma hipótese. Essa prova hipotética consiste num "ambiente local", um contexto diferente em que, para além das outras fbfs da prova, consideramos a hipótese que iniciou a prova, iniciada pela regra da hipótese: a regra que afirma que, em qualquer ponto de uma prova, podemos introduzir qualquer fbf como uma hipótese, começando uma nova prova hipotética.

Uma vez iniciada uma prova hipotética, todas as linhas adicionadas pertencem à mesma até que seja terminada.

Regra da Reiteração

Temos ainda a regra da reiteração, uma regra de inferência especial, específica às provas hipotéticas. Diz-nos que qualquer fbf introduzida num ponto da prova exterior à prova hipotética pode ser utilizado dentro da mesma. O contrário não se aplica.

Introdução da Implicação

Afirma que se numa prova iniciada por uma hipótese $\alpha$ formos capazes de derivar $\beta$, então podemos terminar a prova hipotética, podendo derivar $\alpha\to\beta$ na prova que contém a prova hipotética. Abreviada por $I\to, (n, m)$, onde $n$ e $m$ são, respetivamente, a linha onde a hipótese foi introduzida e a fbf associada derivada.

Voltando atrás e pensando no que é uma implicação, temos que, com premissas verdadeiras e conclusão verdadeira, a implicação é válida. Ora, se a partir de $a$ é possível provar $b$, então a implicação $a\to b$ é válida!

Eliminação da Implicação

Regra que nos diz que de uma prova que contém tanto uma fbf $\alpha$ como uma outra $\alpha\to\beta$ podemos derivar $\beta$. Abreviada por $E\to, (n, m)$, onde $n$ e $m$ são, respetivamente, as linhas onde $\alpha$ e $\alpha\to\beta$ foram introduzidas.

Esta regra poderá fazer mais sentido se pensarmos mais uma vez no significado da implicação: só podemos ter uma implicação válida caso, tendo as premissas verdadeiras, a conclusão não possa ser falsa. Ora, se temos $a \to b$ e $a$ na prova, teremos necessariamente que $a$ é verdadeiro, e seguindo este fio lógico, $b$ também terá de o ser.

A eliminação da implicação tem um aspeto deste género:

Introdução da Negação

Utiliza o conceito de prova por absurdo - se a partir de uma dada hipótese podemos derivar uma contradição, então rejeitamos essa mesma hipótese, aceitando a sua negação, visto que caso contrário chegaríamos a uma conclusão absurda. Abreviada por $I\neg, (n, (m, k))$, onde $n$, $m$ e $k$ representam, respetivamente, a linha da introdução da hipótese, e as linhas correspondentes à contradição.

A introdução da negação tem sempre um aspeto deste género:

Eliminação da Negação

Afirma que negar uma proposição duas vezes é o mesmo que a afirmar. Abreviada por $E\neg, n$, onde $n$ é a linha onde apareceu a fbf duplamente negada.

A eliminação da negação tem sempre um aspeto deste género:

Introdução da Disjunção

Tem em conta o significado intuitivo de uma disjunção - esta apenas requer que um dos elementos se verifique para ser verdadeira. Assim sendo, partindo de uma fbf $\alpha$, podemos derivar tanto $\alpha\vee\beta$ como $\beta\vee\alpha$, sendo $\beta$ qualquer fbf. Abreviada por $I\vee, n$, com $n$ sendo a linha onde a fbf $\alpha$ foi introduzida.

A introdução da disjunção tem sempre um aspeto deste género:

ou

Eliminação da Disjunção

"A regra mais complicada", segundo o prof. Pavão Martins. A partir dela, podemos retirar que, tendo por base uma fbf do tipo $\alpha\vee\beta$, caso sejamos capazes de derivar uma terceira fbf $\gamma$ a partir de provas hipotéticas iniciadas por tanto $\alpha$ como por $\beta$, então certamente que $\gamma$ se verifica - voltando à tal intuição associada à disjunção, se pelo menos um elemento é verdadeiro e podemos derivar uma fbf tanto de um como de outro, então podemos garantidamente derivar $\gamma$ de uma fbf verdadeira, pelo que $\gamma$ verificar-se-á.

Abreviada por $E\vee, (n, (o, p), (r, s))$, onde $n$ representa a fbf disjunta inicial, $o$ e $r$ o início de cada hipótese e $p$ e $s$ a derivação da fbf pretendida, dentro da respetiva hipótese. A eliminação da disjunção tem sempre um aspeto deste género:

Teorema

Corresponde a uma fbf que pode ser obtida a partir de uma prova que não contém qualquer premissa, pode ser obtida "do nada". Seja $\alpha$ um teorema, podemos escrever $\varnothing\vdash\alpha$ ou, até, de um modo mais simples, $\vdash\alpha$.