Lógica e Computação

A Lógica proporciona um enquadramento formal para descrever e analizar com rigor um determinado assunto.

O objetivo principal deste texto é apresentar a Lógica como uma ferramenta para a descrição e análise de sistemas informáticos.

Sintaxe e Semântica

Por formal entende-se o tipo de regras, por exemplo, da aritmética ou da sintaxe de programas. Uma expressão aritmética como $$2+3\times 4$$ tem uma estrutura que segue um conjunto de definições sintáticas, que determinam o que pode ser escrito.

• Por exemplo $43\times 2+$ é uma expressão incorreta porque não respeita as definições habituais das expressões aritméticas (porém segue a reversed polish notation).

Por outro lado, o valor resulta de definições semânticas. Por exemplo

• A igualdade $x+y=y+x$ diz que as expressões $x+y$ e $y+x$ têm o mesmo valor.
  • As expressões $x+y$ e $y+x$ são diferentes, porque começam por símbolos diferentes, $x$ e $y$.
  • Mas ambas definem o mesmo valor.
• Outras igualdades deste tipo, como $x+0=x$ ou $(x+1)\times y=x\times y+y$ permitem deduzir, por fim, que $2+3\times 4=14$.

• As definições sintáticas especificam o que pode ser escrito, ie as expressões corretas.
• As definições semânticas definem o valor das expressões corretas.

Dedução

Também interessa a noção de dedução: quais são as conclusões de hipóteses dadas?

Em termos práticos:

• Quais são as consequências de certas ações?
  • Se $x=7$ qual o valor de $x^2-x$?
• Quais são os meios necessários para um dado objetivo?
  • Qual o valor de $x$ quando $x^2-x=42$?

Este interesse vai além da aritmética. Em geral, como é que a estrutura e o valor permitem chegar a conclusões a partir de hipóteses dadas?.

Uma dedução ou prova é uma sequência de passos que começa com hipóteses e termina numa conclusão. Cada um desses passos deve depender apenas das hipóteses e dos passos anteriores, pela aplicação de regras rigorosas.

Hipóteses, passos e conclusão são proposições (ou fórmulas) e as regras definem como certas proposições (ou fórmulas) são conclusão de outras.

A distinção entre estrutura e valor leva a dois tipos de consequência:

• A consequência sintática $H⊢t$ diz que há uma prova da conclusão $t$ a partir das hipóteses $H$ .
• A consequência semântica $H\models t$ diz que a conclusão $t$ é verdadeira sempre que as hipóteses $H$ são verdadeiras.

No primeiro caso, a consequência sintática, não participam os valores verdade/falso. Só é considerada a estrutura da proposições.

Para a consequência semântica interessam os valores verdade/falso e, também, a estrutura. Por exemplo, usando $\mathtt{v}$ para verdade e $\mathtt{f}$ para falso, na tabela

os valores booleanos na coluna $x\vee y$ dependem dos valores $\mathtt{v}$/$\mathtt{f}$ de $x$ e de $y$ e também da estrutura de $x\vee y$; a coluna $x\wedge y$ é diferente porque, embora dependa exatamente dos mesmos valores, tem uma estrutura diferente.

Informática

No caso da informática a descrição e a análise rigorosa de um sistema (ou programa) é fundamental.

Dado o seguinte programa:

#![allow(unused)]
fn main() {
fn answer(x: i32) -> i32  {
    2 * x
}

let y = answer(21);
println!("The answer is {y}.");
}

Os termos usados, como fc, println! ou os parêntesis {, } não são arbitrários; têm de ser exatamente aqueles e não outros. Além disso, a ordem por que são escritos também segue regras precisas. Por exemplo, o fragmento

#![allow(unused)]
fn main() {
answer() {fn} 2 * x i32 i32;
}

é incorreto.

Além das regras de escrita para programas corretos, também é necessário rigor na execução de um programa. O programa acima deve produzir o texto 42 na consola.

Estes dois aspetos dos programas, a escrita (sintaxe) e a execução (semântica), têm de ser definidas rigorosamente num sistema formal.

A lógica é esse sistema, capaz de definir formalmente tanto a sintaxe como a semântica dos programas.

Além de correto, um programa deve ter um comportamento bem definido. Consideremos a seguinte função:

#![allow(unused)]
fn main() {
fn sum(x: i32) -> i32 {
    // x >= 0
    let mut y = 0;
    let mut z = 0;
    while z !== x {
        z = z + 1;
        y = y + z;
    }
    // y = 0 + 1 + ... + x
    y
}
}

Como garantir que o valor devolvido por sum(x) é $y={\sum }_{z=1}^{x}z$ quando $x\ge 0$?

Uma resposta formal a este problema também permite considerar as seguintes questões:

• Como definir um programa correto?
• Como descrever o comportamento de um programa?
• Como provar que um programa funciona de acordo com as especificações?
• Como desenvolver componentes adicionais?
• Como analizar e tratar situações críticas, de erro, entradas incorretas, etc?
• Como coordenar equipas de dezenas, centenas ou milhares de engenheiros informáticos, com experiências e formações variadas?

Estas questões não podem ser respondidas ad hoc. Precisam de respostas obtidas com rigor e objetividade.

Um sistema informático crítico não pode ter uma estrutura ambígua ou subjetiva; tem de ser descrito objetivamente de forma a que diferentes equipas o possam analizar, utilizar, desenvolver, corrigir, manter, expandir, substituir, etc

Por exemplo, a documentação de uma linguagem, como a rust, de uma biblioteca, como a Distributed, a especificação de um formato, como o yaml, formalizam o que se pode escrever e o respetivo comportamento.

Esquema de Programa

Para concretizar o objetivo deste curso o programa segue os seguintes assuntos:

1. A lógica proposicional é relativamente simples e flexível para descrever alguns domínios simples. No entanto tem limitações que limitam o seu uso em casos reais.
2. A lógica de primeira ordem é significativamente mais expressiva e resolve muitas das limitações da lógica proposicional. Essa expressividade vem à custa de alguma complexidade e limites computacionais.
3. A verificação de programas ilustra uma aplicação da lógica à informática:
   • Dada a especificação formal do comportamento de um programa, como deduzir com rigor que o programa funciona como pretendido?

Lógica Proposicional

Na Lógica Proposicional são definidos os conceitos base para a descrição e análise de teorias formais.

O domínio é descrito por proposições, que são formadas por átomos ligados por conectivos e têm valores verdade/falso.

• Objetivos: Descrever proposições, saber como chegar a conclusões a partir de hipóteses dadas e relacionar a estrutura com o valor de uma proposição.

• Plano: Definir uma linguagem adequada para proposições. Descrever regras de dedução e definir o cálculo do valor das proposições.

• Avaliar: Quais são limites computacionais e expressivos?

• Utilizar: Que problemas podem ser descritos e resolvidos?

Sintaxe da Lógica Proposicional

A sintaxe é o início da formalização da dedução.

$$\begin{array}{cc}\neg p& p\wedge q\\ p\vee q& p\to q\end{array}$$

Sobre a definição das proposições:

• Intuitivamente uma "proposição" é uma frase que podemos dizer que é "verdadeira" ou "falsa".
• Formalmente uma "proposição" é uma estrutura que resulta de "conectivos" aplicados a "átomos".
• Casos atómicos: proposições indivisíveis ("está a chover.").
• Casos estruturados:
  • negação "não está a chover"
  • conjunção "está a chover e a fazer sol"
  • disjunção "está a chover ou a fazer sol"
  • implicação "se está a fazer sol então não está a chover"

Nesta parte não interessa ainda o valor (verdade/falso) duma proposição, mas na sua sintaxe.

Proposições

$$\begin{array}{c}\text{Lisboa eˊ a Capital de Portugal},\text{Estaˊ a chover},\text{2 eˊ maior que 3}\\ \text{Quando haˊ nuvens o Sol na˜o brilha},\text{As plantas na˜o sa˜o animais}\\ \text{Todos os ano˜es sa˜o amigos dos elfos}\end{array}$$

Uma proposição descreve um facto.

Definição (Proposição)

Seja $\mathcal{A}$ um conjunto de símbolos.

Uma proposição é uma expressão que resulta exclusivamente de um dos seguintes casos:

• Um átomo (ou proposição atómica ou letra proposicional) é um elemento de $\mathcal{A}$. $$a,b,\dots ,p,q,\dots ,x,y,z$$
• A negação de uma proposição. Se $p$ é uma proposição então $$(\neg p)$$ é uma proposição.
• A conjunção, a disjunção, ou a implicação de duas proposições. Se $p$ e $q$ forem proposições então $$\begin{array}{rl}& (p\wedge q)\\ & (p\vee q)\\ & (p\to q)\end{array}$$ também são proposições.

Regras de Precedência

Usam-se regras de precedência para simplificar proposições.

Por exemplo, a proposição $$((\neg a)\to (b\vee (c\wedge d)))$$ pode ser simplificada como $$\neg a\to b\vee c\wedge d.$$

Regras de Precedência

1. Os parêntesis têm precedência sobre os conectivos.
2. A negação tem precedência sobre os outros conectivos.
3. A conjunção e a disjunção têm precedência sobre a implicação.
4. A conjunção tem precedência sobre a disjunção.

Formalmente, a expressão $\neg a\to b\vee c\wedge d$ não é uma proposição. Mas as regras de precedência definem sem ambiguidade a proposição $((\neg a)\to (b\vee (c\wedge d)))$.

Árvore de Sintaxe

Uma proposição pode ser representada graficamente.

Por exemplo $$\neg a\to b\vee c\wedge d$$ define a árvore

%%{init: {'theme':'neutral'}}%%
    graph TD
        impl(($$\to$$)) --> nota(($$\neg$$))
        nota --> a(($$a$$))
        impl --> or(($$\vee$$))
        or --> b(($$b$$))
        or --> andcd(($$\wedge$$))
        andcd --> c(($$c$$))
        andcd --> d(($$d$$))

enquanto que $$(\neg a\to b)\vee c\wedge d$$ define

%%{init: {'theme':'neutral'}}%%
    graph TD
        or(($$\vee$$)) --> impl(($$\to$$))
        impl --> nota(($$\neg$$))
        impl --> b(($$b$$))
        nota --> a(($$a$$))
        or --> andcd(($$\wedge$$))
        andcd --> c(($$c$$))
        andcd --> d(($$d$$))

Exemplos de Proposições

• $a$ representa "está a chover".
• $b$ representa "o número cinco é par".
• $c$ representa "Coimbra fica em Portugal".
• $\neg a$: "não está a chover".
• $\neg b$: "o número cinco é ímpar".
• $\neg c$: "Coimbra não fica em Portugal".
• $\neg \neg a$: "é falso que não está a chover".
• $a\wedge b$: "está a chover e o número cinco é par".
• $a\wedge \neg a$: "está a chover e não está a chover".
• $a\wedge a$: "está a chover e está a chover".
• $a\to \neg b\wedge c$: "Se está a chover então o número cinco não é par e Coimbra fica em Portugal".
  • A escrita natural é ambígua: "Coimbra fica em Portugal" depende, ou não, de "Está a chover"? isto é, aquela frase significa $a\to (\neg b\wedge c)$ ou $(a\to \neg b)\wedge c$?
• $a\vee b$: "está a chover ou cinco é par".
• $a\vee \neg a$: "ou está a chover ou não está a chover".
• $a\vee a$: "está a chover ou está a chover".
• $a\vee (\neg b\wedge c)$: "ou está a chover ou cinco não é par e Coimbra fica em Portugal".
• $a\to b$: "se está a chover então cinco é par".
• $a\to \neg a$: "se está a chover então não está a chover".
• $a\to a$: "se está a chover então está a chover".
• $b\to \neg c$: "Coimbra não fica em Portugal porque cinco é par".
• $\text{penso}\to \text{existo}$: "penso, logo existo".

Observações

• Erros sintáticos: $p\wedge \wedge q,q\neg \wedge ,\dots$
• Não são proposições: perguntas "O café está frio?" e imperativos "Corre!".
• Coloquialismos, ie frases comuns que correspondem a proposições:
  • "a exceto se b", "a a não ser que b": $a\vee b$
    • "chove exceto se faz sol", "chove a não ser que faça sol"
    • Um caso é alternativo ao outro; Acontece um sempre que não acontece o outro.
  • "b porque a", "quando a também b", "b sempre que a": $a\to b$.
    • "quando faz sol também passeio",
    • "passeio sempre que faz sol",
    • "passeio porque faz sol"
      • Se fizer sol então passeio. Porém, também posso passear sem que faça sol.

Conectivos Derivados

$$\begin{array}{ccccc}\neg & \wedge & \top & \uparrow & \leftrightarrow \\ \vee & \to & \perp & \downarrow & \oplus \end{array}$$

Os símbolos $\neg ,\wedge ,\vee ,\to$ designam-se conectivos pois conectam (ligam) proposições mais simples.

A definição de proposição exclui certos conectivos comuns, como $\top ,\perp ,\leftrightarrow$ e $\oplus$. De facto, é possível dispensar quase todos os conectivos e começar apenas com, por exemplo $\neg ,\vee$ e definir os restantes conectivos à custa destes.

Como numa linguagem de programação, onde instruções e operações simples definem outras mais complexas.

No entanto, para facilitar a escrita é comum usarem-se outros conectivos.

Definição (Conectivos Derivados)

Sejam $p,q$ duas proposições.

Embora sintaticamente estes novos conectivos sejam representados por símbolos "novos", o que esta tabela define é a "forma equivalente" que fica "abreviada" de acordo com esta tabela.

Isto é $p\otimes q$ não é uma proposição mas uma "abreviatura" da "forma expandida" $\neg \left(p\leftrightarrow q\right)$ que, por sua vez, é uma abreviatura de $\neg \left(\left(p\to q\right)\wedge \left(q\to p\right)\right)$ e esta expressão já é uma proposição.

Dedução Natural Proposicional

$$H⊢p$$

Uma descoberta contra-intuitiva (dos filósofos Gregos).

Algumas deduções resultam apenas da forma (sintaxe, estrutura) das proposições envolvidas; o assunto tratado é irrelevante.

Por exemplo as duas deduções

• "Se está frio então levo o cachecol. Está frio. Portanto, levo o cachecol." e
• "Se o orçamento chumbar então o governo cai. O orçamento chumbou. Portanto, o governo cai."

são sobre assuntos muito diferentes mas partilham a mesma forma (estrutura):

$$\frac{a\to ba}{b}$$

Pretente-se definir e usar regras formais para deduzir consequências, $p$, dadas certas hipóteses, $H$, independentemente do assunto que está a ser tratado.

O que significa $H⊢p$?

• A hipótese, $H$, é um conjunto de proposições: expressões construídas a partir de átomos ligados por conectivos.
• A conclusão, $p$, é uma proposição.
• As regras dizem respeito aos conectivos e são de dois tipos: introdução ou eliminação.
• Uma prova de $p$ com hipóteses $H$ resulta de aplicar as regras linha-a-linha de forma que:
  1. Cada linha ou é uma hipótese de $H$ ou uma proposição que depende das linhas anteriores por aplicação de uma regra.
  2. Na última linha está a proposição $p$.
• A notação $H⊢p$ significa "existe uma prova de $p$ com hipóteses em $H$" ou que "$p$ é consequência (formal) das hipóteses $H$".

As proposições são definidas com conectivos e as regras estão organizadas por esses conectivos.

Existem regras para $\neg$, $\vee$, $\wedge$, etc

Além disso, há regras de introdução, em que a conclusão é formada por um certo conectivo, e regras de eliminação em que o conectivo está numa das hipóteses.

Conjunção

$${\wedge }_1^{-}{\wedge }_2^{-}{\wedge }^{+}$$

Eliminação da Conjunção

Eliminação da conjunção (esquerda) (${\wedge }_1^{-}$)

$${\wedge }_1^{-}:p\wedge q⊢p$$ ou $$\frac{\begin{array}{c}p\wedge q\end{array}}{p}\left({\wedge }_1^{-}\right)$$

Esta regra chama-se "eliminação da conjunção à esquerda", representa-se por ${\wedge }_1^{-}$ e diz que se $p\wedge q$ é uma das hipóteses, pode concluir-se $p$.

• É uma regra de eliminação da conjunção porque a conjunção ocorre nas hipóteses.
• "Esquerda" significa que na conclusão ocorre a proposição esquerda, o $p$.

Esta, e qualquer outra regra, é apresentada de duas formas equivalentes:

• horizontal "$p\wedge q⊢p$" usa o símbolo $⊢$ de consequência (formal); à esquerda estão as hipóteses e à direita a conclusão.
• vertical "$\frac{p\wedge q}{p}$" parece uma fração; em cima estão as hipóteses e por baixo a conclusão.

Eliminação da conjunção (direita) (${\wedge }_2^{-}$)

$${\wedge }_2^{-}:p\wedge q⊢q$$ ou $$\frac{\begin{array}{c}p\wedge q\end{array}}{q}\left({\wedge }_2^{-}\right)$$

Esta regra é semelhante à anterior, com a diferença que a consequência é o lado direito da hipótese.

Provas em Tabela

Como aplicar as regras para fazer uma prova?

Uma prova em tabela tem o seguinte aspeto

e o resultado é

$$\text{faz sol}\wedge \text{vou aˋ praia}⊢\text{faz sol}$$

isto é, $\text{faz sol}$ é consequência da hipótese $\text{faz sol}\wedge \text{vou aˋ praia}$.

Outra forma de dizer o mesmo:

Existe uma prova de $\text{faz sol}$ a partir da hipótese $\text{faz sol}\wedge \text{vou aˋ praia}$.

A construção de uma prova é organizada numa tabela:

1. As linhas são escritas de cima para baixo.
2. Cada linha tem um número, na coluna "Linha", definido sequencialmente: 1, 2, 3, etc.
3. Na coluna "Proposição" está uma proposição que pode ser um de dois casos:
   1. É uma hipótese e assinala-se um $H$ na coluna "Regra" ou
   2. Resulta das linhas anteriores por aplicação de uma regra. Nesse caso:
      1. Na coluna "Regra" escreve-se o nome da regra. Por exemplo, ${\wedge }_1^{-}$.
      2. Na coluna "Hipóteses" escrevem-se os números da linhas onde estão as hipóteses da regra aplicada. Por exemplo, 1.
4. Na última linha está a conclusão da prova, que depende da hipóteses colocadas na prova.

Introdução da Conjunção

Introdução da Conjunção (${\wedge }^{+}$)

$${\wedge }^{+}:\left\{p,q\right\}⊢p\wedge q$$ ou $$\frac{\begin{array}{c}pq\end{array}}{p\wedge q}\left({\wedge }^{+}\right)$$

Esta regra chama-se "introdução da conjunção", representa-se por ${\wedge }^{+}$ e diz que se as hipóteses forem $p$ e $q$ então pode concluir-se $p\wedge q$.

• É uma regra de introdução da conjunção porque a conjunção ocorre na conclusão.
• Neste caso a conclusão depende de duas hipóteses.

Exemplos

1. As hipóteses estão indicadas nas linhas 1 e 2.
2. Na linha 3 é aplicada a regra ${\wedge }^{+}$ com hipoteses na linhas 1 e 2.

Desta tabela pode escrever-se

$$\left\{\text{faz sol},\text{vou aˋ praia}\right\}⊢\text{faz sol}\wedge \text{vou aˋ praia}$$

Isto é $$\text{faz sol}\wedge \text{vou aˋ praia}$$ é consequência das hipóteses $\left\{\text{faz sol},\text{vou aˋ praia}\right\}$.

Exemplo. Idempotência da conjunção, $p⊣⊢p\wedge p$ .

Primeiro

mostra que $p⊢p\wedge p$.

Depois

mostra que $p\wedge p⊢p$.

Combinando as duas conclusões,

$$p⊣⊢p\wedge p$$

Exemplo. Comutatividade da conjunção, $p\wedge q⊢q\wedge p$.

Exemplo. Eliminação e introdução da conjunção.

Dupla Negação

$$\neg {\neg }^{+}\neg {\neg }^{-}$$

As regras que dizem respeito à negação "simples", como $\neg p$ são um pouco mais sofisticadas, e ficam para mais tarde. Já as regras para a "dupla negação", como $\neg \neg p$ são bastante simples.

Intuitivamente, a "dupla negação", $\neg \neg p$ é como o "simétrico do simétrico", $--x=x$.

Introdução da dupla negação ($\neg {\neg }^{+}$)

$$\neg {\neg }^{+}:p⊢\neg \neg p$$ ou $$\frac{\begin{array}{c}p\end{array}}{\neg \neg p}\left(\neg {\neg }^{+}\right).$$

Eliminação da dupla negação ($\neg {\neg }^{-}$)

$$\neg {\neg }^{-}:\neg \neg p⊢p$$ ou $$\frac{\begin{array}{c}\neg \neg p\end{array}}{p}\left(\neg {\neg }^{-}\right).$$

Implicação

$${\to }^{-},\mathbb{MP}{\to }^{+}$$

Eliminação da Implicação

Eliminação da Implicação ou Modus Ponens (${\to }^{-},\mathbb{MP}$)

$${\to }^{-}\text{ou}\mathbb{MP}:\left\{p,p\to q\right\}⊢q$$ ou $$\frac{\begin{array}{c}pp\to q\end{array}}{q}\left({\to }^{-}\text{ou}\mathbb{MP}\right)$$

Modus Ponens é uma expressão latina e designa uma das primeiras, e mais importantes, regras de inferência.

Sobre o Modus Ponens:

1. "está frio."
2. "se está frio então levo cachecol."
3. portanto "levo cachecol".

Em tabela:

Exemplo. Cadeia de Implicações I

$$p,p\to q,q\to r⊢r$$

Introdução da Implicação

Nesta regra aparece um tipo novo de hipótese, uma sub-prova com hipóteses locais, representada por $\left[\cdots \right]$ na forma horizontal e por $\boxed{⋮}$ na forma vertical.

Introdução da Implicação (${\to }^{+}$)

$${\to }^{+}:\left\{\left[p⊢q\right]\right\}⊢p\to q$$ ou $$\frac{\begin{array}{c}\boxed{\begin{array}{cc}p& H\\ ⋮& \\ q& \end{array}}\end{array}}{p\to q}\left({\to }^{+}\right).$$

As hipóteses locais duma sub-prova são descartadas com a aplicação da regra.

Exemplo. Cadeia de Implicações II

$$p\to q,q\to r⊢p\to r$$

Este exemplo ilustra o processo de descarte das hipóteses locais de uma sub-prova:

1. Na linha 3 é introduzida a hipótese $p$.
2. As linhas 4 e 5 dependem dessa hipótese.
3. Na linha 6 é a aplicada a regra ${\to }^{+}$, em que
   1. A sub-prova da hipótese desta regra ocorre nas linhas 3 - 5 da prova.
      • E escreve-se 3 - 5 na coluna "Hipóteses".
   2. A aplicação desta regra descarta toda a sub-prova.
      • E escreve-se (6) na coluna "Hipóteses" da linha 3, onde inicia a sub-prova.

Exemplo. Cadeia de Implicações III

$$p\to q⊢\left(q\to r\right)\to \left(p\to r\right)$$

Este exemplo continua o anterior: Na linha 7 ocorre uma nova aplicação da regra ${\to }^{+}$.

1. Esta aplicação usa as linhas 2 - 6 como sub-prova.
2. A hipótese da linha 2 é descartada, sendo indicado que esse descarte é feito na linha 7.

Disjunção

$${\vee }_1^{+}{\vee }_2^{+}{\vee }^{-}$$

As regras da disjunção são menos diretas do que as anteriores:

1. Existem dois casos para a introdução: esquerdo e direito. Tal como as regras de eliminação da conjunção.
2. A regra da eliminação descarta duas sub-provas.

Introdução da Disjunção

Introdução da disjunção (esquerda) (${\vee }_1^{+}$)

$${\vee }_1^{+}:p⊢p\vee q$$ ou $$\frac{\begin{array}{c}p\end{array}}{p\vee q}\left({\vee }_1^{+}\right)$$

Introdução da disjunção (direita) (${\vee }_2^{+}$)

$${\vee }_2^{+}:q⊢p\vee q$$ ou $$\frac{\begin{array}{c}q\end{array}}{p\vee q}\left({\vee }_2^{+}\right)$$

Nestas regras a conclusão inclui um predicado que não ocorre nas hipóteses — $q$ na regra esquerda e $p$ na direita:

• Este predicado pode ser um qualquer, o que dá uma grande liberdade para a construção da prova.
• Porém, se esse predicado não for bem escolhido em nada contribui para a conclusão a que se pretende escolher.

Eliminação da Disjunção

Esta regra é, talvez, a mais complexa da Dedução Natural Proposicional:

• As hipóteses são:
  • Uma disjunção, $p\vee q$;
  • A sub-prova $p⊢r$, que é descartada com a aplicação da regra;
  • A sub-prova $q⊢r$, que também é descartada com a aplicação da regra;
• Uma sub-prova tem como hipótese um dos "casos" de $p\vee q$, o predicado $p$.
• A outra sub-prova tem como hipótese o outro "caso" de $p\vee q$, o predicado $q$.
• Em cada uma das sub-provas a conclusão, $r$:
  • É comum às sub-provas;
  • Não ocorre na disjunção $p\vee q$;
  • Portanto, $r$ pode ser escolhido sem restrições mas com o fim da prova em mente.

Eliminação da Disjunção (${\vee }^{-}$)

$${\vee }^{-}:\left\{p\vee q,\left[p⊢r\right],\left[q⊢r\right]\right\}⊢r$$ ou $$\frac{\begin{array}{ccc}p\vee q& \boxed{\begin{array}{cc}p& H\\ ⋮& \\ r& \end{array}}& \boxed{\begin{array}{cc}q& H\\ ⋮& \\ r& \end{array}}\end{array}}{r}\left({\vee }^{-}\right)$$

(Semi-)Propriedade Distributiva

$$\left(p\vee q\right)\wedge \left(p\vee r\right)⊢p\vee \left(q\wedge r\right)$$

As sub-provas foram indentadas para facilitar a leitura. Esta indentação é opcional e nem sempre será aplicada.

A regra ${\vee }^{-}$ é aplicada duas vezes:

• Na linha 12:
  • A disjunção, $p\vee r$, está na linha 6;
  • Uma sub-prova, de $p\vee \left(q\wedge r\right)$, com hipótese $p$, em 7 - 8;
  • A outra sub-prova, também de $p\vee \left(q\wedge r\right)$, mas com hipótese $r$, em 9 - 11;
• Na linha 13:
  • A disjunção, $p\vee q$, está na linha 2;
  • Uma sub-prova, de $p\vee \left(q\wedge r\right)$, com hipótese $p$, em 5 - 6;
  • A outra sub-prova, também de $p\vee \left(q\wedge r\right)$, mas com hipótese $q$, em 5 - 12;

Pode parecer estranho porque é que $p\vee \left(q\wedge r\right)$ aparece cinco vezes como conclusão, nas linhas 4, 8, 11, 12 e 13.

Nas últimas três foram descartadas hipóteses temporárias, para sub-provas. Até ao descarte essas hipóteses estão "ativas" e teriam de aparecer na lista de hipóteses "final":

• Na linha 11 as hipóteses ativas são:
  • Linha 1: $\left(p\vee q\right)\wedge \left(p\vee r\right)$.
  • Linha 3: $p$.
  • Linha 5: $q$.
  • Linha 7: $p$.
  • Linha 9: $r$.
• Na linha 12, quando é aplicada a regra ${\vee }^{-}$, são descratadas as hipóteses 7 e 9 e permanecem ativas:
  • Linha 1: $\left(p\vee q\right)\wedge \left(p\vee r\right)$.
  • Linha 3: $p$.
  • Linha 5: $q$.
• Na linha 13, depois de aplicada a regra, são descartadas as hipóteses 3 e 5 e permanece ativa a linha 1.

Negação e Contradição

$${\neg }^{+}{\perp }^{+}{\perp }^{-}$$

A contradição ($\perp$) está relacionada com a negação ($\neg$) pois $\perp$ é definida como $q\wedge \neg q$.

A contratição, $\perp$, é o primeiro conectivo derivado dos quatro iniciais, $\wedge ,\vee ,\to$ e $\neg$.

Informalmente, $\perp$ pode ser lido como "falso".

Introdução da Negação

Introdução da Negação (${\neg }^{+}$)

$${\neg }^{+}:\left\{\left[p⊢q\wedge \neg q\right]\right\}⊢\neg p$$ ou $$\frac{\begin{array}{c}\boxed{\begin{array}{cc}p& H\\ ⋮& \\ q\wedge \neg q& \end{array}}\end{array}}{\neg p}\left({\neg }^{+}\right).$$

Esta regra pode ser lida da seguinte forma:

Se a hipótese $p$ leva a uma contradição, $q\wedge \neg q$, é porque essa hipótese é "falsa". Portanto, a sua negação, $\neg p$, tem de ser "verdadeira".

• Esta regra tem como hipótese apenas uma sub-prova, que é descartada juntamente com a respetiva hipótese, na aplicação.
• Na conclusão da sub-prova o predicado $q$ não ocorre (necessariamente) na hipótese $p$.

Contradição

Definição (Contradição, $\perp$)

• Qualquer proposição da forma $p\wedge \neg p$ é uma contradição.

• Usa-se o símbolo $\perp$ para representar contradições.

Não é evidente (por enquanto) que esta definição de $\perp$ seja legítima!

• Porque é que não depende de $p$?
• O $\perp$ de $p\wedge \neg p$ é o mesmo de $q\wedge \neg q$?

Com esta definição a regra ${\neg }^{+}$ pode ser re-escrita da seguinte forma:

Introdução da Negação (${\neg }^{+}$) (versão alternativa)

$${\neg }^{+}:\left\{\left[p⊢\perp \right]\right\}⊢\neg p$$ ou $$\frac{\begin{array}{c}\boxed{\begin{array}{cc}p& H\\ ⋮& \\ \perp & \end{array}}\end{array}}{\neg p}\left({\neg }^{+}\right).$$

Numa prova pode ser usada qualquer uma das versões da regra ${\neg }^{+}$.

Introdução da Contradição

Este novo conectivo tem as respetivas regras de dedução.

Introdução da Contradição (${\perp }^{+}$)

$${\perp }^{+}:\left\{p,\neg p\right\}⊢\perp$$ ou $$\frac{\begin{array}{cc}p& \neg p\end{array}}{\perp }\left({\perp }^{+}\right)$$

Esta regra tem duas hipóteses contraditórias $p$ e $\neg p$ e a conclusão é $\perp$.

Eliminação da Contradição

Eliminação da Contradição (${\perp }^{-}$)

$${\perp }^{-}:\perp ⊢p$$ ou $$\frac{\begin{array}{c}\perp \end{array}}{p}\left({\perp }^{-}\right)$$

Pode ser escolhida qualquer proposição $p$ na conclusão esta regra.

Efeito da Contradição

A regra ${\perp }^{-}$ pode ser lida como "de uma contradição é sempre possível concluir qualquer proposição".

Em termos práticos a lógica e a dedução natural são utilizadas para descrever e analizar um certo problema. Por exemplo, um programa, uma empresa, etc.

Supondo que a Dona Entrelinha é gestora (CEO!) de uma padaria e vai aplicar a lógica e a dedução natural para descrever e analisar o fluxo de trabalho. Começou com um conjunto de regras para o dia-a-dia da padaria:

$$H=\left\{\begin{array}{rl}\text{pa˜o}& \to \text{ingredientes},\\ \text{lucro}& \to \text{clientes}\wedge \text{pa˜o},\\ \text{clientes}\wedge \neg \text{pa˜o}& \to \neg \text{lucro},\\ \neg \text{clientes}& \to \neg \text{lucro},\\ \text{clientes}\vee \neg \text{clientes}& \end{array}\right\}$$

Certo dia houve falta de farinha, pelo que a Dona Entrelinha acrescentou $\neg \text{ingredientes}$ às regras e antecipou que, nesse dia, não teria lucro: $H,\neg \text{ingredientes}⊢\neg \text{lucro}$ porque

Tentado manter o lucro, a Dona Entrelinha foi a uma padaria rival e comprou pão. Mas, com o stress da situação, esqueceu-se de retirar das hipóteses as proposições sobre os ingredientes. Ficou então com hipóteses $$H,\neg \text{ingredientes},\text{pa˜o}$$

Ora, neste caso

Na linha 5 podemos escrever qualquer proposição, i.e. qualquer proposição é consequência de $H,\neg \text{ingredientes},\text{pa˜o}$ !

Esta situação não é desejável porque qualquer teoria (conjunto de hipóteses) "útil" deve distinguir "verdade" de "falso"; os "factos" dos "enganos".

Uma teoria que permita contradições não é "útil" porque qualquer proposição é consequência dessa teoria.

E, se qualquer proposição é consequência, também a sua negação o é; se $H⊢p$ para qualquer proposição $p$, então também $H⊢\neg p$.

Programação Lógica

As hipóteses iniciais da Dona Entrelinha podem ser descritas pelo seguinte programa ASP:

ingredientes :- pao.
clientes :- lucro.
pao :- lucro.
-lucro :- clientes, -pao.
-lucro :- -clientes.
clientes ; -clientes.

Como é normal em programação lógica:

• Em vez de $a\to b$ escreve-se $b\leftarrow a$ usando a sintaxe b :- a, que se lê "b se a". Adicionalmente,
• A negação $\neg a$ é representada por -a.
• A conjunção $a\wedge b$ por a, b.
• A disjunção $a\vee b$ por a; b.

Pode-se perguntar em que circunstâncias este programa é satisfeito. O resultado é

Solving...
Answer: 1
-clientes -lucro
Answer: 2
clientes
SATISFIABLE

Isto é, há duas formas (answer sets) destas regras serem cumpridas:

• Ou não há clientes nem lucro (Answer: 1).
• Ou há clientes, mas não a garantia de lucro (Answer: 2) .

Recursos

• A linguagem ASP (Answer set programming) na wikipedia.
• O sistema Potassco inclui o programa clingo que pode ser instalado ou correr no browser.

Introdução de Teses

$${\mathbb{T}}^{+}$$

Esta regra permite usar provas anteriores como regras: se previamente foi provado que $H⊢p$ e na prova actual ocorrem todas as hipóteses de $H$ então $p$ é uma conclusão.

Introdução de Teses (${\mathbb{T}}^{+}$)

$${\mathbb{T}}^{+}:\left\{\left[H⊢p\right],H\right\}⊢p$$ ou $$\frac{\begin{array}{cc}\boxed{\begin{array}{c}H\\ ⋮\\ p\end{array}}& H\end{array}}{p}\left({\mathbb{T}}^{+}\right).$$

A sub-prova $H⊢p$ é descartada na aplicação desta regra.

Regras Derivadas

$$\mathbb{MT}\mathbb{RA}\mathbb{TE}$$

Certas regras facilitam e reduzem significativamente o número de passos numa prova.

• É necessário demonstrar que as regras novas resultam das anteriores.
• Também algumas regras anteriores são redundantes: umas resultam das restantes.

Modus Tollens ($\mathbb{MT}$)

$$\mathbb{MT}:p\to q,\neg q⊢\neg p$$ ou $$\frac{\begin{array}{cc}p\to q& \neg q\end{array}}{\neg p}\left(\mathbb{MT}\right).$$

Demonstração.

Redução ao Absurdo ($\mathbb{RA}$)

$$\mathbb{RA}:\left[\neg p⊢\perp \right]⊢p$$ ou $$\frac{\begin{array}{c}\boxed{\begin{array}{cc}\neg p& H\\ ⋮& \\ \perp & \end{array}}\end{array}}{p}\left(\mathbb{RA}\right).$$

Demonstração.

Terceiro Excluído ($\mathbb{TE}$)

$$\mathbb{TE}:⊢p\vee \neg p$$ ou $$\frac{\begin{array}{c}\end{array}}{p\vee \neg p}\left(\mathbb{TE}\right).$$

Demonstração.

Exemplo. Regras Derivadas

A regra $\neg {\neg }^{+}:p⊢\neg \neg p$ como resultado de ${\perp }^{-},{\perp }^{+}$.

Demonstração.

Isto é $p⊢\neg \neg p$ ou $$\frac{\begin{array}{c}p\end{array}}{\neg \neg p}\left(\neg {\neg }^{+}\right)$$

Tabela de Regras

Resumo das regras da Dedução Natural Proposicional.

$$\begin{array}{crlcrl}\text{regra}& \text{hipoˊteses}& \text{concl.}& \text{regra}& \text{hipoˊteses}& \text{concl.}\\ & & & & & \\ {\wedge }_1^{-}& p\wedge q& ⊢p& & & \\ {\wedge }_2^{-}& p\wedge q& ⊢q& {\wedge }^{+}& p,q& ⊢p\wedge q\\ & & & & & \\ \neg {\neg }^{-}& \neg \neg p& ⊢p& \neg {\neg }^{+}& p& ⊢\neg \neg p\\ & & & & & \\ \mathbb{MP}& p,p\to q& ⊢q& {\to }^{+}& \left[p⊢q\right]& ⊢p\to q\\ & & & & & \\ {\vee }^{-}& p\vee q,\left[p⊢r\right],\left[q⊢r\right]& ⊢r& {\vee }_1^{+}& p& ⊢p\vee q\\ & & & {\vee }_2^{+}& q& ⊢p\vee q\\ & & & & & \\ & & & {\neg }^{+}& \left[p⊢\perp \right]& ⊢\neg p\\ & & & & & \\ {\perp }^{-}& \perp & ⊢p& {\perp }^{+}& p,\neg p& ⊢\perp \\ & & & & & \\ {\mathbb{T}}^{+}& \left[H⊢p\right],H& ⊢p& \mathbb{MT}& p\to q,\neg q& ⊢\neg p\\ & & & & & \\ \mathbb{RA}& \left[\neg p⊢\perp \right]& ⊢p& \mathbb{TE}& & ⊢p\vee \neg p\end{array}$$

Consequência Sintática Proposicional

$$H⊢p$$

Uma regra, $\mathbf{R}$, especifica como certas hipóteses, $H$, produzem uma determinada conclusão, $p$:

$$\frac{\begin{array}{c}H\end{array}}{p}\left(\mathbf{R}\right).$$

Encadeando várias regras obtém-se uma prova, apresentada numa tabela:

em que cada linha depende das anteriores não descartadas, por aplicação de uma regra.

Por fim, a relação entre as hipóteses não descartadas, $H$, e a conclusão na última linha, $p$, é representada por $H⊢p$ e diz-se que $p$ é consequência sintática de $H$.

Definição (Teorema)

Uma proposição $p$ é um teorema se $⊢p$, isto é, se $p$ pode ser demonstrada sem hipóteses.

Pode parecer estranho como fazer uma prova sem hipóteses. Mas já vimos como podemos "descartar" hipóteses usando implicações, pela regra ${\to }^{+}:\left\{\left[p⊢q\right]\right\}⊢p\to q$.

A continuação do exemplo da cadeia de implicações serve para ilustrar este ponto.

Exemplo. Cadeia de Implicações IV

$$⊢p\to q\to \left(\left(q\to r\right)\to \left(p\to r\right)\right)$$

Este exemplo mostra uma prova em que todas as hipóteses foram descartadas. Formalmente seria $$\varnothing ⊢\left(p\to q\right)\to ((q\to r)\to (p\to r))$$ para indicar que o conjunto de hipóteses é vazio, $\varnothing$, mas pode ser abreviado para $$⊢\left(p\to q\right)\to ((q\to r)\to (p\to r))$$

De acordo com a definição de teorema, $$\left(p\to q\right)\to ((q\to r)\to (p\to r))$$ é um teorema porque tem uma prova sem hipóteses "ativas".

Semântica Proposicional

$$H\models p$$

Como definir valores booleanos $\mathtt{v},\mathtt{f}$ de proposições?

As regras da dedução natural usam apenas a sintaxe das proposições, e permitem determinar se uma conclusão $p$ é consequência de certas hipóteses $H$. Nesse caso escreve-se $H⊢p$.

$H⊢p$ não é booleana no sentido em que não depende dos valores $\mathtt{v},\mathtt{f}$ das hipóteses $H$ nem da conclusão $p$.

Os valores booleanos das proposições baseiam-se em valorações.

São funções que associam os valores booleanos $\mathtt{v},\mathtt{f}$ aos átomos e daí, respeitando a estrutura dos conectivos, a todas as proposições.

O que significa $H\models p$?

• A hipótese, $H$, é um conjunto de proposições.
• A conclusão, $p$, também é uma proposição.
• As valorações define os valores booleanos $\mathtt{v},\mathtt{f}$ de todas as proposições.
• A notação $H\models p$ significa que "se todas as hipóteses $H$ são verdadeiras então também $p$ é verdadeira."

Valoração

$$v\left(p\right)$$

Definição (Valoração)

Uma valoração é qualquer função $v$ que associa um valor booleano, $\mathtt{v}$ ou $\mathtt{f}$, a cada proposição, de forma que:

• Para cada átomo $a,b,\cdots ,p,q,r,\dots ,x,y,z$ o valor é definido explicitamente.
• Para cada conectivo $\neg ,\wedge ,\vee ,\to$, resulta da tabela

$$\begin{array}{cccccc}p& q& \neg p& p\wedge q& p\vee q& p\to q\\ \mathtt{v}& \mathtt{v}& \mathtt{f}& \mathtt{v}& \mathtt{v}& \mathtt{v}\\ \mathtt{v}& \mathtt{f}& \mathtt{f}& \mathtt{f}& \mathtt{v}& \mathtt{f}\\ \mathtt{f}& \mathtt{v}& \mathtt{v}& \mathtt{f}& \mathtt{v}& \mathtt{v}\\ \mathtt{f}& \mathtt{f}& \mathtt{v}& \mathtt{f}& \mathtt{f}& \mathtt{v}\end{array}$$

Exemplo. Valorações

Sejam $p,q$ duas proposições atómicas.

Se $v\left(p\right)=\mathtt{v},v\left(q\right)=\mathtt{v}$ então $$\begin{array}{rlrlrl}v\left(\neg p\right)& =\mathtt{f}& v\left(\neg q\right)& =\mathtt{f}& v\left(p\wedge q\right)& =\mathtt{v}\\ v\left(p\vee q\right)& =\mathtt{v}& v\left(p\to q\right)& =\mathtt{v}& v\left(p\to \neg q\right)& =\mathtt{f}\end{array}$$

Se $v\left(p\right)=\mathtt{f},v\left(q\right)=\mathtt{v}$ então $$\begin{array}{rlrlrl}v\left(\neg p\right)& =\mathtt{v}& v\left(\neg q\right)& =\mathtt{f}& v\left(p\wedge q\right)& =\mathtt{f}\\ v\left(p\vee q\right)& =\mathtt{v}& v\left(p\to q\right)& =\mathtt{v}& v\left(p\to \neg q\right)& =\mathtt{v}\end{array}$$

O valor booleano de uma proposição depende apenas dos valores booleanos dos átomos que ocorrem nessa proposição.

A definição de $\perp$.

Previamente $\perp$ foi definido como uma "representação" de $p\wedge \neg p$. Então foi questionado se o $\perp$ que representa $p\wedge \neg p$ será o mesmo que representa, por exemplo, $q\wedge \neg q$.

• Na tabela de $p\wedge \neg p$ todas as linhas são $\mathtt{f}$, tal como serão em $q\wedge \neg q$ ou em $r\wedge \neg r$ ou ...
• ...ou em qualquer outra proposição que resulte de substituir $p$ em $p\wedge \neg p$, como $\left(p\vee r\right)\wedge \left(\neg r\wedge \neg p\right)$ por exemplo.

Isto é, $\perp$ é "sempre $\mathtt{f}$". Analogamente, $\top$ é "sempre $\mathtt{v}$".

Número de Valorações

Dados dois átomos, $p$ e $q$, quantas valorações diferentes existem para $p,q$?

• Como $v\left(p\right)$ só pode ter dois valores, e $v\left(q\right)$ também, as valorações possíveis para $p,q$ são:

$$\begin{array}{rlrlr}{v}_1\left(p\right)& =\mathtt{v}& & v_1\left(q\right)& =\mathtt{v}\\ v_2\left(p\right)& =\mathtt{v}& & v_2\left(q\right)& =\mathtt{f}\\ v_3\left(p\right)& =\mathtt{f}& & v_3\left(q\right)& =\mathtt{v}\\ v_4\left(p\right)& =\mathtt{f}& & v_4\left(q\right)& =\mathtt{f}\end{array}$$

ou em tabela

$$\begin{array}{ccc}v& p& q\\ v_1& \mathtt{v}& \mathtt{v}\\ v_2& \mathtt{v}& \mathtt{f}\\ v_3& \mathtt{f}& \mathtt{v}\\ v_4& \mathtt{f}& \mathtt{f}\end{array}$$